:- module(_,_,[]).           % For pure LP, depth-first search rule
% :- module(_,_,[sr/bfall]).   % For pure LP, breadth-first search rule, all predicates
% :- module(_,_,[bf]).         % For pure LP, breadth-first for selected predicates (with <-)
% :- module(_,_,[sr/afall]).   % 

% -------------------------------------------------------------------
% A first program: the pets database.

%% pet(atm::x) {
%%     animal(x); 
%%     barks(x);
%%             }
%% pet(atm::x) {
%%     animal(x); 
%%     meows(x);
%%             }
%%     

pet(X) :-
    animal(X),
    barks(X).
pet(X) :-
    animal(X),
    meows(X).

animal(tim).
animal(spot).
animal(hobbes).

barks(spot).

meows(tim).

roars(hobbes).

%  Some examples of queries. Copy on the right, hit 
%  ENTER to execute, and then ; for other solutions.
%  ?- pet(spot).
%  ?- pet(X).

% -------------------------------------------------------------------
% Some examples of unifications: do them first by hand! (following the
% unification algorithm) and check them after in the Prolog top level

% p(X,f(b)) = p(a,Y).

% p(X,f(Y)) = p(a,g(b)).

% p(X,X) = p(f(Z),f(W)).

% p(X,f(Y)) = p(Z,X).

% p(X,f(X)) = p(Z,Z).

% With this last one try also:
% ?- use_module(library(iso_misc)).
% ?- unify_with_occurs_check(p(X,f(X)),p(Z,Z)).

% -------------------------------------------------------------------
% Controlling search 1): order of literals in the body of clauses:

a1(X,Y) :-
    p(X),
    q(X,Y).
b1(X,Y) :-
    q(X,Y),
    p(X).

p(X):- X = 4.
p(X):- X = 5.

q(X, Y):- X = 1, Y = a, compute_a_lot.
q(X, Y):- X = 2, Y = b, compute_a_lot.
q(X, Y):- X = 4, Y = c, compute_a_lot.
q(X, Y):- X = 4, Y = d, compute_a_lot.


:- use_module(library(system),[pause/1]).
compute_a_lot :- pause(3).

% -------------------------------------------------------------------
% Controlling search 2): order of clauses in a predicate:

a2(X,Y) :- 
    p(X),
    q1(X,Y).
b2(X,Y) :-
    p(X),
    q2(X,Y).

%% p(X):- X = 4.
%% p(X):- X = 5.

q1(X, Y):- X = 1, Y = a, compute_a_lot.
q1(X, Y):- X = 2, Y = b, compute_a_lot.
q1(X, Y):- X = 4, Y = c, compute_a_lot.
q1(X, Y):- X = 4, Y = d, compute_a_lot.

q2(X, Y):- X = 4, Y = d, compute_a_lot.
q2(X, Y):- X = 4, Y = c, compute_a_lot.
q2(X, Y):- X = 1, Y = a, compute_a_lot.
q2(X, Y):- X = 2, Y = b, compute_a_lot.

% If we run:
% ?- a(X,Y).
% we get:
% X = 4,
% Y = c ? ;
% X = 4,
% Y = d ? ;
% 
% and for: 
% ?- b(X,Y).
% we get: 
% X = 4,
% Y = d ? ;
% X = 4,
% Y = c ? ;

% -------------------------------------------------------------------
% Role of unification

% is_animal(A), named(A,Name).

is_animal(dog(tim)).

named(dog(Name),Name).

% -------------------------------------------------------------------
% The classic family database:

father_of(john, peter).
father_of(john, mary).
father_of(peter, michael). 

mother_of(mary, david).
mother_of(jill, john).

grandfather_of(L,M) :-
    father_of(L,N),
    father_of(N,M).
grandfather_of(X,Y) :-
    father_of(X,Z),
    mother_of(Z,Y).  

% Some queries:
%
% ?- father_of(john,peter).
% ?- father_of(john,david).
% ?- father_of(john,X).
% ?- grandfather_of(X,michael).
% ?- grandfather_of(X,Y).
% ?- grandfather_of(X,X).

% Exercises:

% Write the rules for grandmother_of/2!
% Try it with:
% ?- grandmother_of(X,Y).

grandmother_of(L,M) :- mother_of(L,N), father_of(N,M).
grandmother_of(X,Y) :- mother_of(X,Z), mother_of(Z,Y).  

% Also: parent/2, ancestor/2. 

parent(X,Y) :- father_of(X,Y).
parent(X,Y) :- mother_of(X,Y).

ancestor(X,Y) :- parent(X,Y).
ancestor(X,Y) :- parent(X,Z), ancestor(Z,Y).

% Some queries to try: 
% ?- ancestor(john,michael).
% ?- ancestor(john,elisabeth).
% ?- ancestor(john,X).
% ?- ancestor(X,elisabeth).
% ?- ancestor(X,michael).


% Also: related/2 (have a common ancestor)
related(X,Y) :- ancestor(Z,X), ancestor(Z,Y).

% Queries to try: 
% ?- related(peter,mary).
% ?- related(peter,david).
% ?- related(mary,elisabeth).
% ?- related(michael,mary).
% ?- related(peter,X).
% ?- related(john,peter). (john is not related to peter!)

ancestor2(X,X).
ancestor2(X,Y) :- parent(X,Z), ancestor2(Z,Y).

related2(X,Y) :- ancestor2(Z,X), ancestor2(Z,Y).
% queries: related2(john,peter). (it works!)
%          related2(peter,X).    (duplicated answers!)


% -------------------------------------------------------------------
% A circuit topology example:

% The actual circuit

