(*** 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; fun length (_ :: xs) = length xs + 1 | length [] = 0; fun at (x::xs) i = if i=0 then x else at xs (i-1); 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! ***) val Fname = ref("F"); fun newname(r) = (r := !r ^ "'"; !r); (*** Terms ***) infix 9 $; datatype term = V of string | C of string | B of int | op $ of term * term | A of term; fun newV() = V(newname(Fname)); fun B1(B i) = i; fun strip t = let fun strip(s$t,ts) = strip(s,t::ts) | strip p = p in strip(t,[]) end; fun abs(_::xs,t) = abs(xs,A t) | abs([],t) = t; fun hnf(xs,F,ss) = abs(xs, foldl op $ (F,ss)); (*** Substitutions ***) fun occ F S = let fun occ(V G) = (F=G) orelse (case assoc G S of Some(s) => occ s | None => false) | occ(s$t) = occ s orelse occ t | occ(A s) = occ s | occ(_) = false in occ end; fun mapbnd f = let fun mpb d (B i) = B(if i i+1); fun red (A s) (B i :: bs) js = red s bs (i::js) | red s bs js = foldl op $ (mapbnd (at js) s, bs); fun devar S s = case strip s of (V F,is) => (case assoc F S of Some(t) => devar S (red t is []) | None => s) | _ => s; (*** Unification ***) exception Unif; fun pos p (x::xs) = if p x then B(length xs) :: pos p xs else pos p xs | pos p [] = []; fun idx (b::bs) b' = if b=b' then B(length bs) else idx bs b' | idx [] _ = B(~10000); fun zip (x::xs) (y::ys) = (x,y) :: zip xs ys | zip [] [] = [] | zip _ _ = raise Unif; fun proj(S,s) = case strip(devar S s) of (A t,_) => proj(S,t) | (C _,ss) => foldl proj (S,ss) | (B i,ss) => if i<0 then raise Unif else foldl proj (S,ss) | (V F,bs) => (F,hnf(bs, newV(), pos (fn B i => i >= 0) bs))::S; fun flexflex1(F,ym,zn,S) = if ym=zn then S else (F, hnf(ym, newV(), pos op = (zip ym zn))) :: S; fun lam(im,G,jn) = hnf(im, G, map (idx im) jn); fun flexflex2(F,im,G,jn,S) = if im subset jn then (G, lam(jn,V F,im)) :: S else if jn subset im then (F, lam(im,V G,jn)) :: S else let val kl = im /\ jn and H = newV() in (F, lam(im,H,kl)) :: (G, lam(jn,H,kl)) :: 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,im,t,S) = if occ F S t then raise Unif else let val u = mapbnd (B1 o (idx im) o B) t in proj((F,abs(im,u))::S,u) end; fun unif (S,(s,t)) = case (devar S s,devar S t) of (A s, A t) => unif (S,(s,t)) | (A s,t) => unif (S,(s,(incr t)$(B 0))) | (s,A t) => unif (S,((incr s)$(B 0),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);