(* 
	1: input is in the form of term list list
	2: in this input each term list represents an expression
	3: output gives two lists . first is the list gives us disa	      greement set if complete unification takes place then it 		 comes out to be []
	4: 2nd list gives us unifier
	5: when an illegel input occurs then first list is empty 	      & 2nd list contains VAR"illegel"
						*)	
signature UNIFY =
sig 
	datatype Term = VAR of string
		| CONST of string
		| OPR1 of string * Term
		| OPR2 of string * Term * Term
		| OPR3 of string * Term * Term * Term
	val unify : Term list list -> Term list * (Term*Term) list
end;

structure unify : UNIFY =
struct


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

fun     dis_coll([]) = []
|	dis_coll(xs) = hd(hd(xs))::dis_coll(tl(xs));	
	

fun 	get_element(VAR(x)) = [x]
|	get_element(CONST(x)) = [x]
|	get_element(OPR1(x,y)) = get_element(y)
|	get_element(OPR2(x,y,z)) = get_element(y)@get_element(z)
|	get_element(OPR3(a,x,y,z)) = get_element(x)@get_element(y)@get_element(z);

fun     cr_level(OPR1(x,y)) = [y]
|	cr_level(OPR2(x,y,z)) = [y,z]
|	cr_level(OPR3(a,b,c,d)) = [b,c,d]
|	cr_level(_) = [];
 
fun     member(x,[]) = false
|       member(x,ys) = if x=hd(ys) then true else member(x,tl(ys));

fun 	com(VAR(x),VAR(y)) = true
|	com(VAR(x),CONST(y)) = true
|	com(CONST(x),VAR(y)) = true
|	com(VAR(x),xs) = if member(x,get_element(xs)) then false else true
|  	com(xs,VAR(x)) = if member(x,get_element(xs)) then false else true
|	com(OPR1(a,b),OPR1(c,d)) = (a=c)
|	com(OPR2(a,b,c),OPR2(d,e,f)) = (a=d)
|	com(OPR3(a,b,c,d),OPR3(e,f,g,h)) = (a=e)
|	com(x,y) = (x=y);


fun 	get_type(VAR(x)) = "VAR"
|	get_type(CONST(x)) = "CONST"
|	get_type(OPR1(x,y)) = "OPR1"
|	get_type(OPR2(a,b,c)) = "OPR2"
|	get_type(OPR3(a,b,c,d)) = "OPR3";

fun 	c_type([]) = false
|	c_type(x) = get_type(hd(x))=get_type(hd(tl(x))) andalso c_type(tl(x)); 	


fun   	ch_sametype([]) = true
|	ch_sametype(xs) = if tl(xs) = [] then true
	else get_type(hd(xs))=get_type(hd(tl(xs))) andalso ch_sametype(tl(xs));	

fun 	ch_equality([]) = true
|	ch_equality(xs) = if tl(xs)=[] then true 
			else hd(xs)=hd(tl(xs)) andalso ch_equality(tl(xs))

fun 	ch_con(x,[]) = true
|	ch_con(x,xs) = if tl(xs)=[] then com(x,hd(xs)) 
		else com(x,hd(tl(xs))) andalso ch_con(x,tl(xs)) andalso 
			ch_con(hd(tl(xs)),tl(xs));

fun 	set_subdset([],_) = []
|	set_subdset(xs,i) = if get_type(List.nth(xs,i))="VAR" then 
		List.nth(xs,i)::List.take(xs,i)@List.drop(xs,i+1)
			else set_subdset(xs,i+1);

fun 	set_dset([]) = []
|	set_dset(xs) = if ch_con(hd(xs),xs) then xs
			else if c_type(xs) then xs
			else  set_subdset(xs,0);

