/* cut */
     p1(X,Y) :- p2(X), !, p3(Y).
     p1(X,Y) :- p4(Y).
     /* if p2 then p3 else p4 */
     p2(a).
     p2(b).
     p3(b).
     p4(a).
     p5(a).
     p5(b).
 
    
     ?- p1(a,a).
         --> no

     ?- p5(X), p1(X,X).
         --> X = b ; 
         --> no


/* equality */
     ?- f(a) == f(a).
         --> yes
     ?- c == X.
         --> no
     ?- f(X) == f(X).
         --> X = _0

     ?- f(a) \== f(a).
         --> no
     ?- c \== b.
         --> yes
     ?- f(X) \== f(X).
         --> no

     ?- X = a.
         --> X = a
     ?- f(X,Y) = f(a,b).
         --> X = a , Y = b

/* recognizers */
     ?- atom(paulette).
         --> yes
     ?- atom(friend(sandra)).
         --> no
     ?- atom(X).
         --> no
     ?- atom(123).
         --> no

     ?- integer(123).
         --> yes
     ?- integer(1.23).
         --> no

     ?- number(123).
         --> yes
     ?- number(1.23).
         --> yes
     ?- atomic(paulette).
         --> yes
     ?- atomic(friend(sandra)).
         --> no
     ?- atomic(X).
         --> no
     ?- atomic(123).
         --> yes

     ?- var(f(X)).
         --> no
     ?- var(X).
         --> X = _0

     ?- X=a, var(X).
         --> no
     ?- var(X), X=a, atom(X).
         --> X = a 
     ?- X=Y, var(X), var(Y).
         --> X = _0 , Y = _0 
     ?- X=f(Y).
         --> X = f(_1) , Y = _1 
     ?- X=f(Y), var(X).
         --> no

/* arithmetic */
     ?- 3 == 3.
         --> yes
     ?- 1+2 == +(1,2).
         --> yes
     ?- 1+2 == 3.
         --> no
     ?- 1+2 = 3.
         --> no
     ?- X is 12+44.
         --> X = 56 
     ?- X is 1+2*3.
         --> X = 7 
     ?- 7 is 1+2*3.
         --> yes
     ?- 9 is 1+2*3.
         --> no
     ?- X = 22, Y is 2*X.
         --> X = 22 , Y = 44 
     ?- X is 2+3, Y is X+X.
         --> X = 5 , Y = 10 
     ?- X = 2+3, Y is X+X.
         --> X = 2+3 , Y = 10 

     ?- X is log(2).
         --> X = 0.693147 
     ?- X is log10(2).
         --> X = 0.30103 
     ?- 3 is 2+1.
         --> yes
     ?- x is 4+3.
         --> no
     ?- X is 4+P.
         --> ! Error: not a number
     ?- f(X) is 3+8.
         --> no
     ?- X = log10(2), Y is X.
         --> X = log10(2) , Y = 0.30103 
     ?- X = Y + log10(Z), Y = 1, Z = 6-4, R is X.
         --> X=1+log10(6-4), Y=1, Z=6-4, R=1.30103 

     /* factorial */
     fact(1,1) :- !.
     fact(N,R) :- integer(N), N > 1, N1 is N-1, 
                  fact(N1,R1), R is N*R1.

     /* pattern matching */
     ?- [H|T] = [a].
         --> H = a , T = [] 
     ?- [A1,A2,_,A4 |T] = [what,we,call,a,rose].
         --> A1 = what, A2 = we, A4 = a, T = [rose] 
/* difference lists */
  dappend(Xs-Ys,Ys-Zs,Xs-Zs).

  image2(Xs,Ys) :- dimage(Xs,Ys-[]).
  dimage([],Xs-Xs).
  dimage([X|Xs],Ys-Zs) :- dimage(Xs,Ys-[X|Zs]).

  ?- dimage([a,b],L-[]).
      --> L = [b,a] 
  ?- image2([a,b,c],L).
      --> L = [c,b,a] 
  ?- image2(L,[b,a]).
      --> L = [a,b] 

  ?- dimage([a,b], L-[]).
%    dimage([b],L-[a])
%    dimage([],L-[b,a])
%    dimage([],[b,a]-[b,a])
      --> L = [b,a]

  flatten([],[]).
  flatten(X,[X]) :- atomic(X), X \= [].
  flatten([X|Xs],Ys) :-
    flatten(X,Us),
    flatten(Xs,Vs),
    append(Us,Vs,Ys).

  dflatten([],Xs-Xs).
  dflatten(X,[X|Xs]-Xs) :- atomic(X), X \= [].
  dflatten([X|Xs],Ys-Zs) :-
    dflatten(X,Us-As),
    dflatten(Xs,Vs-Bs),
    dappend(Us-As,Vs-Bs,Ys-Zs).

  dflatten([],Xs-Xs).
  dflatten(X,[X|Xs]-Xs) :- atomic(X), X \= [].
  dflatten([X|Xs],Ys-Zs) :- 
    dflatten(X,Ys-Rs),
    dflatten(Xs,Rs-Zs),
/*  dappend(Ys-Rs,Rs-Zs,Ys-Zs).  /*


/* i/o */
     ?- read(X).
         |: f(a).
         --> X = f(a) 
     ?- read(f(X)).
         |: f(p).
         --> X = p 
     ?- read(f(X)).
         |: [p].
         --> no
     ?- get(X).
         |: a
         --> X = 97 
     ?- get(X).
         |: ]
         --> X = 93 
     ?- X='Do you like cold haggis ?' , write(X).
         Do you like cold haggis ?
         --> X = Do you like cold haggis ?
     ?- put(97).
         a
         --> yes

