%% Copyright (C) 2014 Keith Clark, Peter Robinson
%% Email: klc@doc.ic.ac.uk, pjr@itee.uq.edu.au
%%
%% This library is free software; you can redistribute it and/or modify
%% it under the terms of the GNU General Public License as published by
%% the Free Software Foundation; either version 2 of the License, or
%% (at your option) any later version.
%%
%% This library is distributed in the hope that it will be useful,
%% but WITHOUT ANY WARRANTY; without even the implied warranty of
%% MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
%% GNU General Public License for more details.
%%
%% You should have received a copy of the GNU General Public License
%% along with this program; if not, write to the Free Software
%% Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA  02111-1307  USA

% A % to end-of-line is a comment
% Declarations and definitions can be given in any order
% A terminating .<newline> is optional but each rule and clause must 
% start at left end of  a new line and a continuation over several lines
% must  indent all but the first line in from left end by at least 
% one space or tab.  An idea borrowed from Python. 


% Data base style relations and finite sets of atomic values as types
%*********************************************************************
% For these types sub-type relation is subset relation.


% disjunction of atoms - enumerated type
gender ::=  male | female 
% gender is a sub-type of atom, atomic and term

% ranges of integers - range types
age ::= (0 .. 110)	      
digit ::= (0 .. 9) 	     
% digit  is a sub-type of age, a sub-type of int, hence num, hence term
                               	       	 
% disjunction of types - union type
atomOrNat ::= atom || nat
%int and atom are both sub-types of atomOrNat, which is a 
% sub-type of atomic and of term 

% simple relations with type declarations. If none given type term is 
% assumed for every argument. 

man ::= roger | tom | bill | alan | graham | keith | sam
woman ::= june | mary | rose | penny | sue | helen | veronica
  % implicitly also facts man(roger) .... woman(june)...
  % restricts allowed names that can be used for men and women

human ::= man || woman
  % implicitly also two clauses defining human

%%% try:  isa(H,human).

belief age_of: (human,age)   % default mode ? for both args, since a belief can b updated
age_of(roger,60)
age_of(tom,26)
age_of(june,23)
age_of(bill,40)
age_of(mary,40)
age_of(rose,40)
age_of(penny,1)
  % type check effectively checks for spelling errors in names and invalid age values

%%% sample queries

%%% P ? age_of(P,A) & A>39.
%%% 2 P ? age_of(P,A) & A>39.
%%% exists A age_of(P,A) & A>39.

%%% P :: age_of(P,A) & A>39.

%%% X*2 :: X in [3.4, 9.2, -6, 3.5, -4.7, 7].

% defined person relation
person: (?human,?gender,?age) <=     % all args can be given or not in a call
person(H,male,A) <= isa(H,man) & age_of(H,A)
person(H,female,A) <= isa(H,woman) & age_of(H,A)

% <= is like :- in Prolog
% & is  conjunc

% child facts
belief child_of : (human,human)
child_of(tom,roger) 
child_of(june,roger) 
child_of(rose,mary)
child_of(rose,bill)
child_of(penny,rose)

descendant_is: (!human,?human) <=       % first arg (an ancestor) must be given 
descendant_is(P,C) <= child_of(C,P).
descendant_is(A,D) <= child_of(C,A) & descendant_is(C,D)

ancestor_is: (!human, ?human) <=      % first arg (a descendant) must be given 
ancestor_is(C,P) <= child_of(C,P)
ancestor_is(D,A) <= child_of(D,P) & descendant_is(P,A)

% in above we have different order of body conds for different uses. 


only_has_adult_children : (?human) <=
only_has_adult_children( P) <=  
	once(child_of(_,P)) & 
	forall C (child_of(C,P) => exists A (person(C,_,A) & A>20))


children_are : (?human,?{(age,human)}) <=
children_are(P, Cs) <= 
		isa(P,human) & Cs = {(A,C) :: child_of(C,P) & age_of(C,A)}
% :: is read as "such that"

