%%%% These headers with org-style bullets are for Emacs outshine mode.
%%%% (Try with M-x outshine-mode: the sections fold and unfold as in org.)
%% * Headers
:- module(_,_,[]).           % For pure LP, depth-first search rule
% :- module(_,_,[sr/idall]).   % For pure LP, iterative deepening search rule, all predicates
% :- 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).

% Compare the time running
% ?- time(a(X,Y)).
% or
% ?- time(b(X,Y)).
% 
% Note that optimal order depends on the variable 
% instantiation mode. E.g., for q(X,d), p(X), this 
% order is better than p(X), q(X,d).

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

a2(X,Y) :- 
    q(X,Y), 
    p(X).

b2(X,Y) :-
    qr(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.

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

% Compare the time running
% ?- time(a(X,Y)).
% or
% ?- time(b(X,Y)).
% 
% Also, the order of solutions is different:
% 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).

%% named(D,Name) :-
%%     D = dog(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).

%% * Family database 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).

% -------------------------------------------------------------------
%% * Data structures - 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 databases:

:- 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!

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

%% % Equivalently:

%% is_date(X) :-
%%     X = 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 - naturals:

%% ** Type definition

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).

rat(X/Y) :- pint(X), pint(Y).

%% ** Operations

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/3

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

%% 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/2

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

%% square(s s 0, Y).
%% square(X, s s s s 0 ).
%% square(X, Y).

% -------------------------------------------------------------------
%% ** Exercise: exp/3

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/2

factorial(0, s(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/3

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

% -------------------------------------------------------------------
%% * Defining mod(X,Y,Z)
% “Z is the remainder from dividing X by Y”

% Specification: 
% ∃Q s.t. X = Y ∗ Q + Z   ∧   Z < Y

% We can simply write the specification:
mod(X,Y,Z) :- 
    less(Z,Y),
    times(Y,_Q,W),
    plus(W,Z,X).

% 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).

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


% ?- 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).

% This second is more efficient than the first one
% for several query modes.

% -------------------------------------------------------------------
%% * 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,ackermann(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) ).

% 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 in other modes:
% ?- 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).

%% 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) ).

%% ackmann_(  0,   N, s N).
%% ackmann_(s M,   0, ~ackmann_(M, s 0)).
%% ackmann_(s M, s N, ~ackmann_(M, ~ackmann_(s M, N) )).


% -------------------------------------------------------------------
%% * Lists

% -------------------------------------------------------------------
%% ** Type definition

%% 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:

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

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

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


% -------------------------------------------------------------------
%% ** Operations on lists:

add_el(L,X,NL) :- 
    NL = [X|L]. % This never necessary!

% 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).

% Try:
% ?- list_member(b, [a,b,c]).
% ?- list_member(X, [a,b,c]).
% ?- list_member(a, L). 
% Try also uncommenting above :- use_package(sr/bfall).

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

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

% Try:
% ?- 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),
    plus(H,ST,S).

% Try:
% ?- sumlist([s(0),s(s(0)),s(0)],N).
% ?- sumlist(L,s(s(s(0)))).
% ?- sumlist(L,S).
% Try with and without bfall

% -------------------------------------------------------------------
%% ** Exercises: 
% Define prefix(X,Y): `X` is a prefix of list `Y`.
% E.g.:  prefix([a,b], [a,b,c,d]).
% Define suffix/2, sublist/2, ... 


% |----------Y---------|
% |----X----|

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).

% |----------Y---------|
%            |----X----|

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).
*/

% |----------Y---------|
% |    |---X-----|
% |    |-------Z-------|

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).


% Another definition for sublist

sublist3(X,Y) :- 
    list_append(Aux,_,Y),
    list_append(_,X,Aux).

% Another 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).

% -------------------------------------------------------------------
%% ** Lists - append:

% append(X,Y,Z): list Z is X and Y concatenated
list_append([],L,L) :- 
    list(L).
list_append([X|Xs],Ys,[X|Zs]) :- 
    list_append(Xs,Ys,Zs).

% Try:
% ?- 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

% First version - from definition
% Given a list [H|T] the reversed version has H at the 
% end of the list that is the result of reversing T

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

% Try:
% ?- 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]). 

% Try:
% ?- 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).

% Try:
% ?- 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(runtime, [_,_]),
    list_reverse(L,_RL),
    statistics(runtime, [_,T]).
rev_acc(N,T) :-
    length(L,N),
    statistics(runtime, [_,_]),
    reverse_acc(L,_RL),
    statistics(runtime, [_,T]).