/* findall */
     perm([],[]).
     perm([H|L],Z) :- perm(L,Y),insert(H,Y,Z).

     ?- perm([a,b,c],L).
         --> L = [a,b,c] ;
         --> L = [b,a,c] ;
         --> L = [b,c,a] ;
         --> L = [a,c,b] ;
         --> L = [c,a,b] ;
         --> L = [c,b,a] ;
         --> no

	all_perm(L) :- perm(L,R), write(R), nl, fail.

     ?- all_perm(['A', 'B', 'C']).
         [A,B,C]
         [B,A,C]
         [B,C,A]
         [A,C,B]
         [C,A,B]
         [C,B,A]
         --> no

     ?- findall(L,perm(['A', 'B', 'C'],L),LL).
         --> LL = [[A,B,C],[B,A,C],[B,C,A],
                   [A,C,B],[C,A,B],[C,B,A]]

/* term analysis */
     ?- f(a,b,c) =.. L.
         --> L = [f,a,b,c] 
     ?- f(a,b,c) =.. [F|Args].
         --> F = f , Args = [a,b,c] 
     ?- (a*b+c) =.. [Op|Args].
         --> Op = + , Args = [a*b,c] 

     ?- functor(owns(john,umbrella), F, N).
         --> F = owns , N = 2 
     ?- functor(f(a,b), f, 2).
         --> yes
     ?- arg(2, owns(john, umbrella), A).
         --> A = umbrella 
     ?- name(blabla,L).
         --> L = [98,108,97,98,108,97] 
     ?- name(bac, [A|_]) , name(X,[A]).
         --> A = 98 , X = b 

/* all */
mother(vera,julie).     father(joseluis,julie).
mother(vera,alice).     father(joseluis,alice).
mother(mary,joseluis).  father(alfonso,joseluis).
mother(anne,vera).      father(andrew,vera).
grandfather(X,Y) :- father(X,Z),mother(Z,Y).
grandfather(X,Y) :- father(X,Z),father(Z,Y).
grandmother(X,Y) :- mother(X,Z),mother(Z,Y).
grandmother(X,Y) :- mother(X,Z),father(Z,Y).

all(F) :- functor(T,F,2), T, write('the '), 
          write(F), arg(2,T,A2), write(' of '), 
          write(A2), arg(1,T,A1),
          write(' is '), write(A1),nl,fail.

     ?- all(grandmother).
         the grandmother of julie is anne
         the grandmother of alice is anne
         the grandmother of julie is mary
         the grandmother of alice is mary
         --> no

/* primitive sort */
?- sort([2,2,3,1],L).
 --> L = [1,2,3]

?- sort([[a],[a,b],f(x),f(a,b),f(a,X),X],L).
 --> X = _31 , 
     L = [_31,f(x),[a],[a,b],f(a,_31),f(a,b)] 

?- sort([[a],[a,b],f(x),f(a,b),f(a,X),X],L).
 --> L = [X,f(x),f(a,X),f(a,b),[a],[a,b]]

/* naive queens */
permut([],[]).
permut(Xs,[Z|Zs]) :- select(Z,Xs,Ys), permut(Ys,Zs).

range(N,N,[N]).
range(M,N,[M|Ns]) :- M<N, M1 is M+1, range(M1,N,Ns).

attack(X,Xs) :- attack(X,1,Xs).

attack(X,N,[Y|Ys]) :- X is Y+N.
attack(X,N,[Y|Ys]) :- X is Y-N.
attack(X,N,[Y|Ys]) :- N1 is N+1, attack(X,N1,Ys).

safe([]).
safe([Q|Qs]) :- safe(Qs), not attack(Q,Qs).

queens(N,Qs) :- range(1,N,Ns), permut(Ns,Qs), safe(Qs).

/* queens */
range(N,N,[N]).
range(M,N,[M|Ns]) :- M<N, M1 is M+1, range(M1,N,Ns).

attack(X,Xs) :- attack(X,1,Xs).

attack(X,N,[Y|Ys]) :- X is Y+N.
attack(X,N,[Y|Ys]) :- X is Y-N.
attack(X,N,[Y|Ys]) :- N1 is N+1, attack(X,N1,Ys).

queens(N,Qs) :- range(1,N,Ns), queens(Ns,[],Qs).

queens([],Qs,Qs).
queens(UQs,SQs,Qs) :- select(Q,UQs,UQs1),
                      not attack(Q,SQs),
                      queens(UQs1,[Q|SQs],Qs).

/* toy ai */
trans(S1,S2,P) :- t0(S1,S2,[S1],P).

t0(S,S,V,[]).
t0(S1,S2,V,[A|As]) :-
  legal(A,S1), 
  res(A,S1,S), 
  not member(S,V), 
  t0(S,S2,[S|V],As).

legal(m(B,Y,P),S) :- 
  on(B,Y,S), cl(B,S), p(P), cl(P,S).
legal(m(B1,Y,B2),S) :- 
  on(B1,Y,S), cl(B1,S), b(B2), B1\=B2, cl(B2,S).

on(X,Y,S) :- member([X|Y],S).

cl(X,S) :- member([Y|X],S),!,fail.
cl(X,S).

res(m(X,Y,Z),S,S1) :- sub([X|Y],[X|Z],S,S1).

member(X,[X|Xs]).
member(X,[Y|Ys]) :- member(X,Ys).

sub(X,Y,[X|Xs],[Y|Xs]).
sub(X,Y,[Z|Xs],[Z|Ys]) :- sub(X,Y,Xs,Ys).

p(p).  p(q).  p(r).  
b(a).  b(b).  b(c).  

?- trans([[a|b],[b|p],[c|r]],[[a|b],[b|c],[c|r]],Z).
   Z = [m(a,b,q),m(a,q,c),m(b,p,q),m(a,c,p),
m(a,p,b),m(c,r,p),m(a,b,r),m(a,r,c),m(b,q,r),
m(a,c,q),m(a,q,b),m(c,p,q),m(a,b,p),m(a,p,c),
m(b,r,p),m(a,c,r),m(b,p,a),m(c,q,p),m(b,a,c),
m(a,r,q),m(b,c,a),m(c,p,r),m(b,a,c),m(a,q,p),
m(a,p,b)]
Yes ,
...

