datatype Term = VAR of string
	| CONST of string
	| OPR1 of string * Term
	| OPR2 of string * Term * Term
	| OPR3 of string * Term * Term*Term

(*checks if the term is a variable or not*)
fun isvar(CONST(c:string))=false
        |isvar(VAR(x:string))=true
        |isvar(OPR1(f,a))=false
        |isvar(OPR2(f,a,b))=false
        |isvar(OPR3(f,a,b,c))=false;

(*compares 2 terms for equality*)
fun comp2(CONST(c1),CONST(c2))=if c1=c2 then true else false
	|comp2(VAR(x),VAR(y))=if x=y then true else false
	|comp2(OPR1(f,a),OPR1(g,b))=if f=g then comp2(a,b) else false
	|comp2(OPR2(f,a,b),OPR2(g,c,d))=if f=g then comp2(a,c) andalso comp2(b,d) else false
	|comp2(OPR3(f,a,b,c),OPR3(g,p,q,r))=if f=g then comp2(a,p) andalso comp2(b,q) andalso comp2(c,r) else false

(*checks if the variable is present in the given term , called only after checking fo variable *)
fun ispresent(VAR(x):Term,CONST(c))=false
	|ispresent(VAR(x),VAR(y))=if x=y then true else false
	|ispresent(VAR(x),OPR1(f,a))=ispresent(VAR(x),a)
	|ispresent(VAR(x),OPR2(f,a,b))=ispresent(VAR(x),a) andalso ispresent(VAR(x),b) 
	|ispresent(VAR(x),OPR3(f,a,b,c))=ispresent(VAR(x),a) andalso ispresent(VAR(x),b) andalso ispresent(VAR(x),c);


(* the replacement set , contains the pair of variables replaced and term by which replaced *)
val z=[(VAR("a"),VAR("b"))];

(* replaces all instances of the variable x by the term p in the given term *)
fun repvar(CONST(c),p:Term,x:string)=CONST(c)
	|repvar(VAR(a),p,x)=if a=x then p else VAR(a)
	|repvar(OPR1(f,a),p,x)=if isvar(a) then if a=VAR(x) then OPR1(f,p)
						else OPR1(f,a)
				else OPR1(f,repvar(a,p,x))
	|repvar(OPR2(f,a,b),p,x)=if isvar(a) then if  a= VAR(x) then OPR2(f,p,repvar(b,p,x))
						  else OPR2(f,a,repvar(b,p,x))
				 else if isvar(b) then if  b=VAR(x) then OPR2(f,repvar(a,p,x),p)
						       else OPR2(f,repvar(a,p,x),b)
				 else OPR2(f,repvar(a,p,x),repvar(b,p,x))
	|repvar(OPR3(f,a,b,c),p,x)=if isvar(a) then if a=VAR(x) then OPR3(f,p,repvar(b,p,x),repvar(c,p,x)) 
						    else OPR3(f,a,repvar(b,p,x),repvar(c,p,x))
				   else if isvar(b) then if b=VAR(x) then OPR3(f,repvar(a,p,x),p,repvar(c,p,x)) 
							 else OPR3(f,repvar(a,p,x),b,repvar(c,p,x))
				   else if isvar(c) then if c=VAR(x) then OPR3(f,repvar(a,p,x),repvar(b,p,x),p) 
							 else OPR3(f,repvar(a,p,x),repvar(b,p,x),c)
				   else OPR3(f,repvar(a,p,x),repvar(b,p,x),repvar(c,p,x));

(* replaces the variable x by the term p in the whole term list given along *)
fun repvarall([]:Term list,p:Term,VAR(x):Term,z)=[]
	|repvarall(a::[],p,VAR(x),z)=repvar(a,p,x)::[]
	|repvarall(a::l,p,VAR(x),z)=repvar(a,p,x)::repvarall(l,p,VAR(x),z);


