(*** Basic Library ***) fun foldl f (a,x::xs) = foldl f (f(a,x),xs) | foldl f (a,[]) = a; fun foldr f (x::xs,a) = f(x,foldr f (xs,a)) | foldr f ([],a) = a; datatype 'a option = Some of 'a | None; fun assoc x ((y,t)::ps) = if x=y then Some(t) else assoc x ps | assoc x [] = None; infix mem; fun (x mem (y::ys)) = x=y orelse x mem ys | (x mem []) = false; infix subset; fun (x::xs) subset ys = (x mem ys) andalso (xs subset ys) | [] subset ys = true; infix /\; fun ((x::xs) /\ ys) = if x mem ys then x::(xs /\ ys) else xs /\ ys | ([] /\ _) = []; (*** Generation of new names --- non functional! ***) (*** Assumption: names in input terms are not primed ***) val Fname = ref("F"); val Bname = ref("x"); fun newname(r) = (r := !r ^ "'"; !r); fun newB() = newname Bname; (*** Terms ***) infix 9 $; infixr \; datatype term = V of string (* free var *) | B of string (* bound var *) | C of string (* constant *) | op $ of term * term (* application *) | op \ of string * term; (* abstraction *) fun newV() = V(newname Fname); fun B1(B s) = s; fun strip t = let fun strip(s$t,ts) = strip(s,t::ts) | strip p = p in strip(t,[]) end; fun abs(xs,t) = foldr op \ (map B1 xs,t); fun hnf(xs,F,ss) = abs(xs, foldl op $ (F,ss)); (*** Substitutions ***) fun occ F S (V G) = (F=G) orelse (case assoc G S of Some(s) => occ F S s | None => false) | occ F S (s$t) = occ F S s orelse occ F S t | occ F S (_\s) = occ F S s | occ F S (_) = false; fun subst y x = let fun sub(b as B z) = if z=x then B y else b | sub(s1$s2) = (sub s1) $ (sub s2) | sub(t as z\s) = if z=x then t else if z<>y then z \ sub s else let val z' = newB() in z' \ sub(subst z' z s) end | sub(s) = s in sub end; fun red (x\s) (y::ys) = red (subst (B1 y) x s) ys | red s (y::ys) = red (s$y) ys | red s [] = s; fun devar S t = case strip t of (V F,ys) => (case assoc F S of Some(t) => devar S (red t ys) | None => t) | _ => t; (*** Unification ***) exception Unif; fun proj W (S,s) = case strip(devar S s) of (x\t,_) => proj (x::W) (S,t) | (C _,ss) => foldl (proj W) (S,ss) | (B x,ss) => if x mem W then foldl (proj W) (S,ss) else raise Unif | (V F,ss) => if (map B1 ss) subset W then S else (F, hnf(ss, newV(), ss /\ (map B W))) :: S; fun eqs (x::xs) (y::ys) = if x=y then x::eqs xs ys else eqs xs ys | eqs [] [] = [] | eqs _ _ = raise Unif; fun flexflex1(F,ym,zn,S) = if ym=zn then S else (F, hnf(ym, newV(), eqs ym zn)) :: S; fun flexflex2(F,ym,G,zn,S) = if ym subset zn then (G, hnf(zn,V F,ym)) :: S else if zn subset ym then (F, hnf(ym,V G,zn)) :: S else let val xk = ym /\ zn and H = newV() in (F, hnf(ym,H,xk)) :: (G, hnf(zn,H,xk)) :: S end; fun flexflex(F,ym,G,zn,S) = if F=G then flexflex1(F,ym,zn,S) else flexflex2(F,ym,G,zn,S); fun flexrigid(F,ym,t,S) = if occ F S t then raise Unif else proj (map B1 ym) (((F,abs(ym,t))::S),t); fun zip (x::xs) (y::ys) = (x,y) :: zip xs ys | zip [] [] = [] | zip _ _ = raise Unif; fun unif (S,(s,t)) = case (devar S s,devar S t) of (x\s,y\t) => unif (S,(s,if x=y then t else subst x y t)) | (x\s,t) => unif (S,(s,t$(B x))) | (s,x\t) => unif (S,(s$(B x),t)) | (s,t) => cases S (s,t) and cases S (s,t) = case (strip s,strip t) of ((V F,ym),(V G,zn)) => flexflex(F,ym,G,zn,S) | ((V F,ym),_) => flexrigid(F,ym,t,S) | (_,(V F,ym)) => flexrigid(F,ym,s,S) | ((a,sm),(b,tn)) => rigidrigid(a,sm,b,tn,S) and rigidrigid(a,ss,b,ts,S) = if a <> b then raise Unif else foldl unif (S,zip ss ts);