0

1 
(* Title: unify


2 
ID: $Id$


3 
Author: Lawrence C Paulson, Cambridge University Computer Laboratory


4 
Copyright Cambridge University 1992


5 


6 
HigherOrder Unification


7 


8 
Potential problem: type of Vars is often ignored, so two Vars with same


9 
indexname but different types can cause errors!


10 
*)


11 


12 


13 
signature UNIFY =


14 
sig


15 
structure Sign: SIGN


16 
structure Envir : ENVIR


17 
structure Sequence : SEQUENCE


18 
(*references for control and tracing*)


19 
val trace_bound: int ref


20 
val trace_simp: bool ref


21 
val trace_types: bool ref


22 
val search_bound: int ref


23 
(*other exports*)


24 
val combound : (term*int*int) > term


25 
val rlist_abs: (string*typ)list * term > term


26 
val smash_unifiers : Sign.sg * Envir.env * (term*term)list


27 
> (Envir.env Sequence.seq)


28 
val unifiers: Sign.sg * Envir.env * ((term*term)list)


29 
> (Envir.env * (term * term)list) Sequence.seq


30 
end;


31 


32 
functor UnifyFun (structure Sign: SIGN and Envir: ENVIR and Sequence: SEQUENCE


33 
and Pattern:PATTERN


34 
sharing type Sign.sg = Pattern.sg


35 
and type Envir.env = Pattern.env)


36 
: UNIFY =


37 
struct


38 


39 
structure Sign = Sign;


40 
structure Envir = Envir;


41 
structure Sequence = Sequence;


42 
structure Pretty = Sign.Syntax.Pretty;


43 


44 
(*Unification options*)


45 


46 
val trace_bound = ref 10 (*tracing starts above this depth, 0 for full*)


47 
and search_bound = ref 20 (*unification quits above this depth*)


48 
and trace_simp = ref false (*print dpairs before calling SIMPL*)


49 
and trace_types = ref false (*announce potential incompleteness


50 
of type unification*)


51 


52 
val sgr = ref(Sign.pure);


53 


54 
type binderlist = (string*typ) list;


55 


56 
type dpair = binderlist * term * term;


57 


58 
fun body_type(Envir.Envir{iTs,...}) =


59 
let fun bT(Type("fun",[_,T])) = bT T