% Try: 
% ?- rev_naive(N,T).
% ?- rev_acc(N,T)
% For N = 100, 1000, 10000, 20000, 100000, 100000

% -------------------------------------------------------------------
%% * (Binary) Trees 

%% ** Type definition

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

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

%% ** Exercises

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)
% -------------------------------------------------------------------
%% ** Polymorphic tree member

% We can write a 'polymorphic' member that works 
% with both lists and trees. 

%! lt_member(X,LT): X is a member of the list or tree LT.

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).

% Try:
% ?- lt_member(M,[1,2,3]).
% ?- tree_example(_T), lt_member(M,_T).

% However: 
% ?- lt_member(M,T).
% We also get elements that are of mixed type --because 
% that is what we specified! If we want to separate the 
% types:

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

% Try:
% ?- lt_member_separate(M,[1,2,3]).
% ?- tree_example(_T), lt_member_separate(M,_T).
% And: 
% ?- lt_member_separate(M,T).
% Now we obtain separated types!

%--------------------------------------------------------------------
%% ** Trees example: polynomials

%%% NEEDS TURNING OFF funtional package, or :- fun_eval arith(false).

% polynomial(T,X): `T` is a polynomial in `X`.
% E.g.: a * x ^ s(s(0)) + b

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)

% -------------------------------------------------------------------
%% ** Trees example: symbolic derivation

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( s(s(s(0)))*x+0 , V , 0*x+s(s(s(0)))*s(0) + 0 ).
% ?- deriv(E,x,0*x+s(s(s(0)))*s(0)+0).

% Exercise (not too easy): write simplify, and run backwards.

% Version using functional notation: 
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).

% -------------------------------------------------------------------
%% * Graphs

%% ** Directed, acyclic graphs (fact representation)

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

path_da(X,Y) :-
	edge_da(X,Y).
path_da(X,Y) :-
	edge_da(X,Z),
	path_da(Z,Y).

circuit_da :- path_da(A,A).

% ------------------------------------------------
% Example (directed, acyclic graph): 
%
%   a ----> b             f
%   |       |             |
%   v       v             v
%   c ----> d ----> e     g
%           |
%           v
%           h
% ------------------------------------------------

edge_da(a,b).
edge_da(a,c).
edge_da(b,d).
edge_da(c,d).
edge_da(d,e).
edge_da(d,h).
edge_da(f,g).

% Try:
% ?- path_da(a,e). % yes
% ?- path_da(a,g). % no
% ?- path_da(c,X). % Nodes that c is connected to.
% ?- path_da(X,Y). % All connected nodes.
%                  % Duplicate solutions for different paths.

% Note that more needed if graph is not directed.
% Also if it has cycles.

% -------------------------------------------------------------------
%% ** Directed, acyclic graphs (list representation)

% (Same example)
graph_da([
    edge(a,b),
    edge(a,c),
    edge(b,d),
    edge(c,d),
    edge(d,e),
    edge(d,h),
    edge(f,g) ]).

path_l(X,Y,G) :-
    list_member(edge(X,Y),G).
path_l(X,Y,G) :-
    list_member(edge(X,Z),G),
    path_l(Z,Y,G).

% Try:
% ?- graph_da(_G), path_l(a,e,_G). % yes
% ?- graph_da(_G), path_l(a,g,_G). % no
% ?- graph_da(_G), path_l(c,X,_G). % Nodes that c is connected to.
% ?- graph_da(_G), path_l(X,Y,_G). % All connected nodes.
%               % Duplicate solutions for different paths.

% -------------------------------------------------------------------
%% ** Undirected graphs

path_a(X,Y) :-
	connected_a(X,Y).
path_a(X,Y) :-
	connected_a(X,Z),
	path_a(Z,Y).

connected_a(X,Y) :- edge_da(X,Y).
connected_a(X,Y) :- edge_da(Y,X).

circuit_a :- path_a(A,A).

% Try:
% ?- path_a(a,e). % yes
% But: 
% ?- path_a(c,X). % nodes that c is conn to - but duplicates (infinite)
% ?- path_a(X,Y). % also duplicates (infinite)
% ?- path_a(a,g). % loops

% We need to deal with cycles!

% -------------------------------------------------------------------
%% ** Dealing with cycles (list representation)

% ------------------------------------------------
% Example (directed graph, with cycle): 
%
%   a <---- b             f
%   |       ^             |
%   v       |             v
%   c ----> d ----> e     g
%           |
%           v
%           h
% ------------------------------------------------

%% List representation: 
graph([
    edge(a,c),
    edge(c,d),
    edge(d,b),
    edge(b,a),
    edge(d,e),
    edge(d,h),
    edge(f,g) ]).

