src/Pure/envir.ML
changeset 51700 c8f2bad67dbb
parent 43278 1fbdcebb364b
child 51701 1e29891759c4
     1.1 --- a/src/Pure/envir.ML	Fri Apr 12 12:20:51 2013 +0200
     1.2 +++ b/src/Pure/envir.ML	Fri Apr 12 14:54:14 2013 +0200
     1.3 @@ -19,11 +19,11 @@
     1.4    val insert_sorts: env -> sort list -> sort list
     1.5    val genvars: string -> env * typ list -> env * term list
     1.6    val genvar: string -> env * typ -> env * term
     1.7 -  val lookup: env * (indexname * typ) -> term option
     1.8 -  val lookup': tenv * (indexname * typ) -> term option
     1.9 -  val update: ((indexname * typ) * term) * env -> env
    1.10 +  val lookup1: tenv -> indexname * typ -> term option
    1.11 +  val lookup: env -> indexname * typ -> term option
    1.12 +  val update: (indexname * typ) * term -> env -> env
    1.13    val above: env -> int -> bool
    1.14 -  val vupdate: ((indexname * typ) * term) * env -> env
    1.15 +  val vupdate: (indexname * typ) * term -> env -> env
    1.16    val norm_type_same: Type.tyenv -> typ Same.operation
    1.17    val norm_types_same: Type.tyenv -> typ list Same.operation
    1.18    val norm_type: Type.tyenv -> typ -> typ
    1.19 @@ -114,19 +114,17 @@
    1.20      NONE => NONE
    1.21    | SOME (U, t) => if check (T, U) then SOME t else var_clash xi T U);
    1.22  
    1.23 -(* When dealing with environments produced by matching instead *)
    1.24 -(* of unification, there is no need to chase assigned TVars.   *)
    1.25 -(* In this case, we can simply ignore the type substitution    *)
    1.26 -(* and use = instead of eq_type.                               *)
    1.27 -
    1.28 -fun lookup' (tenv, p) = lookup_check (op =) tenv p;
    1.29 +(*When dealing with environments produced by matching instead
    1.30 +  of unification, there is no need to chase assigned TVars.
    1.31 +  In this case, we can simply ignore the type substitution
    1.32 +  and use = instead of eq_type.*)
    1.33 +val lookup1 = lookup_check (op =);
    1.34  
    1.35 -fun lookup2 (tyenv, tenv) =
    1.36 -  lookup_check (Type.eq_type tyenv) tenv;
    1.37 +fun lookup2 (tyenv, tenv) = lookup_check (Type.eq_type tyenv) tenv;
    1.38  
    1.39 -fun lookup (Envir {tenv, tyenv, ...}, p) = lookup2 (tyenv, tenv) p;
    1.40 +fun lookup (Envir {tenv, tyenv, ...}) = lookup2 (tyenv, tenv);
    1.41  
    1.42 -fun update (((xi, T), t), Envir {maxidx, tenv, tyenv}) =
    1.43 +fun update ((xi, T), t) (Envir {maxidx, tenv, tyenv}) =
    1.44    Envir {maxidx = maxidx, tenv = Vartab.update_new (xi, (T, t)) tenv, tyenv = tyenv};
    1.45  
    1.46  (*Determine if the least index updated exceeds lim*)
    1.47 @@ -135,16 +133,16 @@
    1.48    (case Vartab.min_key tyenv of SOME (_, i) => i > lim | NONE => true);
    1.49  
    1.50  (*Update, checking Var-Var assignments: try to suppress higher indexes*)
    1.51 -fun vupdate ((aU as (a, U), t), env as Envir {tyenv, ...}) =
    1.52 +fun vupdate (aU as (a, U), t) (env as Envir {tyenv, ...}) =
    1.53    (case t of
    1.54      Var (nT as (name', T)) =>
    1.55        if a = name' then env     (*cycle!*)
    1.56        else if Term_Ord.indexname_ord (a, name') = LESS then
    1.57 -        (case lookup (env, nT) of  (*if already assigned, chase*)
    1.58 -          NONE => update ((nT, Var (a, T)), env)
    1.59 -        | SOME u => vupdate ((aU, u), env))
    1.60 -      else update ((aU, t), env)
    1.61 -  | _ => update ((aU, t), env));
    1.62 +        (case lookup env nT of  (*if already assigned, chase*)
    1.63 +          NONE => update (nT, Var (a, T)) env
    1.64 +        | SOME u => vupdate (aU, u) env)
    1.65 +      else update (aU, t) env
    1.66 +  | _ => update (aU, t) env);
    1.67  
    1.68  
    1.69  
    1.70 @@ -168,7 +166,7 @@
    1.71  fun norm_term1 tenv : term Same.operation =
    1.72    let
    1.73      fun norm (Var v) =
    1.74 -          (case lookup' (tenv, v) of
    1.75 +          (case lookup1 tenv v of
    1.76              SOME u => Same.commit norm u
    1.77            | NONE => raise Same.SAME)
    1.78        | norm (Abs (a, T, body)) = Abs (a, T, norm body)
    1.79 @@ -229,7 +227,7 @@
    1.80  fun head_norm env =
    1.81    let
    1.82      fun norm (Var v) =
    1.83 -        (case lookup (env, v) of
    1.84 +        (case lookup env v of
    1.85            SOME u => head_norm env u
    1.86          | NONE => raise Same.SAME)
    1.87        | norm (Abs (a, T, body)) = Abs (a, T, norm body)
    1.88 @@ -309,7 +307,7 @@
    1.89  
    1.90  fun subst_term1 tenv = Term_Subst.map_aterms_same
    1.91    (fn Var v =>
    1.92 -        (case lookup' (tenv, v) of
    1.93 +        (case lookup1 tenv v of
    1.94            SOME u => u
    1.95          | NONE => raise Same.SAME)
    1.96      | _ => raise Same.SAME);
    1.97 @@ -320,7 +318,7 @@
    1.98      fun subst (Const (a, T)) = Const (a, substT T)
    1.99        | subst (Free (a, T)) = Free (a, substT T)
   1.100        | subst (Var (xi, T)) =
   1.101 -          (case lookup' (tenv, (xi, T)) of
   1.102 +          (case lookup1 tenv (xi, T) of
   1.103              SOME u => u
   1.104            | NONE => Var (xi, substT T))
   1.105        | subst (Bound _) = raise Same.SAME