60 
 bT(T as TVar(ixn,_)) = (case assoc(iTs,ixn) of


61 
None => T  Some(T') => bT T')


62 
 bT T = T


63 
in bT end;


64 


65 
fun binder_types(Envir.Envir{iTs,...}) =


66 
let fun bTs(Type("fun",[T,U])) = T :: bTs U


67 
 bTs(T as TVar(ixn,_)) = (case assoc(iTs,ixn) of


68 
None => []  Some(T') => bTs T')


69 
 bTs _ = []


70 
in bTs end;


71 


72 
fun strip_type env T = (binder_types env T, body_type env T);


73 


74 


75 
(*Put a term into head normal form for unification.


76 
Operands need not be in normal form. Does etaexpansions on the head,


77 
which involves renumbering (thus copying) the args. To avoid this


78 
inefficiency, avoid partial application: if an atom is applied to


79 
any arguments at all, apply it to its full number of arguments.


80 
For


81 
rbinder = [(x1,T),...,(xm,Tm)] (user's var names preserved!)


82 
args = [arg1,...,argn]


83 
the value of


84 
(xm,...,x1)(head(arg1,...,argn)) remains invariant.


85 
*)


86 


87 
local exception SAME


88 
in


89 
fun head_norm (env,t) : term =


90 
let fun hnorm (Var (v,T)) =


91 
(case Envir.lookup (env,v) of


92 
Some u => head_norm (env, u)


93 
 None => raise SAME)


94 
 hnorm (Abs(a,T,body)) = Abs(a, T, hnorm body)


95 
 hnorm (Abs(_,_,body) $ t) =


96 
head_norm (env, subst_bounds([t], body))


97 
 hnorm (f $ t) =


98 
(case hnorm f of


99 
Abs(_,_,body) =>


100 
head_norm (env, subst_bounds([t], body))


101 
 nf => nf $ t)


102 
 hnorm _ = raise SAME


103 
in hnorm t handle SAME=> t end


104 
end;


105 


106 


107 
(*finds type of term without checking that combinations are consistent


108 
rbinder holds types of bound variables*)


109 
fun fastype (Envir.Envir{iTs,...}) =


110 
let val funerr = "fastype: expected function type";


111 
fun fast(rbinder, f$u) =


112 
(case (fast (rbinder, f)) of


113 
Type("fun",[_,T]) => T


114 
 TVar(ixn,_) =>


115 
(case assoc(iTs,ixn) of


116 
Some(Type("fun",[_,T])) => T


117 
 _ => raise TERM(funerr, [f$u]))


118 
 _ => raise TERM(funerr, [f$u]))


119 
 fast (rbinder, Const (_,T)) = T


120 
 fast (rbinder, Free (_,T)) = T


121 
 fast (rbinder, Bound i) =


122 
(#2 (nth_elem (i,rbinder))


123 
handle LIST _=> raise TERM("fastype: Bound", [Bound i]))


124 
 fast (rbinder, Var (_,T)) = T


125 
 fast (rbinder, Abs (_,T,u)) = T > fast (("",T) :: rbinder, u)


126 
in fast end;


127 


128 


129 
(*Eta normal form*)


130 
fun eta_norm(env as Envir.Envir{iTs,...}) =


131 
let fun etif (Type("fun",[T,U]), t) =


132 
Abs("", T, etif(U, incr_boundvars 1 t $ Bound 0))


133 
 etif (TVar(ixn,_),t) =


134 
(case assoc(iTs,ixn) of


135 
None => t  Some(T) => etif(T,t))


136 
 etif (_,t) = t;


137 
fun eta_nm (rbinder, Abs(a,T,body)) =


138 
Abs(a, T, eta_nm ((a,T)::rbinder, body))


139 
 eta_nm (rbinder, t) = etif(fastype env (rbinder,t), t)


140 
in eta_nm end;


141 


142 


143 
(*OCCURS CHECK


144 
Does the uvar occur in the term t?


145 
two forms of search, for whether there is a rigid path to the current term.


146 
"seen" is list of variables passed thru, is a memo variable for sharing.


147 
This version searches for nonrigid occurrence, returns true if found. *)


148 
fun occurs_terms (seen: (indexname list) ref,


149 
env: Envir.env, v: indexname, ts: term list): bool =


150 
let fun occurs [] = false


151 
 occurs (t::ts) = occur t orelse occurs ts


152 
and occur (Const _) = false


153 
 occur (Bound _) = false


154 
 occur (Free _) = false


155 
 occur (Var (w,_)) =


156 
if w mem !seen then false


157 
else if v=w then true


158 
(*no need to lookup: v has no assignment*)


159 
else (seen := w:: !seen;


160 
case Envir.lookup(env,w) of


161 
None => false


162 
 Some t => occur t)


163 
 occur (Abs(_,_,body)) = occur body


164 
 occur (f$t) = occur t orelse occur f


165 
in occurs ts end;


166 


167 


168 


169 
(* f(a1,...,an) > (f, [a1,...,an]) using the assignments*)


170 
fun head_of_in (env,t) : term = case t of


171 
f$_ => head_of_in(env,f)


172 
 Var (v,_) => (case Envir.lookup(env,v) of


173 
Some u => head_of_in(env,u)  None => t)


174 
 _ => t;


175 


176 


177 
datatype occ = NoOcc  Nonrigid  Rigid;


178 


179 
(* Rigid occur check


180 
Returns Rigid if it finds a rigid occurrence of the variable,


181 
Nonrigid if it finds a nonrigid path to the variable.


182 
NoOcc otherwise.


183 
Continues searching for a rigid occurrence even if it finds a nonrigid one.


184 


185 
Condition for detecting nonunifable terms: [ section 5.3 of Huet (1975) ]


186 
a rigid path to the variable, appearing with no arguments.


187 
Here completeness is sacrificed in order to reduce danger of divergence:


188 
reject ALL rigid paths to the variable.


189 
Could check for rigid paths to bound variables that are out of scope.


190 
Not necessary because the assignment test looks at variable's ENTIRE rbinder.


191 


192 
Treatment of head(arg1,...,argn):


193 
If head is a variable then no rigid path, switch to nonrigid search


194 
for arg1,...,argn.


195 
If head is an abstraction then possibly no rigid path (head could be a


196 
constant function) so again use nonrigid search. Happens only if


197 
term is not in normal form.


198 


199 
Warning: finds a rigid occurrence of ?f in ?f(t).


200 
Should NOT be called in this case: there is a flexflex unifier


201 
*)


202 
fun rigid_occurs_term (seen: (indexname list)ref, env, v: indexname, t) =


203 
let fun nonrigid t = if occurs_terms(seen,env,v,[t]) then Nonrigid


204 
else NoOcc


205 
fun occurs [] = NoOcc


206 
 occurs (t::ts) =


207 
(case occur t of


208 
Rigid => Rigid


209 
 oc => (case occurs ts of NoOcc => oc  oc2 => oc2))


210 
and occomb (f$t) =


211 
(case occur t of


212 
Rigid => Rigid


213 
 oc => (case occomb f of NoOcc => oc  oc2 => oc2))


214 
 occomb t = occur t


215 
and occur (Const _) = NoOcc


216 
 occur (Bound _) = NoOcc


217 
 occur (Free _) = NoOcc


218 
 occur (Var (w,_)) =


219 
if w mem !seen then NoOcc


220 
else if v=w then Rigid


221 
else (seen := w:: !seen;


222 
case Envir.lookup(env,w) of


223 
None => NoOcc


224 
 Some t => occur t)


225 
 occur (Abs(_,_,body)) = occur body


226 
 occur (t as f$_) = (*switch to nonrigid search?*)


227 
(case head_of_in (env,f) of


228 
Var (w,_) => (*w is not assigned*)


229 
if v=w then Rigid


230 
else nonrigid t


231 
 Abs(_,_,body) => nonrigid t (*not in normal form*)


232 
 _ => occomb t)


233 
in occur t end;


234 


235 


236 
exception CANTUNIFY; (*Signals nonunifiability. Does not signal errors!*)


237 
exception ASSIGN; (*Raised if not an assignment*)


238 


239 


240 
fun unify_types(T,U, env as Envir.Envir{asol,iTs,maxidx}) =


241 
if T=U then env else


242 
let val iTs' = Sign.Type.unify (#tsig(Sign.rep_sg (!sgr))) ((U,T),iTs)


243 
in Envir.Envir{asol=asol,maxidx=maxidx,iTs=iTs'}


244 
end handle Sign.Type.TUNIFY => raise CANTUNIFY;


245 


246 
fun test_unify_types(args as (T,U,_)) =


247 
let val sot = Sign.string_of_typ (!sgr);


248 
fun warn() = writeln("Potential loss of completeness: "^sot U^" = "^sot T);


249 
val env' = unify_types(args)


250 
in if is_TVar(T) orelse is_TVar(U) then warn() else ();


251 
env'


252 
end;


253 


254 
(*Is the term etaconvertible to a single variable with the given rbinder?


255 
Examples: ?a ?f(B.0) ?g(B.1,B.0)


256 
Result is var a for use in SIMPL. *)


257 
fun get_eta_var ([], _, Var vT) = vT


258 
 get_eta_var (_::rbinder, n, f $ Bound i) =


259 
if n=i then get_eta_var (rbinder, n+1, f)


260 
else raise ASSIGN


261 
 get_eta_var _ = raise ASSIGN;


262 


263 


264 
(* ([xn,...,x1], t) ======> (x1,...,xn)t *)


265 
fun rlist_abs ([], body) = body


266 
 rlist_abs ((a,T)::pairs, body) = rlist_abs(pairs, Abs(a, T, body));


267 


268 


269 
(*Solve v=u by assignment  "fixedpoint" to Huet  if v not in u.


270 
If v occurs rigidly then nonunifiable.


271 
If v occurs nonrigidly then must use full algorithm. *)


272 
fun assignment (env, rbinder, t, u) =


273 
let val (v,T) = get_eta_var(rbinder,0,t)


274 
in case rigid_occurs_term (ref[], env, v, u) of


275 
NoOcc => let val env = unify_types(body_type env T,


276 
fastype env (rbinder,u),env)


277 
in Envir.update ((v, rlist_abs(rbinder,u)), env) end


278 
 Nonrigid => raise ASSIGN


279 
 Rigid => raise CANTUNIFY


280 
end;


281 


282 


283 
(*Extends an rbinder with a new disagreement pair, if both are abstractions.


284 
Tries to unify types of the bound variables!


285 
Checks that binders have same length, since terms should be etanormal;


286 
if not, raises TERM, probably indicating type mismatch.


287 
Uses variable a (unless the null string) to preserve user's naming.*)


288 
fun new_dpair (rbinder, Abs(a,T,body1), Abs(b,U,body2), env) =


289 
let val env' = unify_types(T,U,env)


290 
val c = if a="" then b else a


291 
in new_dpair((c,T) :: rbinder, body1, body2, env') end


292 
 new_dpair (_, Abs _, _, _) = raise TERM ("new_dpair", [])


293 
 new_dpair (_, _, Abs _, _) = raise TERM ("new_dpair", [])


294 
 new_dpair (rbinder, t1, t2, env) = ((rbinder, t1, t2), env);


295 


296 


297 
fun head_norm_dpair (env, (rbinder,t,u)) : dpair * Envir.env =


298 
new_dpair (rbinder,


299 
eta_norm env (rbinder, head_norm(env,t)),


300 
eta_norm env (rbinder, head_norm(env,u)), env);


301 


302 


303 


304 
(*flexflex: the flexflex pairs, flexrigid: the flexrigid pairs


305 
Does not perform assignments for flexflex pairs:


306 
may create nonrigid paths, which prevent other assignments*)


307 
fun SIMPL0 (dp0, (env,flexflex,flexrigid))


308 
: Envir.env * dpair list * dpair list =


309 
let val (dp as (rbinder,t,u), env) = head_norm_dpair(env,dp0);


310 
fun SIMRANDS(f$t, g$u, env) =


311 
SIMPL0((rbinder,t,u), SIMRANDS(f,g,env))


312 
 SIMRANDS (t as _$_, _, _) =


313 
raise TERM ("SIMPL: operands mismatch", [t,u])


314 
 SIMRANDS (t, u as _$_, _) =


315 
raise TERM ("SIMPL: operands mismatch", [t,u])


316 
 SIMRANDS(_,_,env) = (env,flexflex,flexrigid);


317 
in case (head_of t, head_of u) of


318 
(Var(_,T), Var(_,U)) =>


319 
let val T' = body_type env T and U' = body_type env U;


320 
val env = unify_types(T',U',env)


321 
in (env, dp::flexflex, flexrigid) end


322 
 (Var _, _) =>


323 
((assignment (env,rbinder,t,u), flexflex, flexrigid)


324 
handle ASSIGN => (env, flexflex, dp::flexrigid))


325 
 (_, Var _) =>


326 
((assignment (env,rbinder,u,t), flexflex, flexrigid)


327 
handle ASSIGN => (env, flexflex, (rbinder,u,t)::flexrigid))


328 
 (Const(a,T), Const(b,U)) =>


329 
if a=b then SIMRANDS(t,u, unify_types(T,U,env))


330 
else raise CANTUNIFY


331 
 (Bound i, Bound j) =>


332 
if i=j then SIMRANDS(t,u,env) else raise CANTUNIFY


333 
 (Free(a,T), Free(b,U)) =>


334 
if a=b then SIMRANDS(t,u, unify_types(T,U,env))


335 
else raise CANTUNIFY


336 
 _ => raise CANTUNIFY


337 
end;


338 


339 


340 
(* changed(env,t) checks whether the head of t is a variable assigned in env*)


341 
fun changed (env, f$_) = changed (env,f)


342 
 changed (env, Var (v,_)) =


343 
(case Envir.lookup(env,v) of None=>false  _ => true)


344 
 changed _ = false;


345 


346 


347 
(*Recursion needed if any of the 'head variables' have been updated


348 
Clever would be to redo just the affected dpairs*)


349 
fun SIMPL (env,dpairs) : Envir.env * dpair list * dpair list =


350 
let val all as (env',flexflex,flexrigid) =


351 
foldr SIMPL0 (dpairs, (env,[],[]));


352 
val dps = flexrigid@flexflex


353 
in if exists (fn ((_,t,u)) => changed(env',t) orelse changed(env',u)) dps


354 
then SIMPL(env',dps) else all


355 
end;


356 


357 


358 
(*computes t(Bound(n+k1),...,Bound(n)) *)


359 
fun combound (t, n, k) =


360 
if k>0 then combound (t,n+1,k1) $ (Bound n) else t;


361 


362 


363 
(*Makes the terms E1,...,Em, where Ts = [T...Tm].


364 
Each Ei is ?Gi(B.(n1),...,B.0), and has type Ti


365 
The B.j are bound vars of binder.


366 
The terms are not made in etanormalform, SIMPL does that later.


367 
If done here, etaexpansion must be recursive in the arguments! *)


368 
fun make_args name (binder: typ list, env, []) = (env, []) (*frequent case*)


369 
 make_args name (binder: typ list, env, Ts) : Envir.env * term list =


370 
let fun funtype T = binder>T;


371 
val (env', vars) = Envir.genvars name (env, map funtype Ts)


372 
in (env', map (fn var=> combound(var, 0, length binder)) vars) end;


373 


374 


375 
(*Abstraction over a list of types, like list_abs*)


376 
fun types_abs ([],u) = u


377 
 types_abs (T::Ts, u) = Abs("", T, types_abs(Ts,u));


378 


379 
(*Abstraction over the binder of a type*)


380 
fun type_abs (env,T,t) = types_abs(binder_types env T, t);


381 


382 


383 
(*MATCH taking "big steps".


384 
Copies u into the Var v, using projection on targs or imitation.


385 
A projection is allowed unless SIMPL raises an exception.


386 
Allocates new variables in projection on a higherorder argument,


387 
or if u is a variable (flexflex dpair).


388 
Returns long sequence of every way of copying u, for backtracking


389 
For example, projection in ?b'(?a) may be wrong if other dpairs constrain ?a.


390 
The order for trying projections is crucial in ?b'(?a)


391 
NB "vname" is only used in the call to make_args!! *)


392 
fun matchcopy vname = let fun mc(rbinder, targs, u, ed as (env,dpairs))


393 
: (term * (Envir.env * dpair list))Sequence.seq =


394 
let (*Produce copies of uarg and cons them in front of uargs*)


395 
fun copycons uarg (uargs, (env, dpairs)) =


396 
Sequence.maps(fn (uarg', ed') => (uarg'::uargs, ed'))


397 
(mc (rbinder, targs,eta_norm env (rbinder,head_norm(env,uarg)),


398 
(env, dpairs)));


399 
(*Produce sequence of all possible ways of copying the arg list*)


400 
fun copyargs [] = Sequence.cons( ([],ed), Sequence.null)


401 
 copyargs (uarg::uargs) =


402 
Sequence.flats (Sequence.maps (copycons uarg) (copyargs uargs));


403 
val (uhead,uargs) = strip_comb u;


404 
val base = body_type env (fastype env (rbinder,uhead));


405 
fun joinargs (uargs',ed') = (list_comb(uhead,uargs'), ed');


406 
(*attempt projection on argument with given typ*)


407 
val Ts = map (curry (fastype env) rbinder) targs;


408 
fun projenv (head, (Us,bary), targ, tail) =


409 
let val env = if !trace_types then test_unify_types(base,bary,env)


410 
else unify_types(base,bary,env)


411 
in Sequence.seqof (fn () =>


412 
let val (env',args) = make_args vname (Ts,env,Us);


413 
(*higherorder projection: plug in targs for bound vars*)


414 
fun plugin arg = list_comb(head_of arg, targs);


415 
val dp = (rbinder, list_comb(targ, map plugin args), u);


416 
val (env2,frigid,fflex) = SIMPL (env', dp::dpairs)


417 
(*may raise exception CANTUNIFY*)


418 
in Some ((list_comb(head,args), (env2, frigid@fflex)),


419 
tail)


420 
end handle CANTUNIFY => Sequence.pull tail)


421 
end handle CANTUNIFY => tail;


422 
(*make a list of projections*)


423 
fun make_projs (T::Ts, targ::targs) =


424 
(Bound(length Ts), T, targ) :: make_projs (Ts,targs)


425 
 make_projs ([],[]) = []


426 
 make_projs _ = raise TERM ("make_projs", u::targs);


427 
(*try projections and imitation*)


428 
fun matchfun ((bvar,T,targ)::projs) =


429 
(projenv(bvar, strip_type env T, targ, matchfun projs))


430 
 matchfun [] = (*imitation last of all*)


431 
(case uhead of


432 
Const _ => Sequence.maps joinargs (copyargs uargs)


433 
 Free _ => Sequence.maps joinargs (copyargs uargs)


434 
 _ => Sequence.null) (*if Var, would be a loop!*)


435 
in case uhead of


436 
Abs(a, T, body) =>


437 
Sequence.maps(fn (body', ed') => (Abs (a,T,body'), ed'))


438 
(mc ((a,T)::rbinder,


439 
(map (incr_boundvars 1) targs) @ [Bound 0], body, ed))


440 
 Var (w,uary) =>


441 
(*a flexflex dpair: make variable for t*)


442 
let val (env', newhd) = Envir.genvar (#1 w) (env, Ts> base)


443 
val tabs = combound(newhd, 0, length Ts)


444 
val tsub = list_comb(newhd,targs)


445 
in Sequence.single (tabs, (env', (rbinder,tsub,u):: dpairs))


446 
end


447 
 _ => matchfun(rev(make_projs(Ts, targs)))


448 
end


449 
in mc end;


450 


451 


452 
(*Call matchcopy to produce assignments to the variable in the dpair*)


453 
fun MATCH (env, (rbinder,t,u), dpairs)


454 
: (Envir.env * dpair list)Sequence.seq =


455 
let val (Var(v,T), targs) = strip_comb t;


456 
val Ts = binder_types env T;


457 
fun new_dset (u', (env',dpairs')) =


458 
(*if v was updated to s, must unify s with u' *)


459 
case Envir.lookup(env',v) of


460 
None => (Envir.update ((v, types_abs(Ts, u')), env'), dpairs')


461 
 Some s => (env', ([], s, types_abs(Ts, u'))::dpairs')


462 
in Sequence.maps new_dset


463 
(matchcopy (#1 v) (rbinder, targs, u, (env,dpairs)))


464 
end;


465 


466 


467 


468 
(**** Flexflex processing ****)


469 


470 
(*At end of unification, do flexflex assignments like ?a > ?f(?b)


471 
Attempts to update t with u, raising ASSIGN if impossible*)


472 
fun ff_assign(env, rbinder, t, u) : Envir.env =


473 
let val (v,T) = get_eta_var(rbinder,0,t)


474 
in if occurs_terms (ref[], env, v, [u]) then raise ASSIGN


475 
else let val env = unify_types(body_type env T,fastype env (rbinder,u),env)


476 
in Envir.vupdate ((v, rlist_abs(rbinder, u)), env) end


477 
end;


478 


479 


480 
(*Flex argument: a term, its type, and the index that refers to it.*)


481 
type flarg = {t: term, T: typ, j: int};


482 


483 


484 
(*Form the arguments into records for deletion/sorting.*)


485 
fun flexargs ([],[],[]) = [] : flarg list


486 
 flexargs (j::js, t::ts, T::Ts) = {j=j, t=t, T=T} :: flexargs(js,ts,Ts)


487 
 flexargs _ = error"flexargs";


488 


489 


490 
(*If an argument contains a banned Bound, then it should be deleted.


491 
But if the path is flexible, this is difficult; the code gives up!*)


492 
exception CHANGE and CHANGE_FAIL; (*rigid and flexible occurrences*)


493 


494 


495 
(*Squash down indices at level >=lev to delete the js from a term.


496 
flex should initially be false, since the empty path is rigid.*)


497 
fun change_bnos (lev, js, flex) t =


498 
let val (head,args) = strip_comb t


499 
val flex' = flex orelse is_Var head


500 
val head' = case head of


501 
Bound i =>


502 
if i<lev then Bound i


503 
else if (ilev) mem js


504 
then if flex then raise CHANGE_FAIL


505 
else raise CHANGE


506 
else Bound (i  length (filter (fn j => j < ilev) js))


507 
 Abs (a,T,t) => Abs (a, T, change_bnos(lev+1, js, flex) t)


508 
 _ => head


509 
in list_comb (head', map (change_bnos (lev, js, flex')) args)


510 
end;


511 


512 


513 
(*Change indices, delete the argument if it contains a banned Bound*)


514 
fun change_arg js ({j,t,T}, args) : flarg list =


515 
{j=j, t= change_bnos(0,js,false)t, T=T} :: args handle CHANGE => args;


516 


517 


518 
(*Sort the arguments to create assignments if possible:


519 
create etaterms like ?g(B.1,B.0) *)


520 
fun arg_less ({t= Bound i1,...}, {t= Bound i2,...}) = (i2<i1)


521 
 arg_less (_:flarg, _:flarg) = false;


522 


523 
(*Test whether the new term would be etaequivalent to a variable 


524 
if so then there is no point in creating a new variable*)


525 
fun decreasing n ([]: flarg list) = (n=0)


526 
 decreasing n ({j,...}::args) = j=n1 andalso decreasing (n1) args;


527 


528 
(*Delete banned indices in the term, simplifying it.


529 
Force an assignment, if possible, by sorting the arguments.


530 
Update its head; squash indices in arguments. *)


531 
fun clean_term banned (env,t) =


532 
let val (Var(v,T), ts) = strip_comb t


533 
val (Ts,U) = strip_type env T


534 
and js = length ts  1 downto 0


535 
val args = sort arg_less


536 
(foldr (change_arg banned) (flexargs (js,ts,Ts), []))


537 
val ts' = map (#t) args


538 
in


539 
if decreasing (length Ts) args then (env, (list_comb(Var(v,T), ts')))


540 
else let val (env',v') = Envir.genvar (#1v) (env, map (#T) args > U)


541 
val body = list_comb(v', map (Bound o #j) args)


542 
val env2 = Envir.vupdate (((v, types_abs(Ts, body)), env'))


543 
(*the vupdate affects ts' if they contain v*)


544 
in


545 
(env2, Envir.norm_term env2 (list_comb(v',ts')))


546 
end


547 
end;


548 


549 


550 
(*Add tpair if not trivial or already there.


551 
Should check for swapped pairs??*)


552 
fun add_tpair (rbinder, (t0,u0), tpairs) : (term*term) list =


553 
if t0 aconv u0 then tpairs


554 
else


555 
let val t = rlist_abs(rbinder, t0) and u = rlist_abs(rbinder, u0);


556 
fun same(t',u') = (t aconv t') andalso (u aconv u')


557 
in if exists same tpairs then tpairs else (t,u)::tpairs end;


558 


559 


560 
(*Simplify both terms and check for assignments.


561 
Bound vars in the binder are "banned" unless used in both t AND u *)


562 
fun clean_ffpair ((rbinder, t, u), (env,tpairs)) =


563 
let val loot = loose_bnos t and loou = loose_bnos u


564 
fun add_index (((a,T), j), (bnos, newbinder)) =


565 
if j mem loot andalso j mem loou


566 
then (bnos, (a,T)::newbinder)


567 
else (j::bnos, newbinder);


568 
val indices = 0 upto (length rbinder  1);


569 
val (banned,rbin') = foldr add_index (rbinder~~indices, ([],[]));


570 
val (env', t') = clean_term banned (env, t);


571 
val (env'',u') = clean_term banned (env',u)


572 
in (ff_assign(env'', rbin', t', u'), tpairs)


573 
handle ASSIGN => (ff_assign(env'', rbin', u', t'), tpairs)


574 
handle ASSIGN => (env'', add_tpair(rbin', (t',u'), tpairs))


575 
end


576 
handle CHANGE_FAIL => (env, add_tpair(rbinder, (t,u), tpairs));


577 


578 


579 
(*IF the flexflex dpair is an assignment THEN do it ELSE put in tpairs


580 
eliminates trivial tpairs like t=t, as well as repeated ones


581 
trivial tpairs can easily escape SIMPL: ?A=t, ?A=?B, ?B=t gives t=t


582 
Resulting tpairs MAY NOT be in normal form: assignments may occur here.*)


583 
fun add_ffpair ((rbinder,t0,u0), (env,tpairs))


584 
: Envir.env * (term*term)list =


585 
let val t = Envir.norm_term env t0 and u = Envir.norm_term env u0


586 
in case (head_of t, head_of u) of


587 
(Var(v,T), Var(w,U)) => (*Check for identical variables...*)


588 
if v=w then (*...occur check would falsely return true!*)


589 
if T=U then (env, add_tpair (rbinder, (t,u), tpairs))


590 
else raise TERM ("add_ffpair: Var name confusion", [t,u])


591 
else if xless(v,w) then (*prefer to update the LARGER variable*)


592 
clean_ffpair ((rbinder, u, t), (env,tpairs))


593 
else clean_ffpair ((rbinder, t, u), (env,tpairs))


594 
 _ => raise TERM ("add_ffpair: Vars expected", [t,u])


595 
end;


596 


597 


598 
(*Print a tracing message + list of dpairs.


599 
In t==u print u first because it may be rigid or flexible 


600 
t is always flexible.*)


601 
fun print_dpairs msg (env,dpairs) =


602 
let fun pdp (rbinder,t,u) =


603 
let fun termT t = Sign.pretty_term (!sgr)


604 
(Envir.norm_term env (rlist_abs(rbinder,t)))


605 
val bsymbs = [termT u, Pretty.str" =?=", Pretty.brk 1,


606 
termT t];


607 
in writeln(Pretty.string_of(Pretty.blk(0,bsymbs))) end;


608 
in writeln msg; seq pdp dpairs end;


609 


610 


611 
(*Unify the dpairs in the environment.


612 
Returns flexflex disagreement pairs NOT IN normal form.


613 
SIMPL may raise exception CANTUNIFY. *)


614 
fun hounifiers (sg,env, tus : (term*term)list)


615 
: (Envir.env * (term*term)list)Sequence.seq =


616 
let fun add_unify tdepth ((env,dpairs), reseq) =


617 
Sequence.seqof (fn()=>


618 
let val (env',flexflex,flexrigid) =


619 
(if tdepth> !trace_bound andalso !trace_simp


620 
then print_dpairs "Enter SIMPL" (env,dpairs) else ();


621 
SIMPL (env,dpairs))


622 
in case flexrigid of


623 
[] => Some (foldr add_ffpair (flexflex, (env',[])), reseq)


624 
 dp::frigid' =>


625 
if tdepth > !search_bound then


626 
(prs"***Unification bound exceeded\n"; Sequence.pull reseq)


627 
else


628 
(if tdepth > !trace_bound then


629 
print_dpairs "Enter MATCH" (env',flexrigid@flexflex)


630 
else ();


631 
Sequence.pull (Sequence.its_right (add_unify (tdepth+1))


632 
(MATCH (env',dp, frigid'@flexflex), reseq)))


633 
end


634 
handle CANTUNIFY =>


635 
(if tdepth > !trace_bound then writeln"Failure node" else ();


636 
Sequence.pull reseq));


637 
val dps = map (fn(t,u)=> ([],t,u)) tus


638 
in sgr := sg;


639 
add_unify 1 ((env,dps), Sequence.null)


640 
end;


641 


642 
fun unifiers(params) =


643 
Sequence.cons((Pattern.unify(params), []), Sequence.null)


644 
handle Pattern.Unif => Sequence.null


645 
 Pattern.Pattern => hounifiers(params);


646 


647 


648 
(*For smash_flexflex1*)


649 
fun var_head_of (env,t) : indexname * typ =


650 
case head_of (strip_abs_body (Envir.norm_term env t)) of


651 
Var(v,T) => (v,T)


652 
 _ => raise CANTUNIFY; (*not flexible, cannot use trivial substitution*)


653 


654 


655 
(*Eliminate a flexflex pair by the trivial substitution, see Huet (1975)


656 
Unifies ?f(t1...rm) with ?g(u1...un) by ?f > %x1...xm.?a, ?g > %x1...xn.?a


657 
Unfortunately, unifies ?f(t,u) with ?g(t,u) by ?f, ?g > %(x,y)?a,


658 
though just ?g>?f is a more general unifier.


659 
Unlike Huet (1975), does not smash together all variables of same type 


660 
requires more work yet gives a less general unifier (fewer variables).


661 
Handles ?f(t1...rm) with ?f(u1...um) to avoid multiple updates. *)


662 
fun smash_flexflex1 ((t,u), env) : Envir.env =


663 
let val (v,T) = var_head_of (env,t)


664 
and (w,U) = var_head_of (env,u);


665 
val (env', var) = Envir.genvar (#1v) (env, body_type env T)


666 
val env'' = Envir.vupdate((w, type_abs(env',U,var)), env')


667 
in if (v,T)=(w,U) then env'' (*the other update would be identical*)


668 
else Envir.vupdate((v, type_abs(env',T,var)), env'')


669 
end;


670 


671 


672 
(*Smash all flexflexpairs. Should allow selection of pairs by a predicate?*)


673 
fun smash_flexflex (env,tpairs) : Envir.env =


674 
foldr smash_flexflex1 (tpairs, env);


675 


676 
(*Returns unifiers with no remaining disagreement pairs*)


677 
fun smash_unifiers (sg, env, tus) : Envir.env Sequence.seq =


678 
Sequence.maps smash_flexflex (unifiers(sg,env,tus));


679 


680 
end;
