--- 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<lev then Bound i
- else if (i-lev) mem_int banned
- then raise CHANGE_FAIL (**flexible occurrence: give up**)
- else Bound (i - length (List.filter (fn j => 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<lev then Bound i
+ else if (i-lev) mem_int banned
+ then raise CHANGE_FAIL (**flexible occurrence: give up**)
+ else Bound (i - length (List.filter (fn j => 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;