% Le plus simple ...

solve(A) :- A.



% toy_shell

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

% encore très simple

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


% On remplace ``(E,(F,(G,H)))'' par ``[E,F,G,H]''.

% style classique

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

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


% Affichage indenté des sous-buts.

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

% exemples

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

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

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

% plus informatif

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

% La négation

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

% Détection des branches trop longues

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

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

% SYSTEME EXPERT

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

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

/* Exemple d'utilisation

?- 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