/tmp/mosstmp/csu01102/unify.sml(*Basically i m passing as output as 4-tuple
if it is LEGAL EXPRESSION :: then TUPLE -> (!.whether it can be unified?[BOOLEAN]
2.REDUCED LIST OF TERMS AFTER THE SUBSITUTION
3.MGU-(term1,term2) list where {term1/term2}
4.whether it is LEGAL
if it is ILLEGAL :then tuple -> 1.FALSE
2.iilegal expression
3.[]
4.iilegal expression
*)
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 -> bool * Term list * (Term * Term) list * string
end;
structure uni: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
exception e;
exception Except ;
fun RAIS(A,B)=if (A=B) then false
else true;
fun getname(OPR1(A1,A2))=A1
| getname(OPR3(B1,B2,B3,B4))=B1
| getname(OPR2(B1,B2,B3))=B1
| getname(_)="arbit";
fun RaiseE(VAR(A),CONST(B))=RAIS(A,B)
| RaiseE(VAR(A),B)=RAIS(A,getname(B))
| RaiseE(CONST(A),VAR(B))=RAIS(A,B)
| RaiseE(OPR1(A1,A2),CONST(B1))=RAIS(A1,B1)
| RaiseE(CONST(A1),OPR3(B1,B2,B3,B4))=RAIS(A1,B1)
| RaiseE(OPR2(A1,A2,A3),CONST(B1))=RAIS(A1,B1)
| RaiseE(OPR1(A1,A2),OPR2(B1,B2,B3))=RAIS(A1,B1)
| RaiseE(OPR1(A1,A2),OPR3(B1,B2,B3,B4))=RAIS(A1,B1)
| RaiseE(OPR2(A1,A2,A3),OPR3(B1,B2,B3,B4))=RAIS(A1,B1)
| RaiseE(A,B)=true;
fun getE(VAR(A),CONST(B))=if(A=B) then [VAR(A),CONST(B)] else []
| getE(VAR(A),VAR(B))=[]
| getE(VAR(A),B)=if(A=getname(B)) then [VAR(A),B] else []
| getE(CONST(A),VAR(B))=if(A=B) then [CONST(A),VAR(B)] else []
| getE(OPR1(A1,A2),CONST(B1))=if (A1=B1) then [OPR1(A1,A2),CONST(B1)] else []
| getE(CONST(A1),OPR3(B1,B2,B3,B4))=if (A1=B1) then [CONST(A1),OPR3(B1,B2,B3,B4)] else []
| getE(OPR2(A1,A2,A3),CONST(B1))=if (A1=B1) then [OPR2(A1,A2,A3),CONST(B1)] else []
| getE(OPR1(A1,A2),OPR2(B1,B2,B3))=if (A1=B1) then [OPR1(A1,A2),OPR2(B1,B2,B3)] else []
| getE(OPR1(A1,A2),OPR3(B1,B2,B3,B4))=if (A1=B1) then [OPR1(A1,A2),OPR3(B1,B2,B3,B4)] else []
| getE(OPR2(A1,A2,A3),OPR3(B1,B2,B3,B4))=if(A1=B1) then[OPR2(A1,A2,A3),OPR3(B1,B2,B3,B4)] else []
| getE(A,B)=[];
fun find(a,[])=true
| find(a,xs::L)=RaiseE(a,xs) andalso find(a,L);
(* <param same lists>*)
fun FindE([],MM)=true
| FindE(xs::LL,MM)=find(xs,MM) andalso FindE(LL,MM);
(* <param L,[]> *)
fun dofor(a,[])=[]
| dofor(a,xs::L)=getE(a,xs)@dofor(a,L);
fun Illegal([],H)=[]
| Illegal(a::G,H)=dofor(a,G@H)@Illegal(G,a::H);
(* Finds out the disagreement set *)
fun DCompare(VAR(A),VAR(B))=if(A=B) then []
else [VAR(A),VAR(B)]
| DCompare(CONST(A),CONST(B))=if(A=B) then []
else [CONST(A),CONST(B)]
| DCompare(A,VAR(B))=[VAR(B),A]
| DCompare(VAR(A),B)=[VAR(A),B]
| DCompare(A,CONST(B))=[A,CONST(B)]
| DCompare(CONST(A),B)=[CONST(A),B]
| DCompare(OPR1(A1,A2),OPR1(B1,B2))=if(A1=B1) then if(A2=B2) then []
else DCompare(A2,B2)
else [OPR1(A1,A2),OPR1(B1,B2)]
| DCompare(OPR2(A1,A2,A3),OPR2(B1,B2,B3))=if(A1=B1) then (if(A3=B3) then DCompare(A2,B2)
else DCompare(A3,B3))
else [OPR2(A1,A2,A3),OPR2(B1,B2,B3)]
| DCompare(OPR3(A1,A2,A3,A4),OPR3(B1,B2,B3,B4))=if(A1=B1) then if(not(A2=B2)) then DCompare(A2,B2) else if(not(A3=B3)) then DCompare(A3,B3)
else DCompare(A4,B4)
else [OPR3(A1,A2,A3,A4),OPR3(B1,B2,B3,B4)]
| DCompare(A,B)=if(A=B) then []
else [A,B];
(* Boolean :find if there is an occurence of A*)
fun Search(A,VAR(B))=if(A=VAR(B)) then true
else false
| Search(A,OPR1(B1,B2))=Search(A,B2)
| Search(A,OPR2(B1,B2,B3))=Search(A,B2) orelse Search(A,B3)
| Search(A,OPR3(B1,B2,B3,B4))=Search(A,B2) orelse Search(A,B3) orelse Search(A,B4)
| Search(A,CONST(B))=false;
(* replaces A by C in a term *)
fun replace(VAR(A),VAR(B),C)= if(A=B) then C
else VAR(B)
| replace(VAR(A),CONST(B),C)=CONST(B)
| replace(A,OPR1(B1,B2),C)=OPR1(B1,replace(A,B2,C))
| replace(A,OPR2(B1,B2,B3),C)=OPR2(B1,replace(A,B2,C),replace(A,B3,C))
| replace(A,OPR3(B1,B2,B3,B4),C)=OPR3(B1,replace(A,B2,C),replace(A,B3,C),replace(A,B4,C))
| replace(A,B,C)=B;
fun mgu([],(A,B))=[(A,B)]
| mgu(L ,(A,B))=(A,B)::L;
fun seeempty([])=true
| seeempty(L)=false;
fun YComparedo(A,[])=[]
| YComparedo(A,a::L)=DCompare(A,a) @ YComparedo(A,L);
(* PAss as parameter a::L=W ,gives back disagreement set *)
fun disagree([],_)=[]
| disagree(a::L,W)=YComparedo(a,W)@disagree(L,W);
fun isPresent (a, []) = false
| isPresent (a, b::L) = (a = b) orelse isPresent (a, L);
(* Remove all the duplicate occurences <param=two same lists> *)
fun rdup([],[])=[]
| rdup([],Y)=Y
| rdup(mm::L,Y)=if(isPresent(mm,L@Y)) then rdup(L@Y,[])
else rdup(L,mm::Y);
fun Disagreement(L)=rdup(L,L);
(* To find illegal expression *)
fun IllegalE(L)=Disagreement(Illegal(L,[]));
(* Find if any var is present *)
fun varpresent([])=false
| varpresent(VAR(A)::L)=true
| varpresent(_::L)=varpresent(L);
fun varfind([])= raise Except
| varfind(VAR(A)::L)=VAR(A)
| varfind(_::L)=varfind(L);
(* if there exist an expreesion containing, the( var )a *)
fun eexist(a,[])=true
| eexist(a,b::K)=if(Search(a,b)) then false
else eexist(a,K);
(* GIVE back an expression not containing var-a *)
fun gete(a,[])=raise Except
| gete(a,b::K)=if(not (Search(a,b))) then b
else gete(a,K);
fun removea(a,[])=[]
| removea(a,xs::L)=if(a=xs) then removea(a,L)
else xs::removea(a,L); (* <param list,disagreement set >*)
fun removeD(D,DS)=let
val Set=disagree(D,D)
val mgu=if(varpresent(Set)) then if(eexist(varfind(Set),removea(varfind(Set),rdup(Set,Set)))) then (varfind(Set),gete(varfind(Set),Set))::DS
else let
val valtemp= varfind(Set)
val temp = removea(varfind(Set),Set)
in if(varpresent(temp)) then (varfind(temp),valtemp) ::DS
else DS
end
else DS
in mgu
end;
fun single([a])=true
| single(_)=false
fun Replace([],_)=[]
| Replace(P,[])=P
| Replace(xs::P,(a,b)::mg)=replace(a,xs,b)::Replace(P,(a,b)::mg);
(* <param --list,diagreement set*)
fun Driver(M,MD)= let
val X=removeD(M,MD)
val Y=rdup(Replace(M,removeD(M,MD)),Replace(M, removeD(M,MD)))
in if(single(Y)) then (true,Y,X,"LEGAL EXPRESSION")
else if(X=removeD(Y,X)) then (false,Y,Disagreement(X),"LEGAL EXPRESSION")
else Driver(Y,X)
end;
fun unifynex([])=raise e
| unifynex(J)=if(disagree(J,J)=[]) then (true,J,[],"LEGAL EXPRESSION")
else Driver(J,[]);
fun unify(L)=if(FindE(L,L)) then unifynex(L)
else (false,IllegalE(L),[]," ->(Non-empty List returns illegal match found ) ILLEGAL EXPRESSION : e");
end;