--- a/src/Pure/envir.ML Fri Apr 12 12:20:51 2013 +0200
+++ b/src/Pure/envir.ML Fri Apr 12 14:54:14 2013 +0200
@@ -19,11 +19,11 @@
val insert_sorts: env -> sort list -> sort list
val genvars: string -> env * typ list -> env * term list
val genvar: string -> env * typ -> env * term
- val lookup: env * (indexname * typ) -> term option
- val lookup': tenv * (indexname * typ) -> term option
- val update: ((indexname * typ) * term) * env -> env
+ val lookup1: tenv -> indexname * typ -> term option
+ val lookup: env -> indexname * typ -> term option
+ val update: (indexname * typ) * term -> env -> env
val above: env -> int -> bool
- val vupdate: ((indexname * typ) * term) * env -> env
+ val vupdate: (indexname * typ) * term -> env -> env
val norm_type_same: Type.tyenv -> typ Same.operation
val norm_types_same: Type.tyenv -> typ list Same.operation
val norm_type: Type.tyenv -> typ -> typ
@@ -114,19 +114,17 @@
NONE => NONE
| SOME (U, t) => if check (T, U) then SOME t else var_clash xi T U);
-(* When dealing with environments produced by matching instead *)
-(* of unification, there is no need to chase assigned TVars. *)
-(* In this case, we can simply ignore the type substitution *)
-(* and use = instead of eq_type. *)
-
-fun lookup' (tenv, p) = lookup_check (op =) tenv p;
+(*When dealing with environments produced by matching instead
+ of unification, there is no need to chase assigned TVars.
+ In this case, we can simply ignore the type substitution
+ and use = instead of eq_type.*)
+val lookup1 = lookup_check (op =);
-fun lookup2 (tyenv, tenv) =
- lookup_check (Type.eq_type tyenv) tenv;
+fun lookup2 (tyenv, tenv) = lookup_check (Type.eq_type tyenv) tenv;
-fun lookup (Envir {tenv, tyenv, ...}, p) = lookup2 (tyenv, tenv) p;
+fun lookup (Envir {tenv, tyenv, ...}) = lookup2 (tyenv, tenv);
-fun update (((xi, T), t), Envir {maxidx, tenv, tyenv}) =
+fun update ((xi, T), t) (Envir {maxidx, tenv, tyenv}) =
Envir {maxidx = maxidx, tenv = Vartab.update_new (xi, (T, t)) tenv, tyenv = tyenv};
(*Determine if the least index updated exceeds lim*)
@@ -135,16 +133,16 @@
(case Vartab.min_key tyenv of SOME (_, i) => i > lim | NONE => true);
(*Update, checking Var-Var assignments: try to suppress higher indexes*)
-fun vupdate ((aU as (a, U), t), env as Envir {tyenv, ...}) =
+fun vupdate (aU as (a, U), t) (env as Envir {tyenv, ...}) =
(case t of
Var (nT as (name', T)) =>
if a = name' then env (*cycle!*)
else if Term_Ord.indexname_ord (a, name') = LESS then
- (case lookup (env, nT) of (*if already assigned, chase*)
- NONE => update ((nT, Var (a, T)), env)
- | SOME u => vupdate ((aU, u), env))
- else update ((aU, t), env)
- | _ => update ((aU, t), env));
+ (case lookup env nT of (*if already assigned, chase*)
+ NONE => update (nT, Var (a, T)) env
+ | SOME u => vupdate (aU, u) env)
+ else update (aU, t) env
+ | _ => update (aU, t) env);
@@ -168,7 +166,7 @@
fun norm_term1 tenv : term Same.operation =
let
fun norm (Var v) =
- (case lookup' (tenv, v) of
+ (case lookup1 tenv v of
SOME u => Same.commit norm u
| NONE => raise Same.SAME)
| norm (Abs (a, T, body)) = Abs (a, T, norm body)
@@ -229,7 +227,7 @@
fun head_norm env =
let
fun norm (Var v) =
- (case lookup (env, v) of
+ (case lookup env v of
SOME u => head_norm env u
| NONE => raise Same.SAME)
| norm (Abs (a, T, body)) = Abs (a, T, norm body)
@@ -309,7 +307,7 @@
fun subst_term1 tenv = Term_Subst.map_aterms_same
(fn Var v =>
- (case lookup' (tenv, v) of
+ (case lookup1 tenv v of
SOME u => u
| NONE => raise Same.SAME)
| _ => raise Same.SAME);
@@ -320,7 +318,7 @@
fun subst (Const (a, T)) = Const (a, substT T)
| subst (Free (a, T)) = Free (a, substT T)
| subst (Var (xi, T)) =
- (case lookup' (tenv, (xi, T)) of
+ (case lookup1 tenv (xi, T) of
SOME u => u
| NONE => Var (xi, substT T))
| subst (Bound _) = raise Same.SAME
--- a/src/Pure/pattern.ML Fri Apr 12 12:20:51 2013 +0200
+++ b/src/Pure/pattern.ML Fri Apr 12 14:54:14 2013 +0200
@@ -93,7 +93,7 @@
else ()
fun occurs(F,t,env) =
- let fun occ(Var (G, T)) = (case Envir.lookup (env, (G, T)) of
+ let fun occ(Var (G, T)) = (case Envir.lookup env (G, T) of
SOME(t) => occ t
| NONE => F=G)
| occ(t1$t2) = occ t1 orelse occ t2
@@ -152,7 +152,7 @@
fun mknewhnf(env,binders,is,F as (a,_),T,js) =
let val (env',G) = Envir.genvar a (env,type_of_G env (T,length is,js))
- in Envir.update (((F, T), mkhnf (binders, is, G, js)), env') end;
+ in Envir.update ((F, T), mkhnf (binders, is, G, js)) env' end;
(*predicate: downto0 (is, n) <=> is = [n, n - 1, ..., 0]*)
@@ -189,7 +189,7 @@
val Hty = type_of_G env (Fty,length js,ks)
val (env',H) = Envir.genvar a (env,Hty)
val env'' =
- Envir.update (((F, Fty), mkhnf (binders, js, H, ks)), env')
+ Envir.update ((F, Fty), mkhnf (binders, js, H, ks)) env'
in (app(H,ls),env'') end
| _ => raise Pattern))
and prs(s::ss,env,d,binders) =
@@ -219,12 +219,12 @@
let fun ff(F,Fty,is,G as (a,_),Gty,js) =
if subset (op =) (js, is)
then let val t= mkabs(binders,is,app(Var(G,Gty),map (idx is) js))
- in Envir.update (((F, Fty), t), env) end
+ in Envir.update ((F, Fty), t) env end
else let val ks = inter (op =) js is
val Hty = type_of_G env (Fty,length is,map (idx is) ks)
val (env',H) = Envir.genvar a (env,Hty)
fun lam(is) = mkabs(binders,is,app(H,map (idx is) ks));
- in Envir.update (((G, Gty), lam js), Envir.update (((F, Fty), lam is), env'))
+ in Envir.update ((G, Gty), lam js) (Envir.update ((F, Fty), lam is) env')
end;
in if Term_Ord.indexname_ord (G,F) = LESS then ff(F,Fty,is,G,Gty,js) else ff(G,Gty,js,F,Fty,is) end
@@ -273,7 +273,7 @@
and flexrigid thy (params as (env,binders,F,Fty,is,t)) =
if occurs(F,t,env) then (ocheck_fail thy (F,t,binders,env); raise Unif)
else (let val (u,env') = proj(t,env,binders,is)
- in Envir.update (((F, Fty), mkabs (binders, is, u)), env') end
+ in Envir.update ((F, Fty), mkabs (binders, is, u)) env' end
handle Unif => (proj_fail thy params; raise Unif));
fun unify thy = unif thy [];
@@ -319,7 +319,7 @@
fun mtch k (instsp as (tyinsts,insts)) = fn
(Var(ixn,T), t) =>
if k > 0 andalso Term.is_open t then raise MATCH
- else (case Envir.lookup' (insts, (ixn, T)) of
+ else (case Envir.lookup1 insts (ixn, T) of
NONE => (typ_match thy (T, fastype_of t) tyinsts,
Vartab.update_new (ixn, (T, t)) insts)
| SOME u => if t aeconv u then instsp else raise MATCH)
@@ -374,7 +374,7 @@
in case ph of
Var(ixn,T) =>
let val is = ints_of pargs
- in case Envir.lookup' (itms, (ixn, T)) of
+ in case Envir.lookup1 itms (ixn, T) of
NONE => (iTs,match_bind(itms,binders,ixn,T,is,obj))
| SOME u => if obj aeconv (red u is []) then env
else raise MATCH
--- a/src/Pure/proofterm.ML Fri Apr 12 12:20:51 2013 +0200
+++ b/src/Pure/proofterm.ML Fri Apr 12 14:54:14 2013 +0200
@@ -468,7 +468,7 @@
(Type.lookup (Envir.type_env env) ixnS; NONE) handle TYPE _ =>
SOME (ixnS, TFree ("'dummy", S))) (Term.add_tvars t []),
map_filter (fn (ixnT as (_, T)) =>
- (Envir.lookup (env, ixnT); NONE) handle TYPE _ =>
+ (Envir.lookup env ixnT; NONE) handle TYPE _ =>
SOME (ixnT, Free ("dummy", T))) (Term.add_vars t [])) t;
fun norm_proof env =
--- a/src/Pure/unify.ML Fri Apr 12 12:20:51 2013 +0200
+++ b/src/Pure/unify.ML Fri Apr 12 14:54:14 2013 +0200
@@ -120,7 +120,7 @@
(*no need to lookup: v has no assignment*)
else
(seen := w :: !seen;
- case Envir.lookup (env, (w, T)) of
+ case Envir.lookup env (w, T) of
NONE => false
| SOME t => occur t)
| occur (Abs (_, _, body)) = occur body
@@ -133,7 +133,7 @@
(case t of
f $ _ => head_of_in (env, f)
| Var vT =>
- (case Envir.lookup (env, vT) of
+ (case Envir.lookup env vT of
SOME u => head_of_in (env, u)
| NONE => t)
| _ => t);
@@ -187,7 +187,7 @@
else if Term.eq_ix (v, w) then Rigid
else
(seen := w :: !seen;
- case Envir.lookup (env, (w, T)) of
+ case Envir.lookup env (w, T) of
NONE => NoOcc
| SOME t => occur t)
| occur (Abs (_, _, body)) = occur body
@@ -239,7 +239,7 @@
(case rigid_occurs_term (Unsynchronized.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
+ in Envir.update (vT, Logic.rlist_abs (rbinder, u)) env end
| Nonrigid => raise ASSIGN
| Rigid => raise CANTUNIFY)
end;
@@ -310,7 +310,7 @@
(* changed(env,t) checks whether the head of t is a variable assigned in env*)
fun changed (env, f $ _) = changed (env, f)
- | changed (env, Var v) = (case Envir.lookup (env, v) of NONE => false | _ => true)
+ | changed (env, Var v) = (case Envir.lookup env v of NONE => false | _ => true)
| changed _ = false;
@@ -429,8 +429,8 @@
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')
+ (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)))
@@ -447,7 +447,7 @@
if occurs_terms (Unsynchronized.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
+ in Envir.vupdate (vT, Logic.rlist_abs (rbinder, u)) env end
end;
@@ -536,7 +536,7 @@
let
val (env', v') = Envir.genvar (#1 v) (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'));
+ 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;
@@ -669,10 +669,10 @@
val vT as (v, T) = var_head_of (env, t)
and wU as (w, U) = var_head_of (env, u);
val (env', var) = Envir.genvar (#1 v) (env, body_type env T);
- val env'' = Envir.vupdate ((wU, type_abs (env', U, var)), env');
+ val env'' = Envir.vupdate (wU, type_abs (env', U, var)) env';
in
if vT = wU then env'' (*the other update would be identical*)
- else Envir.vupdate ((vT, type_abs (env', T, var)), env'')
+ else Envir.vupdate (vT, type_abs (env', T, var)) env''
end;