tuned certify_typ/term;

--- a/src/Pure/sign.ML	Tue Jun 22 09:51:23 2004 +0200
+++ b/src/Pure/sign.ML	Tue Jun 22 09:51:39 2004 +0200
@@ -671,8 +671,8 @@
 (*read and certify typ wrt a signature*)
 local
   fun read_typ_aux rd cert (sg, def_sort) str =
-    (#1 (cert (tsig_of sg) (rd (sg, def_sort) str))
-      handle TYPE (msg, _, _) => (error_msg msg; err_in_type str));
+    cert (tsig_of sg) (rd (sg, def_sort) str)
+      handle TYPE (msg, _, _) => (error_msg msg; err_in_type str);
 in
   val read_typ          = read_typ_aux read_raw_typ Type.cert_typ;
   val read_typ_raw      = read_typ_aux read_raw_typ Type.cert_typ_raw;
@@ -686,8 +686,8 @@
 
 val certify_class = Type.cert_class o tsig_of;
 val certify_sort = Type.cert_sort o tsig_of;
-val certify_typ = #1 oo (Type.cert_typ o tsig_of);
-val certify_typ_raw = #1 oo (Type.cert_typ_raw o tsig_of);
+val certify_typ = Type.cert_typ o tsig_of;
+val certify_typ_raw = Type.cert_typ_raw o tsig_of;
 
 fun certify_tyname sg c =
   if is_some (Symtab.lookup (#types (Type.rep_tsig (tsig_of sg)), c)) then c
@@ -702,22 +702,6 @@
 
 local
 
-(*certify types of term and compute maxidx*)
-fun cert_term_types certT =
-  let
-    fun cert (Const (a, T)) = let val (T', i) = certT T in (Const (a, T'), i) end
-      | cert (Free (a, T)) = let val (T', i) = certT T in (Free (a, T'), i) end
-      | cert (Var (xi as (_, i), T)) =
-          let val (T', j) = certT T in (Var (xi, T'), Int.max (i, j)) end
-      | cert (t as Bound _) = (t, ~1)
-      | cert (Abs (a, T, t)) =
-          let val (T', i) = certT T and (t', j) = cert t
-          in (Abs (a, T', t'), Int.max (i, j)) end
-      | cert (t $ u) =
-          let val (t', i) = cert t and (u', j) =  cert u
-          in (t' $ u', Int.max (i, j)) end;
-  in cert end;
-
 (*compute and check type of the term*)
 fun type_check pp sg tm =
   let
@@ -797,7 +781,7 @@
   let
     val _ = check_stale sg;
 