/* toy ai (bis) */
trans(S1,S2,P) :- t0(S1,S2,[S1],P).

t0(S,S,V,[]).
t0(S1,S2,V,[A|As]) :-
  next(A,S1,S2), res(A,S1,S),
  not member(S,V), t0(S,S2,[S|V],As).

next(A,S1,S2) :- hint(A,S2), legal(A,S1).
next(A,S1,S2) :- legal(A,S1).

hint(m(X,Y,Z),S) :- on(X,Z,S).

legal(m(B,Y,P),S) :-
  on(B,Y,S), cl(B,S), p(P), cl(P,S).
legal(m(B1,Y,B2),S) :-
  on(B1,Y,S), cl(B1,S), b(B2), B1\=B2, cl(B2,S).

on(X,Y,S) :- member([X|Y],S).

cl(X,S) :- member([Y|X],S),!,fail.
cl(X,S).

res(m(X,Y,Z),S,S1) :- sub([X|Y],[X|Z],S,S1).

member(X,[X|Xs]).
member(X,[Y|Ys]) :- member(X,Ys).

sub(X,Y,[X|Xs],[Y|Xs]).
sub(X,Y,[Z|Xs],[Z|Ys]) :- sub(X,Y,Xs,Ys).

p(p).  p(q).  p(r).  
b(a).  b(b).  b(c).  

?- trans([[a|b],[b|p],[c|r]],[[a|b],[b|c],[c|r]],Z).
   Z = [m(a,b,q),m(b,p,c),m(a,q,b)]
Yes ,

...

/* toy ai (ter) */
solve(S,H,[]) :- final(S).
solve(S,H,[M|Ms]) :- 
  move(S,M), res(S,M,S1), legal(S1),
  not member(S1,H), solve(S1,[S1|H],Ms).

test(P,M) :- initial(P,S), solve(S,[S],M).
initial(s0,[gauche,[loup,chevre,chou],[]]).
final([droite,[],[loup,chevre,chou]]).

move([gauche,G,D],C) :- member(C,G).
move([droite,G,D],C) :- member(C,D).
move([B,G,D],alone) .

res([B,G,D],C,[B1,G1,D1]) :- rb(B,B1),rr(C,B,G,D,G1,D1).

rb(gauche,droite).
rb(droite,gauche).

rr(alone,B,G,D,G,D).
rr(C,gauche,G,D,G1,D1) :- select(C,G,G1),insert(C,D,D1).
rr(C,droite,G,D,G1,D1) :- select(C,D,D1),insert(C,G,G1).

select(X,[X|Xs],Xs).
select(X,[Y|Xs],[Y|Ys]) :- select(X,Xs,Ys).

insert(X,[],[X]).
insert(X,[Y|Ys],[X,Y|Ys]) :- avant(X,Y).
insert(X,[Y|Ys],[Y|Zs]) :- avant(Y,X), insert(X,Ys,Zs).

avant(loup,X).
avant(X,chou).

legal([gauche,G,D]) :- not illegal(D).
legal([droite,G,D]) :- not illegal(G).

illegal(R) :- member(loup,R), member(chevre,R).
illegal(R) :- member(chevre,R), member(chou,R).

member(X,[X|Xs]).
member(X,[Y|Ys]) :- member(X,Ys).

?- test(P,M).
  P = s0
  M = [chevre,alone,loup,chevre,chou,alone,chevre]
Yes ,
  P = s0
  M = [chevre,alone,loup,chevre,chou,alone,chevre]
Yes ,
  P = s0
  M = [chevre,alone,chou,chevre,loup,alone,chevre]
Yes ,
  P = s0
  M = [chevre,alone,chou,chevre,loup,alone,chevre]
Yes ,
No





/* term analysis (bis) */
subterm(Term,Term).
subterm(Sub,Term) :- compound(Term), 
                     functor(Term,F,N),
                     subterm(N,Sub,Term).

subterm(N,Sub,Term) :- arg(N,Term,Arg), 
                       subterm(Sub,Arg).
subterm(N,Sub,Term) :- N > 1, N1 is N-1,
                       subterm(N1,Sub,Term).

substitute(Old,New,Old,New).

substitute(Old,New,Term,Term)
 :- atomic(Term) , Term \= Old.

substitute(Old,New,Term,Term1)
 :- compound(Term),
    functor(Term,F,N),
    functor(Term1,F,N),
    substitute(N,Old,New,Term,Term1).

substitute(N,Old,New,Term,Term1)
 :- N > 0,
    arg(N,Term,Arg),
    substitute(Old,New,Arg,Arg1),
    arg(N,Term1,Arg1),
    N1 is N-1,
    substitute(N1,Old,New,Term,Term1).

substitute(0,Old,New,Term,Term1).

/* trace */
substitute(cat,dog,owns(jane,cat),X)      X=owns(jane,
    atomic(owns(jane,cat))               f       cat)
substitute(cat,dog,owns(jane,cat),X)
    compound(owns(jane,cat))
    functor(owns(jane,cat),F,N)           F=owns, N=2
    functor(X,owns,2)                     X=owns(X1,X2)
    substitute(2,cat,dog,
               owns(jane,cate),owns(X1,X2))
        2 > 0
        arg(2,owns(jane,cat),Arg)         Arg=cat
        substitute(cat,dog,cat,Arg1)      Arg1=dog
        arg(2,owns(X1,X2),dog)            X2=dog
        N1 is 2-1                         N1=1
        substitute(1,cat,dog,
                   owns(jane,cat),owns(X1,dog))
            1 > 0
            arg(1,owns(jane,cat),Arg2)    Arg2=jane
            substitute(cat,dog,jane,Arg3) Arg3=jane
                atomic(jane)
                jane \= cat
            arg(1,owns(X1,dog),jane)      X1=jane
            N2 is 1-1                     N2=0
            substitute(0,cat,dog,
                       owns(jane,cat),owns(jane,dog))
                0 > 0                    f
            substitute(0,cat,dog,
                       owns(jane,cat),owns(jane,dog))
                true
                    Output: (X=owns(jane,dog))

