# HG changeset patch # User wenzelm # Date 1150139944 -7200 # Node ID 227a01b8db8090efbfb584b37c07660848284c38 # Parent 3a4ca87efdc550963c920925967a3016aea77361 added matchers, matches_list; tuned interfaces; diff -r 3a4ca87efdc5 -r 227a01b8db80 src/Pure/unify.ML --- a/src/Pure/unify.ML Mon Jun 12 21:19:03 2006 +0200 +++ b/src/Pure/unify.ML Mon Jun 12 21:19:04 2006 +0200 @@ -12,43 +12,43 @@ signature UNIFY = sig - (*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 smash_unifiers: theory * Envir.env * (term * term) list -> Envir.env Seq.seq val unifiers: theory * Envir.env * ((term * term) list) -> (Envir.env * (term * term) list) Seq.seq + val smash_unifiers: theory -> (term * term) list -> Envir.env -> Envir.env Seq.seq + val matchers: theory -> (term * term) list -> Envir.env Seq.seq + val matches_list: theory -> term list -> term list -> bool end -structure Unify : UNIFY = +structure Unify : UNIFY = struct (*Unification options*) -val trace_bound = ref 25 (*tracing starts above this depth, 0 for full*) -and search_bound = ref 30 (*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 trace_bound = ref 25 (*tracing starts above this depth, 0 for full*) +and search_bound = ref 30 (*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*) type binderlist = (string*typ) list; type dpair = binderlist * term * term; -fun body_type(Envir.Envir{iTs,...}) = +fun body_type(Envir.Envir{iTs,...}) = let fun bT(Type("fun",[_,T])) = bT T | bT(T as TVar ixnS) = (case Type.lookup (iTs, ixnS) of - NONE => T | SOME(T') => bT T') + NONE => T | SOME(T') => bT T') | bT T = T in bT end; -fun binder_types(Envir.Envir{iTs,...}) = +fun binder_types(Envir.Envir{iTs,...}) = let fun bTs(Type("fun",[T,U])) = T :: bTs U | bTs(T as TVar ixnS) = (case Type.lookup (iTs, ixnS) of - NONE => [] | SOME(T') => bTs T') + NONE => [] | SOME(T') => bTs T') | bTs _ = [] in bTs end; @@ -60,19 +60,19 @@ (*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 ixnS, t) = - (case Type.lookup (iTs, ixnS) of - NONE => t | SOME(T) => etif(T,t)) - | etif (_,t) = t; + Abs("", T, etif(U, incr_boundvars 1 t $ Bound 0)) + | etif (TVar ixnS, t) = + (case Type.lookup (iTs, ixnS) 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) + 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? + 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. @@ -81,22 +81,22 @@ that ?x::?'a is unified with f(?x::T), which may lead to a cyclic substitution when ?'a is instantiated with T later. *) fun occurs_terms (seen: (indexname list) ref, - env: Envir.env, v: indexname, ts: term list): bool = + env: Envir.env, v: indexname, ts: term list): bool = let fun occurs [] = false - | occurs (t::ts) = occur t orelse occurs ts + | occurs (t::ts) = occur t orelse occurs ts and occur (Const _) = false - | occur (Bound _) = false - | occur (Free _) = false - | occur (Var (w, T)) = - if mem_ix (w, !seen) then false - else if eq_ix(v,w) then true - (*no need to lookup: v has no assignment*) - else (seen := w:: !seen; - case Envir.lookup (env, (w, T)) of - NONE => false - | SOME t => occur t) - | occur (Abs(_,_,body)) = occur body - | occur (f$t) = occur t orelse occur f + | occur (Bound _) = false + | occur (Free _) = false + | occur (Var (w, T)) = + if mem_ix (w, !seen) then false + else if eq_ix(v,w) then true + (*no need to lookup: v has no assignment*) + else (seen := w:: !seen; + case Envir.lookup (env, (w, T)) of + NONE => false + | SOME t => occur t) + | occur (Abs(_,_,body)) = occur body + | occur (f$t) = occur t orelse occur f in occurs ts end; @@ -104,8 +104,8 @@ (* 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 vT => (case Envir.lookup (env, vT) of - SOME u => head_of_in(env,u) | NONE => t) + | Var vT => (case Envir.lookup (env, vT) of + SOME u => head_of_in(env,u) | NONE => t) | _ => t; @@ -121,24 +121,24 @@ 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. +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 +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. + 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 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) = + | occurs (t::ts) = (case occur t of Rigid => Rigid | oc => (case occurs ts of NoOcc => oc | oc2 => oc2)) @@ -148,28 +148,28 @@ | 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, T)) = - if mem_ix (w, !seen) then NoOcc - else if eq_ix(v,w) then Rigid - else (seen := w:: !seen; - case Envir.lookup (env, (w, T)) 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 eq_ix(v,w) then Rigid - else nonrigid t - | Abs(_,_,body) => nonrigid t (*not in normal form*) - | _ => occomb t) + | occur (Bound _) = NoOcc + | occur (Free _) = NoOcc + | occur (Var (w, T)) = + if mem_ix (w, !seen) then NoOcc + else if eq_ix(v,w) then Rigid + else (seen := w:: !seen; + case Envir.lookup (env, (w, T)) 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 eq_ix(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*) +exception CANTUNIFY; (*Signals non-unifiability. Does not signal errors!*) +exception ASSIGN; (*Raised if not an assignment*) fun unify_types thy (T,U, env as Envir.Envir{asol,iTs,maxidx}) = @@ -191,8 +191,8 @@ 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 + if n=i then get_eta_var (rbinder, n+1, f) + else raise ASSIGN | get_eta_var _ = raise ASSIGN; @@ -202,11 +202,11 @@ fun assignment thy (env, rbinder, t, u) = let val vT as (v,T) = get_eta_var (rbinder, 0, t) in case rigid_occurs_term (ref [], env, v, u) of - NoOcc => let val env = unify_types thy (body_type env T, - fastype env (rbinder,u),env) - in Envir.update ((vT, Logic.rlist_abs (rbinder, u)), env) end - | Nonrigid => raise ASSIGN - | Rigid => raise CANTUNIFY + NoOcc => let val env = unify_types thy (body_type env T, + fastype env (rbinder,u),env) + in Envir.update ((vT, Logic.rlist_abs (rbinder, u)), env) end + | Nonrigid => raise ASSIGN + | Rigid => raise CANTUNIFY end; @@ -214,11 +214,11 @@ 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.*) + Uses variable a (unless the null string) to preserve user's naming.*) fun new_dpair thy (rbinder, Abs(a,T,body1), Abs(b,U,body2), env) = - let val env' = unify_types thy (T,U,env) - val c = if a="" then b else a - in new_dpair thy ((c,T) :: rbinder, body1, body2, env') end + let val env' = unify_types thy (T,U,env) + val c = if a="" then b else a + in new_dpair thy ((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); @@ -226,8 +226,8 @@ fun head_norm_dpair thy (env, (rbinder,t,u)) : dpair * Envir.env = new_dpair thy (rbinder, - eta_norm env (rbinder, Envir.head_norm env t), - eta_norm env (rbinder, Envir.head_norm env u), env); + eta_norm env (rbinder, Envir.head_norm env t), + eta_norm env (rbinder, Envir.head_norm env u), env); @@ -238,34 +238,34 @@ do so caused numerous problems with no compensating advantage. *) fun SIMPL0 thy (dp0, (env,flexflex,flexrigid)) - : Envir.env * dpair list * dpair list = + : Envir.env * dpair list * dpair list = let val (dp as (rbinder,t,u), env) = head_norm_dpair thy (env,dp0); - fun SIMRANDS(f$t, g$u, env) = - SIMPL0 thy ((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); + fun SIMRANDS(f$t, g$u, env) = + SIMPL0 thy ((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 thy (T',U',env) - in (env, dp::flexflex, flexrigid) end + let val T' = body_type env T and U' = body_type env U; + val env = unify_types thy (T',U',env) + in (env, dp::flexflex, flexrigid) end | (Var _, _) => - ((assignment thy (env,rbinder,t,u), flexflex, flexrigid) - handle ASSIGN => (env, flexflex, dp::flexrigid)) + ((assignment thy (env,rbinder,t,u), flexflex, flexrigid) + handle ASSIGN => (env, flexflex, dp::flexrigid)) | (_, Var _) => - ((assignment thy (env,rbinder,u,t), flexflex, flexrigid) - handle ASSIGN => (env, flexflex, (rbinder,u,t)::flexrigid)) + ((assignment thy (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 thy (T,U,env)) - else raise CANTUNIFY + if a=b then SIMRANDS(t,u, unify_types thy (T,U,env)) + else raise CANTUNIFY | (Bound i, Bound j) => - if i=j then SIMRANDS(t,u,env) else raise CANTUNIFY + 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 thy (T,U,env)) - else raise CANTUNIFY + if a=b then SIMRANDS(t,u, unify_types thy (T,U,env)) + else raise CANTUNIFY | _ => raise CANTUNIFY end; @@ -281,22 +281,22 @@ Clever would be to re-do just the affected dpairs*) fun SIMPL thy (env,dpairs) : Envir.env * dpair list * dpair list = let val all as (env',flexflex,flexrigid) = - foldr (SIMPL0 thy) (env,[],[]) dpairs; - val dps = flexrigid@flexflex + foldr (SIMPL0 thy) (env,[],[]) dpairs; + val dps = flexrigid@flexflex in if exists (fn ((_,t,u)) => changed(env',t) orelse changed(env',u)) dps then SIMPL thy (env',dps) else all end; -(*Makes the terms E1,...,Em, where Ts = [T...Tm]. +(*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. + 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) + val (env', vars) = Envir.genvars name (env, map funtype Ts) in (env', map (fn var=> Logic.combound(var, 0, length binder)) vars) end; @@ -315,16 +315,16 @@ 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) + The order for trying projections is crucial in ?b'(?a) NB "vname" is only used in the call to make_args!! *) -fun matchcopy thy vname = let fun mc(rbinder, targs, u, ed as (env,dpairs)) - : (term * (Envir.env * dpair list))Seq.seq = +fun matchcopy thy vname = let fun mc(rbinder, targs, u, ed as (env,dpairs)) + : (term * (Envir.env * dpair list))Seq.seq = let (*Produce copies of uarg and cons them in front of uargs*) fun copycons uarg (uargs, (env, dpairs)) = - Seq.map(fn (uarg', ed') => (uarg'::uargs, ed')) - (mc (rbinder, targs,eta_norm env (rbinder, Envir.head_norm env uarg), - (env, dpairs))); - (*Produce sequence of all possible ways of copying the arg list*) + Seq.map(fn (uarg', ed') => (uarg'::uargs, ed')) + (mc (rbinder, targs,eta_norm env (rbinder, Envir.head_norm env uarg), + (env, dpairs))); + (*Produce sequence of all possible ways of copying the arg list*) fun copyargs [] = Seq.cons ([],ed) Seq.empty | copyargs (uarg::uargs) = Seq.maps (copycons uarg) (copyargs uargs); val (uhead,uargs) = strip_comb u; @@ -332,45 +332,45 @@ 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 thy (base,bary,env) - else unify_types thy (base,bary,env) - in Seq.make (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 thy (env', dp::dpairs) - (*may raise exception CANTUNIFY*) - in SOME ((list_comb(head,args), (env2, frigid@fflex)), - tail) - end handle CANTUNIFY => Seq.pull tail) - end handle CANTUNIFY => tail; + fun projenv (head, (Us,bary), targ, tail) = + let val env = if !trace_types then test_unify_types thy (base,bary,env) + else unify_types thy (base,bary,env) + in Seq.make (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 thy (env', dp::dpairs) + (*may raise exception CANTUNIFY*) + in SOME ((list_comb(head,args), (env2, frigid@fflex)), + tail) + end handle CANTUNIFY => Seq.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) + (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)) + (projenv(bvar, strip_type env T, targ, matchfun projs)) | matchfun [] = (*imitation last of all*) - (case uhead of - Const _ => Seq.map joinargs (copyargs uargs) - | Free _ => Seq.map joinargs (copyargs uargs) - | _ => Seq.empty) (*if Var, would be a loop!*) + (case uhead of + Const _ => Seq.map joinargs (copyargs uargs) + | Free _ => Seq.map joinargs (copyargs uargs) + | _ => Seq.empty) (*if Var, would be a loop!*) in case uhead of - Abs(a, T, body) => - Seq.map(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 = Logic.combound(newhd, 0, length Ts) - val tsub = list_comb(newhd,targs) - in Seq.single (tabs, (env', (rbinder,tsub,u):: dpairs)) - end + Abs(a, T, body) => + Seq.map(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 = Logic.combound(newhd, 0, length Ts) + val tsub = list_comb(newhd,targs) + in Seq.single (tabs, (env', (rbinder,tsub,u):: dpairs)) + end | _ => matchfun(rev(make_projs(Ts, targs))) end in mc end; @@ -378,14 +378,14 @@ (*Call matchcopy to produce assignments to the variable in the dpair*) fun MATCH thy (env, (rbinder,t,u), dpairs) - : (Envir.env * dpair list)Seq.seq = + : (Envir.env * dpair list)Seq.seq = let val (Var (vT as (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', vT) of - NONE => (Envir.update ((vT, types_abs(Ts, u')), env'), dpairs') - | SOME s => (env', ([], s, types_abs(Ts, u'))::dpairs') + (*if v was updated to s, must unify s with u' *) + case Envir.lookup (env', vT) of + NONE => (Envir.update ((vT, types_abs(Ts, u')), env'), dpairs') + | SOME s => (env', ([], s, types_abs(Ts, u'))::dpairs') in Seq.map new_dset (matchcopy thy (#1 v) (rbinder, targs, u, (env,dpairs))) end; @@ -394,15 +394,15 @@ (**** Flex-flex processing ****) -(*At end of unification, do flex-flex assignments like ?a -> ?f(?b) +(*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 thy (env, rbinder, t, u) : Envir.env = +fun ff_assign thy (env, rbinder, t, u) : Envir.env = let val vT as (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 thy (body_type env T, - fastype env (rbinder,u), - env) - in Envir.vupdate ((vT, Logic.rlist_abs (rbinder, u)), env) end + fastype env (rbinder,u), + env) + in Envir.vupdate ((vT, Logic.rlist_abs (rbinder, u)), env) end end; @@ -423,34 +423,34 @@ (*Check whether the 'banned' bound var indices occur rigidly in t*) -fun rigid_bound (lev, banned) t = - let val (head,args) = strip_comb t - in +fun rigid_bound (lev, banned) t = + let val (head,args) = strip_comb t + in case head of - Bound i => (i-lev) mem_int banned orelse - exists (rigid_bound (lev, banned)) args - | Var _ => false (*no rigid occurrences here!*) - | Abs (_,_,u) => - rigid_bound(lev+1, banned) u orelse - exists (rigid_bound (lev, banned)) args - | _ => exists (rigid_bound (lev, banned)) args + Bound i => (i-lev) mem_int banned orelse + exists (rigid_bound (lev, banned)) args + | Var _ => false (*no rigid occurrences here!*) + | Abs (_,_,u) => + rigid_bound(lev+1, banned) u orelse + exists (rigid_bound (lev, banned)) args + | _ => exists (rigid_bound (lev, banned)) args end; (*Squash down indices at level >=lev to delete the banned from a term.*) fun change_bnos banned = - let fun change lev (Bound i) = - if i j < i-lev) banned)) - | change lev (Abs (a,T,t)) = Abs (a, T, change(lev+1) t) - | change lev (t$u) = change lev t $ change lev u - | change lev t = t + let fun change lev (Bound i) = + if i j < i-lev) banned)) + | change lev (Abs (a,T,t)) = Abs (a, T, change(lev+1) t) + | change lev (t$u) = change lev t $ change lev u + | change lev t = t in change 0 end; (*Change indices, delete the argument if it contains a banned Bound*) fun change_arg banned ({j,t,T}, args) : flarg list = - if rigid_bound (0, banned) t then args (*delete argument!*) + if rigid_bound (0, banned) t then args (*delete argument!*) else {j=j, t= change_bnos banned t, T=T} :: args; @@ -469,19 +469,19 @@ 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 (make_ord arg_less) - (foldr (change_arg banned) [] (flexargs (js,ts,Ts))) - val ts' = map (#t) args + val (Ts,U) = strip_type env T + and js = length ts - 1 downto 0 + val args = sort (make_ord 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, T), types_abs(Ts, body)), env')) - (*the vupdate affects ts' if they contain v*) - in - (env2, Envir.norm_term env2 (list_comb(v',ts'))) + val body = list_comb(v', map (Bound o #j) args) + val env2 = Envir.vupdate ((((v, T), 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; @@ -489,7 +489,7 @@ (*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 + if t0 aconv u0 then tpairs else let val t = Logic.rlist_abs(rbinder, t0) and u = Logic.rlist_abs(rbinder, u0); fun same(t',u') = (t aconv t') andalso (u aconv u') @@ -498,12 +498,12 @@ (*Simplify both terms and check for assignments. Bound vars in the binder are "banned" unless used in both t AND u *) -fun clean_ffpair thy ((rbinder, t, u), (env,tpairs)) = +fun clean_ffpair thy ((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_int loot andalso j mem_int loou - then (bnos, (a,T)::newbinder) (*needed by both: keep*) - else (j::bnos, newbinder); (*remove*) + fun add_index (((a,T), j), (bnos, newbinder)) = + if j mem_int loot andalso j mem_int loou + then (bnos, (a,T)::newbinder) (*needed by both: keep*) + else (j::bnos, newbinder); (*remove*) val indices = 0 upto (length rbinder - 1); val (banned,rbin') = foldr add_index ([],[]) (rbinder~~indices); val (env', t') = clean_term banned (env, t); @@ -517,18 +517,18 @@ (*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 + 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 thy ((rbinder,t0,u0), (env,tpairs)) +fun add_ffpair thy ((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 eq_ix(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 thy ((rbinder, u, t), (env,tpairs)) + if eq_ix(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 thy ((rbinder, u, t), (env,tpairs)) else clean_ffpair thy ((rbinder, t, u), (env,tpairs)) | _ => raise TERM ("add_ffpair: Vars expected", [t,u]) end; @@ -548,31 +548,31 @@ (*Unify the dpairs in the environment. - Returns flex-flex disagreement pairs NOT IN normal form. + Returns flex-flex disagreement pairs NOT IN normal form. SIMPL may raise exception CANTUNIFY. *) -fun hounifiers (thy,env, tus : (term*term)list) +fun hounifiers (thy,env, tus : (term*term)list) : (Envir.env * (term*term)list)Seq.seq = let fun add_unify tdepth ((env,dpairs), reseq) = - Seq.make (fn()=> - let val (env',flexflex,flexrigid) = - (if tdepth> !trace_bound andalso !trace_simp - then print_dpairs thy "Enter SIMPL" (env,dpairs) else (); - SIMPL thy (env,dpairs)) - in case flexrigid of - [] => SOME (foldr (add_ffpair thy) (env',[]) flexflex, reseq) - | dp::frigid' => - if tdepth > !search_bound then - (warning "Unification bound exceeded"; Seq.pull reseq) - else - (if tdepth > !trace_bound then - print_dpairs thy "Enter MATCH" (env',flexrigid@flexflex) - else (); - Seq.pull (Seq.it_right (add_unify (tdepth+1)) - (MATCH thy (env',dp, frigid'@flexflex), reseq))) - end - handle CANTUNIFY => - (if tdepth > !trace_bound then tracing"Failure node" else (); - Seq.pull reseq)); + Seq.make (fn()=> + let val (env',flexflex,flexrigid) = + (if tdepth> !trace_bound andalso !trace_simp + then print_dpairs thy "Enter SIMPL" (env,dpairs) else (); + SIMPL thy (env,dpairs)) + in case flexrigid of + [] => SOME (foldr (add_ffpair thy) (env',[]) flexflex, reseq) + | dp::frigid' => + if tdepth > !search_bound then + (warning "Unification bound exceeded"; Seq.pull reseq) + else + (if tdepth > !trace_bound then + print_dpairs thy "Enter MATCH" (env',flexrigid@flexflex) + else (); + Seq.pull (Seq.it_right (add_unify (tdepth+1)) + (MATCH thy (env',dp, frigid'@flexflex), reseq))) + end + handle CANTUNIFY => + (if tdepth > !trace_bound then tracing"Failure node" else (); + Seq.pull reseq)); val dps = map (fn(t,u)=> ([],t,u)) tus in add_unify 1 ((env, dps), Seq.empty) end; @@ -591,8 +591,8 @@ (*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. + 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. *) @@ -611,7 +611,58 @@ foldr smash_flexflex1 env tpairs; (*Returns unifiers with no remaining disagreement pairs*) -fun smash_unifiers (thy, env, tus) : Envir.env Seq.seq = +fun smash_unifiers thy tus env = Seq.map smash_flexflex (unifiers(thy,env,tus)); + +(*Pattern matching*) +fun pattern_matchers thy pairs (Envir.Envir {asol = tenv, iTs = tyenv, maxidx}) = + let val (tyenv', tenv') = fold (Pattern.match thy) pairs (tyenv, tenv) + in Seq.single (Envir.Envir {asol = tenv', iTs = tyenv', maxidx = maxidx}) end + handle Pattern.MATCH => Seq.empty; + +(*General matching -- keeps variables disjoint*) +fun matchers _ [] = Seq.single (Envir.empty ~1) + | matchers thy pairs = + let + val maxidx = fold (Term.maxidx_term o #2) pairs ~1; + val offset = maxidx + 1; + val pairs' = map (apfst (Logic.incr_indexes ([], offset))) pairs; + val maxidx' = fold (fn (t, u) => Term.maxidx_term t #> Term.maxidx_term u) pairs' ~1; + + val pat_tvars = fold (Term.add_tvars o #1) pairs' []; + val pat_vars = fold (Term.add_vars o #1) pairs' []; + + val decr_indexesT = + Term.map_atyps (fn T as TVar ((x, i), S) => + if i > maxidx then TVar ((x, i - offset), S) else T | T => T); + val decr_indexes = + Term.map_term_types decr_indexesT #> + Term.map_aterms (fn t as Var ((x, i), T) => + if i > maxidx then Var ((x, i - offset), T) else t | t => t); + + fun norm_tvar (Envir.Envir {iTs = tyenv, ...}) ((x, i), S) = + ((x, i - offset), (S, decr_indexesT (Envir.norm_type tyenv (TVar ((x, i), S))))); + fun norm_var (env as Envir.Envir {iTs = tyenv, ...}) ((x, i), T) = + let + val T' = Envir.norm_type tyenv T; + val t' = Envir.norm_term env (Var ((x, i), T')); + in ((x, i - offset), (decr_indexesT T', decr_indexes t')) end; + + fun result env = + (warning "FIXME"; if Envir.above env maxidx then + SOME (Envir.Envir {maxidx = maxidx, + iTs = Vartab.make (map (PolyML.print o (norm_tvar env)) pat_tvars), + asol = Vartab.make (map (PolyML.print o (norm_var env)) pat_vars)}) + else NONE); + + val empty = Envir.empty maxidx'; + in + Seq.append (pattern_matchers thy pairs empty) + (Seq.map_filter result (smash_unifiers thy pairs' empty)) + end; + +fun matches_list thy ps os = + length ps = length os andalso is_some (Seq.pull (matchers thy (ps ~~ os))); + end;