-    val (tm', maxidx) = cert_term_types (Type.cert_typ (tsig_of sg)) tm;
+    val tm' = map_term_types (Type.cert_typ (tsig_of sg)) tm;
     val tm' = if tm = tm' then tm else tm';  (*avoid copying of already normal term*)
 
     fun err msg = raise TYPE (msg, [], [tm']);
@@ -818,7 +802,7 @@
   in
     check_atoms tm';
     nodup_vars tm';
-    (tm', type_check pp sg tm', maxidx)
+    (tm', type_check pp sg tm', maxidx_of_term tm')
   end;
 
 end;
@@ -1001,8 +985,7 @@
     raw_consts =
   let
     val prep_typ = compress_type o Type.varifyT o Type.no_tvars o
-     (if syn_only then #1 o Type.cert_typ_syntax tsig
-      else Term.no_dummyT o #1 o Type.cert_typ tsig);
+     (if syn_only then Type.cert_typ_syntax tsig else Term.no_dummyT o Type.cert_typ tsig);
     fun prep_const (c, ty, mx) = (c, prep_typ ty, mx) handle TYPE (msg, _, _) =>
       (error_msg msg; err_in_const (const_name path c mx));
 

--- a/src/Pure/type.ML	Tue Jun 22 09:51:23 2004 +0200
+++ b/src/Pure/type.ML	Tue Jun 22 09:51:39 2004 +0200
@@ -32,9 +32,9 @@
   val cert_class: tsig -> class -> class
   val cert_sort: tsig -> sort -> sort
   val witness_sorts: tsig -> sort list -> sort list -> (typ * sort) list
-  val cert_typ: tsig -> typ -> typ * int
-  val cert_typ_syntax: tsig -> typ -> typ * int
-  val cert_typ_raw: tsig -> typ -> typ * int
+  val cert_typ: tsig -> typ -> typ
+  val cert_typ_syntax: tsig -> typ -> typ
+  val cert_typ_raw: tsig -> typ -> typ
 
   (*special treatment of type vars*)
   val strip_sorts: typ -> typ
@@ -144,20 +144,15 @@
 fun bad_nargs t = "Bad number of arguments for type constructor: " ^ quote t;
 fun undecl_type c = "Undeclared type constructor: " ^ quote c;
 
-local
-
-fun inst_typ env = Term.map_type_tvar (fn (var as (v, _)) =>
-  (case Library.assoc_string_int (env, v) of
-    Some U => inst_typ env U
-  | None => TVar var));
-
 fun certify_typ normalize syntax tsig ty =
   let
     val TSig {classes, types, ...} = tsig;
     fun err msg = raise TYPE (msg, [ty], []);
 
-    val maxidx = Term.maxidx_of_typ ty;
-    val idx = maxidx + 1;
+    fun inst_typ env (Type (c, Ts)) = Type (c, map (inst_typ env) Ts)
+      | inst_typ env (T as TFree (x, _)) = if_none (Library.assoc_string (env, x)) T
+      | inst_typ _ T = T;
+
 
     val check_syntax =
       if syntax then K ()
@@ -172,28 +167,24 @@
               Some (LogicalType n, _) => (nargs n; Type (c, Ts'))
             | Some (Abbreviation (vs, U, syn), _) => (nargs (length vs);
                 if syn then check_syntax c else ();
-                if normalize then
-                  inst_typ (map (rpair idx) vs ~~ Ts') (Term.incr_tvar idx U)
+                if normalize then inst_typ (vs ~~ Ts') U
                 else Type (c, Ts'))
             | Some (Nonterminal, _) => (nargs 0; check_syntax c; T)
             | None => err (undecl_type c))
           end
       | cert (TFree (x, S)) = TFree (x, Sorts.certify_sort classes S)
       | cert (TVar (xi as (_, i), S)) =
-          if i < 0 then err ("Malformed type variable: " ^ quote (Term.string_of_vname xi))
+          if i < 0 then
+            err ("Malformed type variable: " ^ quote (Term.string_of_vname xi))
           else TVar (xi, Sorts.certify_sort classes S);
 
     val ty' = cert ty;
-    val ty' = if ty = ty' then ty else ty';  (*avoid copying of already normal type*)
-  in (ty', maxidx) end;  
-
-in
+  in if ty = ty' then ty else ty' end;  (*avoid copying of already normal type*)
 
 val cert_typ         = certify_typ true false;
 val cert_typ_syntax  = certify_typ true true;
 val cert_typ_raw     = certify_typ false true;
 
-end;
 
 
 (** special treatment of type vars **)
@@ -279,15 +270,13 @@
 
 (* instantiation *)
 
-fun type_of_sort pp tsig (T, S) =
-  if of_sort tsig (T, S) then T
-  else raise TYPE ("Type not of sort " ^ Pretty.string_of_sort pp S, [T], []);
-
 fun inst_typ_tvars pp tsig tye =
   let
     fun inst (var as (v, S)) =
       (case assoc_string_int (tye, v) of
-        Some U => type_of_sort pp tsig (U, S)
+        Some U =>
+          if of_sort tsig (U, S) then U
+          else raise TYPE ("Type not of sort " ^ Pretty.string_of_sort pp S, [U], [])
       | None => TVar var);
   in map_type_tvar inst end;
 
@@ -303,8 +292,9 @@
   let
     fun match (subs, (TVar (v, S), T)) =
           (case Vartab.lookup (subs, v) of
-            None => (Vartab.update_new ((v, type_of_sort Pretty.pp_undef tsig (T, S)), subs)
-              handle TYPE _ => raise TYPE_MATCH)
+            None =>
+              if of_sort tsig (T, S) then Vartab.update ((v, T), subs)
+              else raise TYPE_MATCH
           | Some U => if U = T then subs else raise TYPE_MATCH)
       | match (subs, (Type (a, Ts), Type (b, Us))) =
           if a <> b then raise TYPE_MATCH
@@ -552,7 +542,7 @@
   let
     fun err msg =
       error (msg ^ "\nThe error(s) above occurred in type abbreviation: " ^ quote a);
-    val rhs' = strip_sorts (varifyT (no_tvars (#1 (cert_typ_syntax tsig rhs))))
+    val rhs' = strip_sorts (no_tvars (cert_typ_syntax tsig rhs))
       handle TYPE (msg, _, _) => err msg;
   in
     (case duplicates vs of

--- a/src/Pure/type_infer.ML	Tue Jun 22 09:51:23 2004 +0200
+++ b/src/Pure/type_infer.ML	Tue Jun 22 09:51:39 2004 +0200
@@ -477,7 +477,7 @@
     val raw_env = Syntax.raw_term_sorts tm;
     val sort_of = get_sort tsig def_sort map_sort raw_env;
 
-    val certT = #1 o Type.cert_typ tsig o map_type;
+    val certT = Type.cert_typ tsig o map_type;
     fun decodeT t = certT (Syntax.typ_of_term sort_of map_sort t);
 
     fun decode (Const ("_constrain", _) $ t $ typ) =
@@ -518,7 +518,7 @@
     map_const map_type map_sort used freeze pat_Ts raw_ts =
   let
     val {classes, arities, ...} = Type.rep_tsig tsig;
-    val pat_Ts' = map (#1 o Type.cert_typ tsig) pat_Ts;
+    val pat_Ts' = map (Type.cert_typ tsig) pat_Ts;
     val is_const = is_some o const_type;
     val raw_ts' =
       map (decode_types tsig is_const def_type def_sort map_const map_type map_sort) raw_ts;