/* metalogic predicates */
plus(X,Y,Z) :- nonvar(X), nonvar(Y), Z is X+Y.

plus(X,Y,Z) :- nonvar(X), nonvar(Z), Y is Z-X.

plus(X,Y,Z) :- nonvar(Y), nonvar(Z), X is Z-Y.

grandparent(X,Z) :- nonvar(X),
                    parent(X,Y), parent(Y,Z).

grandparent(X,Z) :- nonvar(Z),
                    parent(Y,Z), parent(X,Y).

ground(Term) :- nonvar(Term),
                atomic(Term).

ground(Term) :- nonvar(Term),
                compound(Term),
                functor(Term,F,N),
                ground(N,Term).

ground(0,Term).

ground(N,Term) :- N > 0,
                  arg(N,Term,Arg),
                  ground(Arg),
                  N1 is N-1,
                  ground(N1,Term).

/* unification */
unify0(X,X).

unify(X,Y) :- var(X), var(Y), X=Y.

unify(X,Y) :- var(X), nonvar(Y), X=Y.

unify(X,Y) :- var(Y), nonvar(X), Y=X.

unify(X,Y) :- nonvar(X), nonvar(Y),
              atomic(X), atomic(Y), X=Y.

unify(X,Y) :- nonvar(X), nonvar(Y),
              compound(X), compound(Y),
              term_unify(X,Y).

term_unify(X,Y) :- functor(X,F,N),
                   functor(Y,F,N),
                   unify_args(N,X,Y).

unify_args(N,X,Y) :- N > 0,
                     unify_arg(N,X,Y),
                     N1 is N-1,
                     unify_args(N1,X,Y).

unify_args(0,X,Y).

unify_arg(N,X,Y) :- arg(N,X,ArgX),
                    arg(N,Y,ArgY),
                    unify(ArgX,ArgY).

/* no occurrence ? */
unify(X,Y) :- var(X), var(Y), X=Y.
unify(X,Y) :- var(X), nonvar(Y), no_oc(X,Y), X=Y.
unify(X,Y) :- var(Y), nonvar(X), no_oc(Y,X), Y=X.
unify(X,Y) :- nonvar(X), nonvar(Y),
              atomic(X), atomic(Y), X=Y.
unify(X,Y) :- nonvar(X), nonvar(Y),
              compound(X), compound(Y),
              term_unify(X,Y).

term_unify(X,Y) :- functor(X,F,N), functor(Y,F,N),
                   unify_args(N,X,Y).
unify_args(N,X,Y) :- N > 0, unify_arg(N,X,Y),
                     N1 is N-1, unify_args(N1,X,Y).
unify_args(0,X,Y).
unify_arg(N,X,Y) :- arg(N,X,ArgX), arg(N,Y,ArgY),
                    unify(ArgX,ArgY).

no_oc(X,Y) :- var(Y), X \== Y.
no_oc(X,Y) :- nonvar(Y), atomic(Y).
no_oc(X,Y) :- nonvar(Y), compound(Y),
              functor(Y,F,N), no_oc(N,X,Y).

no_oc(N,X,Y) :- N > 0, arg(N,Y,Arg), no_oc(X,Arg),
                N1 is N-1, no_oc(N1,X,Y).

no_oc(0,X,Y).

/* memoize */
hanoi_1(0,A,B,C,0) :- !.
hanoi_1(N,A,B,C,NMoves) :-
   N1 is N-1, 
   hanoi_1(N1,A,C,B,NM1),
   hanoi_1(N1,C,B,A,NM2),
   NMoves is NM1+1+NM2.

hanoi_2(0,A,B,C,0) :- !.
hanoi_2(N,A,B,C,NMoves) :- 
   N1 is N-1, 
   lemma(hanoi_2(N1,A,C,B,NM1)),
   hanoi_2(N1,C,B,A,NM2),
   NMoves is NM1+1+NM2.

lemma(P) :- P, asserta((P :- !)).

test_hanoi_2(N,LPegs,NMoves) :- 
   hanoi_2(N,A,B,C,NMoves),
   LPegs = [A,B,C].


| ?- listing.
append('[]', A, A).
append([B|C], A, [B|D]) :-
        append(C, A, D).
hanoi_1(0, _, _, _, 0) :- !.
hanoi_1(A, B, C, D, E) :-
        F is A-1,
        hanoi_1(F, B, D, C, G),
        hanoi_1(F, D, C, B, H),
        E is G+1+H.
hanoi_2(0, _, _, _, 0) :- !.
hanoi_2(A, B, C, D, E) :-
        F is A-1,
        lemma(hanoi_2(F,B,D,C,G)),
        hanoi_2(F, D, C, B, H),
        E is G+1+H.
lemma(A) :-
        A,
        asserta((A:-'!')).
test_hanoi_2(A, B, C) :-
        hanoi_2(A, D, E, F, C),
        B=[D,E,F].

| ?- hanoi_1(12,a,b,c,LM).

LM = 4095?
yes        /* TRES LENT !! */

| ?- test_hanoi_2(12,[a,b,c],LM).

LM = 4095?
yes        /* TRES RAPIDE !! */

| ?- listing.
append('[]', A, A).
append([B|C], A, [B|D]) :-
        append(C, A, D).
hanoi_1(0, _, _, _, 0) :- !.
hanoi_1(A, B, C, D, E) :-
        F is A-1,
        hanoi_1(F, B, D, C, G),
        hanoi_1(F, D, C, B, H),
        E is G+1+H.