resistor(power,n1).
resistor(power,n2). 

transistor(n2,ground,n1).
transistor(n3,n4,n2).
transistor(n5,ground,n4).

% Some circuit 'theory'

inverter(Input,Output) :- 
   transistor(Input,ground,Output), 
   resistor(power,Output).

nand_gate(Input1,Input2,Output) :-
   transistor(Input1,X,Output),
   transistor(Input2,ground,X), 
   resistor(power,Output).

and_gate(Input1,Input2,Output) :-
   nand_gate(Input1,Input2,X), 
   inverter(X, Output).

% Some queries to find gates in the circuit:
% ?- inverter(In,Out).
% ?- and_gate(In1,In2,Out).
% ?- nand_gate(In1,In2,Out).

% -------------------------------------------------------------------
% Course info:

% course_raw(copmlog,Day,StartH,StartM,FinishH,FinishM,C,D,E,F).
% course_raw(complog,Day,StartH,StartM,FinishH,FinishM,_,_,_,_).

course_raw(complog,wed,18,30,20,30,'M.','Hermenegildo',new,5102).

course(complog,Time,Lecturer, Location) :-
    Time = t(wed,18:30,20:30),
    Lecturer = lect('M.','Hermenegildo'),
    Location = loc(new,5102).

% Some queries:
% course(complog,Time, A, B).
% course(complog,Time, _, _).

% -------------------------------------------------------------------
%% named_resistor(res(P1,P2),P1,P2) :- resistor(P1,P2).
%% named_transistor(trans(P1,P2,P3),P1,P2,P3) :- transistor(P1,P2,P3).
% -------------------------------------------------------------------
% The circuit topology example revisited (using data structures):

named_resistor(r1,power,n1).
named_resistor(r2,power,n2). 

named_transistor(t1,n2,ground,n1).
named_transistor(t2,n3,n4,n2).
named_transistor(t3,n5,ground,n4).

named_inverter(inv(T,R),Input,Output) :-
    named_transistor(T,Input,ground,Output),
    named_resistor(R,power,Output). 

named_nand_gate(nand(T1,T2,R),Input1,Input2,Output) :-
    named_transistor(T1,Input1,X,Output),
    named_transistor(T2,Input2,ground,X),
    named_resistor(R,power,Output). 

named_and_gate(and(N,I),Input1,Input2,Output) :-
    named_nand_gate(N,Input1,Input2,X),
    named_inverter(I,X,Output).

% Some queries:
% ?- named_inverter(Inv,I,O).
% ?- named_and_gate(G,In1,In2,Out).
% ?- named_resistor(R1,P1,P2).
% ?- named_transistor(T1,P1,P2,P3).

% -------------------------------------------------------------------
% Relational database:

:- use_package(argnames).

:- argnames person(name,age,sex).

person(brown,20,male).                 
person(jones,21,female).	       
person(smith,36,male).   	       

:- argnames person2(name,age,sex).

person2(cabeza,33,male).    
person2(bueno,39,male).     
person2(jones,21,female).   

:- argnames lived_in(name,town,years).

lived_in(brown,london,15).
lived_in(brown,york,5).
lived_in(jones,paris,21).
lived_in(smith,brussels,15).
lived_in(smith,santander,5).

% Projection:
city(C) :- 
    lived_in(_,C,_).
% Try:
% ?- city(C).

% Alternative definition, using argnames: 
city_(C) :- 
    lived_in${town => C}.

% Try:
% ?- city_(C).

% Union:
all_persons(Name,Age,Sex) :- 
    person(Name,Age,Sex).
all_persons(Name,Age,Sex) :- 
    person2(Name,Age,Sex).

% Try:
% ?- all_persons(Name,Age,Sex).

