--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/unify.ML Thu Sep 16 12:20:38 1993 +0200
@@ -0,0 +1,680 @@
+(* Title: unify
+ ID: $Id$
+ Author: Lawrence C Paulson, Cambridge University Computer Laboratory
+ Copyright Cambridge University 1992
+
+Higher-Order Unification
+
+Potential problem: type of Vars is often ignored, so two Vars with same
+indexname but different types can cause errors!
+*)
+
+
+signature UNIFY =
+sig
+ structure Sign: SIGN
+ structure Envir : ENVIR
+ structure Sequence : SEQUENCE
+ (*references for control and tracing*)
+ val trace_bound: int ref
+ val trace_simp: bool ref
+ val trace_types: bool ref
+ val search_bound: int ref
+ (*other exports*)
+ val combound : (term*int*int) -> term
+ val rlist_abs: (string*typ)list * term -> term
+ val smash_unifiers : Sign.sg * Envir.env * (term*term)list
+ -> (Envir.env Sequence.seq)
+ val unifiers: Sign.sg * Envir.env * ((term*term)list)
+ -> (Envir.env * (term * term)list) Sequence.seq
+end;
+
+functor UnifyFun (structure Sign: SIGN and Envir: ENVIR and Sequence: SEQUENCE
+ and Pattern:PATTERN
+ sharing type Sign.sg = Pattern.sg
+ and type Envir.env = Pattern.env)
+ : UNIFY =
+struct
+
+structure Sign = Sign;
+structure Envir = Envir;
+structure Sequence = Sequence;
+structure Pretty = Sign.Syntax.Pretty;
+
+(*Unification options*)
+
+val trace_bound = ref 10 (*tracing starts above this depth, 0 for full*)
+and search_bound = ref 20 (*unification quits above this depth*)
+and trace_simp = ref false (*print dpairs before calling SIMPL*)
+and trace_types = ref false (*announce potential incompleteness
+ of type unification*)
+
+val sgr = ref(Sign.pure);
+
+type binderlist = (string*typ) list;
+
+type dpair = binderlist * term * term;
+
+fun body_type(Envir.Envir{iTs,...}) =
+let fun bT(Type("fun",[_,T])) = bT T
+ | bT(T as TVar(ixn,_)) = (case assoc(iTs,ixn) of
+ None => T | Some(T') => bT T')
+ | bT T = T
+in bT end;
+
+fun binder_types(Envir.Envir{iTs,...}) =
+let fun bTs(Type("fun",[T,U])) = T :: bTs U
+ | bTs(T as TVar(ixn,_)) = (case assoc(iTs,ixn) of
+ None => [] | Some(T') => bTs T')
+ | bTs _ = []
+in bTs end;
+
+fun strip_type env T = (binder_types env T, body_type env T);
+
+
+(*Put a term into head normal form for unification.
+ Operands need not be in normal form. Does eta-expansions on the head,
+ which involves renumbering (thus copying) the args. To avoid this
+ inefficiency, avoid partial application: if an atom is applied to
+ any arguments at all, apply it to its full number of arguments.
+ For
+ rbinder = [(x1,T),...,(xm,Tm)] (user's var names preserved!)
+ args = [arg1,...,argn]
+ the value of
+ (xm,...,x1)(head(arg1,...,argn)) remains invariant.
+*)
+
+local exception SAME
+in
+ fun head_norm (env,t) : term =
+ let fun hnorm (Var (v,T)) =
+ (case Envir.lookup (env,v) of
+ Some u => head_norm (env, u)
+ | None => raise SAME)
+ | hnorm (Abs(a,T,body)) = Abs(a, T, hnorm body)
+ | hnorm (Abs(_,_,body) $ t) =
+ head_norm (env, subst_bounds([t], body))
+ | hnorm (f $ t) =
+ (case hnorm f of
+ Abs(_,_,body) =>
+ head_norm (env, subst_bounds([t], body))
+ | nf => nf $ t)
+ | hnorm _ = raise SAME
+ in hnorm t handle SAME=> t end
+end;
+
+
+(*finds type of term without checking that combinations are consistent
+ rbinder holds types of bound variables*)
+fun fastype (Envir.Envir{iTs,...}) =
+let val funerr = "fastype: expected function type";
+ fun fast(rbinder, f$u) =
+ (case (fast (rbinder, f)) of
+ Type("fun",[_,T]) => T
+ | TVar(ixn,_) =>
+ (case assoc(iTs,ixn) of
+ Some(Type("fun",[_,T])) => T
+ | _ => raise TERM(funerr, [f$u]))
+ | _ => raise TERM(funerr, [f$u]))
+ | fast (rbinder, Const (_,T)) = T
+ | fast (rbinder, Free (_,T)) = T
+ | fast (rbinder, Bound i) =
+ (#2 (nth_elem (i,rbinder))
+ handle LIST _=> raise TERM("fastype: Bound", [Bound i]))
+ | fast (rbinder, Var (_,T)) = T
+ | fast (rbinder, Abs (_,T,u)) = T --> fast (("",T) :: rbinder, u)
+in fast end;
+
+
+(*Eta normal form*)
+fun eta_norm(env as Envir.Envir{iTs,...}) =
+ let fun etif (Type("fun",[T,U]), t) =
+ Abs("", T, etif(U, incr_boundvars 1 t $ Bound 0))
+ | etif (TVar(ixn,_),t) =
+ (case assoc(iTs,ixn) of
+ None => t | Some(T) => etif(T,t))
+ | etif (_,t) = t;
+ fun eta_nm (rbinder, Abs(a,T,body)) =
+ Abs(a, T, eta_nm ((a,T)::rbinder, body))
+ | eta_nm (rbinder, t) = etif(fastype env (rbinder,t), t)
+ in eta_nm end;
+
+
+(*OCCURS CHECK
+ Does the uvar occur in the term t?
+ two forms of search, for whether there is a rigid path to the current term.
+ "seen" is list of variables passed thru, is a memo variable for sharing.
+ This version searches for nonrigid occurrence, returns true if found. *)
+fun occurs_terms (seen: (indexname list) ref,
+ env: Envir.env, v: indexname, ts: term list): bool =
+ let fun occurs [] = false
+ | occurs (t::ts) = occur t orelse occurs ts
+ and occur (Const _) = false
+ | occur (Bound _) = false
+ | occur (Free _) = false
+ | occur (Var (w,_)) =
+ if w mem !seen then false
+ else if v=w then true
+ (*no need to lookup: v has no assignment*)
+ else (seen := w:: !seen;
+ case Envir.lookup(env,w) of
+ None => false
+ | Some t => occur t)
+ | occur (Abs(_,_,body)) = occur body
+ | occur (f$t) = occur t orelse occur f
+ in occurs ts end;
+
+
+
+(* f(a1,...,an) ----> (f, [a1,...,an]) using the assignments*)
+fun head_of_in (env,t) : term = case t of
+ f$_ => head_of_in(env,f)
+ | Var (v,_) => (case Envir.lookup(env,v) of
+ Some u => head_of_in(env,u) | None => t)
+ | _ => t;
+
+
+datatype occ = NoOcc | Nonrigid | Rigid;
+
+(* Rigid occur check
+Returns Rigid if it finds a rigid occurrence of the variable,
+ Nonrigid if it finds a nonrigid path to the variable.
+ NoOcc otherwise.
+ Continues searching for a rigid occurrence even if it finds a nonrigid one.
+
+Condition for detecting non-unifable terms: [ section 5.3 of Huet (1975) ]
+ a rigid path to the variable, appearing with no arguments.
+Here completeness is sacrificed in order to reduce danger of divergence:
+ reject ALL rigid paths to the variable.
+Could check for rigid paths to bound variables that are out of scope.
+Not necessary because the assignment test looks at variable's ENTIRE rbinder.
+
+Treatment of head(arg1,...,argn):
+If head is a variable then no rigid path, switch to nonrigid search
+for arg1,...,argn.
+If head is an abstraction then possibly no rigid path (head could be a
+ constant function) so again use nonrigid search. Happens only if
+ term is not in normal form.
+
+Warning: finds a rigid occurrence of ?f in ?f(t).
+ Should NOT be called in this case: there is a flex-flex unifier
+*)
+fun rigid_occurs_term (seen: (indexname list)ref, env, v: indexname, t) =
+ let fun nonrigid t = if occurs_terms(seen,env,v,[t]) then Nonrigid
+ else NoOcc
+ fun occurs [] = NoOcc
+ | occurs (t::ts) =
+ (case occur t of
+ Rigid => Rigid
+ | oc => (case occurs ts of NoOcc => oc | oc2 => oc2))
+ and occomb (f$t) =
+ (case occur t of
+ Rigid => Rigid
+ | oc => (case occomb f of NoOcc => oc | oc2 => oc2))
+ | occomb t = occur t
+ and occur (Const _) = NoOcc
+ | occur (Bound _) = NoOcc
+ | occur (Free _) = NoOcc
+ | occur (Var (w,_)) =
+ if w mem !seen then NoOcc
+ else if v=w then Rigid
+ else (seen := w:: !seen;
+ case Envir.lookup(env,w) of
+ None => NoOcc
+ | Some t => occur t)
+ | occur (Abs(_,_,body)) = occur body
+ | occur (t as f$_) = (*switch to nonrigid search?*)
+ (case head_of_in (env,f) of
+ Var (w,_) => (*w is not assigned*)
+ if v=w then Rigid
+ else nonrigid t
+ | Abs(_,_,body) => nonrigid t (*not in normal form*)
+ | _ => occomb t)
+ in occur t end;
+
+
+exception CANTUNIFY; (*Signals non-unifiability. Does not signal errors!*)
+exception ASSIGN; (*Raised if not an assignment*)
+
+
+fun unify_types(T,U, env as Envir.Envir{asol,iTs,maxidx}) =
+ if T=U then env else
+ let val iTs' = Sign.Type.unify (#tsig(Sign.rep_sg (!sgr))) ((U,T),iTs)
+ in Envir.Envir{asol=asol,maxidx=maxidx,iTs=iTs'}
+ end handle Sign.Type.TUNIFY => raise CANTUNIFY;
+
+fun test_unify_types(args as (T,U,_)) =
+let val sot = Sign.string_of_typ (!sgr);
+ fun warn() = writeln("Potential loss of completeness: "^sot U^" = "^sot T);
+ val env' = unify_types(args)
+in if is_TVar(T) orelse is_TVar(U) then warn() else ();
+ env'
+end;
+
+(*Is the term eta-convertible to a single variable with the given rbinder?
+ Examples: ?a ?f(B.0) ?g(B.1,B.0)
+ Result is var a for use in SIMPL. *)
+fun get_eta_var ([], _, Var vT) = vT
+ | get_eta_var (_::rbinder, n, f $ Bound i) =
+ if n=i then get_eta_var (rbinder, n+1, f)
+ else raise ASSIGN
+ | get_eta_var _ = raise ASSIGN;
+
+
+(* ([xn,...,x1], t) ======> (x1,...,xn)t *)
+fun rlist_abs ([], body) = body
+ | rlist_abs ((a,T)::pairs, body) = rlist_abs(pairs, Abs(a, T, body));
+
+
+(*Solve v=u by assignment -- "fixedpoint" to Huet -- if v not in u.
+ If v occurs rigidly then nonunifiable.
+ If v occurs nonrigidly then must use full algorithm. *)
+fun assignment (env, rbinder, t, u) =
+ let val (v,T) = get_eta_var(rbinder,0,t)
+ in case rigid_occurs_term (ref[], env, v, u) of
+ NoOcc => let val env = unify_types(body_type env T,
+ fastype env (rbinder,u),env)
+ in Envir.update ((v, rlist_abs(rbinder,u)), env) end
+ | Nonrigid => raise ASSIGN
+ | Rigid => raise CANTUNIFY
+ end;
+
+
+(*Extends an rbinder with a new disagreement pair, if both are abstractions.
+ Tries to unify types of the bound variables!
+ Checks that binders have same length, since terms should be eta-normal;
+ if not, raises TERM, probably indicating type mismatch.
+ Uses variable a (unless the null string) to preserve user's naming.*)
+fun new_dpair (rbinder, Abs(a,T,body1), Abs(b,U,body2), env) =
+ let val env' = unify_types(T,U,env)
+ val c = if a="" then b else a
+ in new_dpair((c,T) :: rbinder, body1, body2, env') end
+ | new_dpair (_, Abs _, _, _) = raise TERM ("new_dpair", [])
+ | new_dpair (_, _, Abs _, _) = raise TERM ("new_dpair", [])
+ | new_dpair (rbinder, t1, t2, env) = ((rbinder, t1, t2), env);
+
+
+fun head_norm_dpair (env, (rbinder,t,u)) : dpair * Envir.env =
+ new_dpair (rbinder,
+ eta_norm env (rbinder, head_norm(env,t)),
+ eta_norm env (rbinder, head_norm(env,u)), env);
+
+
+
+(*flexflex: the flex-flex pairs, flexrigid: the flex-rigid pairs
+ Does not perform assignments for flex-flex pairs:
+ may create nonrigid paths, which prevent other assignments*)
+fun SIMPL0 (dp0, (env,flexflex,flexrigid))
+ : Envir.env * dpair list * dpair list =
+ let val (dp as (rbinder,t,u), env) = head_norm_dpair(env,dp0);
+ fun SIMRANDS(f$t, g$u, env) =
+ SIMPL0((rbinder,t,u), SIMRANDS(f,g,env))
+ | SIMRANDS (t as _$_, _, _) =
+ raise TERM ("SIMPL: operands mismatch", [t,u])
+ | SIMRANDS (t, u as _$_, _) =
+ raise TERM ("SIMPL: operands mismatch", [t,u])
+ | SIMRANDS(_,_,env) = (env,flexflex,flexrigid);
+ in case (head_of t, head_of u) of
+ (Var(_,T), Var(_,U)) =>
+ let val T' = body_type env T and U' = body_type env U;
+ val env = unify_types(T',U',env)
+ in (env, dp::flexflex, flexrigid) end
+ | (Var _, _) =>
+ ((assignment (env,rbinder,t,u), flexflex, flexrigid)
+ handle ASSIGN => (env, flexflex, dp::flexrigid))
+ | (_, Var _) =>
+ ((assignment (env,rbinder,u,t), flexflex, flexrigid)
+ handle ASSIGN => (env, flexflex, (rbinder,u,t)::flexrigid))
+ | (Const(a,T), Const(b,U)) =>
+ if a=b then SIMRANDS(t,u, unify_types(T,U,env))
+ else raise CANTUNIFY
+ | (Bound i, Bound j) =>
+ if i=j then SIMRANDS(t,u,env) else raise CANTUNIFY
+ | (Free(a,T), Free(b,U)) =>
+ if a=b then SIMRANDS(t,u, unify_types(T,U,env))
+ else raise CANTUNIFY
+ | _ => raise CANTUNIFY
+ end;
+
+
+(* changed(env,t) checks whether the head of t is a variable assigned in env*)
+fun changed (env, f$_) = changed (env,f)
+ | changed (env, Var (v,_)) =
+ (case Envir.lookup(env,v) of None=>false | _ => true)
+ | changed _ = false;
+
+
+(*Recursion needed if any of the 'head variables' have been updated
+ Clever would be to re-do just the affected dpairs*)
+fun SIMPL (env,dpairs) : Envir.env * dpair list * dpair list =
+ let val all as (env',flexflex,flexrigid) =
+ foldr SIMPL0 (dpairs, (env,[],[]));
+ val dps = flexrigid@flexflex
+ in if exists (fn ((_,t,u)) => changed(env',t) orelse changed(env',u)) dps
+ then SIMPL(env',dps) else all
+ end;
+
+
+(*computes t(Bound(n+k-1),...,Bound(n)) *)
+fun combound (t, n, k) =
+ if k>0 then combound (t,n+1,k-1) $ (Bound n) else t;
+
+
+(*Makes the terms E1,...,Em, where Ts = [T...Tm].
+ Each Ei is ?Gi(B.(n-1),...,B.0), and has type Ti
+ The B.j are bound vars of binder.
+ The terms are not made in eta-normal-form, SIMPL does that later.
+ If done here, eta-expansion must be recursive in the arguments! *)
+fun make_args name (binder: typ list, env, []) = (env, []) (*frequent case*)
+ | make_args name (binder: typ list, env, Ts) : Envir.env * term list =
+ let fun funtype T = binder--->T;
+ val (env', vars) = Envir.genvars name (env, map funtype Ts)
+ in (env', map (fn var=> combound(var, 0, length binder)) vars) end;
+
+
+(*Abstraction over a list of types, like list_abs*)
+fun types_abs ([],u) = u
+ | types_abs (T::Ts, u) = Abs("", T, types_abs(Ts,u));
+
+(*Abstraction over the binder of a type*)
+fun type_abs (env,T,t) = types_abs(binder_types env T, t);
+
+
+(*MATCH taking "big steps".
+ Copies u into the Var v, using projection on targs or imitation.
+ A projection is allowed unless SIMPL raises an exception.
+ Allocates new variables in projection on a higher-order argument,
+ or if u is a variable (flex-flex dpair).
+ Returns long sequence of every way of copying u, for backtracking
+ For example, projection in ?b'(?a) may be wrong if other dpairs constrain ?a.
+ The order for trying projections is crucial in ?b'(?a)
+ NB "vname" is only used in the call to make_args!! *)
+fun matchcopy vname = let fun mc(rbinder, targs, u, ed as (env,dpairs))
+ : (term * (Envir.env * dpair list))Sequence.seq =
+let (*Produce copies of uarg and cons them in front of uargs*)
+ fun copycons uarg (uargs, (env, dpairs)) =
+ Sequence.maps(fn (uarg', ed') => (uarg'::uargs, ed'))
+ (mc (rbinder, targs,eta_norm env (rbinder,head_norm(env,uarg)),
+ (env, dpairs)));
+ (*Produce sequence of all possible ways of copying the arg list*)
+ fun copyargs [] = Sequence.cons( ([],ed), Sequence.null)
+ | copyargs (uarg::uargs) =
+ Sequence.flats (Sequence.maps (copycons uarg) (copyargs uargs));
+ val (uhead,uargs) = strip_comb u;
+ val base = body_type env (fastype env (rbinder,uhead));
+ fun joinargs (uargs',ed') = (list_comb(uhead,uargs'), ed');
+ (*attempt projection on argument with given typ*)
+ val Ts = map (curry (fastype env) rbinder) targs;
+ fun projenv (head, (Us,bary), targ, tail) =
+ let val env = if !trace_types then test_unify_types(base,bary,env)
+ else unify_types(base,bary,env)
+ in Sequence.seqof (fn () =>
+ let val (env',args) = make_args vname (Ts,env,Us);
+ (*higher-order projection: plug in targs for bound vars*)
+ fun plugin arg = list_comb(head_of arg, targs);
+ val dp = (rbinder, list_comb(targ, map plugin args), u);
+ val (env2,frigid,fflex) = SIMPL (env', dp::dpairs)
+ (*may raise exception CANTUNIFY*)
+ in Some ((list_comb(head,args), (env2, frigid@fflex)),
+ tail)
+ end handle CANTUNIFY => Sequence.pull tail)
+ end handle CANTUNIFY => tail;
+ (*make a list of projections*)
+ fun make_projs (T::Ts, targ::targs) =
+ (Bound(length Ts), T, targ) :: make_projs (Ts,targs)
+ | make_projs ([],[]) = []
+ | make_projs _ = raise TERM ("make_projs", u::targs);
+ (*try projections and imitation*)
+ fun matchfun ((bvar,T,targ)::projs) =
+ (projenv(bvar, strip_type env T, targ, matchfun projs))
+ | matchfun [] = (*imitation last of all*)
+ (case uhead of
+ Const _ => Sequence.maps joinargs (copyargs uargs)
+ | Free _ => Sequence.maps joinargs (copyargs uargs)
+ | _ => Sequence.null) (*if Var, would be a loop!*)
+in case uhead of
+ Abs(a, T, body) =>
+ Sequence.maps(fn (body', ed') => (Abs (a,T,body'), ed'))
+ (mc ((a,T)::rbinder,
+ (map (incr_boundvars 1) targs) @ [Bound 0], body, ed))
+ | Var (w,uary) =>
+ (*a flex-flex dpair: make variable for t*)
+ let val (env', newhd) = Envir.genvar (#1 w) (env, Ts---> base)
+ val tabs = combound(newhd, 0, length Ts)
+ val tsub = list_comb(newhd,targs)
+ in Sequence.single (tabs, (env', (rbinder,tsub,u):: dpairs))
+ end
+ | _ => matchfun(rev(make_projs(Ts, targs)))
+end
+in mc end;
+
+
+(*Call matchcopy to produce assignments to the variable in the dpair*)
+fun MATCH (env, (rbinder,t,u), dpairs)
+ : (Envir.env * dpair list)Sequence.seq =
+ let val (Var(v,T), targs) = strip_comb t;
+ val Ts = binder_types env T;
+ fun new_dset (u', (env',dpairs')) =
+ (*if v was updated to s, must unify s with u' *)
+ case Envir.lookup(env',v) of
+ None => (Envir.update ((v, types_abs(Ts, u')), env'), dpairs')
+ | Some s => (env', ([], s, types_abs(Ts, u'))::dpairs')
+ in Sequence.maps new_dset
+ (matchcopy (#1 v) (rbinder, targs, u, (env,dpairs)))
+ end;
+
+
+
+(**** Flex-flex processing ****)
+
+(*At end of unification, do flex-flex assignments like ?a -> ?f(?b)
+ Attempts to update t with u, raising ASSIGN if impossible*)
+fun ff_assign(env, rbinder, t, u) : Envir.env =
+let val (v,T) = get_eta_var(rbinder,0,t)
+in if occurs_terms (ref[], env, v, [u]) then raise ASSIGN
+ else let val env = unify_types(body_type env T,fastype env (rbinder,u),env)
+ in Envir.vupdate ((v, rlist_abs(rbinder, u)), env) end
+end;
+
+
+(*Flex argument: a term, its type, and the index that refers to it.*)
+type flarg = {t: term, T: typ, j: int};
+
+
+(*Form the arguments into records for deletion/sorting.*)
+fun flexargs ([],[],[]) = [] : flarg list
+ | flexargs (j::js, t::ts, T::Ts) = {j=j, t=t, T=T} :: flexargs(js,ts,Ts)
+ | flexargs _ = error"flexargs";
+
+
+(*If an argument contains a banned Bound, then it should be deleted.
+ But if the path is flexible, this is difficult; the code gives up!*)
+exception CHANGE and CHANGE_FAIL; (*rigid and flexible occurrences*)
+
+
+(*Squash down indices at level >=lev to delete the js from a term.
+ flex should initially be false, since the empty path is rigid.*)
+fun change_bnos (lev, js, flex) t =
+ let val (head,args) = strip_comb t
+ val flex' = flex orelse is_Var head
+ val head' = case head of
+ Bound i =>
+ if i<lev then Bound i
+ else if (i-lev) mem js
+ then if flex then raise CHANGE_FAIL
+ else raise CHANGE
+ else Bound (i - length (filter (fn j => j < i-lev) js))
+ | Abs (a,T,t) => Abs (a, T, change_bnos(lev+1, js, flex) t)
+ | _ => head
+ in list_comb (head', map (change_bnos (lev, js, flex')) args)
+ end;
+
+
+(*Change indices, delete the argument if it contains a banned Bound*)
+fun change_arg js ({j,t,T}, args) : flarg list =
+ {j=j, t= change_bnos(0,js,false)t, T=T} :: args handle CHANGE => args;
+
+
+(*Sort the arguments to create assignments if possible:
+ create eta-terms like ?g(B.1,B.0) *)
+fun arg_less ({t= Bound i1,...}, {t= Bound i2,...}) = (i2<i1)
+ | arg_less (_:flarg, _:flarg) = false;
+
+(*Test whether the new term would be eta-equivalent to a variable --
+ if so then there is no point in creating a new variable*)
+fun decreasing n ([]: flarg list) = (n=0)
+ | decreasing n ({j,...}::args) = j=n-1 andalso decreasing (n-1) args;
+
+(*Delete banned indices in the term, simplifying it.
+ Force an assignment, if possible, by sorting the arguments.
+ Update its head; squash indices in arguments. *)
+fun clean_term banned (env,t) =
+ let val (Var(v,T), ts) = strip_comb t
+ val (Ts,U) = strip_type env T
+ and js = length ts - 1 downto 0
+ val args = sort arg_less
+ (foldr (change_arg banned) (flexargs (js,ts,Ts), []))
+ val ts' = map (#t) args
+ in
+ if decreasing (length Ts) args then (env, (list_comb(Var(v,T), ts')))
+ else let val (env',v') = Envir.genvar (#1v) (env, map (#T) args ---> U)
+ val body = list_comb(v', map (Bound o #j) args)
+ val env2 = Envir.vupdate (((v, types_abs(Ts, body)), env'))
+ (*the vupdate affects ts' if they contain v*)
+ in
+ (env2, Envir.norm_term env2 (list_comb(v',ts')))
+ end
+ end;
+
+
+(*Add tpair if not trivial or already there.
+ Should check for swapped pairs??*)
+fun add_tpair (rbinder, (t0,u0), tpairs) : (term*term) list =
+ if t0 aconv u0 then tpairs
+ else
+ let val t = rlist_abs(rbinder, t0) and u = rlist_abs(rbinder, u0);
+ fun same(t',u') = (t aconv t') andalso (u aconv u')
+ in if exists same tpairs then tpairs else (t,u)::tpairs end;
+
+
+(*Simplify both terms and check for assignments.
+ Bound vars in the binder are "banned" unless used in both t AND u *)
+fun clean_ffpair ((rbinder, t, u), (env,tpairs)) =
+ let val loot = loose_bnos t and loou = loose_bnos u
+ fun add_index (((a,T), j), (bnos, newbinder)) =
+ if j mem loot andalso j mem loou
+ then (bnos, (a,T)::newbinder)
+ else (j::bnos, newbinder);
+ val indices = 0 upto (length rbinder - 1);
+ val (banned,rbin') = foldr add_index (rbinder~~indices, ([],[]));
+ val (env', t') = clean_term banned (env, t);
+ val (env'',u') = clean_term banned (env',u)
+ in (ff_assign(env'', rbin', t', u'), tpairs)
+ handle ASSIGN => (ff_assign(env'', rbin', u', t'), tpairs)
+ handle ASSIGN => (env'', add_tpair(rbin', (t',u'), tpairs))
+ end
+ handle CHANGE_FAIL => (env, add_tpair(rbinder, (t,u), tpairs));
+
+
+(*IF the flex-flex dpair is an assignment THEN do it ELSE put in tpairs
+ eliminates trivial tpairs like t=t, as well as repeated ones
+ trivial tpairs can easily escape SIMPL: ?A=t, ?A=?B, ?B=t gives t=t
+ Resulting tpairs MAY NOT be in normal form: assignments may occur here.*)
+fun add_ffpair ((rbinder,t0,u0), (env,tpairs))
+ : Envir.env * (term*term)list =
+ let val t = Envir.norm_term env t0 and u = Envir.norm_term env u0
+ in case (head_of t, head_of u) of
+ (Var(v,T), Var(w,U)) => (*Check for identical variables...*)
+ if v=w then (*...occur check would falsely return true!*)
+ if T=U then (env, add_tpair (rbinder, (t,u), tpairs))
+ else raise TERM ("add_ffpair: Var name confusion", [t,u])
+ else if xless(v,w) then (*prefer to update the LARGER variable*)
+ clean_ffpair ((rbinder, u, t), (env,tpairs))
+ else clean_ffpair ((rbinder, t, u), (env,tpairs))
+ | _ => raise TERM ("add_ffpair: Vars expected", [t,u])
+ end;
+
+
+(*Print a tracing message + list of dpairs.
+ In t==u print u first because it may be rigid or flexible --
+ t is always flexible.*)
+fun print_dpairs msg (env,dpairs) =
+ let fun pdp (rbinder,t,u) =
+ let fun termT t = Sign.pretty_term (!sgr)
+ (Envir.norm_term env (rlist_abs(rbinder,t)))
+ val bsymbs = [termT u, Pretty.str" =?=", Pretty.brk 1,
+ termT t];
+ in writeln(Pretty.string_of(Pretty.blk(0,bsymbs))) end;
+ in writeln msg; seq pdp dpairs end;
+
+
+(*Unify the dpairs in the environment.
+ Returns flex-flex disagreement pairs NOT IN normal form.
+ SIMPL may raise exception CANTUNIFY. *)
+fun hounifiers (sg,env, tus : (term*term)list)
+ : (Envir.env * (term*term)list)Sequence.seq =
+ let fun add_unify tdepth ((env,dpairs), reseq) =
+ Sequence.seqof (fn()=>
+ let val (env',flexflex,flexrigid) =
+ (if tdepth> !trace_bound andalso !trace_simp
+ then print_dpairs "Enter SIMPL" (env,dpairs) else ();
+ SIMPL (env,dpairs))
+ in case flexrigid of
+ [] => Some (foldr add_ffpair (flexflex, (env',[])), reseq)
+ | dp::frigid' =>
+ if tdepth > !search_bound then
+ (prs"***Unification bound exceeded\n"; Sequence.pull reseq)
+ else
+ (if tdepth > !trace_bound then
+ print_dpairs "Enter MATCH" (env',flexrigid@flexflex)
+ else ();
+ Sequence.pull (Sequence.its_right (add_unify (tdepth+1))
+ (MATCH (env',dp, frigid'@flexflex), reseq)))
+ end
+ handle CANTUNIFY =>
+ (if tdepth > !trace_bound then writeln"Failure node" else ();
+ Sequence.pull reseq));
+ val dps = map (fn(t,u)=> ([],t,u)) tus
+ in sgr := sg;
+ add_unify 1 ((env,dps), Sequence.null)
+ end;
+
+fun unifiers(params) =
+ Sequence.cons((Pattern.unify(params), []), Sequence.null)
+ handle Pattern.Unif => Sequence.null
+ | Pattern.Pattern => hounifiers(params);
+
+
+(*For smash_flexflex1*)
+fun var_head_of (env,t) : indexname * typ =
+ case head_of (strip_abs_body (Envir.norm_term env t)) of
+ Var(v,T) => (v,T)
+ | _ => raise CANTUNIFY; (*not flexible, cannot use trivial substitution*)
+
+
+(*Eliminate a flex-flex pair by the trivial substitution, see Huet (1975)
+ Unifies ?f(t1...rm) with ?g(u1...un) by ?f -> %x1...xm.?a, ?g -> %x1...xn.?a
+ Unfortunately, unifies ?f(t,u) with ?g(t,u) by ?f, ?g -> %(x,y)?a,
+ though just ?g->?f is a more general unifier.
+ Unlike Huet (1975), does not smash together all variables of same type --
+ requires more work yet gives a less general unifier (fewer variables).
+ Handles ?f(t1...rm) with ?f(u1...um) to avoid multiple updates. *)
+fun smash_flexflex1 ((t,u), env) : Envir.env =
+ let val (v,T) = var_head_of (env,t)
+ and (w,U) = var_head_of (env,u);
+ val (env', var) = Envir.genvar (#1v) (env, body_type env T)
+ val env'' = Envir.vupdate((w, type_abs(env',U,var)), env')
+ in if (v,T)=(w,U) then env'' (*the other update would be identical*)
+ else Envir.vupdate((v, type_abs(env',T,var)), env'')
+ end;
+
+
+(*Smash all flex-flexpairs. Should allow selection of pairs by a predicate?*)
+fun smash_flexflex (env,tpairs) : Envir.env =
+ foldr smash_flexflex1 (tpairs, env);
+
+(*Returns unifiers with no remaining disagreement pairs*)
+fun smash_unifiers (sg, env, tus) : Envir.env Sequence.seq =
+ Sequence.maps smash_flexflex (unifiers(sg,env,tus));
+
+end;