hanoi_2(11, _, _, _, 2047) :- !.
hanoi_2(10, _, _, _, 1023) :- !.
hanoi_2(9, _, _, _, 511) :- !.
hanoi_2(8, _, _, _, 255) :- !.
hanoi_2(7, _, _, _, 127) :- !.
hanoi_2(6, _, _, _, 63) :- !.
hanoi_2(5, _, _, _, 31) :- !.
hanoi_2(4, _, _, _, 15) :- !.
hanoi_2(3, _, _, _, 7) :- !.
hanoi_2(2, _, _, _, 3) :- !.
hanoi_2(1, _, _, _, 1) :- !.
hanoi_2(0, _, _, _, 0) :- !.
hanoi_2(A, B, C, D, E) :-
        F is A-1,
        lemma(hanoi_2(F,B,D,C,G)),
        hanoi_2(F, D, C, B, H),
        E is G+1+H.
lemma(A) :-
        A,
        asserta((A:-'!')).
test_hanoi_2(A, B, C) :-
        hanoi_2(A, D, E, F, C),
        B=[D,E,F].




/* METAINTERPRETATION */
toy_shell :- prompt, read(G), toy_shell(G).

toy_shell(exit) :- !.
toy_shell(G) :- ground(G), !, solve_g(G), toy_shell.
toy_shell(G) :- solve_ng(G), toy_shell.

solve_ng(G) :- G, write(G), nl, fail.
solve_ng(G) :- write('No (more) solution'), nl.

solve_g(G) :- G, !, write('Yes'), nl.
solve_g(G) :- write('No'), nl.

prompt :- write('Next command ? ').


?- toy_shell.
Next command ? append(X,Y,[1,2,3,4]).
append([],[1,2,3,4],[1,2,3,4])
append([1],[2,3,4],[1,2,3,4])
append([1,2],[3,4],[1,2,3,4])
append([1,2,3],[4],[1,2,3,4])
append([1,2,3,4],[],[1,2,3,4])
No (more) solution
Next command ? X is 2+3 .
5 is 2+3
No (more) solution
Next command ? exit.

Yes

?- toy_shell.
Next command ? append(X,[a,b],Y).
append([],[a,b],[a,b])
append([_1],[a,b],[_1,a,b])
append([_1,_2,_3],[a,b],[_1,_2,_3,a,b])
[diverge]

% 3
solve(true).
solve((A,B)) :- solve(A),solve(B).
solve(A) :- rule(A,B),solve(B).

A.		  
B :- C,D.	    
E :- F,G,H.

rule(A,true).	  
rule(B,(C,D)).  
rule(E,(F,(G,H))).

% 4
rule(member(X,[X|Ys]),true).
rule(member(X,[Y|Ys]),member(X,Ys)).

?- solve(member(X,[a,b,c])).
Call: solve(member(_1,[a,b,c])) ? 
  Call: rule(member(_1,[a,b,c]),_2) ? 
  Exit: rule(member(a,[a,b,c]),true) ? 
  Call: solve(true) ? 
  Exit: solve(true) ? 
Exit: solve(member(a,[a,b,c])) ? 
X = a ;

  Redo: rule(member(_1,[a,b,c]),_2) ? 
  Exit: rule(member(_1,[a,b,c]),member(_1,[b,c])) ? 
  Call: solve(member(_1,[b,c])) ? 
    Call: rule(member(_1,[b,c]),_4) ? 
    Exit: rule(member(b,[b,c]),true) ? 
    Call: solve(true) ? 
    Exit: solve(true) ? 
  Exit: solve(member(b,[b,c])) ? 
Exit: solve(member(b,[a,b,c])) ? 
X = b ;
...

% 5
solve([]) :- !.
solve([G|Gs]) :- !, rule(G,T), 
                 append(T,Gs,Gs1), solve(Gs1).
solve(G) :- solve([G]).

% CPS
solve(G) :- solve(G,[]).

solve([],[]).
solve([],[G|Gs]) :- solve(G,Gs).
solve([A|B],Gs) :- append(B,Gs,Gs1), solve(A,Gs1).
solve(A,Gs) :- rule(A,B), solve(B,Gs).


% 6
dis_gl([],L) :- !.
dis_gl(G,0) :- !, dis_gl(G), display('?\n').
dis_gl(G,L) :- L1 is L-1, display('  '), dis_gl(G,L1).

dis_sl([],L) :- !.
dis_sl(G,0) :- !, dis_gl(G), display('!\n').
dis_sl(G,L) :- L1 is L-1, display('  '), dis_sl(G,L1).

dis_gl([]) :- !.
dis_gl([G]) :- !, display(G).
dis_gl([G1|[G2|Gs]]) :- !, display(G1), display(','),
                        dis_gl([G2|Gs]).
dis_gl(G) :- dis_gl([G]).

solve([],L) :- !.
solve([G|Gs],L) :- !, rule(G,T), L1 is L+1,
                   append(T,Gs,Gs1), dis_gl(Gs1,L1),
                   solve(Gs1,L1), dis_sl(Gs1,L1).
solve(G,L) :- solve([G],L).

metatrace(G) :- dis_gl(G,1), solve(G,1), dis_sl(G,1).

% 7
rule(append([],Ys,Ys),[]).
rule(append([X|Xs],Ys,[X|Zs]), [append(Xs,Ys,Zs)]).


?- metatrace(append([a,b],[c,d],Xs)).
  append([a,b],[c,d],_10)?
    append([b],[c,d],_20)?
      append([],[c,d],_30)?
      append([],[c,d],[c,d])!
    append([b],[c,d],[b,c,d])!
  append([a,b],[c,d],[a,b,c,d])!
  Xs = [a,b,c,d]
Yes ,
No

% 8-9
rule(member(X,[X|Ys]),[]).
rule(member(X,[Y|Ys]),[member(X,Ys)]).
rule(member2a(X,Xss),[member(X,Xs),member(Xs,Xss)]).
rule(member2b(X,Xss),[member(Xs,Xss),member(X,Xs)]).

