diff -r 000000000000 -r a5a9c433f639 src/Pure/unify.ML --- /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 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 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;