berghofe@15797: (* Title: Pure/unify.ML clasohm@0: ID: $Id$ wenzelm@16425: Author: Lawrence C Paulson, Cambridge University Computer Laboratory clasohm@0: Copyright Cambridge University 1992 clasohm@0: wenzelm@16425: Higher-Order Unification. clasohm@0: wenzelm@16425: Types as well as terms are unified. The outermost functions assume wenzelm@16425: the terms to be unified already have the same type. In resolution, wenzelm@16425: this is assured because both have type "prop". clasohm@0: *) clasohm@0: wenzelm@16425: signature UNIFY = wenzelm@16425: sig 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 wenzelm@16425: val unifiers: theory * Envir.env * ((term * term) list) -> wenzelm@16425: (Envir.env * (term * term) list) Seq.seq wenzelm@19864: val smash_unifiers: theory -> (term * term) list -> Envir.env -> Envir.env Seq.seq wenzelm@19864: val matchers: theory -> (term * term) list -> Envir.env Seq.seq wenzelm@19864: val matches_list: theory -> term list -> term list -> bool wenzelm@16425: end clasohm@0: wenzelm@19864: structure Unify : UNIFY = clasohm@0: struct clasohm@0: clasohm@0: (*Unification options*) clasohm@0: wenzelm@19864: val trace_bound = ref 25 (*tracing starts above this depth, 0 for full*) wenzelm@19864: and search_bound = ref 30 (*unification quits above this depth*) wenzelm@19864: and trace_simp = ref false (*print dpairs before calling SIMPL*) wenzelm@19876: and trace_types = ref false (*announce potential incompleteness of type unification*) clasohm@0: clasohm@0: type binderlist = (string*typ) list; clasohm@0: clasohm@0: type dpair = binderlist * term * term; clasohm@0: wenzelm@19864: fun body_type(Envir.Envir{iTs,...}) = clasohm@0: let fun bT(Type("fun",[_,T])) = bT T berghofe@15797: | bT(T as TVar ixnS) = (case Type.lookup (iTs, ixnS) of wenzelm@19864: NONE => T | SOME(T') => bT T') clasohm@0: | bT T = T clasohm@0: in bT end; clasohm@0: wenzelm@19864: fun binder_types(Envir.Envir{iTs,...}) = clasohm@0: let fun bTs(Type("fun",[T,U])) = T :: bTs U berghofe@15797: | bTs(T as TVar ixnS) = (case Type.lookup (iTs, ixnS) of wenzelm@19864: 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: berghofe@12231: fun fastype env (Ts, t) = Envir.fastype env (map snd Ts) t; 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) = wenzelm@19864: Abs("", T, etif(U, incr_boundvars 1 t $ Bound 0)) wenzelm@19864: | etif (TVar ixnS, t) = wenzelm@19864: (case Type.lookup (iTs, ixnS) of wenzelm@19864: NONE => t | SOME(T) => etif(T,t)) wenzelm@19864: | etif (_,t) = t; clasohm@0: fun eta_nm (rbinder, Abs(a,T,body)) = wenzelm@19864: Abs(a, T, eta_nm ((a,T)::rbinder, body)) wenzelm@19864: | eta_nm (rbinder, t) = etif(fastype env (rbinder,t), t) clasohm@0: in eta_nm end; clasohm@0: clasohm@0: clasohm@0: (*OCCURS CHECK wenzelm@19864: 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. berghofe@15797: This version searches for nonrigid occurrence, returns true if found. berghofe@15797: Since terms may contain variables with same name and different types, berghofe@15797: the occurs check must ignore the types of variables. This avoids berghofe@15797: that ?x::?'a is unified with f(?x::T), which may lead to a cyclic berghofe@15797: substitution when ?'a is instantiated with T later. *) clasohm@0: fun occurs_terms (seen: (indexname list) ref, wenzelm@19864: env: Envir.env, v: indexname, ts: term list): bool = clasohm@0: let fun occurs [] = false wenzelm@19864: | occurs (t::ts) = occur t orelse occurs ts clasohm@0: and occur (Const _) = false wenzelm@19864: | occur (Bound _) = false wenzelm@19864: | occur (Free _) = false wenzelm@19864: | occur (Var (w, T)) = wenzelm@20083: if member (op =) (!seen) w then false wenzelm@19864: else if eq_ix(v,w) then true wenzelm@19864: (*no need to lookup: v has no assignment*) wenzelm@19864: else (seen := w:: !seen; wenzelm@19864: case Envir.lookup (env, (w, T)) of wenzelm@19864: NONE => false wenzelm@19864: | SOME t => occur t) wenzelm@19864: | occur (Abs(_,_,body)) = occur body wenzelm@19864: | 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) wenzelm@19864: | Var vT => (case Envir.lookup (env, vT) of wenzelm@19864: 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. wenzelm@19864: 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 wenzelm@19864: for arg1,...,argn. wenzelm@19864: 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 wenzelm@19864: 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: *) wenzelm@19864: fun rigid_occurs_term (seen: (indexname list)ref, env, v: indexname, t) = wenzelm@19864: let fun nonrigid t = if occurs_terms(seen,env,v,[t]) then Nonrigid wenzelm@19864: else NoOcc clasohm@0: fun occurs [] = NoOcc wenzelm@19864: | 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 wenzelm@19864: | occur (Bound _) = NoOcc wenzelm@19864: | occur (Free _) = NoOcc wenzelm@19864: | occur (Var (w, T)) = wenzelm@20083: if member (op =) (!seen) w then NoOcc wenzelm@19864: else if eq_ix(v,w) then Rigid wenzelm@19864: else (seen := w:: !seen; wenzelm@19864: case Envir.lookup (env, (w, T)) of wenzelm@19864: NONE => NoOcc wenzelm@19864: | SOME t => occur t) wenzelm@19864: | occur (Abs(_,_,body)) = occur body wenzelm@19864: | occur (t as f$_) = (*switch to nonrigid search?*) wenzelm@19864: (case head_of_in (env,f) of wenzelm@19864: Var (w,_) => (*w is not assigned*) wenzelm@19864: if eq_ix(v,w) then Rigid wenzelm@19864: else nonrigid t wenzelm@19864: | Abs(_,_,body) => nonrigid t (*not in normal form*) wenzelm@19864: | _ => occomb t) clasohm@0: in occur t end; clasohm@0: clasohm@0: wenzelm@19864: exception CANTUNIFY; (*Signals non-unifiability. Does not signal errors!*) wenzelm@19864: exception ASSIGN; (*Raised if not an assignment*) clasohm@0: clasohm@0: wenzelm@16664: fun unify_types thy (T,U, env as Envir.Envir{asol,iTs,maxidx}) = nipkow@1435: if T=U then env wenzelm@16934: else let val (iTs',maxidx') = Sign.typ_unify thy (U, T) (iTs, maxidx) nipkow@1435: in Envir.Envir{asol=asol,maxidx=maxidx',iTs=iTs'} end paulson@1505: handle Type.TUNIFY => raise CANTUNIFY; clasohm@0: wenzelm@16664: fun test_unify_types thy (args as (T,U,_)) = wenzelm@16664: let val str_of = Sign.string_of_typ thy; wenzelm@16664: fun warn() = tracing ("Potential loss of completeness: " ^ str_of U ^ " = " ^ str_of T); wenzelm@16664: val env' = unify_types thy 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) = wenzelm@19864: if n=i then get_eta_var (rbinder, n+1, f) wenzelm@19864: else raise ASSIGN clasohm@0: | get_eta_var _ = raise ASSIGN; 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. *) wenzelm@16664: fun assignment thy (env, rbinder, t, u) = berghofe@15797: let val vT as (v,T) = get_eta_var (rbinder, 0, t) berghofe@15797: in case rigid_occurs_term (ref [], env, v, u) of wenzelm@19864: NoOcc => let val env = unify_types thy (body_type env T, wenzelm@19864: fastype env (rbinder,u),env) wenzelm@19864: in Envir.update ((vT, Logic.rlist_abs (rbinder, u)), env) end wenzelm@19864: | Nonrigid => raise ASSIGN wenzelm@19864: | 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. wenzelm@19864: Uses variable a (unless the null string) to preserve user's naming.*) wenzelm@16664: fun new_dpair thy (rbinder, Abs(a,T,body1), Abs(b,U,body2), env) = wenzelm@19864: let val env' = unify_types thy (T,U,env) wenzelm@19864: val c = if a="" then b else a wenzelm@19864: in new_dpair thy ((c,T) :: rbinder, body1, body2, env') end wenzelm@16664: | new_dpair _ (_, Abs _, _, _) = raise TERM ("new_dpair", []) wenzelm@16664: | new_dpair _ (_, _, Abs _, _) = raise TERM ("new_dpair", []) wenzelm@16664: | new_dpair _ (rbinder, t1, t2, env) = ((rbinder, t1, t2), env); clasohm@0: clasohm@0: wenzelm@16664: fun head_norm_dpair thy (env, (rbinder,t,u)) : dpair * Envir.env = wenzelm@16664: new_dpair thy (rbinder, wenzelm@19864: eta_norm env (rbinder, Envir.head_norm env t), wenzelm@19864: eta_norm env (rbinder, Envir.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: *) wenzelm@16664: fun SIMPL0 thy (dp0, (env,flexflex,flexrigid)) wenzelm@19864: : Envir.env * dpair list * dpair list = wenzelm@16664: let val (dp as (rbinder,t,u), env) = head_norm_dpair thy (env,dp0); wenzelm@19864: fun SIMRANDS(f$t, g$u, env) = wenzelm@19864: SIMPL0 thy ((rbinder,t,u), SIMRANDS(f,g,env)) wenzelm@19864: | SIMRANDS (t as _$_, _, _) = wenzelm@19864: raise TERM ("SIMPL: operands mismatch", [t,u]) wenzelm@19864: | SIMRANDS (t, u as _$_, _) = wenzelm@19864: raise TERM ("SIMPL: operands mismatch", [t,u]) wenzelm@19864: | SIMRANDS(_,_,env) = (env,flexflex,flexrigid); clasohm@0: in case (head_of t, head_of u) of clasohm@0: (Var(_,T), Var(_,U)) => wenzelm@19864: let val T' = body_type env T and U' = body_type env U; wenzelm@19864: val env = unify_types thy (T',U',env) wenzelm@19864: in (env, dp::flexflex, flexrigid) end clasohm@0: | (Var _, _) => wenzelm@19864: ((assignment thy (env,rbinder,t,u), flexflex, flexrigid) wenzelm@19864: handle ASSIGN => (env, flexflex, dp::flexrigid)) clasohm@0: | (_, Var _) => wenzelm@19864: ((assignment thy (env,rbinder,u,t), flexflex, flexrigid) wenzelm@19864: handle ASSIGN => (env, flexflex, (rbinder,u,t)::flexrigid)) clasohm@0: | (Const(a,T), Const(b,U)) => wenzelm@19864: if a=b then SIMRANDS(t,u, unify_types thy (T,U,env)) wenzelm@19864: else raise CANTUNIFY clasohm@0: | (Bound i, Bound j) => wenzelm@19864: if i=j then SIMRANDS(t,u,env) else raise CANTUNIFY clasohm@0: | (Free(a,T), Free(b,U)) => wenzelm@19864: if a=b then SIMRANDS(t,u, unify_types thy (T,U,env)) wenzelm@19864: 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) berghofe@15797: | changed (env, Var v) = skalberg@15531: (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*) wenzelm@16664: fun SIMPL thy (env,dpairs) : Envir.env * dpair list * dpair list = clasohm@0: let val all as (env',flexflex,flexrigid) = wenzelm@19864: foldr (SIMPL0 thy) (env,[],[]) dpairs; wenzelm@19864: val dps = flexrigid@flexflex clasohm@0: in if exists (fn ((_,t,u)) => changed(env',t) orelse changed(env',u)) dps wenzelm@16664: then SIMPL thy (env',dps) else all clasohm@0: end; clasohm@0: clasohm@0: wenzelm@19864: (*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. wenzelm@19864: 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; wenzelm@19864: val (env', vars) = Envir.genvars name (env, map funtype Ts) wenzelm@18945: in (env', map (fn var=> Logic.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. wenzelm@19864: The order for trying projections is crucial in ?b'(?a) clasohm@0: NB "vname" is only used in the call to make_args!! *) wenzelm@19864: fun matchcopy thy vname = let fun mc(rbinder, targs, u, ed as (env,dpairs)) wenzelm@19864: : (term * (Envir.env * dpair list))Seq.seq = clasohm@0: let (*Produce copies of uarg and cons them in front of uargs*) clasohm@0: fun copycons uarg (uargs, (env, dpairs)) = wenzelm@19864: Seq.map(fn (uarg', ed') => (uarg'::uargs, ed')) wenzelm@19864: (mc (rbinder, targs,eta_norm env (rbinder, Envir.head_norm env uarg), wenzelm@19864: (env, dpairs))); wenzelm@19864: (*Produce sequence of all possible ways of copying the arg list*) wenzelm@19473: fun copyargs [] = Seq.cons ([],ed) Seq.empty wenzelm@17344: | copyargs (uarg::uargs) = Seq.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; wenzelm@19864: fun projenv (head, (Us,bary), targ, tail) = wenzelm@19864: let val env = if !trace_types then test_unify_types thy (base,bary,env) wenzelm@19864: else unify_types thy (base,bary,env) wenzelm@19864: in Seq.make (fn () => wenzelm@19864: let val (env',args) = make_args vname (Ts,env,Us); wenzelm@19864: (*higher-order projection: plug in targs for bound vars*) wenzelm@19864: fun plugin arg = list_comb(head_of arg, targs); wenzelm@19864: val dp = (rbinder, list_comb(targ, map plugin args), u); wenzelm@19864: val (env2,frigid,fflex) = SIMPL thy (env', dp::dpairs) wenzelm@19864: (*may raise exception CANTUNIFY*) wenzelm@19864: in SOME ((list_comb(head,args), (env2, frigid@fflex)), wenzelm@19864: tail) wenzelm@19864: end handle CANTUNIFY => Seq.pull tail) wenzelm@19864: end handle CANTUNIFY => tail; clasohm@0: (*make a list of projections*) clasohm@0: fun make_projs (T::Ts, targ::targs) = wenzelm@19864: (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) = wenzelm@19864: (projenv(bvar, strip_type env T, targ, matchfun projs)) clasohm@0: | matchfun [] = (*imitation last of all*) wenzelm@19864: (case uhead of wenzelm@19864: Const _ => Seq.map joinargs (copyargs uargs) wenzelm@19864: | Free _ => Seq.map joinargs (copyargs uargs) wenzelm@19864: | _ => Seq.empty) (*if Var, would be a loop!*) clasohm@0: in case uhead of wenzelm@19864: Abs(a, T, body) => wenzelm@19864: Seq.map(fn (body', ed') => (Abs (a,T,body'), ed')) wenzelm@19864: (mc ((a,T)::rbinder, wenzelm@19864: (map (incr_boundvars 1) targs) @ [Bound 0], body, ed)) wenzelm@19864: | Var (w,uary) => wenzelm@19864: (*a flex-flex dpair: make variable for t*) wenzelm@19864: let val (env', newhd) = Envir.genvar (#1 w) (env, Ts---> base) wenzelm@19864: val tabs = Logic.combound(newhd, 0, length Ts) wenzelm@19864: val tsub = list_comb(newhd,targs) wenzelm@19864: in Seq.single (tabs, (env', (rbinder,tsub,u):: dpairs)) wenzelm@19864: 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*) wenzelm@16664: fun MATCH thy (env, (rbinder,t,u), dpairs) wenzelm@19864: : (Envir.env * dpair list)Seq.seq = berghofe@15797: let val (Var (vT as (v, T)), targs) = strip_comb t; clasohm@0: val Ts = binder_types env T; clasohm@0: fun new_dset (u', (env',dpairs')) = wenzelm@19864: (*if v was updated to s, must unify s with u' *) wenzelm@19864: case Envir.lookup (env', vT) of wenzelm@19864: NONE => (Envir.update ((vT, types_abs(Ts, u')), env'), dpairs') wenzelm@19864: | SOME s => (env', ([], s, types_abs(Ts, u'))::dpairs') wenzelm@4270: in Seq.map new_dset wenzelm@16664: (matchcopy thy (#1 v) (rbinder, targs, u, (env,dpairs))) clasohm@0: end; clasohm@0: clasohm@0: clasohm@0: clasohm@0: (**** Flex-flex processing ****) clasohm@0: wenzelm@19864: (*At end of unification, do flex-flex assignments like ?a -> ?f(?b) clasohm@0: Attempts to update t with u, raising ASSIGN if impossible*) wenzelm@19864: fun ff_assign thy (env, rbinder, t, u) : Envir.env = berghofe@15797: let val vT as (v,T) = get_eta_var(rbinder,0,t) berghofe@15797: in if occurs_terms (ref [], env, v, [u]) then raise ASSIGN wenzelm@16664: else let val env = unify_types thy (body_type env T, wenzelm@19864: fastype env (rbinder,u), wenzelm@19864: env) wenzelm@19864: in Envir.vupdate ((vT, Logic.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*) wenzelm@19864: fun rigid_bound (lev, banned) t = wenzelm@19864: let val (head,args) = strip_comb t wenzelm@19864: in lcp@651: case head of wenzelm@19864: Bound i => (i-lev) mem_int banned orelse wenzelm@19864: exists (rigid_bound (lev, banned)) args wenzelm@19864: | Var _ => false (*no rigid occurrences here!*) wenzelm@19864: | Abs (_,_,u) => wenzelm@19864: rigid_bound(lev+1, banned) u orelse wenzelm@19864: exists (rigid_bound (lev, banned)) args wenzelm@19864: | _ => 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 = wenzelm@19864: let fun change lev (Bound i) = wenzelm@19864: if i j < i-lev) banned)) wenzelm@19864: | change lev (Abs (a,T,t)) = Abs (a, T, change(lev+1) t) wenzelm@19864: | change lev (t$u) = change lev t $ change lev u wenzelm@19864: | 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 = wenzelm@19864: 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) wenzelm@19864: val body = list_comb(v', map (Bound o #j) args) wenzelm@19864: val env2 = Envir.vupdate ((((v, T), types_abs(Ts, body)), env')) wenzelm@19864: (*the vupdate affects ts' if they contain v*) wenzelm@19864: in wenzelm@19864: (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 = wenzelm@19864: if t0 aconv u0 then tpairs clasohm@0: else wenzelm@18945: let val t = Logic.rlist_abs(rbinder, t0) and u = Logic.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 *) wenzelm@19864: fun clean_ffpair thy ((rbinder, t, u), (env,tpairs)) = clasohm@0: let val loot = loose_bnos t and loou = loose_bnos u wenzelm@19864: fun add_index (((a,T), j), (bnos, newbinder)) = wenzelm@19864: if j mem_int loot andalso j mem_int loou wenzelm@19864: then (bnos, (a,T)::newbinder) (*needed by both: keep*) wenzelm@19864: else (j::bnos, newbinder); (*remove*) clasohm@0: val indices = 0 upto (length rbinder - 1); skalberg@15574: 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) wenzelm@16664: in (ff_assign thy (env'', rbin', t', u'), tpairs) wenzelm@16664: handle ASSIGN => (ff_assign thy (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 wenzelm@19864: 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.*) wenzelm@19864: fun add_ffpair thy ((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...*) wenzelm@19864: if eq_ix(v,w) then (*...occur check would falsely return true!*) wenzelm@19864: if T=U then (env, add_tpair (rbinder, (t,u), tpairs)) wenzelm@19864: else raise TERM ("add_ffpair: Var name confusion", [t,u]) wenzelm@19864: else if xless(v,w) then (*prefer to update the LARGER variable*) wenzelm@19864: clean_ffpair thy ((rbinder, u, t), (env,tpairs)) wenzelm@16664: else clean_ffpair thy ((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.*) wenzelm@16664: fun print_dpairs thy msg (env,dpairs) = clasohm@0: let fun pdp (rbinder,t,u) = wenzelm@16664: let fun termT t = Sign.pretty_term thy wenzelm@18945: (Envir.norm_term env (Logic.rlist_abs(rbinder,t))) clasohm@0: val bsymbs = [termT u, Pretty.str" =?=", Pretty.brk 1, clasohm@0: termT t]; wenzelm@12262: in tracing(Pretty.string_of(Pretty.blk(0,bsymbs))) end; skalberg@15570: in tracing msg; List.app pdp dpairs end; clasohm@0: clasohm@0: clasohm@0: (*Unify the dpairs in the environment. wenzelm@19864: Returns flex-flex disagreement pairs NOT IN normal form. clasohm@0: SIMPL may raise exception CANTUNIFY. *) wenzelm@19864: fun hounifiers (thy,env, tus : (term*term)list) wenzelm@4270: : (Envir.env * (term*term)list)Seq.seq = clasohm@0: let fun add_unify tdepth ((env,dpairs), reseq) = wenzelm@19864: Seq.make (fn()=> wenzelm@19864: let val (env',flexflex,flexrigid) = wenzelm@19864: (if tdepth> !trace_bound andalso !trace_simp wenzelm@19864: then print_dpairs thy "Enter SIMPL" (env,dpairs) else (); wenzelm@19864: SIMPL thy (env,dpairs)) wenzelm@19864: in case flexrigid of wenzelm@19864: [] => SOME (foldr (add_ffpair thy) (env',[]) flexflex, reseq) wenzelm@19864: | dp::frigid' => wenzelm@19864: if tdepth > !search_bound then wenzelm@19864: (warning "Unification bound exceeded"; Seq.pull reseq) wenzelm@19864: else wenzelm@19864: (if tdepth > !trace_bound then wenzelm@19864: print_dpairs thy "Enter MATCH" (env',flexrigid@flexflex) wenzelm@19864: else (); wenzelm@19864: Seq.pull (Seq.it_right (add_unify (tdepth+1)) wenzelm@19864: (MATCH thy (env',dp, frigid'@flexflex), reseq))) wenzelm@19864: end wenzelm@19864: handle CANTUNIFY => wenzelm@19864: (if tdepth > !trace_bound then tracing"Failure node" else (); wenzelm@19864: Seq.pull reseq)); clasohm@0: val dps = map (fn(t,u)=> ([],t,u)) tus wenzelm@16425: in add_unify 1 ((env, dps), Seq.empty) end; clasohm@0: wenzelm@18184: fun unifiers (params as (thy, env, tus)) = wenzelm@19473: Seq.cons (fold (Pattern.unify thy) tus env, []) Seq.empty wenzelm@16425: handle Pattern.Unif => Seq.empty wenzelm@16425: | 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 wenzelm@19864: Unfortunately, unifies ?f(t,u) with ?g(t,u) by ?f, ?g -> %(x,y)?a, wenzelm@19864: 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 = berghofe@15797: let val vT as (v,T) = var_head_of (env,t) berghofe@15797: and wU as (w,U) = var_head_of (env,u); clasohm@0: val (env', var) = Envir.genvar (#1v) (env, body_type env T) berghofe@15797: val env'' = Envir.vupdate ((wU, type_abs (env', U, var)), env') berghofe@15797: in if vT = wU then env'' (*the other update would be identical*) berghofe@15797: else Envir.vupdate ((vT, 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 = skalberg@15574: foldr smash_flexflex1 env tpairs; clasohm@0: clasohm@0: (*Returns unifiers with no remaining disagreement pairs*) wenzelm@19864: fun smash_unifiers thy tus env = wenzelm@16425: Seq.map smash_flexflex (unifiers(thy,env,tus)); clasohm@0: wenzelm@19864: wenzelm@19864: (*Pattern matching*) wenzelm@20020: fun first_order_matchers thy pairs (Envir.Envir {asol = tenv, iTs = tyenv, maxidx}) = wenzelm@20020: let val (tyenv', tenv') = fold (Pattern.first_order_match thy) pairs (tyenv, tenv) wenzelm@19864: in Seq.single (Envir.Envir {asol = tenv', iTs = tyenv', maxidx = maxidx}) end wenzelm@19864: handle Pattern.MATCH => Seq.empty; wenzelm@19864: wenzelm@19864: (*General matching -- keeps variables disjoint*) wenzelm@19864: fun matchers _ [] = Seq.single (Envir.empty ~1) wenzelm@19864: | matchers thy pairs = wenzelm@19864: let wenzelm@19864: val maxidx = fold (Term.maxidx_term o #2) pairs ~1; wenzelm@19864: val offset = maxidx + 1; wenzelm@19864: val pairs' = map (apfst (Logic.incr_indexes ([], offset))) pairs; wenzelm@19864: val maxidx' = fold (fn (t, u) => Term.maxidx_term t #> Term.maxidx_term u) pairs' ~1; wenzelm@19864: wenzelm@19864: val pat_tvars = fold (Term.add_tvars o #1) pairs' []; wenzelm@19864: val pat_vars = fold (Term.add_vars o #1) pairs' []; wenzelm@19864: wenzelm@19864: val decr_indexesT = wenzelm@19864: Term.map_atyps (fn T as TVar ((x, i), S) => wenzelm@19864: if i > maxidx then TVar ((x, i - offset), S) else T | T => T); wenzelm@19864: val decr_indexes = wenzelm@19864: Term.map_term_types decr_indexesT #> wenzelm@19864: Term.map_aterms (fn t as Var ((x, i), T) => wenzelm@19864: if i > maxidx then Var ((x, i - offset), T) else t | t => t); wenzelm@19864: wenzelm@19864: fun norm_tvar (Envir.Envir {iTs = tyenv, ...}) ((x, i), S) = wenzelm@19864: ((x, i - offset), (S, decr_indexesT (Envir.norm_type tyenv (TVar ((x, i), S))))); wenzelm@19864: fun norm_var (env as Envir.Envir {iTs = tyenv, ...}) ((x, i), T) = wenzelm@19864: let wenzelm@19864: val T' = Envir.norm_type tyenv T; wenzelm@19864: val t' = Envir.norm_term env (Var ((x, i), T')); wenzelm@19864: in ((x, i - offset), (decr_indexesT T', decr_indexes t')) end; wenzelm@19864: wenzelm@19864: fun result env = wenzelm@19876: if Envir.above env maxidx then (* FIXME proper handling of generated vars!? *) wenzelm@19864: SOME (Envir.Envir {maxidx = maxidx, wenzelm@19866: iTs = Vartab.make (map (norm_tvar env) pat_tvars), wenzelm@19866: asol = Vartab.make (map (norm_var env) pat_vars)}) wenzelm@19866: else NONE; wenzelm@19864: wenzelm@19864: val empty = Envir.empty maxidx'; wenzelm@19864: in wenzelm@19876: Seq.append wenzelm@19920: (Seq.map_filter result (smash_unifiers thy pairs' empty)) wenzelm@20020: (first_order_matchers thy pairs empty) wenzelm@19864: end; wenzelm@19864: wenzelm@19864: fun matches_list thy ps os = wenzelm@19864: length ps = length os andalso is_some (Seq.pull (matchers thy (ps ~~ os))); wenzelm@19864: clasohm@0: end;