?- metatrace(member2a(X,[[a],[b,c]])).
  member2a(_1,[[a],[b,c]])?
    member(_1,_2),member(_2,[[a],[b,c]])?
      member([_1|_3],[[a],[b,c]])?
      member([a],[[a],[b,c]])!
    member(a,[a]),member([a],[[a],[b,c]])!
  member2a(a,[[a],[b,c]])!
X = a ;
        member([_1|_3],[[b,c]])?
        member([b,c],[[b,c]])!
      member([b,c],[[a],[b,c]])!
    member(b,[b,c]),member([b,c],[[a],[b,c]])!
  member2a(b,[[a],[b,c]])!
X = b ;
          member([_1|_3],[])?
      member(_1,_3),member([_4|_3],[[a],[b,c]])?
        member([_4,_1|_5]),[[a],[b,c]])?
          member([_4,_1|_5]),[[b,c]])?
          member([b,c],[[b,c]])!
        member([b,c],[[a],[b,c]])!
      member(c,[c]),member([b,c],[[a],[b,c]])!
    member(c,[b,c]),member([b,c],[[a],[b,c]])!
  member2a(c,[[a],[b,c]])!
X = c ;
            member([_4,_1|_5]),[])?
        member(_1,_5),member([_4,_6|_5],[[a],[b,c]])?
          member([_4,_6,_1|_7],[[a],[b,c]])?
            member([_4,_6,_1|_7],[[b,c]])?
              member([_4,_6,_1|_7],[])?
          member(_1,_7),member([_4,_6,_8|_7],
                               [[a],[b,c]])?
[diverge]

% 10
?- metatrace(append(Xs,Ys,[a,b,c])).
  append(_8,_9,[a,b,c])?
  append([],[a,b,c],[a,b,c])!
  Xs = []
  Ys = [a,b,c] ;
    append(_58,_9,[b,c])?
    append([],[b,c],[b,c])!
  append([a],[b,c],[a,b,c])!
  Xs = [a]
  Ys = [b,c] ;
      append(_78,_9,[c])?
      append([],[c],[c])!
    append([b],[c],[b,c])!
  append([a,b],[c],[a,b,c])!
  Xs = [a,b]
  Ys = [c] ;
        append(_98,_9,[])?
        append([],[],[])!
      append([c],[],[c])!
    append([b,c],[],[b,c])!
  append([a,b,c],[],[a,b,c])!
  Xs = [a,b,c]
  Ys = [] ;
No

% 11
rule(pere(eric,jeanne), []).
rule(pere(paul,jacques), []).
rule(pere(paul,catherine), []).

rule(mere(francoise,catherine), []).
rule(mere(catherine,marie), []).
rule(mere(catherine,jeanne), []).
rule(mere(marie,nathalie), []).

rule(parent(X,Y), [pere(X,Y)]).
rule(parent(X,Y), [mere(X,Y)]).

rule(grandparent(X,Y), [parent(X,Z), parent(Z,Y)]).

% 12-13
?- metatrace(grandparent(X,marie)).
  grandparent(_8,marie)?
    parent(_8,_49),parent(_49,marie)?
      pere(_8,_49),parent(_49,marie)?
        parent(jeanne,marie)?
          pere(jeanne,marie)?
          mere(jeanne,marie)?
        parent(jacques,marie)?
          pere(jacques,marie)?
          mere(jacques,marie)?
        parent(catherine,marie)?
          pere(catherine,marie)?
          mere(catherine,marie)?
          mere(catherine,marie)!
        parent(catherine,marie)!
      pere(paul,catherine),parent(catherine,marie)!
    parent(paul,catherine),parent(catherine,marie)!
  grandparent(paul,marie)!
X = paul ;
      mere(_8,_49),parent(_49,marie)?
        parent(catherine,marie)?
          pere(catherine,marie)?
...   ...   ...   ...   ...   
X = francoise ;
        parent(marie,marie)?
...   ...   ...   ...   ...   
No

% 14
dis_gl([],0) :- !,display('empty goal\n').
dis_gl(G,0) :- !, dis_gl(G), display('?\n').
dis_gl(G,L) :- L1 is L-1, display('  '), dis_gl(G,L1).

dis_gl([]) :- !.
dis_gl([G]) :- !,display(G).
dis_gl([G1|[G2|Gs]]) :-
        !, display(G1), display(','), dis_gl([G2|Gs]).
dis_gl(G) :- dis_gl([G]).

dis_rl(H,[],0) :- !, display(' {'), display(H), display('.}\n').
dis_rl(H,T,0) :- !, display(' {'), display(H),
                 display(' :- '), dis_gl(T), display('.}\n').
dis_rl(H,T,L) :- L1 is L-1, display('  '), dis_rl(H,T,L1).

dis_deduc([],H) :- !, display(H), display('\n').
dis_deduc(T,H) :- dis_gl(T), display(' => '),
                  display(H), display('\n').

norule(0) :- !, display(' {cannot unify.}\n').
norule(L) :- L1 is L-1,display('  '),norule(L1).

find_rl(H,L) :- rule(H1,T1), not not (H1 = H), !.
find_rl(H,L) :- norule(L).

solve([],L) :- !, display('Proof:\n').
solve([G|Gs],L) :- !, find_rl(G,L), rule(G,T), dis_rl(G,T,L),
                   L1 is L+1, append(T,Gs,Gs1), dis_gl(Gs1,L1),
                   solve(Gs1,L1), dis_deduc(T,G).
solve(G,L) :- solve([G],L).

metatrace(G) :- dis_gl(G,1), solve(G,1).