% Difference (note \+ not pure! But see NaF / Clarks's completion later...)
difference(Name,Age,Sex) :- 
    person(Name,Age,Sex), 
    \+ person2(Name,Age,Sex).
difference(Name,Age,Sex) :- 
    person2(Name,Age,Sex),
    \+ person(Name,Age,Sex).
% Try:
% ?- difference(Name,Age,Sex).

% Cartesian Product:
person_X_lived_in(Name1,Age,Sex,Name2,Town,Years) :- 
    person(Name1,Age,Sex), 
    lived_in(Name2,Town,Years).
% Try:
% ?- person_X_lived_in(Name1,Age,Sex,Name2,Town,Years).

% Selection:
underage_person(Name,Age,Sex) :- 
    person(Name,Age,Sex), 
    Age < 21.
% Try:
% ?- underage_person(Name,Age,Sex).

% Intersection:
person_lived_in(Name,Age,Sex,Town,Years) :-
    person(Name,Age,Sex), 
    lived_in(Name,Town,Years).
% Try:
% ?- person_lived_in(Name,Age,Sex,Town,Years).

% Join:
person_joinName_person2(Name,Age,Sex) :-
    person(Name,Age,Sex), 
    person2(Name,_Age2,_Sex2).

% Try:
% ?- person_joinName_person2(Name,Age,Sex).

% -------------------------------------------------------------------
% An example of (non-recursive) types: dates

weekday('Monday').
weekday('Tuesday').
weekday('Wednesday').
weekday('Thursday').
weekday('Friday').
weekday('Saturday').
weekday('Sunday').

day_of_month(1).
day_of_month(2).
% ...
day_of_month(31).

%% % A nice alternative:
%% :- use_package(clpq).
%% day_of_month(X) :- X .>. 0, X .=<. 31.
%% % Use clpfd to enumerate!

date(date(W,D)) :- weekday(W), day_of_month(D).

% Sample queries:
% Checking that something is a date:
% ?- date(date('Monday',31)).
% Checking something that is not a date:
% ?- date(date(a,31)).
% Generating dates (terms of the type): 
% ?- date(D).
% 'Property'-based testing for free!



% -------------------------------------------------------------------
% Simplest recursive type:

nat_num(0).
nat_num(s(X)) :- nat_num(X).

%% :- op(500,fy,-). % <- predefined in system

pint(X)  :- nat_num(X).
pint(-X) :- nat_num(X).

less_or_equal(0,X) :- nat_num(X).
less_or_equal(s(X),s(Y)) :- less_or_equal(X,Y).

 %% Multiple uses: 
 %% less_or_equal(s(0),s(s(0))).
 %% less_or_equal(X,0).
 %% 
 %% Multiple solutions:
 %% less_or_equal(X,s(0)).
 %% less_or_equal(s(s(0)),Y).

less(0,s(X)) :- nat_num(X).
less(s(X),s(Y)) :- less(X,Y).

less_or_equal_pairs(pair(0,X)) :- nat_num(X).
less_or_equal_pairs(pair(s(X),s(Y))) :- less_or_equal_pairs(pair(X,Y)).

%% =<(0,X) :- nat_num(X).
%% =<(s(X),s(Y)) :- =<(X,Y).

%% 0   =<  X   :-  nat_num(X).
%% s(X) =< s(Y) :-  X =< Y.

plus(0,Y,Y) :- nat_num(Y).
plus(s(X),Y,s(Z)) :- plus(X,Y,Z).

 %% Multiple uses: 
 %% plus(s(s(0)),s(0),Z).
 %% plus(s(s(0)),Y,s(0)).
 %% plus(s(0),Y,s(s(s(0)))).
 %%
 %% Multiple solutions: 
 %% plus(X,Y,s(s(s(0)))).


plus_alt(X,0,X) :- nat_num(X).
plus_alt(X,s(Y),s(Z)) :- plus_alt(X,Y,Z).

% -------------------------------------------------------------------
% Exercise:

times(0,Y,0) :- nat_num(Y).
times(s(X),Y,Z) :- plus(W,Y,Z), times(X,Y,W).

%% times(s(s(0)), s(s(0)), Y).
%%% ---> In top pevel: ?- op(500,fy,s). -->
%% times(s s 0, s s 0, Y).
%% times(s s 0, s s 0, s s 0).
%% times(s s 0, Y, s s 0).
%% times(Y, s s 0, s s 0).
% -------------------------------------------------------------------

% -------------------------------------------------------------------
% Exercise:

square(X,Y) :- times(X,X,Y).

%% square(s s 0, Y).
%% square(X, s s s s 0 ).
%% square(X, Y).
% -------------------------------------------------------------------
% Exercise:

exp(0, X, s(0)) :- nat_num(X).
exp(s(N),X,Y) :- exp(N,X,W), times(X,W,Y). 

 %% exp(s(s(0)),s(s(0)),Y).
 %% exp(s(s(0)),s(s(s(0))),Y).
 %% exp(s(s(s(0))),s(s(0)),Y).

% -------------------------------------------------------------------
% Exercise:

factorial(0, 0).
factorial(s(0),s(0)).
factorial(s(N),FN1) :- 
    nat_num(N),
    less_or_equal(s(0),N),
    factorial(N,FN),
    times(s(N),FN,FN1).

% factorial(s s s 0, Z).
% factorial(Z,s s s s s s 0).
% -------------------------------------------------------------------
% Exercise:

min_nat(X,Y,X) :-
    less_or_equal(X,Y).
min_nat(X,Y,Y) :-
    less(Y,X).

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

mod(X,Y,Z) :- 
    less(Z,Y),
    times(Y,_Q,W),
    plus(W,Z,X).

% Another possible definition:
mod2(X,Y,X) :- 
    less(X,Y).
mod2(X,Y,Z) :- 
    plus(X1,Y,X),
    mod2(X1,Y,Z).

% Try:
% ?- op(500,fy,s).
% (defines s as a prefix operator to save us 
%  writing parenthesis)
% ?- mod(s s s s s s s s s s s s s 0, s s s 0, Z).
% ?- mod(s s s s s s s s s s s s s 0, Y, s 0).

% ?- mod2(s s s s s s s s s s s s s 0, s s s 0, Z).
% ?- mod2(s s s s s s s s s s s s s 0, Y, s 0).
% -------------------------------------------------------------------
%% Functions can be coded as predicates with one more 
%% argument, which represents the output.

% E.g., the Ackermann function:
% 
% ackermann(0,N) = N+1
% ackermann(M ,0) = ackermann (M-1 ,1)
% ackermann(M,N) = ackermann (M-1, acker0mann (M,N-1))
% 
% is represented as plain clauses as follows:

ackermann(0,N,s(N)).
ackermann(s(M),0,Val) :-  
    ackermann(M,s(0),Val).
ackermann(s(M),s(N),Val) :- 
    ackermann(s(M),N,Val1),
    ackermann(M,Val1,Val).

% Try:
% ?- op(500,fy,s).
% (defines s as a prefix operator to save us 
%  writing parenthesis)
% ?- ackermann(s s 0, s s s 0, X).

% But now it also runs 'backwards':
% ?- ackermann(s s 0, s s s 0, s s s s s s s s s 0).
% ?- ackermann(s s 0, Y, s s s s s s s s s 0).
% ?- ackermann(X, s s s 0, s s s s s s s s s 0).
% -------------------------------------------------------------------

% -------------------------------------------------------------------
%%% Functional notation:
:- use_package(fsyntax). % Basic functional notation (most useful in practice)
% :- fun_eval defined(true). % Evaluate functors defined as functions
% :- fun_eval arith(true). % Evaluate arithmetic functors
% :- use_package(functional). % fsyntax + both fun_eval's above
% -------------------------------------------------------------------

%% Caveat: combination w/bf not always straightforward

nat(0).
nat(s(X)) :- nat(X).
%% --> 
%% nat := 0.
%% nat := s(X) :- nat(X).
%% --> 
%% nat := 0.
%% nat := s(~nat).
%% -->
%% :- fun_eval(defined(true)). % Evaluate functors defined as funtions
%% nat := 0.
%% nat := s(nat).
%% %% --> 
%% :- op(500,fy,s).
%% nat := 0.
%% nat := s ~nat.
%% 
%% nat := 0 | s ~nat.
%% 
%% sum( 0 ,X) := X :- nat(X).
%% sum(s X,Y) := s ~sum(X,Y).
%% 
%% ackmann(  0,   N) := s N.
%% ackmann(s M,   0) := ~ackmann(M, s 0).
%% ackmann(s M, s N) := ~ackmann(M, ~ackmann(s M, N) ).
%% 
%% p1(~ackmann(s s 0, s s s 0)).
%% 
%% % p2(X) :- X = ~ackmann(s s 0, s s s 0).
%% 
%% % ackmann(s s 0, s s s 0, X).
%% % ackmann(s s 0, s s s 0, s s s s s s s s s 0).
%% % ackmann(s s 0, Y, s s s s s s s s s 0).
% ackmann(X, s s s 0, s s s s s s s s s 0).
%% 
%% :- fun_eval ackmann_/2.
%% 
%% ackmann_(  0,   N) := s N.
%% ackmann_(s M,   0) := ackmann_(M, s 0).
%% ackmann_(s M, s N) := ackmann_(M, ackmann_(s M, N) ).

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

% Operations on lists (never necessary!):

add_el(L,X,NL) :-
    NL = [X|L].

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

list([]).
list([_|Y]) :-
     list(Y).

%% list([]).
%% list(.(_,Y)) :-
%%     list(Y).

% list( [1,2] ).
% list( .(1, .(2, [] ) ) ).

lst1 := [] | [_|~lst1].
% ---> 
%% lst1([]).
%% lst1([_|lst1]).

% ---> 
%% lst([]).
%% lst([_|Y]) :- lst(Y).

%% In depth-first reversing the order of body literals controls enumeration:

% natlist(L): L is a list of naturals
natlist([]).
natlist([X|Y]) :- 
    nat(X),
    natlist(Y).

nlst := [] | [~nat|~nlst].

% GCD ---------------------------------------------------------------
%% gcd(N,N,N) :- less_or_equal(s(0),N).
%% gcd(NpM, M, D) :- plus(N,M,NpM), gcd(N,M,D).
%% gcd(N, NpM, D) :- plus(N,M,NpM), gcd(N,M,D).

%% gcd_(N,   N)   := N         :- less_or_equal(s(0),N).
%% gcd_(NpM, M)   := ~gcd_(N,M) :- plus(N,M,NpM).
%% gcd_(N,   NpM) := ~gcd_(N,M) :- plus(N,M,NpM).

gcd_(         N, N) := N  :- less_or_equal(s(0),N).
gcd_(~plus(N,M), M) := ~gcd_(N,M). 
gcd_(N, ~plus(N,M)) := ~gcd_(N,M).

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


% list_member(X,L): X is a member of list L
list_member(X,[X|L]) :-
    list(L).
list_member(X,[_|T]) :- 
    list_member(X,T).




%% list_member(X,[Z|T]) :- 
%%     ( X=Z , list(T) ) ; list_member(X,T).

%% list_member(X,[X|_]).
%% list_member(X,[_|T]) :- 
%%     list_member(X,T).

 %% Queries:
 %% list_member(b, [a,b,c]).
 %% list_member(X, [a,b,c]).
 %% list_member(a, L). % Nice in bfall!

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

% list_length(L,N): N is the length of list L
list_length([],0).
list_length([_|T],s(N)) :-
    list_length(T,N).

 %% Queries:
 %% list_length([a, b, c], N).
 %% list_length(L, s(s(s(0)))).
 %% list_length(L, 3).
 %% list_length(L, N).
 

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

sumlist([],0).
sumlist([H|T],S) :-
    sumlist(T,ST),
    add(ST,H,S).

add(0,X,X) :- nat(X).
add(s(X),Y,s(Z)) :- add(X,Y,Z).

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

prefix([],X) :- list(X).
prefix([X|Xs],[X|Ys]) :- 
    prefix(Xs,Ys).

% Queries:
% prefix([a,b], [a,b,c,d]). 
% prefix([X,Y], [a,b,c,d]).
% prefix(P, [a,b,c,d]).
% prefix([a,b], L). 
% prefix(P, L).

suffix(X,X) :- list(X).
suffix(X,[_|Ys]) :-
    suffix(X,Ys).

/* Queries:
suffix([c,d], [a,b,c,d]). 
suffix([X,Y], [a,b,c,d]).
suffix(P, [a,b,c,d]).
suffix([a,b], L). 
suffix(P, L).
*/

sublist(X,Y) :- 
    suffix(Z,Y),
    prefix(X,Z).

% Queries:
% sublist([b,c], [a,b,c]).
% sublist(X, [a,b,c]).
% sublist([b,c], [d,a,X,Y]).
% sublist(X, Y).


% Other (equivalent) definition for sublist.

sublist1(X,Y) :- 
    prefix(Z,Y),
    suffix(X,Z).

% Other definition for sublist (no repeated solutions).

sublist2([],Ys) :-
    list(Ys).
sublist2([Xs|Ts],Ys) :-
    prefix([Xs|Ts],Ys).
sublist2([Xs|Ts], [_|Ys]) :-
    sublist2([Xs|Ts], Ys).

%% sublist2([],Ys) :-
%%     list(Ys).
%% sublist2(Xs,Ys) :-
%%     sublist2b(Xs,Ys).
%% sublist2b(Xs,Ys) :-
%%     prefix2(Xs,Ys).
%% sublist2b(Xs,[_|Ys]) :-
%%     sublist2b(Xs,Ys).
%% 
%% prefix2([X],[X|Xs]) :-
%%     list(Xs).
%% prefix2([X|Xs],[X|Ys]) :- 
%%     prefix2(Xs,Ys).

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

list_append([],L,L) :- 
    list(L).
list_append([X|Xs],Ys,[X|Zs]) :- 
    list_append(Xs,Ys,Zs).

% Queries:
% ?- list_append([a,b], [c], X).
% ?- list_append(X, [c], [a,b,c]).
% ?- list_append(X, Y, [a,b,c]).
	
% -------------------------------------------------------------------
% Lists - two definitions of reverse

% list_reverse(X,Y): Y is the list X reversed

list_reverse([],[]).
list_reverse([X|Xs],Ys) :- 
    list_reverse(Xs,Zs),
    list_append(Zs,[X],Ys).

% Queries:
% ?- list_reverse([a,b,c],X).
% ?- list_reverse(X,[c,b,a]).
% ?- list_reverse(X,Y).

% freverse([]) := [].
% freverse([X|Xs]) := ~list_append(~freverse(Xs),[X]). 

% Queries:
% ?- freverse([a,b,c],X).
% ?- freverse(X,[c,b,a]).
% ?- freverse(X,Y).

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

reverse_acc(Xs,Ys) :- 
    reverse_(Xs,[],Ys).

reverse_([],Ys,Ys).
reverse_([X|Xs],Acc,Ys) :-
    NewAcc=[X|Acc],
    reverse_(Xs,NewAcc,Ys).

% Queries:
% ?- reverse_acc([a,b,c],X).
% ?- reverse_acc(X,[c,b,a]).
% ?- reverse_acc(X,Y).

% Cheking execution time: 
:- use_module(engine(runtime_control),[statistics/2]).
:- use_module(library(lists),[length/2]).

rev_naive(N,T) :-
    length(L,N),
    statistics(walltime, [_,_]),
    list_reverse(L,_RL),
    statistics(walltime, [_,T]).
rev_acc(N,T) :-
    length(L,N),
    statistics(walltime, [_,_]),
    reverse_acc(L,_RL),
    statistics(walltime, [_,T]).

% Try: 100, 1000, 10000, 20000, 100000, 1000000

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

binary_tree(void).
binary_tree(tree(_Element,Left,Right)) :- 
    binary_tree(Left),
    binary_tree(Right).

% Try:
% ?- tree_example(T), binary_tree(T).
% ?- binary_tree(tree(a, b, c)).
% ?- binary_tree(tree(a, [], [])).
% ?- binary_tree(T).

binary_t := void | tree(_Element,~binary_t,~binary_t). 

% -------------------------------------------------------------------
%% tree_member(X,tree(X,Left,Right)).

tree_member(X,tree(X,Left,Right)) :- 
    binary_tree(Left),
    binary_tree(Right).
tree_member(X,tree(_,Left,_Right)) :- 
    tree_member(X,Left). 
tree_member(X,tree(_,_Left,Right)) :- 
    tree_member(X,Right).

% Try:
% ?- tree_example(_T), tree_member(b, _T).
% ?- tree_example(_T), tree_member(X, _T).
% ?- tree_example(_T), tree_member(e, _T).
% ?- tree_member(e,T).
% ?- tree_member(e,T), tree_member(a,T).

tree_example(  tree( a,
                   tree( b,
                         void,
                         void
                       ),
                   tree( c,
                         tree( b,
                               void,
                               void
                               ),
                         void
                       )
                   )).

% ?- tree_mem_f(X) := tree(X,~binary_tree,~binary_tree).
% ?- tree_mem_f(X) := tree(_Y,~tree_mem_f(X),_Right).
% ?- tree_mem_f(X) := tree(_Y,_Left,~tree_mem_f(X)).

tree_mem_f(X) := tree(X,~binary_tree,~binary_tree)
               | tree(_Y,~tree_mem_f(X),_Right)
               | tree(_Y,_Left,~tree_mem_f(X)).

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

pre_order(void, []).
pre_order(tree(X,Left,Right), Elements) :-
    pre_order(Left, ElementsLeft),
    pre_order(Right, ElementsRight),
    list_append([X|ElementsLeft], ElementsRight, Elements).

in_order(void, []).
in_order(tree(X,Left,Right), Elements) :-
    in_order(Left, ElementsLeft),
    in_order(Right, ElementsRight),
    list_append(ElementsLeft, [X|ElementsRight], Elements).

post_order(void, []).
post_order(tree(X,Left,Right), Elements) :-
    post_order(Left, ElementsLeft),
    post_order(Right, ElementsRight),
    list_append(ElementsRight, [X], ElementsRight2),
    list_append(ElementsLeft, ElementsRight2, Elements).
	
%% Queries:
%% tree_example(_T),pre_order(_T,List).
%% tree_example(_T),in_order(_T,List).
%% tree_example(_T),post_order(_T,List).  (node list generation)
%% post_order(X,[a,b]).                   (tree generation)
%% tree_example(_T),post_order(_T,[Y|_]). (leftmost leaf)
% -------------------------------------------------------------------

lt_member(X, [X|Y]) :- list(Y).
lt_member(X, [_|T]) :- lt_member(X, T).

lt_member(X, tree(X, L, R)) :- binary_tree(L), binary_tree(R).
lt_member(X, tree(_Y, L, _R)) :- lt_member(X, L). 
lt_member(X, tree(_Y, _L, R)) :- lt_member(X, R).

%% Queries:
%% lt_member(M,[1,2,3]).
%% tree_example(_T), lt_member(M,_T).
%% But: 
%% lt_member(M,T).
%% mixed type!


lt_member_separate(X, Y) :- list_member(X, Y).
lt_member_separate(X, Y) :- tree_member(X, Y).

%% Queries:
%% lt_member_separate(M,[1,2,3]).
%% tree_example(_T), lt_member_separate(M,_T).
%% And: 
%% lt_member_separate(M,T).
%% separated types!

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

polynomial(X,X).
polynomial(Term,_X)  :- 
    pconstant(Term).
polynomial(Term1+Term2,X)  :- 
    polynomial(Term1,X),
    polynomial(Term2,X). 
polynomial(Term1-Term2,X)  :- 
    polynomial(Term1,X), 
    polynomial(Term2,X).
polynomial(Term1*Term2,X)  :- 
    polynomial(Term1,X), 
    polynomial(Term2,X).
polynomial(Term1/Term2,X)  :- 
    polynomial(Term1,X), 
    pconstant(Term2).
polynomial(Term1^N,X)  :- 
    polynomial(Term1,X), 
    nat_num(N).

pconstant(X) :- nat_num(X).
pconstant(a).
pconstant(b).
pconstant(c).

% Try:
% ?- polynomial(a * x ^ s(s(0)) + b, x).
% ?- polynomial(P, x).
% ?- polynomial(    a * x ^ x + b,         x). - No

% Version using functional notation.
% Note that arguments are reversed in this case!
poly_f(X) := X
    | ~pconst_f
    | ~poly_f(X) + ~poly_f(X)
    | ~poly_f(X) - ~poly_f(X)
    | ~poly_f(X) * ~poly_f(X)
    | ~poly_f(X) / ~pconst_f
    | ~poly_f(X) ^ ~nat_num. 

pconst_f := ~nat_num | a | b | c.

% Try:
% ?- poly_f(x, a * x ^ s(s(0)) + b).
% ?- poly_f(x, P).
% ?- poly_f(x, a * x ^ x + b ).  (No)

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

deriv(X,     X, s(0)                 ).
deriv(C,    _X, 0                    ) :- pconstant(C).
deriv(U+V,   X, DU+DV                ) :- deriv(U,X,DU), deriv(V,X,DV). 
deriv(U-V,   X, DU-DV                ) :- deriv(U,X,DU), deriv(V,X,DV).
deriv(U*V,   X, DU*V+U*DV            ) :- deriv(U,X,DU), deriv(V,X,DV).
deriv(U/V,   X, (DU*V-U*DV)/V^s(s(0))) :- deriv(U,X,DU), deriv(V,X,DV).
deriv(U^s(N),X, s(N)*U^N*DU          ) :- deriv(U,X,DU), nat_num(N).
deriv(log(U),X, DU/U                 ) :- deriv(U,X,DU).

% Try:
% ?- deriv(s(s(s(0)))*x+s(s(0)),x,Y).
% ?- deriv(s(s(s(0)))*x+s(s(0)),x,0*x+s(s(s(0)))*s(0)+0).
% ?- deriv(E,x,0*x+s(s(s(0)))*s(0)+0).

% Exercise: write simplify, and run backwards.

derivf(X,          X) := s(0).
derivf(~pconstant, _) := 0.
derivf(U+V,        X) := ~derivf(U,X) + ~derivf(V,X).
derivf(U-V,        X) := ~derivf(U,X) - ~derivf(V,X).
derivf(U*V,        X) := ~derivf(U,X) * V  +  U * ~derivf(V,X).
derivf(U/V,        X) := ( ~derivf(U,X) * V - U * ~derivf(V,X) ) / V^s(s(0)).
derivf(U^s(N),     X) := s(N) * U^N * ~derivf(U,X) :- nat_num(N).
derivf(log(U),     X) := ~derivf(U,X) / U.

% Try:
% ?- derivf(s(s(s(0)))*x+s(s(0)),x,Y).
% ?- derivf(s(s(s(0)))*x+s(s(0)),x,0*x+s(s(s(0)))*s(0)+0).
% ?- derivf(E,x,0*x+s(s(s(0)))*s(0)+0).

simp(X,X) :- nat_num(X).
simp(X,X) :- pconstant(X).
simp(0*_,0).
simp(_*0,0).
simp(0+X,SX) :- simp(X,SX).
simp(X+0,SX) :- simp(X,SX).
simp(s(0)*X,SX) :- simp(X,SX).
simp(X*s(0),SX) :- simp(X,SX).
simp(X/s(0),SX) :- simp(X,SX).


simp(U+V,   S       ) :- simp(U,SU), simp(V,SV), simp(SU+SV, S). 
simp(U-V,   S       ) :- simp(U,SU), simp(V,SV), simp(SU-SV, S).
simp(U*V,   S       ) :- simp(U,SU), simp(V,SV), simp(SU*SV, S).
simp(U/V,   S       ) :- simp(U,SU), simp(V,SV), simp(SU/SV, S).
simp(U^V,   S       ) :- simp(U,SU), simp(V,SV), simp(SU^SV, S).
simp(log(U),log(SU)  ) :- simp(U,SU).

simp(X,SX) :- simp(X,NX), simp(NX,SX).


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

% -------------------------------------------------------------------
% Graph:
% (Exercise:)

% -------------------------------------------------------------------
% Graphs

% path(X,Y) : There is a path from X to Y.
% (transitive closure of the edge relationship).

path(X,Y) :-
	edge(X,Y).
path(X,Y) :-
	edge(X,Z),
	path(Z,Y).

circuit :- path(A,A).

% Note that more needed if graph is not directed!

% -------------------------------------------------------
% Example:   Logic Database + recursion + types.
%            Directed graph.
%
%   a ----> b             f
%   |       |             |
%   v       v             v
%   c ----> d ----> e     g
%           |
%           v
%           h
% -------------------------------------------------------
edge(a,b).
edge(a,c).
edge(b,d).
edge(c,d).
edge(d,e).
edge(d,h).
edge(f,g).

%% Queries:
%% path(a,e). % yes
%% path(a,g). % no
%% path(c,X). % nodes that c is path to.
%% path(X,Y). % path nodes.
%%            % Observe first variable unification.
%%            % Duplicate solutions for different paths.

% -------------------------------------------------------------------
% Exercise:
% Example. The power of unification + database.
%          Coloring a planar map with at most 4 colors.

next(blue,yellow).
next(blue,red).
next(blue,green).
next(yellow,blue).
next(yellow,red).
next(yellow,green).
next(red,blue).
next(red,yellow).
next(red,green).
next(green,blue).
next(green,yellow).
next(green,red).

map_colors(R1,R2,R3,R4,R5,R6) :-
	next(R1,R2),next(R1,R3),
	next(R1,R5),next(R1,R6),
	next(R2,R3),next(R2,R4),
	next(R2,R5),next(R2,R6),
	next(R3,R4),next(R3,R6),
	next(R5,R6).

%% Try:
%% map_colors(R1,R2,R3,R4,R5,R6).

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

% Graph example: 
% Definition of a (generic) non-deterministic, finite automaton: 
accept(S) :- initial(Q), accept_from(S, Q).

accept_from([],Q)     :- final(Q).
accept_from([X|Xs],Q) :- delta(Q, X, NewQ), accept_from(Xs,NewQ).

% A concrete automaton, defined by its initial and final states: 
initial(q0).      final(q0).
% and its transitions: 
delta(q0, a, q1). 
delta(q1, b, q0). 
delta(q1, b, q1).

%            a
%      -------------    
%      |           |   ___
%   ___|__      ___v__/   \
%   | q0 |      | q1 |     | b
%   ------      ------<    |
%      ^           |   \__/
%      |           |
%      -------------    
%            b

% Try::
% Check if these sequences accepted: 
% ?- accept([a,b,b]).
% ?- accept([a,b,b,a]).
% List all sequences of 4 chars: 
% ?- accept([A, B, C, D]).
% List all accepted sequences: 
% ?- accept(X).


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

% Graph example: 
% Definition of a (generic) non-deterministic, stack, finite automaton: 

ndsfa_accept(S) :- 
    ndsfa_initial(Q),
    ndsfa_accept_from(S, Q, []).

ndsfa_accept_from([], Q, [])  :-
    ndsfa_final(Q).
ndsfa_accept_from([X|Xs], Q, S) :-  
    ndsfa_delta(Q, X, S, NewQ, NewS),
    ndsfa_accept_from(Xs, NewQ, NewS).

% A concrete automaton, defined by its initial and final states: 
ndsfa_initial(q0).     
ndsfa_final(q1).

ndsfa_delta(q0, X,     Xs, q0, [X|Xs]).
ndsfa_delta(q0, X,     Xs, q1, [X|Xs]).
ndsfa_delta(q0, _,     Xs, q1,     Xs).
ndsfa_delta(q1, X, [X|Xs], q1,     Xs).

% Try:
% Check if these sequences accepted: 
% ?- ndsfa_accept([a,b,b,a]).
% ?- ndsfa_accept([a,b,c,b,a]).
% ?- ndsfa_accept([a,b,c,c,b,a]).
% ?- ndsfa_accept([a,b,X,a]).
% List all sequences of 4 chars: 
% ?- ndsfa_accept([A, B, C, D]).
% List all accepted sequences: 
% ?- ndsfa_accept(X).

% What is the name of the sequences it reconizes? 


% Alternative: accept only words formed with symbols of 
%              a particular alphabet.
 
ndsfa_accept_alt(S) :- 
    ndsfa_initial_alt(Q),
    ndsfa_accept_from_alt(S, Q, []).

ndsfa_accept_from_alt([], Q, [])  :-
    ndsfa_final_alt(Q).
ndsfa_accept_from_alt([X|Xs], Q, S) :-  
    ndsfa_delta_alt(Q, X, S, NewQ, NewS),
    ndsfa_accept_from_alt(Xs, NewQ, NewS).

% A concrete automaton, defined by its initial and final states: 
ndsfa_initial_alt(q0).     
ndsfa_final_alt(q1).

ndsfa_delta_alt(q0, X,     Xs, q0, [X|Xs]) :- symbol(X).
ndsfa_delta_alt(q0, X,     Xs, q1, [X|Xs]) :- symbol(X).
ndsfa_delta_alt(q0, X,     Xs, q1,     Xs) :- symbol(X).
ndsfa_delta_alt(q1, X, [X|Xs], q1,     Xs) :- symbol(X).
symbol(a).
symbol(b).
symbol(c).

% Try:
% Check if these sequences accepted: 
% ?- ndsfa_accept_alt([a,b,b,a]).
% ?- ndsfa_accept_alt([a,b,c,b,a]).
% ?- ndsfa_accept_alt([a,b,c,c,b,a]).
% ?- ndsfa_accept_alt([a,b,X,a]).
% List all sequences of 4 chars: 
% ?- ndsfa_accept_alt([A, B, C, D]).
% List all accepted sequences: 
% ?- ndsfa_accept_alt(X).



% -------------------------------------------------------------------
% Towers of Hanoi: Move N disks from peg A to peg B using peg C.

hanoi_moves(N,Moves) :-
	hanoi(N,a,b,c,Moves).

hanoi(s(0),A,B,_,[move(A, B)]).
hanoi(s(N),A,B,C,Moves) :- 
    hanoi(N,A,C,B,Moves1),
    hanoi(N,C,B,A,Moves2), 
    list_append(Moves1,[move(A, B)|Moves2],Moves).

% Try:
% ?- hanoi_moves(s(s(s(0))),M).
% ?- hanoi_moves(s(s(s(0))),M), hanoi_moves(N,M).
% ?- hanoi_moves(N,M).

% Try:
% ?- hanoi_test(D).
% and hit Next for increasing numbers of disks.
% Execution time is exponential in the number of disks!

% Note: this Prolog predicate is not pure!
hanoi_test(D) :- 
    between(1,1000,D), 
    decimal_peano(D,N), 
    statistics(walltime, [_,_]),
    hanoi_moves(N,M),
    statistics(walltime, [_,T]),
    length(M,L),
    write(D), write(' disks = '),
    write(L), write(' moves in '),
    write(T), write(' mS'), nl.




% Auxiliary predicates: 
:- use_module(engine(runtime_control),[statistics/2]).
:- use_module(library(write),[write/1]).
:- use_module(engine(io_basic),[nl/0]).
:- use_module(library(lists),[length/2]).
:- use_module(engine(stream_basic),[flush_output/0]).
:- use_module(library(between)).
:- use_module(library(system),[pause/1]).

%% list_append([],L,L) :- 
%%     list(L).
%% list_append([X|Xs],Ys,[X|Zs]) :- 
%%     list_append(Xs,Ys,Zs).

%% list([]).
%% list([_|Y]) :-
%%      list(Y).

decimal_peano(0,0).
decimal_peano(N,s(X)) :-
    N>0,
    NN is N-1,
    decimal_peano(NN,X).



% Aux: 

peano_decimal(P,D) :-
    peano_decimal_(P,0,D).

peano_decimal_(0,N,N).
peano_decimal_(s(X),A,N) :-
    NA is A+1,
    peano_decimal_(X,NA,N). 


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

% -------------------------------------------------------------------
% Hanoi decl: Move N disks from peg A to peg B using peg C.

%% % Simple cases with empty target peg

% Can move A to B
can_move([DA|DAs],       [],       C,
              DAs,     [DA],       C, move(a,b)).

% Can move B to A
can_move(      [], [DB|DBs],       C,
             [DB],      DBs,       C, move(b,a)).

% Can move A to C
can_move([DA|DAs],        B,      [],
              DAs,        B,    [DA], move(a,c)).

% Can move C to A
can_move(     [],         B, [DC|DCs],
            [DC],         B,     DCs, move(c,a)).

% Can move B to C
can_move(      A,  [DB|DBs],      [],
               A,       DBs,    [DB], move(b,c)).

% Can move C to B
can_move(      A,       [], [DC|DCs],
               A,     [DC],      DCs, move(c,b)).

%% % Cases when target peg not empty (need to check size)

%% % Can move A to B
%% can_move(   [DA|DAs],    [DB|DBs],           C,
%%                  DAs, [DA,DB|DBs],           C, move(A,B)) :- DA < DB.
%% 
%% % Can move B to A
%% can_move(   [DA|DAs],    [DB|DBs],           C,
%%          [DB,DA|DAs],         DBs,           C, move(B,A)) :- DB < DA.
%% 
%% % Can move A to C
%% can_move(   [DA|DAs],           B,     [DC|DCs],
%%                  DAs,           B,  [DA,DC|DCs], move(A,C)) :- DA < DC.
%% 
%% % Can move C to A
%% can_move(   [DA|DAs],           B,     [DC|DCs],
%%          [DC,DA|DAs],           B,         DCs, move(C,A)) :- DC < DA.
%% 
%% % Can move B to C
%% can_move(          A,    [DB|DBs],    [DC|DCs],
%%                    A,         DBs, [DB,DC|DCs], move(B,C)) :- DB < DC.
%% 
%% % Can move C to B
%% can_move(          A,    [DB|DBs],    [DC|DCs],
%%                    A, [DC,DB|DBs],         DCs, move(C,B)) :- DC < DB.
%% 
%% solve([],[],C,[],[],C).
%% solve(A,B,C,FA,FB,FC) :- 
%%     can_move(A,B,C,NA,NB,NC),
%%     solve(NA,NB,NC,FA,FB,FC).

%% can_move(      [],        B, [DB|DBs]).
%%              [DB],        B,      DBs).
%% 
%% 
%% 
%% can_move([DA|DAs],        B,  [DC|DCs]
%%           DAs , [DA,DB,DBs], C) :- DA < DB,  :- write('Moving B to C').

%% hanoi_moves([],[],_).
%% hanoi_moves([H],[],_).
% -------------------------------------------------------------------


