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