fun 	replace_term(VAR(x),z,d) = if VAR(x)=z then d else VAR(x)
|	replace_term(CONST(x),z,d) = CONST(x)
|	replace_term(OPR1(a,b),z,d) = OPR1(a,replace_term(b,z,d))
|	replace_term(OPR2(a,b,c),z,d) = OPR2(a,replace_term(b,z,d),replace_term(c,z,d))
|	replace_term(OPR3(a,b,c,e),z,d) = OPR3(a,replace_term(b,z,d),replace_term(c,z,d),replace_term(e,z,d));		

fun 	replace_list([],z,d) = []
|	replace_list(xs,z,d) = replace_term(hd(xs),z,d)::replace_list(tl(xs),z,d);

fun 	replace([],z,d) = []
|	replace(xs,z,d) = replace_list(hd(xs),z,d)::replace(tl(xs),z,d);

fun	var_substitude([],z) = []
|	var_substitude(xs,z) = if tl(z)=[] then xs else 
			var_substitude(replace(xs,hd(tl(z)),hd(z)),List.take(z,1)@List.drop(z,2));

				 
fun 	substitude([],z) = []
|	substitude(xs,z) = if length(z)=2 then replace(xs,hd(z),hd(tl(z)))
				else if get_type(hd(tl(z)))="VAR" then  
			var_substitude(xs,z) else replace(xs,hd(z),hd(tl(z)));

fun  	var_mgu([],ys) = ys 
|	var_mgu(z,ys) = if tl(z)=[] then ys 
			else (hd(tl(z)),hd(z))::var_mgu(tl(z),ys); 		

fun 	create_mgu([],ys) = ys
|	create_mgu(z,ys) = if length(z)=2 then ys@[(hd(tl(z)),hd(z))]
			else if get_type(hd(tl(z)))="VAR" then var_mgu(z,ys)				else ys@[(hd(tl(z)),hd(z))];



fun	reduce_ip([]) = []
|	reduce_ip(xs) = if tl(xs)=[] then [tl(hd(xs))] 
			else tl(hd(xs))::reduce_ip(tl(xs));
				   	
fun 	low_level([]) = []
|	low_level(xs) = if (get_type(hd(hd(xs)))="VAR")=false 
			then cr_level(hd(hd(xs)))::low_level(tl(xs))
			else [];

fun 	ch_f([]) = true
|	ch_f(xs) = if tl(xs)=[] then true else com(hd(hd(xs)),hd(hd(tl(xs)))) 
			andalso ch_f(tl(xs));
			
fun 	find_d([]) = []
|	find_d(xs) = if ch_con(hd(dis_coll(xs)),dis_coll(xs))=false
			 then dis_coll(xs)
			else
			if ch_sametype(dis_coll(xs)) 
                      andalso (get_type(hd(hd(xs)))="VAR")=false 
	 andalso (get_type(hd(hd(xs)))="CONST")=false andalso ch_f(xs)
			then find_d(low_level(xs))
	else if set_dset(dis_coll(xs))=[] orelse ch_equality(dis_coll(xs))
			 then find_d(reduce_ip(xs))
			else dis_coll(xs);

fun rdl([],_) = []
|   rdl(xs,i) = if (i=length(xs)) then xs else
                 if member(List.nth(xs,i),List.drop(xs,i+1)) 
                      	then rdl((List.take(xs,i)@List.drop(xs,i+1)),i)
		     else rdl(xs,i+1);  



fun	unify_hd([],ys) = ([],ys)
|	unify_hd(xs,ys) = if length(xs)=1 then ([],ys)

			else	if ch_con(hd(find_d(xs)),find_d(xs))= false 
				then (find_d(xs),ys)
       else unify_hd(rdl(substitude(xs,find_d(xs)),0),create_mgu(find_d(xs),ys));

fun 	ch_ill([]) = true
|	ch_ill(xs) = if length(xs) =1 then true else 
	length(hd(xs))=length(hd(tl(xs))) andalso ch_ill(tl(xs));

fun	unify([]) = ([],[(VAR"illegel",VAR"illegel")])
|	unify(xs) = if ch_ill(xs) then unify_hd(rdl(xs,0),[])
			else ([],[(VAR"illegel",VAR"illegel")]);

end;