% 15-16
?- metatrace(grandparent(X, marie)).
  grandparent(_8,marie)?
   {grandparent(_8,marie) :- parent(_8,_64), parent(_64,marie).}
    parent(_8,_64), parent(_64,marie)?
     {parent(_8,_64) :- pere(_8,_64).}
      pere(_8,_64), parent(_64,marie)?
       {pere(eric,jeanne).}
        parent(jeanne,marie)?
         {parent(jeanne,marie) :- pere(jeanne,marie).}
          pere(jeanne,marie)?
           {cannot unify.}
         {parent(jeanne,marie) :- mere(jeanne,marie).}
          mere(jeanne,marie)?
           {cannot unify.}
       {pere(paul,jacques).}
        parent(jacques,marie)?
         {parent(jacques,marie) :- pere(jacques,marie).}
          pere(jacques,marie)?
           {cannot unify.}
         {parent(jacques,marie) :- mere(jacques,marie).}
          mere(jacques,marie)?
           {cannot unify.}
       {pere(paul,catherine).}
        parent(catherine,marie)?
         {parent(catherine,marie) :- pere(catherine,marie).}
          pere(catherine,marie)?
           {cannot unify.}
         {parent(catherine,marie) :- mere(catherine,marie).}
          mere(catherine,marie)?
           {mere(catherine,marie).}
            empty goal
...   ...   ...   ...   ...   ...   

Proof:
mere(catherine,marie)
mere(catherine,marie) => parent(catherine,marie)
pere(paul,catherine)
pere(paul,catherine) => parent(paul,catherine)
parent(paul,catherine), parent(catherine,marie)
                     => grandparent(paul,marie)
  X = paul ;

     {parent(_8,_64) :- mere(_8,_64).}
      mere(_8,_64), parent(_64,marie)?
       {mere(francoise,catherine).}
        parent(catherine,marie)?
         {parent(catherine,marie) :- pere(catherine,marie).}
          pere(catherine,marie)?
           {cannot unify.}
         {parent(catherine,marie) :- mere(catherine,marie).}
          mere(catherine,marie)?
           {mere(catherine,marie).}
            empty goal
Proof:
mere(catherine,marie)
mere(catherine,marie) => parent(catherine,marie)
mere(francoise,catherine)
mere(francoise,catherine) => parent(francoise,catherine)
parent(francoise,catherine), parent(catherine,marie)
                          => grandparent(francoise,marie)
  X = francoise ;

...   ...   ...   ...   ...   ...   

% 17
solve([not G|Gs],L) :- display('First solving '),display(G),
                       display('\n'),dis_gl(G,L),solve([G],L),!,
                       display('Successfully solved '),
                       display(G), display('\n'), fail.

solve([not G|Gs],L) :- !, display('Unsuccessfully solved '), 
                       display(G), display(', so going on\n'), 
                       L1 is L+1, dis_gl(Gs,L1), solve(Gs,L1),
                       dis_deduc([], not G).

solve([G|Gs],L) :- !, find_rl(G,L), rule(G,T), dis_rl(G,T,L),
                   L1 is L+1, append(T,Gs,Gs1), dis_gl(Gs1,L1),
                   solve(Gs1,L1), dis_deduc(T,G).

% 18

rule(element(X,[X|Xs]), []).
rule(element(X,[Y|Xs]), [element(X,Xs)]).
rule(car(X,Xs,0), [not element(X,Xs)]).
rule(car(X,Xs,1), [element(X,Xs)]).

?- metatrace(car(3,[1,2,4],X)).
  car(3,[1,2,4],_10)?
   {car(3,[1,2,4],0) :- not(element(3,[1,2,4])).}
    not(element(3,[1,2,4]))?
First solving element(3,[1,2,4])
    element(3,[1,2,4])?
     {element(3,[1,2,4]) :- element(3,[2,4]).}
      element(3,[2,4])?
       {element(3,[2,4]) :- element(3,[4]).}
        element(3,[4])?
         {element(3,[4]) :- element(3,[]).}
          element(3,[])?
           {cannot unify.}
Unsuccessfully solved element(3,[1,2,4]), so going on
      empty goal
Proof:
not(element(3,[1,2,4]))
not(element(3,[1,2,4])) => car(3,[1,2,4],0)

  X = 0;
...   ...   ...   ...   

% 19
?- metatrace(car(3,[1,2,3],X)).
  car(3,[1,2,3],_10)?
   {car(3,[1,2,3],0) :- not(element(3,[1,2,3])).}
    not(element(3,[1,2,3]))?
First solving element(3,[1,2,3])
    element(3,[1,2,3])?
     {element(3,[1,2,3]) :- element(3,[2,3]).}
      element(3,[2,3])?
       {element(3,[2,3]) :- element(3,[3]).}
        element(3,[3])?
         {element(3,[3]).}
          empty goal
Proof:
element(3,[3])
element(3,[3]) => element(3,[2,3])
element(3,[2,3]) => element(3,[1,2,3])
Successfully solved element(3,[1,2,3])
   {car(3,[1,2,3],1) :- element(3,[1,2,3]).}
    element(3,[1,2,3])?
     {element(3,[1,2,3]) :- element(3,[2,3]).}
      element(3,[2,3])?
       {element(3,[2,3]) :- element(3,[3]).}
        element(3,[3])?
         {element(3,[3]).}
          empty goal
Proof:
element(3,[3])
element(3,[3]) => element(3,[2,3])
element(3,[2,3]) => element(3,[1,2,3])
element(3,[1,2,3]) => car(3,[1,2,3],1)

  X = 1 ;
...   ...   

% 20-22
solve(G,L,0) :- !, display('Overflow !!\n'), fail.
solve([],L,DL) :- !, display('Proof:\n').
solve([G|Gs],L,DL) :- !, find_rl(G,L), rule(G,T), 
     dis_rl(G,T,L), L1 is L + 1, DL1 is DL - 1, 
     append(T,Gs,Gs1), dis_gl(Gs1,L1),
     solve(Gs1,L1,DL1), dis_deduc(T,G).
solve(G,L,DL) :- solve([G],L,DL).

metatrace(G,DL) :- dis_gl(G,1), solve(G,1,DL).
metatrace(G) :- dis_gl(G,1), solve(G,1,-1).