num_children: human -> nat       % arg must always be given as a function
num_children(P) ->  #{C :: child_of(C,P)}


% In example below first arg is a list any terms (the most inclsuive type) 
%  and to make the program type
% correct we need to restrict the second clause to only be used when N is
% of type num. 
% Note that if the test between the :: and <= succeeds then we 
% commit to that clause
% so Head :: Test <= Body   is like   Head :- Test, !, Body    in Prolog
% cut, disjunction, if-then-else not supported in QuLog

 % ![term] is list of any terms that must be given as ground value

add_nums_of_list_of_any_term : (![term], ?num) <=
add_nums_of_list_of_any_term([],0)
add_nums_of_list_of_any_term([N | Rest], Total)  :: type(N,num) 
        <=
        add_nums_of_list_of_any_term(Rest, RTotal) &
        Total = RTotal+N
add_nums_of_list_of_any_term([ _Any | Rest], Total) <=
    add_nums_of_list_of_any_term(Rest, Total)
   % we must have the type test in 2nd clause else type error raised 
   % at  RTotal+N


record(T) ::= rec(atom, T)    % A simple parameterised constructor type


% A constuctor type - all alternatives must be 'structs'
% T a type variable so type is polymorphic and recursive

tree(T) ::= empty() | tr(tree(T),T,tree(T))

% int_tree is a type macro
int_tree ::= tree(int)  % can specialise poly type of required


% The <= in type decl below is optional, it emphasises on_tree
% &  is a relatiom
% the !tree(T) means the tree of any element type T must be given 
% as a ground value

on_tree : (?T,!tree(T)) <=     % a polymorphic relation
on_tree(E,tr(_,E,_)) 		    
on_tree(E,tr(Left,_,_)) <=
    on_tree(E,Left)
on_tree(E,tr(_,_,Right)) <= 
    on_tree(E,Right)

%% Lists and sets are primitive parameterised types. 

app: ([T]?,[T]?,[T]?) <= | (![T],![T],?[T]) <= | (?[T],?[T],![T]) <=  
% Alternative mode decls to help compiler
app([],L2,L2)
app([U|L1], L2, [U|L3]) <= app(L1,L2,L3).
%   trailing ? mode means arg can be given as template
% - i.e. as a list containing vars - and may not be ground by an app call

% app([X,2],[6,8,..L1],[1,V,W,..L2]).


% Simple function defs
% ************************

fact : nat->nat 
fact(0)->1.
fact(N) ::  N1 = N-1 & type(N1,nat) -> N*fact(N1).  
% Cannot define as 
% fact(N) :: N>0 -> N*fact(N-1) 
% as type checker cannot infer that N-1 is a natural number
% runtime type check type(N,nat) ensures this is the case, so type check ok

order: [T] -> [T]
order(L) -> []({}(L))

% {} function converts a list to a set, [] converts a set to an ordered list

%%% order([4,-7,8,2,3,-7]).

tree2list : tree(T) -> [T]
tree2list(empty()) -> []
tree2list(tr(LT, V, RT)) -> tree2list(LT) <> [V] <> tree2list(RT)

list2tree : [int] -> tree(int)
list2tree([]) -> empty()
list2tree([H|T]) -> add2tree(H, list2tree(T))

add2tree : (TT, tree(TT)) -> tree(TT)
add2tree(T, empty()) -> tr(empty(), T, empty())
add2tree(T, tr(L, V, R)) :: T @< V -> tr(add2tree(T, L), V, R)    
add2tree(T, tr(L, V, R)) -> tr(L, V, add2tree(T, R))  


% <> a built in function for appending ground lists, can be used to split in a pattern

last : [T] -> T
last(L) :: L =? _<>[E] -> E

% Recursive representation of data
% **********************************
% a different representation of a person as a nested data structure
% containing all their descendants - not practical

personTree ::= 
     malep(atom,age,[personTree]) | femalep(atom,age,[personTree])

belief a_person : (personTree)
a_person( malep( roger,60, [ malep(tom,26,[]), femalep(june,23,[]) ] ) )

child_is : (!personTree,?personTree) <=
child_is(malep(_,_,Children), Child) <= Child in Children
child_is(femalep(_,_,Children), Child ) <=  Child in Children

%-----------

% String and list processing examples
%****************************************

% relations of the same type can be declared in one declaration

sepchar, endchar, symbolchar : (?string) <=
sepchar(" ")
sepchar(",")
sepchar(";")

endchar(".")
endchar("?")
endchar("!")

symbolchar(C) <= sepchar(C)
symbolchar(C) <= endchar(C)
%%% No disjunction in QuLog

spaces, wordchar, word, seps: (!string) <=    % test only defs

spaces(S) :: S =? " " ++  RS?spaces(RS)
spaces(" ")

wordchar(S) <=  #S = 1  & not symbolchar(S)

word(S) :: S =? C?wordchar(C) ++ RS?word(RS)  
word(S) <=  wordchar(S)

seps(Seps) :: Seps =? O?sepchar(O) ++ RSeps?seps(RSeps) 
seps(Sep) <= sepchar(Sep)

words : (!string,?[string]) <=
words(Str,[WStr]) :: Str =? WStr?word(WStr) ++ E?endchar(E)  
words(Str,[W|Words]) :: 
    Str =? W?word(W)++Seps?seps(Seps)++RStr?words(RStr,Words) 

% Try:
%%% Ws :: words("hello keith,     how are   you today?",Ws).
%%%  Ws :: words("a jolly, fat     boy likes the sly, brown fox.",Ws).


% Same sort of thing but with lists, use <> on left hand side of =! spits lists

splitsAroundElement : (![T], ![T], !T, [T], [T]) <=
splitsAroundElement(L1,L2,E,OL1,OL2) <=
                             L1<>L2 =? OL1 <> [E] <> OL2

%%%% Non-parameterised recursive types, parse tree type for simple statements

parse_tree ::= s(noun_phrase_tree,verb_phrase_tree)

%% DCG Rule:  a_parse_tree(s(NPT,VP)) --> a_noun_phrase_tree(NPT), a_verb_phrase_tree(VPT). 

noun_phrase_tree::= np(article,noun_exp_tree) 

%% DCG Rule: a_noun_phrase_tree(np(Art,NET)) --> a_article(A), a_noun_exp_tree(NET)

noun_exp_tree::= ne(adjective,noun_exp_tree) | n(noun)
%% DCG Rules: a_noun_exp_tree(ne(Adj,NET)) --> an_adjective(Adj), a_noun_exp_tree(NET)
%%                    a_noun_exp_tree(n(N)) --> a_noun(N)

verb_phrase_tree::= vp(verb,noun_phrase_tree) | v(verb) | 
                               ndescr(complement,noun_phrase_tree) | 
                               adescr(complement,adjective)

noun::= "boy" | "fox" | "girl" | "ball" | "man" | "woman" | "lady"

%% DCG Rules: a_noun(N) --> [N], type(N,noun).
%% or               a_noun(N) --> [N], isa(N,noun).
%% if we want to generate legal  sentences using the grammar. 

adjective::= "fat" | "jolly" | "red" | "sly" | "brown" | "tall" | "female" | "male"

verb::= "runs" | "jumps" | "kicks" | "likes" | "sings"

complement ::= "is" | "are" | "were" | "was"

article ::= "the" | "a" | "an" | "some" | "all" | "every"

dword::= noun || adjective || verb || complement || article

%%%% Intention %%%
% Intention is to have two options for use of a type description of a parse tree
% 1: a primitive  parse(!atom,?type,![term],?[term]) where the atom arg. is the name of a parse tree
%     type, such as noun_phrase_tree.  A  call 
%     parse(TypeName,Tree,[T1,..,Tn,T'1,...,T'k], R) will check if [T1,..,Tn] are the leaf terms on a 
%     parse tree of the type indicated by the atom TypeName, and if so bind, Tree to this parse tree,
%     and R to [T'1,...,T'k]. It will do this by interpretively walking over the type definitions.
%2:  Generate the DCG as indicated by the comments above and from this generate the difference 
%     list clauses that are a compilation of what the parse primitive does. These will be:

a_parse_tree : (?parse_tree, ![string], ?[string]) <=
a_parse_tree( s(NP,VP), A, C) <= 
     a_noun_phrase_tree(NP, A, B) & a_verb_phrase_tree(VP, B, C)

a_noun_phrase_tree : (?noun_phrase_tree, ![string], ?[string]) <=
a_noun_phrase_tree(np(Ar,NE), A, C) <=
     A = [Ar,..B] &  type(Ar,article) & a_noun_exp_tree(NE, B, C)

a_noun_exp_tree : (?noun_exp_tree, ![string], ?[string]) <=
a_noun_exp_tree(ne(Adj,NE), A, C) <=
     A = [Adj,..B] &  type(Adj,adjective) &  a_noun_exp_tree(NE, B, C)
a_noun_exp_tree(n(N), A, B) <=
     A = [N,..B] & type(N,noun)

a_verb_phrase_tree: (?verb_phrase_tree, ![string], ?[string]) <=
a_verb_phrase_tree(vp(V,NP), A, C) <=
     A = [V,..B] & type(V,verb) &  a_noun_phrase_tree(NP, B, C)
a_verb_phrase_tree(v(V), A, B) <=
     A =  [V,..B] & type(V,verb)
a_verb_phrase_tree(ndescr(V,NP), A, C) <=
     A = [V,..B] & type(V,complement) &  a_noun_phrase_tree(NP, B, C)
a_verb_phrase_tree(adescr(V,Adj), A, C) <=
     A = [V,..B] & type(V,complement) &  B = [Adj,..C] & type(Adj,adjective) 

% ****************************
%%% parse function - no error reports

parseS: string -> parse_tree
parseS(Str) :: words(Str,Ws) & a_parse_tree(PT,Ws,[])  -> PT
parseS(_) -> bottom_

%%%% parseS("a jolly, fat     boy likes the sly, brown fox.").
%%%% parseS("the fat lady sings!").

 % Higher order functions
%**************************** 

mapF : ((T1 -> T2), [T1]) -> [T2]
mapF(_F, []) -> []
mapF(F, [H|T]) -> [F(H)|mapF(F, T)]

% mapF(number_of_children,[roger,mary,bill]) gives [2,1,1] as value

% ! ((!T1,T2)<=) says first arg is a relation over T1,T2 pairs and 
% can be such that
% its first arg must be given and this relation must be given in any call

mapR: (!((!T1,T2)<=), ![T1], [T2]) <=
mapR(_R,[], [])
mapR(R,[H|T],[RH|RT]) <= R(H,RH) & mapR(R,T,RT)

% So mapR(child_of,[amy,rose],Ps) binds Ps to different lists of 
% parents  of amy and rose

% [T1-T2] is type of a list of functions all of type T1->T2

mapFuns : ([T1 -> T2], T1) -> [T2]
mapFuns([], _) -> []
mapFuns([F|Tail], X) -> [F(X)|mapFuns(Tail, X)]


zip : ([T1], [T2]) -> [(T1, T2)]
zip([], _) -> []
zip(_, []) -> []
zip([H1|T1], [H2|T2]) -> [(H1,H2)|zip(T1, T2)]


foldr : (B -> A -> A) -> A -> [B] -> A
foldr(_F)(Z)([]) -> Z
foldr(F)(Z)([H|T]) -> F(H)(foldr(F)(Z)(T))

foldl : (A -> B -> A) -> A -> [B] -> A
foldl(_F)(Z)([]) -> Z
foldl(F)(Z)([H|T]) -> foldl(F)(F(Z)(H))(T)

% The above maps a list of functions over a value X produces a list of 
% their values when applied to X