path(X,Y,G) :-
     list_member(edge(X,Y),G).
path(X,Y,G) :-
    list_select(edge(X,Z),G,GRest),
    path(Z,Y,GRest).

% list_select(X,L,NL): selects an element X out of list L
% and NL is L without X
list_select(X, [X|Xs], Xs).
list_select(X, [Y|Ys], [Y|Zs]) :-
     list_select(X, Ys, Zs).

% Try:
% ?- graph(_G), path(a,e,_G).
% ?- graph(_G), path(a,g,_G).
% ?- graph(_G), path(c,X,_G).
% ?- graph(_G), path(X,Y,_G).

% -------------------------------------------------------------------
%% ** Dealing with cycles in fact representation (but using negation)

path_c_g(Start, End) :-
    path_c_g_(Start, End, [Start]).

path_c_g_(End, End, _Visited).
path_c_g_(Current, End, Visited) :-
    edge(Current, Next),
    \+ list_member(Next, Visited), % Prevent revisiting nodes (cycle check)
    path_c_g_(Next, End, [Next|Visited]).

edge(a,c).
edge(c,d).
edge(d,b).
edge(b,a).
edge(d,e).
edge(d,h).
edge(f,g).

%% Also, the one in the slides:
% edge_da(a,b).
% edge_da(b,c).
% edge_da(c,a).
% edge_da(d,a).
    
%%% Printing path:
%% path_c_g(Start, End, Path) :-
%%     path_c_g_(Start, End, [Start], Path).
%% 
%% path_c_g_(End, End, Visited, Path) :-
%%     list_reverse(Visited, Path).
%% path_c_g_(Current, End, Visited, Path) :-
%%     edge(Current, Next),
%%     \+ list_member(Next, Visited), % Prevent revisiting nodes (cycle check)
%%     path_c_g_(Next, End, [Next|Visited], Path).


% -------------------------------------------------------------------
%% * Example: graph coloring
% 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 application: Non-deterministic, finite automaton

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

accept_from([],Q)     :- final(Q).
accept_from([C|Cs],Q) :- delta(Q, C, NewQ), accept_from(Cs,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 application: Non-deterministic, PushDown Automaton
%   (NPDA, automaton with stack):

% Definition of a (generic) Non-deterministic,  PushDown automaton: 
npda_accept(S) :- 
    npda_initial(Q),
    npda_accept_from(S, Q, []).

npda_accept_from([], Q, [])  :-
    npda_final(Q).
npda_accept_from([C|Cs], Q, Stack) :-  
    npda_delta(Q, C, Stack, NewQ, NewStack),
    npda_accept_from(Cs, NewQ, NewStack).

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

npda_delta(q0, C,     Stack, q0, [C|Stack]).
npda_delta(q0, C,     Stack, q1, [C|Stack]).
npda_delta(q0,_C,     Stack, q1,    Stack).
npda_delta(q1, C, [C|Stack], q1,    Stack).

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

% What is the name of the sequences it reconizes? 


% Alternative: accept only words formed with symbols of 
%              a particular alphabet.
 
npda_accept_alt(S) :- 
    npda_initial_alt(Q),
    npda_accept_from_alt(S, Q, []).

npda_accept_from_alt([], Q, [])  :-
    npda_final_alt(Q).
npda_accept_from_alt([C|Cs], Q, Stack) :-  
    npda_delta_alt(Q, C, Stack, NewQ, NewStack),
    npda_accept_from_alt(Cs, NewQ, NewStack).

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

npda_delta_alt(q0, C,     Stack, q0, [C|Stack]) :- symbol(C).
npda_delta_alt(q0, C,     Stack, q1, [C|Stack]) :- symbol(C).
npda_delta_alt(q0, C,     Stack, q1,     Stack) :- symbol(C).
npda_delta_alt(q1, C, [C|Stack], q1,     Stack) :- symbol(C).
symbol(a).
symbol(b).
symbol(c).

% Try:
% Check if these sequences accepted: 
% ?- npda_accept_alt([a,b,b,a]).
% ?- npda_accept_alt([a,b,c,b,a]).
% ?- npda_accept_alt([a,b,c,c,b,a]).
% ?- npda_accept_alt([a,b,X,a]).
% List all sequences of 4 chars: 
% ?- npda_accept_alt([A, B, C, D]).
% List all accepted sequences: 
% ?- npda_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).

%% ** Measuring performance: 

% 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). 

%%% Local Variables:
%%% mode: ciao
%%% eval: (outshine-mode)
%%% End: