/***************************/
/*                         */
/* Answers to worksheet 16 */
/*                         */
/***************************/

/* Exercise 16.1 Unification                                                */

/* Prolog unification does not implement the `occurs check'. This is the    */
/* check that we are supposed to make in order to stop ourselves from       */
/* unifying, e.g., X with f(X). Prolog does not have this (so as to improve */
/* its execution speed). The cost of this omission is that there are RARE   */
/* cases when, if we are not careful, we will write a program in which      */
/* Prolog does bind X to f(X) giving it an infinite substitution.           */

/* If these rare cases become a concern to us then writing an interpreter   */
/* in which we take over the unification is an option, e.g. using the unif  */
/* program that I mentioned in worksheet 8, which does have an occurs check.*/
/* (In fact, most Prolog's come with a primitive, unify, which does the same*/
/* as my unif program, that you can use.)                                   */


/* Exercise 16.2 Impure Prolog                                              */

/* All that is needed is one extra rule per extralogical construct, which   */
/* traps and directly executes the construct. For example,                  */
/*                                                                          */
/* solve(clause(A, B)) :- clause(A, B).                                     */
/*                                                                          */
/* solve(A<B) :- A<B.                                                       */
/*                                                                          */
/* etc.!                                                                    */
/* Below I give a more elegant solution that uses the primitive `call':     */

solve(true).

solve(Goal) :-
   clause(Goal, Body),
   solve(Body).

solve((Body1, Body2)) :-
   solve(Body1),
   solve(Body2).

solve(Goal) :-
   impure(Goal),
   call(Goal).

impure(clause(A, B)).
impure(A<B).
impure(A=<B).
impure(A>B).
impure(A>=B).
impure(A=:=B).
impure(A=\=B).
impure(V is E).

/* Exercise 16.3 Tracing                                                   */

tracer(Goal) :- tracer(Goal, 0).

display(Goal, Depth) :-
   write_n_spaces(Depth), write(Goal), nl.

write_n_spaces(0).
write_n_spaces(N) :- N > 0, write(' '), N1 is N - 1, write_n_spaces(N1).

tracer(true, Depth).

tracer(Goal, Depth) :-
   clause(Goal, Body),
   display(Goal, Depth),
   NewDepth is Depth + 1,
   tracer(Body, NewDepth).

tracer((Body1, Body2), Depth) :-
   tracer(Body1, Depth), 
   tracer(Body2, Depth).