tuned signature;
authorwenzelm
Fri Apr 12 14:54:14 2013 +0200 (2013-04-12)
changeset 51700c8f2bad67dbb
parent 51699 0539e75b4170
child 51701 1e29891759c4
tuned signature;
tuned comments;
src/Pure/envir.ML
src/Pure/pattern.ML
src/Pure/proofterm.ML
src/Pure/unify.ML
     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
     2.1 --- a/src/Pure/pattern.ML	Fri Apr 12 12:20:51 2013 +0200
     2.2 +++ b/src/Pure/pattern.ML	Fri Apr 12 14:54:14 2013 +0200
     2.3 @@ -93,7 +93,7 @@
     2.4    else ()
     2.5  
     2.6  fun occurs(F,t,env) =
     2.7 -    let fun occ(Var (G, T))   = (case Envir.lookup (env, (G, T)) of
     2.8 +    let fun occ(Var (G, T))   = (case Envir.lookup env (G, T) of
     2.9                                   SOME(t) => occ t
    2.10                                 | NONE    => F=G)
    2.11            | occ(t1$t2)      = occ t1 orelse occ t2
    2.12 @@ -152,7 +152,7 @@
    2.13  
    2.14  fun mknewhnf(env,binders,is,F as (a,_),T,js) =
    2.15    let val (env',G) = Envir.genvar a (env,type_of_G env (T,length is,js))
    2.16 -  in Envir.update (((F, T), mkhnf (binders, is, G, js)), env') end;
    2.17 +  in Envir.update ((F, T), mkhnf (binders, is, G, js)) env' end;
    2.18  
    2.19  
    2.20  (*predicate: downto0 (is, n) <=> is = [n, n - 1, ..., 0]*)
    2.21 @@ -189,7 +189,7 @@
    2.22                            val Hty = type_of_G env (Fty,length js,ks)
    2.23                            val (env',H) = Envir.genvar a (env,Hty)
    2.24                            val env'' =
    2.25 -                            Envir.update (((F, Fty), mkhnf (binders, js, H, ks)), env')
    2.26 +                            Envir.update ((F, Fty), mkhnf (binders, js, H, ks)) env'
    2.27                        in (app(H,ls),env'') end
    2.28                   | _  => raise Pattern))
    2.29          and prs(s::ss,env,d,binders) =
    2.30 @@ -219,12 +219,12 @@
    2.31    let fun ff(F,Fty,is,G as (a,_),Gty,js) =
    2.32              if subset (op =) (js, is)
    2.33              then let val t= mkabs(binders,is,app(Var(G,Gty),map (idx is) js))
    2.34 -                 in Envir.update (((F, Fty), t), env) end
    2.35 +                 in Envir.update ((F, Fty), t) env end
    2.36              else let val ks = inter (op =) js is
    2.37                       val Hty = type_of_G env (Fty,length is,map (idx is) ks)
    2.38                       val (env',H) = Envir.genvar a (env,Hty)
    2.39                       fun lam(is) = mkabs(binders,is,app(H,map (idx is) ks));
    2.40 -                 in Envir.update (((G, Gty), lam js), Envir.update (((F, Fty), lam is), env'))
    2.41 +                 in Envir.update ((G, Gty), lam js) (Envir.update ((F, Fty), lam is) env')
    2.42                   end;
    2.43    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
    2.44  
    2.45 @@ -273,7 +273,7 @@
    2.46  and flexrigid thy (params as (env,binders,F,Fty,is,t)) =
    2.47        if occurs(F,t,env) then (ocheck_fail thy (F,t,binders,env); raise Unif)
    2.48        else (let val (u,env') = proj(t,env,binders,is)
    2.49 -            in Envir.update (((F, Fty), mkabs (binders, is, u)), env') end
    2.50 +            in Envir.update ((F, Fty), mkabs (binders, is, u)) env' end
    2.51              handle Unif => (proj_fail thy params; raise Unif));
    2.52  
    2.53  fun unify thy = unif thy [];
    2.54 @@ -319,7 +319,7 @@
    2.55      fun mtch k (instsp as (tyinsts,insts)) = fn
    2.56          (Var(ixn,T), t)  =>
    2.57            if k > 0 andalso Term.is_open t then raise MATCH
    2.58 -          else (case Envir.lookup' (insts, (ixn, T)) of
    2.59 +          else (case Envir.lookup1 insts (ixn, T) of
    2.60                    NONE => (typ_match thy (T, fastype_of t) tyinsts,
    2.61                             Vartab.update_new (ixn, (T, t)) insts)
    2.62                  | SOME u => if t aeconv u then instsp else raise MATCH)
    2.63 @@ -374,7 +374,7 @@
    2.64      in case ph of
    2.65           Var(ixn,T) =>
    2.66             let val is = ints_of pargs
    2.67 -           in case Envir.lookup' (itms, (ixn, T)) of
    2.68 +           in case Envir.lookup1 itms (ixn, T) of
    2.69                  NONE => (iTs,match_bind(itms,binders,ixn,T,is,obj))
    2.70                | SOME u => if obj aeconv (red u is []) then env
    2.71                            else raise MATCH
     3.1 --- a/src/Pure/proofterm.ML	Fri Apr 12 12:20:51 2013 +0200
     3.2 +++ b/src/Pure/proofterm.ML	Fri Apr 12 14:54:14 2013 +0200
     3.3 @@ -468,7 +468,7 @@
     3.4       (Type.lookup (Envir.type_env env) ixnS; NONE) handle TYPE _ =>
     3.5          SOME (ixnS, TFree ("'dummy", S))) (Term.add_tvars t []),
     3.6     map_filter (fn (ixnT as (_, T)) =>
     3.7 -     (Envir.lookup (env, ixnT); NONE) handle TYPE _ =>
     3.8 +     (Envir.lookup env ixnT; NONE) handle TYPE _ =>
     3.9          SOME (ixnT, Free ("dummy", T))) (Term.add_vars t [])) t;
    3.10  
    3.11  fun norm_proof env =
     4.1 --- a/src/Pure/unify.ML	Fri Apr 12 12:20:51 2013 +0200
     4.2 +++ b/src/Pure/unify.ML	Fri Apr 12 14:54:14 2013 +0200
     4.3 @@ -120,7 +120,7 @@
     4.4              (*no need to lookup: v has no assignment*)
     4.5            else
     4.6              (seen := w :: !seen;
     4.7 -             case Envir.lookup (env, (w, T)) of
     4.8 +             case Envir.lookup env (w, T) of
     4.9                 NONE => false
    4.10               | SOME t => occur t)
    4.11        | occur (Abs (_, _, body)) = occur body
    4.12 @@ -133,7 +133,7 @@
    4.13    (case t of
    4.14      f $ _ => head_of_in (env, f)
    4.15    | Var vT =>
    4.16 -      (case Envir.lookup (env, vT) of
    4.17 +      (case Envir.lookup env vT of
    4.18          SOME u => head_of_in (env, u)
    4.19        | NONE => t)
    4.20    | _ => t);
    4.21 @@ -187,7 +187,7 @@
    4.22            else if Term.eq_ix (v, w) then Rigid
    4.23            else
    4.24              (seen := w :: !seen;
    4.25 -             case Envir.lookup (env, (w, T)) of
    4.26 +             case Envir.lookup env (w, T) of
    4.27                 NONE => NoOcc
    4.28               | SOME t => occur t)
    4.29        | occur (Abs (_, _, body)) = occur body
    4.30 @@ -239,7 +239,7 @@
    4.31      (case rigid_occurs_term (Unsynchronized.ref [], env, v, u) of
    4.32        NoOcc =>
    4.33          let val env = unify_types thy (body_type env T, fastype env (rbinder, u), env)
    4.34 -        in Envir.update ((vT, Logic.rlist_abs (rbinder, u)), env) end
    4.35 +        in Envir.update (vT, Logic.rlist_abs (rbinder, u)) env end
    4.36      | Nonrigid => raise ASSIGN
    4.37      | Rigid => raise CANTUNIFY)
    4.38    end;
    4.39 @@ -310,7 +310,7 @@
    4.40  
    4.41  (* changed(env,t) checks whether the head of t is a variable assigned in env*)
    4.42  fun changed (env, f $ _) = changed (env, f)
    4.43 -  | changed (env, Var v) = (case Envir.lookup (env, v) of NONE => false | _ => true)
    4.44 +  | changed (env, Var v) = (case Envir.lookup env v of NONE => false | _ => true)
    4.45    | changed _ = false;
    4.46  
    4.47  
    4.48 @@ -429,8 +429,8 @@
    4.49      val Ts = binder_types env T;
    4.50      fun new_dset (u', (env', dpairs')) =
    4.51        (*if v was updated to s, must unify s with u' *)
    4.52 -      (case Envir.lookup (env', vT) of
    4.53 -        NONE => (Envir.update ((vT, types_abs (Ts, u')), env'), dpairs')
    4.54 +      (case Envir.lookup env' vT of
    4.55 +        NONE => (Envir.update (vT, types_abs (Ts, u')) env', dpairs')
    4.56        | SOME s => (env', ([], s, types_abs (Ts, u')) :: dpairs'));
    4.57    in
    4.58      Seq.map new_dset (matchcopy thy (#1 v) (rbinder, targs, u, (env, dpairs)))
    4.59 @@ -447,7 +447,7 @@
    4.60      if occurs_terms (Unsynchronized.ref [], env, v, [u]) then raise ASSIGN
    4.61      else
    4.62        let val env = unify_types thy (body_type env T, fastype env (rbinder, u), env)
    4.63 -      in Envir.vupdate ((vT, Logic.rlist_abs (rbinder, u)), env) end
    4.64 +      in Envir.vupdate (vT, Logic.rlist_abs (rbinder, u)) env end
    4.65    end;
    4.66  
    4.67  
    4.68 @@ -536,7 +536,7 @@
    4.69        let
    4.70          val (env', v') = Envir.genvar (#1 v) (env, map #T args ---> U);
    4.71          val body = list_comb (v', map (Bound o #j) args);
    4.72 -        val env2 = Envir.vupdate ((((v, T), types_abs (Ts, body)), env'));
    4.73 +        val env2 = Envir.vupdate ((v, T), types_abs (Ts, body)) env';
    4.74          (*the vupdate affects ts' if they contain v*)
    4.75        in (env2, Envir.norm_term env2 (list_comb (v', ts'))) end
    4.76    end;
    4.77 @@ -669,10 +669,10 @@
    4.78      val vT as (v, T) = var_head_of (env, t)
    4.79      and wU as (w, U) = var_head_of (env, u);
    4.80      val (env', var) = Envir.genvar (#1 v) (env, body_type env T);
    4.81 -    val env'' = Envir.vupdate ((wU, type_abs (env', U, var)), env');
    4.82 +    val env'' = Envir.vupdate (wU, type_abs (env', U, var)) env';
    4.83    in
    4.84      if vT = wU then env''  (*the other update would be identical*)
    4.85 -    else Envir.vupdate ((vT, type_abs (env', T, var)), env'')
    4.86 +    else Envir.vupdate (vT, type_abs (env', T, var)) env''
    4.87    end;
    4.88  
    4.89