<br />
<b>Deprecated</b>:  The each() function is deprecated. This message will be suppressed on further calls in <b>/home/zhenxiangba/zhenxiangba.com/public_html/phproxy-improved-master/index.php</b> on line <b>456</b><br />
For Ia students, please do the following


  Run this program and find that it produces
the following output

 psolver(PRED("grandfather", [ VAR("X"), VAR("Y") ]));
 val it = (false, [], []) : bool * (string * pexp_t) list * 'b list


Make the program work, so that it deduces that philip is the grandfather
of harry and william.  These facts are supposed to come out via the solns 
list.


Ignore the other exercises.

------------


(*
    CBG SQUANDERER PROLOG
    http://www.cl.cam.ac.uk/users/djg/pubs/prolog.txt

Notes: 

For those not familiar with Prolog, the process of unification
is to establish a mapping between pairs of variables or
variables and constants.  

Unification:

In simple terms, X will unifiy with Y if
   1. If X is a constant and Y is a variable, then Y takes on the
value of X
   2. If both X and Y are constants, we fail to unifiy if they are
different
   3. If both X and Y are variables, if one is not already bound
then it takes on the value of the other (which may or may not be
bound already).

For example, we can unify P(x, 22, "cat") with Q(y, y, v) by
setting x=y=22 and v="cat".


Cut and fail:

If the system encounters the FAIL term, the current rule
fails outright.

If the system encounters a CUT term while backtracking,
the current rule fails.  This means that, for example
    N(s,t), P(v), CUT, Q(v,r), S(v,r)
will search out all possible values for r by re-evaluating
Q and S, but if it has not succeeded in this search and needs
to backtrack to find a new value for v, then it fails instead.


List data types:

For the prolog list data types, a constructor called
'cons' needs to be introduced as a new value that variables
can range over.  Cons takes a pair of values and binds
them together.  One is the head of a list and the other
is the tail of a list.  A new special value can also
be used to mark the end of a list, such as 'nil'.

Cons(X, Y) will unifiy with CONS(P, Q) iff X will unifiy with P
and Y will unifiy with Q.

*)

(* -- *)


(*
 * CBG Squander Prolog.
 * Simple prolog interpreter in SML.
 * (C) 2000 DJ Greaves. All rights reserved.
 * 
 * Exercise 1: Complete the unification subroutine
 * Exercise 2: Implement CUT and FAIL 
 * Exercise 3: Implement prolog's list data types.
 * Exercise 4: Use this prolog interpreter for an example that uses difference lists.
 *
 * Note: the first thing to do is to make the system return a result
 * of any sort, otherwise it will not load under ML.
 *)


(* Datatypes used *)
datatype pexp_t = INT of int | VAR of string | STRING of string
;


datatype predicate_t = PRED of string * pexp_t list | CUT | FAIL
;


datatype rule_t = RULE of string * pexp_t list * predicate_t list
;


(* Code database for the example run *)
val gf_r = RULE("grandfather", [ VAR("X"), VAR("Y")], [ PRED("father", [ VAR("X"), VAR("P") ]), PRED("father", [ VAR("P"), VAR("Y") ]) ]);

val f1_r = RULE("father", [ STRING("charles"), STRING("william") ], []);
val f2_r = RULE("father", [ STRING("charles"), STRING("harry") ], []);
val f3_r = RULE("father", [ STRING("philip"), STRING("charles") ], []);

(* Note that prolog is sensitive to the order of the rules. *)
val rules = [ f1_r, f2_r, f3_r, gf_r ];

(* Now the interpreter *)

fun lookup(id, nil) = NONE | lookup(id, (v,e)::t) = if (id=v) then SOME(e) else lookup(id, t)
;

(* 
 * Unification algorithm... needs a bit more work
 *)
fun  
   unif(INT(n), INT(v), env) = (n=v, env)
|  unif(STRING(n), STRING(v), env) = (n=v, env)
|  unif(x, VAR(v), env) = 
	let val vv = lookup(v, env)
	in if (vv=NONE) then (true, (v, x)::env)
           else (valOf(vv)=x, env)
	end

|  unif(VAR(v), x, env) = unif(x, VAR(v), env)
;


fun 
  unif_list(nil, nil, env) = (true, env)
| unif_list(h::t, hh::tt, env) = 
	let val (okf, env') = unif(h, hh, env)
	in if (okf) then unif_list(t, tt, env')
	else (false, env)
	end
;

fun 
   psolve(g, env, nil, rules, solns) = (false, env, solns)
|  psolve(PRED(name, args), env, RULE(name', args', subgoals)::tr, rules, solns) =
	let val (okf, env') = if (name=name') then unif_list(args, args', env) else (false, env)
	    val (okf2, env2) = if (okf) then psolve_list(subgoals, env', rules) else (okf, env')
        in if (okf2) then (true, env2, solns)
        else psolve(PRED(name, args), env, tr, rules, solns)
	end

and
   psolve_list(nil, env, rules) = (true, env)
|  psolve_list(h::t, env, rules) = 
      let val (okf, env', _) = psolve(h, env, rules, rules, [])
	in if (okf) then psolve_list(t, env, rules)
	else (false, env)
	end
;


fun psolver(g) = psolve(g, nil, rules, rules, []);

psolver(PRED("grandfather", [ VAR("X"), VAR("Y") ]));