?- metatrace(member2a(u,[[u]]),4).
  member2a(u,[[u]])?
   {member2a(u,[[u]]) :-
       member(u, _5),member(_5,[[u]]).}
    member(u,_5),member(_5,[[u]])?
     {member(u,[u|_6]).}
      member([u|_6],[[u]])?
       {member([u],[[u]]).}
        empty goal
Proof:
member([u],[[u]])
member(u,[u])
member(u,[u]),member([u],[[u]]) => member2a(u,[[u]])

Yes

?- metatrace(member2a(u,[[v]]),4).
  member2a(u,[[v]])?
   {member2a(u,[[v]]) :-
       member(u,_7),member(_7,[[v]]).}
    member(u,_7),member(_7,[[v]])?
     {member(u,[u|_8]).}
      member([u|_8],[[v]])?
       {member([u|_8],[[v]]) :- member([u|_8],[]).}
        member([u|_8],[])?
         {cannot unify.}
     {member(u,[_9|_8]) :- member(u,_8).}
      member(u,_8),member([_9|_8],[[v]])?
       {member(u,[u|_6]).}
        member(.(_9,[u|_6],[[v]])?
         {member([_9,u|_6],[[v]]) :-
             member([_9,u|_6],[]).}
          member([_9,u|_6],[])?
Overflow !!
       {member(u,[_5|_6]) :- member(u,_6).}
        member(u,_6),member([_9,_5|_6],[[v]])?
         {member(u,[u|_4]).}
          member([_9,_5,u|_4],[[v]])?
Overflow !!
         {member(u,[_3,_4]) :- member(u,_4).}
          member(u,_4),member([_9,_5,_3|_4],[[v]])?
Overflow !!

No

/* TOY EXPERT SYSTEM */
said_true(true).
said_false(false).

known(G) :- said_true(G).
known(G) :- said_false(G).

ask(G) :- query(G,Ans), assert(G,Ans).  

query(G,Ans) :- display('Is '), display(G), 
                display(' true ? (y/n)\n'),
                read_ans(Ans).

assert(G,'y') :- assert(said_true(G)).
assert(G,'n') :- assert(said_false(G)).

read_ans(Ans) :- read(Ans), check_ans(Ans), !.
read_ans(Ans) :- read_ans(Ans).

check_ans(y).
check_ans(n).

solve([G|Gs],L) :- askable(G), not known(G),
                   ask(G), fail.

solve([G|Gs],L) :- askable(G), said_true(G), !, 
                   disp_us(G,yes,L), L1 is L+1,
                   dis_gl(Gs,L1), 
                   solve(Gs,L1), dis_deduc([],G).

solve([G|Gs],L) :- askable(G), said_false(G), !, 
                   disp_us(G,no,L), fail.


disp_us(G,yes,0) :- !, display(' {user says that '),
                    display(G), display(' is true.}\n').

disp_us(G,no,0) :- !, display(' {user says that '),
                   display(G), display(' is false.}\n').

disp_us(G,Ans,L) :- L1 is L-1, display('  '),
                    disp_us(G,Ans,L1).

rule(place(D,top), [pastry(D),size(D,small)]).
rule(place(D,mid), [pastry(D),size(D,big)]).
rule(place(D,mid), [main(D)]).
rule(place(D,low), [slow(D)]).
rule(pastry(D), [type(D,cake)]).
rule(pastry(D), [type(D,bread)]).
rule(main(D), [type(D,meat)]).
rule(slow(D), [type(D,pudding)]).

askable(type(D,T)) :- !.
askable(size(D,S)) :- !.

?- metatrace(place(dish1,W)).
  place(dish1, _G244)?
   {place(dish1, top) :- pastry(dish1),
                         size(dish1, small).}
    pastry(dish1),size(dish1, small)?
     {pastry(dish1) :- type(dish1, cake).}
      type(dish1, cake),size(dish1, small)?
Is type(dish1, cake) true ? (y/n)
|: y.
       {user says that type(dish1, cake) is true.}
        size(dish1, small)?
Is size(dish1, small) true ? (y/n)
|: n.
         {user says that size(dish1, small) is false.}
     {pastry(dish1) :- type(dish1, bread).}
      type(dish1, bread),size(dish1, small)?
Is type(dish1, bread) true ? (y/n)
|: n.
       {user says that type(dish1, bread) is false.}

   {place(dish1, mid) :- pastry(dish1),
                         size(dish1, big).}
    pastry(dish1),size(dish1, big)?
     {pastry(dish1) :- type(dish1, cake).}
      type(dish1, cake),size(dish1, big)?
       {user says that type(dish1, cake) is true.}
        size(dish1, big)?
Is size(dish1, big) true ? (y/n)
|: y.
         {user says that size(dish1, big) is true.}
          empty goal
Proof:
size(dish1, big)
type(dish1, cake)
type(dish1, cake) => pastry(dish1)
pastry(dish1),size(dish1, big) => place(dish1, mid)

W = mid ;
...   ...   ...   ...   

...   ...   ...   ...   
   {place(dish1,mid) :- pastry(dish1),
                        size(dish1,big).}
    pastry(dish1), size(dish1,big)?
     {pastry(dish1) :- type(dish1,cake).}
      type(dish1,cake), size(dish1,big)?
       {user says that type(dish1,cake) is true.}
        size(dish1,big)?
Is size(dish1,big) true ? (y/n)
|: y.
         {user says that size(dish1,big) is true.}
          empty goal
Proof:
size(dish1,big)
type(dish1,cake)
type(dish1,cake) => pastry(dish1)
pastry(dish1), size(dish1,big) => place(dish1,mid)
  W = mid ;
     {pastry(dish1) :- type(dish1,bread).}
      type(dish1,bread), size(dish1,big)?
       {user says that type(dish1,bread) is false.}
   {place(dish1,mid) :- main(dish1).}
    main(dish1)?
     {cannot unify.}
   {place(dish1,low) :- slow(dish1).}
    slow(dish1)?
     {cannot unify.}
No