(* This file defines a first order language with substitution and unification. 
 Variables are represented in a list; integers are used for constants.  The unification
 algorithm is based on Martelli and Montanari's system of transformations.
 The "term" datatype defines a signature for group theory.  Ultimately, this program
 will be expended to encompass term rewritting and Knuth-Bendix Completion.
                                                 - Chuck Liang, October 1998       *)

datatype term = const of int | var of string | inv of term | dot of term*term ;

(* a substitution is represented as a list of pairs (x,t)  *)

(* The substitution homomorphism: *)
fun subst S (const T) = (const T)
  | subst nil (var T) = (var T)
  | subst (((var A),T)::R) (var B) = if (A=B) then T else (subst R (var B))
  | subst S (inv T) = (inv (subst S T))
  | subst S (dot(A,B)) = dot((subst S A),(subst S B));

(* apply substitution to a list of pairs: *)
fun listsubst S nil = nil
  | listsubst S ((A,B)::R) = (((subst S A),(subst S B))::(listsubst S R));

(* difference pairs in a list of (s,t) *)

(* prettyprint function for abstract groups (const 1 = identity) *)

fun pretty (var X) = print X 
  | pretty (const O)  = print "1"
  | pretty (inv T) = (pretty T; print "~")
  | pretty (dot(A,B)) = (print "("; pretty A; print "*"; pretty B; print ")");

fun prettysubst nil = print "\n"
  | prettysubst ((A,B)::R) = 
	(print "("; pretty A; print "="; pretty B; print ") "; prettysubst R);
 

(* --- The TRANSFORMATIONS  (the first two are applied exhaustively, the last two
       are applied to one pair at a time *)

(* Triviality Elimination *)
fun trivElim nil = nil
  | trivElim ((A,B)::C) = if (A=B) then (trivElim C) else ((A,B)::(trivElim C));

(* Variable Positioning *)
fun nonvar (const T) = true
  | nonvar (inv T) = true
  | nonvar (dot(A,B)) = true
  | nonvar (var S) = false;

fun varPos nil = nil
  | varPos ((A,B)::R) = 
	if ((nonvar A) andalso (not (nonvar B))) then ((B,A)::(varPos R))
		else ((A,B)::(varPos R));

(* Term Decomposition *)
fun tmDecomp nil  = nil
  | tmDecomp ((inv A,inv B)::R) = ((A,B)::R)
  | tmDecomp ((dot(A,B),dot(C,D))::R) = ((A,C)::((B,D)::R))
  | tmDecomp (A::R) = (A::(tmDecomp R));

(* Variable Elimination *)
fun occurcheck (var X) (const T) = true
  | occurcheck (var X) (var Y) = not (X = Y)
  | occurcheck (var X) (inv T) = occurcheck (var X) T
  | occurcheck (var X) (dot(A,B)) = (occurcheck (var X) A) andalso (occurcheck (var X) B);

fun occurin (var X) nil = false     (* determines if x occurs elsewhere in list *)
  | occurin (var X) ((A,B)::R) = 
	(not (occurcheck (var X) A)) orelse (not (occurcheck (var X) B))
	  orelse (occurin (var X) R);

fun delete A nil = nil 
  | delete A (B::R) = if (A=B) then (delete A R) else (B::(delete A R));

fun remDups nil = nil     	(* remove duplicates from a list *)
  | remDups (A::R) = (A::(remDups (delete A R)));

fun varElim S = 
  let fun varE S nil = S
        | varE S ((A,B)::R) = 
           if ((not (nonvar A)) andalso (occurcheck A B)) 
			andalso (occurin A (delete (A,B) S)) then
	     ((A,B)::(listsubst [(A,B)] (delete (A,B) S)))
			(* this always introduces a trivial pair *)
	   else (varE S R);
  in (varE S S) end;

     
(* Unification Procedure *)
fun unique (var X) nil = false
  | unique (var X) ((A,B)::R) = if ((var X)=A) then (not (unique (var X) R))
	else (unique (var X) R);

fun idemcheck (var X) nil = true
  | idemcheck (var X) ((A,B)::R) = 
	(occurcheck (var X) B) andalso (idemcheck (var X) R);

fun solvedform S nil = true   (* intended to be called as (solvedform S S) initially *)
  | solvedform S ((A,B)::R) =
  	(not (nonvar A)) andalso (unique A S)
	  andalso (idemcheck A S) andalso (solvedform S R);

(* the unify function keeps applying transformations until 
   either a solved form is reached or no transformation has any effect: *)
fun unify S = if (solvedform S S) then (print "Solution: "; S) 
		else let val S2 = (varElim (varPos (tmDecomp (trivElim S))))
		       in
			(      prettysubst S2;  
			 if (S2=S) then (print "No Solution; stuck at: "; S)
				else unify S2)
	     	     end;



(* substitution and unification tests *)

subst [(var "x",const 1)] (dot(var "x",inv(var "x")));
unify [(var "x",const 1)];
prettysubst (unify [((dot(var "x",var "y")),dot(inv(const 1),var "z"))]);
prettysubst (unify [((dot(var "x",var "y")),dot(inv(const 1),var "x"))]);
prettysubst (unify [(dot(var "x",var "x"),dot(var "y",var "z"))]);
unify [((dot(var "x",var "y")),dot(inv(var "y"),var "x"))];