--- a/src/Pure/unify.ML Thu Jun 30 19:43:50 2005 +0200
+++ b/src/Pure/unify.ML Thu Jun 30 19:49:41 2005 +0200
@@ -36,6 +36,9 @@
and trace_types = ref false (*announce potential incompleteness
of type unification*)
+val thy_ref = ref (NONE: theory option);
+fun thy () = the (! thy_ref);
+
type binderlist = (string*typ) list;
type dpair = binderlist * term * term;
@@ -174,16 +177,16 @@
exception ASSIGN; (*Raised if not an assignment*)
-fun unify_types thy (T,U, env as Envir.Envir{asol,iTs,maxidx}) =
+fun unify_types(T,U, env as Envir.Envir{asol,iTs,maxidx}) =
if T=U then env
- else let val (iTs',maxidx') = Type.unify (Sign.tsig_of thy) (iTs, maxidx) (U, T)
+ else let val (iTs',maxidx') = Type.unify (Sign.tsig_of (thy ())) (iTs, maxidx) (U, T)
in Envir.Envir{asol=asol,maxidx=maxidx',iTs=iTs'} end
handle Type.TUNIFY => raise CANTUNIFY;
-fun test_unify_types thy (args as (T,U,_)) =
-let val str_of = Sign.string_of_typ thy;
- fun warn() = tracing ("Potential loss of completeness: " ^ str_of U ^ " = " ^ str_of T);
- val env' = unify_types thy args
+fun test_unify_types(args as (T,U,_)) =
+let val sot = Sign.string_of_typ (thy ());
+ fun warn() = tracing ("Potential loss of completeness: "^sot U^" = "^sot T);
+ val env' = unify_types(args)
in if is_TVar(T) orelse is_TVar(U) then warn() else ();
env'
end;
@@ -206,10 +209,10 @@
(*Solve v=u by assignment -- "fixedpoint" to Huet -- if v not in u.
If v occurs rigidly then nonunifiable.
If v occurs nonrigidly then must use full algorithm. *)
-fun assignment thy (env, rbinder, t, u) =
+fun assignment (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,
+ NoOcc => let val env = unify_types(body_type env T,
fastype env (rbinder,u),env)
in Envir.update ((vT, rlist_abs (rbinder, u)), env) end
| Nonrigid => raise ASSIGN
@@ -222,17 +225,17 @@
Checks that binders have same length, since terms should be eta-normal;
if not, raises TERM, probably indicating type mismatch.
Uses variable a (unless the null string) to preserve user's naming.*)
-fun new_dpair thy (rbinder, Abs(a,T,body1), Abs(b,U,body2), env) =
- let val env' = unify_types thy (T,U,env)
+fun new_dpair (rbinder, Abs(a,T,body1), Abs(b,U,body2), env) =
+ let val env' = unify_types(T,U,env)
val c = if a="" then b else a
- in new_dpair 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);
+ in new_dpair((c,T) :: rbinder, body1, body2, env') end
+ | new_dpair (_, Abs _, _, _) = raise TERM ("new_dpair", [])
+ | new_dpair (_, _, Abs _, _) = raise TERM ("new_dpair", [])
+ | new_dpair (rbinder, t1, t2, env) = ((rbinder, t1, t2), env);
-fun head_norm_dpair thy (env, (rbinder,t,u)) : dpair * Envir.env =
- new_dpair thy (rbinder,
+fun head_norm_dpair (env, (rbinder,t,u)) : dpair * Envir.env =
+ new_dpair (rbinder,
eta_norm env (rbinder, Envir.head_norm env t),
eta_norm env (rbinder, Envir.head_norm env u), env);
@@ -244,11 +247,11 @@
Does not even identify Vars in dpairs such as ?a =?= ?b; an attempt to
do so caused numerous problems with no compensating advantage.
*)
-fun SIMPL0 thy (dp0, (env,flexflex,flexrigid))
+fun SIMPL0 (dp0, (env,flexflex,flexrigid))
: Envir.env * dpair list * dpair list =
- let val (dp as (rbinder,t,u), env) = head_norm_dpair thy (env,dp0);
+ let val (dp as (rbinder,t,u), env) = head_norm_dpair(env,dp0);
fun SIMRANDS(f$t, g$u, env) =
- SIMPL0 thy ((rbinder,t,u), SIMRANDS(f,g,env))
+ SIMPL0((rbinder,t,u), SIMRANDS(f,g,env))
| SIMRANDS (t as _$_, _, _) =
raise TERM ("SIMPL: operands mismatch", [t,u])
| SIMRANDS (t, u as _$_, _) =
@@ -257,21 +260,21 @@
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)
+ val env = unify_types(T',U',env)
in (env, dp::flexflex, flexrigid) end
| (Var _, _) =>
- ((assignment thy (env,rbinder,t,u), flexflex, flexrigid)
+ ((assignment (env,rbinder,t,u), flexflex, flexrigid)
handle ASSIGN => (env, flexflex, dp::flexrigid))
| (_, Var _) =>
- ((assignment thy (env,rbinder,u,t), flexflex, flexrigid)
+ ((assignment (env,rbinder,u,t), flexflex, flexrigid)
handle ASSIGN => (env, flexflex, (rbinder,u,t)::flexrigid))
| (Const(a,T), Const(b,U)) =>
- if a=b then SIMRANDS(t,u, unify_types thy (T,U,env))
+ if a=b then SIMRANDS(t,u, unify_types(T,U,env))
else raise CANTUNIFY
| (Bound i, Bound j) =>
if i=j then SIMRANDS(t,u,env) else raise CANTUNIFY
| (Free(a,T), Free(b,U)) =>
- if a=b then SIMRANDS(t,u, unify_types thy (T,U,env))
+ if a=b then SIMRANDS(t,u, unify_types(T,U,env))
else raise CANTUNIFY
| _ => raise CANTUNIFY
end;
@@ -286,12 +289,12 @@
(*Recursion needed if any of the 'head variables' have been updated
Clever would be to re-do just the affected dpairs*)
-fun SIMPL thy (env,dpairs) : Envir.env * dpair list * dpair list =
+fun SIMPL (env,dpairs) : Envir.env * dpair list * dpair list =
let val all as (env',flexflex,flexrigid) =
- foldr (SIMPL0 thy) (env,[],[]) dpairs;
+ foldr SIMPL0 (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
+ then SIMPL(env',dps) else all
end;
@@ -329,7 +332,7 @@
For example, projection in ?b'(?a) may be wrong if other dpairs constrain ?a.
The order for trying projections is crucial in ?b'(?a)
NB "vname" is only used in the call to make_args!! *)
-fun matchcopy thy vname = let fun mc(rbinder, targs, u, ed as (env,dpairs))
+fun matchcopy 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)) =
@@ -346,14 +349,14 @@
(*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)
+ let val env = if !trace_types then test_unify_types(base,bary,env)
+ else unify_types(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)
+ val (env2,frigid,fflex) = SIMPL (env', dp::dpairs)
(*may raise exception CANTUNIFY*)
in SOME ((list_comb(head,args), (env2, frigid@fflex)),
tail)
@@ -390,7 +393,7 @@
(*Call matchcopy to produce assignments to the variable in the dpair*)
-fun MATCH thy (env, (rbinder,t,u), dpairs)
+fun MATCH (env, (rbinder,t,u), dpairs)
: (Envir.env * dpair list)Seq.seq =
let val (Var (vT as (v, T)), targs) = strip_comb t;
val Ts = binder_types env T;
@@ -400,7 +403,7 @@
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)))
+ (matchcopy (#1 v) (rbinder, targs, u, (env,dpairs)))
end;
@@ -409,10 +412,10 @@
(*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(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,
+ else let val env = unify_types(body_type env T,
fastype env (rbinder,u),
env)
in Envir.vupdate ((vT, rlist_abs (rbinder, u)), env) end
@@ -511,7 +514,7 @@
(*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 ((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
@@ -521,8 +524,8 @@
val (banned,rbin') = foldr add_index ([],[]) (rbinder~~indices);
val (env', t') = clean_term banned (env, t);
val (env'',u') = clean_term banned (env',u)
- in (ff_assign thy (env'', rbin', t', u'), tpairs)
- handle ASSIGN => (ff_assign thy (env'', rbin', u', t'), tpairs)
+ in (ff_assign(env'', rbin', t', u'), tpairs)
+ handle ASSIGN => (ff_assign(env'', rbin', u', t'), tpairs)
handle ASSIGN => (env'', add_tpair(rbin', (t',u'), tpairs))
end
handle CHANGE_FAIL => (env, add_tpair(rbinder, (t,u), tpairs));
@@ -532,7 +535,7 @@
eliminates trivial tpairs like t=t, as well as repeated ones
trivial tpairs can easily escape SIMPL: ?A=t, ?A=?B, ?B=t gives t=t
Resulting tpairs MAY NOT be in normal form: assignments may occur here.*)
-fun add_ffpair thy ((rbinder,t0,u0), (env,tpairs))
+fun add_ffpair ((rbinder,t0,u0), (env,tpairs))
: Envir.env * (term*term)list =
let val t = Envir.norm_term env t0 and u = Envir.norm_term env u0
in case (head_of t, head_of u) of
@@ -541,8 +544,8 @@
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))
+ clean_ffpair ((rbinder, u, t), (env,tpairs))
+ else clean_ffpair ((rbinder, t, u), (env,tpairs))
| _ => raise TERM ("add_ffpair: Vars expected", [t,u])
end;
@@ -550,9 +553,9 @@
(*Print a tracing message + list of dpairs.
In t==u print u first because it may be rigid or flexible --
t is always flexible.*)
-fun print_dpairs thy msg (env,dpairs) =
+fun print_dpairs msg (env,dpairs) =
let fun pdp (rbinder,t,u) =
- let fun termT t = Sign.pretty_term thy
+ let fun termT t = Sign.pretty_term (thy ())
(Envir.norm_term env (rlist_abs(rbinder,t)))
val bsymbs = [termT u, Pretty.str" =?=", Pretty.brk 1,
termT t];
@@ -569,24 +572,25 @@
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))
+ then print_dpairs "Enter SIMPL" (env,dpairs) else ();
+ SIMPL (env,dpairs))
in case flexrigid of
- [] => SOME (foldr (add_ffpair thy) (env',[]) flexflex, reseq)
+ [] => SOME (foldr add_ffpair (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)
+ print_dpairs "Enter MATCH" (env',flexrigid@flexflex)
else ();
Seq.pull (Seq.it_right (add_unify (tdepth+1))
- (MATCH thy (env',dp, frigid'@flexflex), reseq)))
+ (MATCH (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
+ val _ = thy_ref := SOME thy;
in add_unify 1 ((env, dps), Seq.empty) end;
fun unifiers params =