% function that returns a function that will eventually add two ints

add : int -> (int -> int)
add(N)(M) -> N+M

curry : ((T1,T2) -> T3) -> T1 -> T2 -> T3
curry(F)(X)(Y) -> F(X,Y)
  % So curry(*) is same as the add function above

uncurry : (T1 -> T2 -> T3) -> (T1,T2) -> T3
uncurry(F)(X,Y) -> F(X)(Y)
  % so uncurry(add) is same as primitive function * 
  % It has type (int,int)=>int 

%%%% currying relations

curryR: ((T1,!T2)<=) -> T1 -> (!T2)<= |	
	((T1,?T2)<=) -> T1 -> (?T2)<= |
	((T1,T2?)<=) -> T1 -> (T2?) <=

curryR(Rel)(X)(Y) <= Rel(X,Y)

% Example 
% curryR(child_of(rose)) is a monadic relation true of parents of rose
% it can be passed round as a higher order value as a monadic rel
% over atoms.
% curryR(rose)(P) 
% will bind P to a parent of rose. 

uncurryR: (T1 -> (!T2)<=) -> ((T1,!T2)<=) |
	  (T1 -> (?T2)<=) -> ((T1,?T2)<=) |
	  (T1 -> (?T2)<=) -> ((T1,?T2)<=) |
	  (T1 -> (T2?)<=) -> ((T1,T2?)<=)
uncurryR(FR)(X,Y) <= FR(X)(Y)


% Esoteric Church numerals for the FP gurus
%***********************************************

%% church is a type macro
church(T) ::= (T -> T) -> T -> T

zero : church(_)
zero(_F)(X) -> X

one : church(_)
one -> succ(zero)
  % note that we don't have to supply args in this case - like a 'macro'
  
succ : church(T) -> church(T)
succ(N)(F)(X) -> F(N(F)(X))

plus : church(T) -> church(T) -> church(T)
plus(A)(B)(F)(X) -> A(F)(B(F)(X))

mult : church(T) -> church(T) -> church(T)
mult(A)(B)(F) -> A(B(F))

inc : nat -> nat
inc(N) -> N+1.

% mult(succ(succ(one)))(succ(one))(inc)(0).

% ---------

% Sets can be manipulated using union, diff and inter set operations
% Or by being converted to lists and then converted back. 
%*******************************************
  
% {T} is type for a set of T values. 
% [T] is type for a list of T values. 

equal_sets: (!{T}, !{T}) <=
equal_sets(S1,S2) <= 
     forall E1 (E1 in S1 => E1 in S2) & 
     forall E2 (E2 in S2 => E2 in S1)

unionDiff: ({T},{T},{T}) -> {T}
unionDiff(A, B, C) -> A union B diff C  % same as (A union B) diff C



%%% Action rules  
%*****************