(* finds the term where unification can take place*)
(* then calls repvarall to replace the term in the whole of list *)
(* returns the term list after replacing*)
(* also adds the term that is being replaced with the one replacing ,in  z*)
fun match2(CONST(c1),CONST(c2),t:Term list)=t
	|match2(VAR(x),CONST(c),t)=t
	|match2(VAR(x),VAR(y),t)=repvarall(t,VAR(y),VAR(x),(VAR(x),VAR(y))::z)
	|match2(VAR(x),OPR1(f,a),t)=if not(ispresent(VAR(x),OPR1(f,a))) then repvarall(t,OPR1(f,a),VAR(x),(VAR(x),OPR1(f,a))::z) else t
	|match2(VAR(x),OPR2(f,a,b),t)=if not(ispresent(VAR(x),OPR2(f,a,b))) then repvarall(t,OPR2(f,a,b),VAR(x),(VAR(x),OPR2(f,a,b))::z) else t
	|match2(VAR(x),OPR3(f,a,b,c),t)=if not(ispresent(VAR(x),OPR3(f,a,b,c))) then repvarall(t,OPR3(f,a,b,c),VAR(x),(VAR(x),OPR3(f,a,b,c))::z) else t
	|match2(OPR1(f,a),OPR1(g,b),t)=if f=g then if isvar(a) then if not(ispresent(a,b)) then repvarall(t,b,a,(a,b)::z)  
								    else t 
						   else match2(a,b,t)
					else t
	|match2(OPR2(f,a,b),OPR2(g,c,d),t)=if f=g then if isvar(a) then if not(ispresent(a,c)) then match2(b,d,repvarall(t,c,a,(a,c)::z))
									else t
						       else match2(b,d,match2(a,c,t)) 
					   else t
	|match2(OPR3(f,a,b,c),OPR3(g,p,q,r),t)=if f=g then if isvar(a) then if not(ispresent(a,p)) then match2(b,q,match2(c,r,repvarall(t,p,a,(a,p)::z)))
									    else t
							   else match2(b,q,match2(c,r,match2(a,p,t)))
						else t;

(* returns the arity of the term *)
fun arity(CONST(c):Term)=0
	|arity(VAR(x))=1
	|arity(OPR1(f,a))=2
	|arity(OPR2(f,a,b))=3
	|arity(OPR3(f,a,b,c))=4

(* cleans up the list of the possible duplication and then returns the cleaned list *)
fun cleanup1([]:Term list,t:Term,l:Term list)=l
	|cleanup1(a::[],t,l)=[a]
	|cleanup1(a::b::x,t,l)=if comp2(a,t) then cleanup1(b::x,t,l) else cleanup1(b::x,t,a::l);

fun cleanup2([]:Term list,l:Term list)=l
	|cleanup2(a::[],l)=cleanup2([],cleanup1(l,a,[]))
	|cleanup2(a::b::x,l)=cleanup2(b::x,cleanup1(l,a,[]));

(* checks if the term t can be replaced *)
(* then calls the match2 for the replacement *)
(*returns the term list after checking *)
fun part1(t:Term,[]:Term list)=[]
	|part1(t,a::[])=if arity(a)=arity(t) then match2(t,a,a::[]) else [a]
	|part1(t,a::b::x)=if arity(a)=arity(t) then part1(t,cleanup2(match2(t,a,a::b::x)@part1(t,b::x),match2(t,a,a::b::x)@part1(t,b::x))) 
			  else a::b::x;

(* runs the function part1 for all terms in the given list *)
fun unify2([]:Term list,l:Term list)=l
	|unify2(a::[],l)=[a]
	|unify2(a::b::x,l)=unify2(b::x,part1(a,l));

(*the first term is checked for unification with other term in the list *)
(*if possible then replacement and cleanup are done for this term *)
(*if not then the other terms are also checked in the same way *)
(* returns the term list containing the non unifiable terms*)
(* if all of them unify then "z" has the pairs of replaced terms with the replacing term *)

fun unify(l:Term list)=unify2(l,l);