% ~>> is optional type annotation for an action procedure as this is
% the `do' operator of an action rule. 
% An action rule can update a belief relation, 
% send messages and fork query threads. 

new_child : (!human, !age, !human, !human) ~>> 
new_child(C, A, M, F) ~>> 
    remember child_of(C,M) ; remember child_of(C,F)  ; remember age_of(C,A)
% remembers three new fact, C, M and F must all be atoms of human type. 

%%% Try:  new_child(helen,6,veronica,graham).
%%% The: show child_of.

remove_child : (!human) ~>>
remove_child(C) ~>> forall P (child_of(C,P) ~>> forget(child_of(C,P)))
% ~>> used in the forall as the consequent is an action

birthday : (!human) ~>>
birthday(P) :: person(P, _, A) & Z = A+1 & type(Z, age) ~>> 
         replace age_of(P, A) by age_of(P, A)
birthday(P) ~>> writeLine([P,'would have an invalid age'])

% Actions for giving run-time error messages 

all_dict_words: (![string]) <=
all_dict_words(Wrds) <= forall W (W in Wrds => type(W, !dword))

%%% do_parse action - error reports at each stage
do_parse: (!string, ?parse_tree) ~>>  % default for actions is ground input mode
do_parse(Str,PT) ~>> 
     to_words(Str,Wrds) ; writeLine(['Word list: ',Wrds]); 
     check_dict(Wrds) ;   writeLine(["All words in dictionary"]);
     to_parse_tree(Wrds,PT)

to_words: (!string, ?[string]) ~>>
to_words(Str,Wrds) :: words(Str,Wrds)
to_words(Str,_) ~>> writeLine(['Cannot split into words: ',Str]); fail

check_dict: (![string]) ~>>
check_dict(Wrds) :: all_dict_words(Wrds)
check_dict(Wrds) ~>> writeLine(['Unknown words in: ',Wrds]); fail

to_parse_tree: (![string], ?parse_tree) ~>>
to_parse_tree(Wrds,PT) :: a_parse_tree(PT,Wrds,[])  
to_parse_tree(Wrds,_) ~>> writeLine(['Cannot parse word list: ',Wrds]); fail



% Global values
%****************

% Global values can be used to store and update int or num values
% and are declared as follows.

int a:=0
num b:=0.0

% An example use - if a global value is to be modified it can only be
% done in an action

inc_a : (?int) ~>>
inc_a(N) :: N = $a+1 ~>> a +:= 1

% $a evaluates to the value stored in a and a :=+ 1 replaces the
% old value in a by its increment


%% We can give type declarations that have alternatives for modes and/or types
%% For example 

my_abs : (int -> int) | (num -> num)

my_abs(X) -> abs(X)

%% It's possible to access all of Qu-Prolog's builtin definitions by simply 
%% giving type declarations.
%% No checking is done so the user needs to be confident of the correctness
%% of the declaration (and relation/action annotations need to be given)


%% Example sorting programs

smallest_and_rest : (num, [num], ?num, ?[num]) <=

smallest_and_rest(X, [], X, []) :: true
smallest_and_rest(X, [H,..T], Y, [H,..R]) :: X < H <= 
                     smallest_and_rest(X, T, Y, R)
smallest_and_rest(X, [H,..T], Y, [X,..R]) <= 
                     smallest_and_rest(H, T, Y, R)

%% Selection Sort
ssort : [num] -> [num]
ssort([]) -> []
ssort(L) :: L = [_] -> L
ssort([H,..T]) :: smallest_and_rest(H, T, X, Rest) -> [X,..ssort(Rest)]


partition : (num, [num]) -> ([num], [num])
partition(_X, []) -> ([], [])
partition(X, [H,..T]) :: H < X & partition(X, T) = (P1, P2) -> ([H,..P1], P2)
partition(X, [H,..T]) :: partition(X, T) = (P1, P2) -> (P1, [H,..P2])

%% Quicksort
qsort : [num] -> [num]
qsort([]) -> []
qsort(L) :: L = [_] -> L
qsort(L) :: L = [X, Y] & X < Y -> L
qsort(L) :: L = [X, Y] -> [Y, X]
qsort([P,..Rest]) :: partition(P, Rest) = (P1, P2) 
        -> qsort(P1) <> [P,..qsort(P2)]


split : [num] -> ([num], [num])
split([]) -> ([], [])
split(L) :: L = [_] -> (L, [])
split([X1, X2,..L]) :: split(L) = (L1, L2) -> ([X1,..L1], [X2,..L2])
 
%% merge and msort are used in QuProlog so we use different names

merge1 : ([num], [num]) -> [num]
merge1([], L) -> L
merge1(L, []) -> L
merge1([X,..XR], [Y,..YR]) :: X < Y -> [X,..merge1(XR, [Y,..YR])]
merge1([X,..XR], [Y,..YR]) -> [Y,..merge1([X,..XR], YR)]

%% Mergesort
msort1 : [num] -> [num]
msort1([]) -> []
msort1(L) :: L = [_] -> L
msort1(L) :: (L1, L2) = split(L) -> merge1(msort1(L1), msort1(L2))