tuned certify_typ/term;
authorwenzelm
Tue Jun 22 09:51:39 2004 +0200 (2004-06-22 ago)
changeset 14993802f3732a54e
parent 14992 a16bc5abad45
child 14994 7d8501843146
tuned certify_typ/term;
src/Pure/sign.ML
src/Pure/type.ML
src/Pure/type_infer.ML
     1.1 --- a/src/Pure/sign.ML	Tue Jun 22 09:51:23 2004 +0200
     1.2 +++ b/src/Pure/sign.ML	Tue Jun 22 09:51:39 2004 +0200
     1.3 @@ -671,8 +671,8 @@
     1.4  (*read and certify typ wrt a signature*)
     1.5  local
     1.6    fun read_typ_aux rd cert (sg, def_sort) str =
     1.7 -    (#1 (cert (tsig_of sg) (rd (sg, def_sort) str))
     1.8 -      handle TYPE (msg, _, _) => (error_msg msg; err_in_type str));
     1.9 +    cert (tsig_of sg) (rd (sg, def_sort) str)
    1.10 +      handle TYPE (msg, _, _) => (error_msg msg; err_in_type str);
    1.11  in
    1.12    val read_typ          = read_typ_aux read_raw_typ Type.cert_typ;
    1.13    val read_typ_raw      = read_typ_aux read_raw_typ Type.cert_typ_raw;
    1.14 @@ -686,8 +686,8 @@
    1.15  
    1.16  val certify_class = Type.cert_class o tsig_of;
    1.17  val certify_sort = Type.cert_sort o tsig_of;
    1.18 -val certify_typ = #1 oo (Type.cert_typ o tsig_of);
    1.19 -val certify_typ_raw = #1 oo (Type.cert_typ_raw o tsig_of);
    1.20 +val certify_typ = Type.cert_typ o tsig_of;
    1.21 +val certify_typ_raw = Type.cert_typ_raw o tsig_of;
    1.22  
    1.23  fun certify_tyname sg c =
    1.24    if is_some (Symtab.lookup (#types (Type.rep_tsig (tsig_of sg)), c)) then c
    1.25 @@ -702,22 +702,6 @@
    1.26  
    1.27  local
    1.28  
    1.29 -(*certify types of term and compute maxidx*)
    1.30 -fun cert_term_types certT =
    1.31 -  let
    1.32 -    fun cert (Const (a, T)) = let val (T', i) = certT T in (Const (a, T'), i) end
    1.33 -      | cert (Free (a, T)) = let val (T', i) = certT T in (Free (a, T'), i) end
    1.34 -      | cert (Var (xi as (_, i), T)) =
    1.35 -          let val (T', j) = certT T in (Var (xi, T'), Int.max (i, j)) end
    1.36 -      | cert (t as Bound _) = (t, ~1)
    1.37 -      | cert (Abs (a, T, t)) =
    1.38 -          let val (T', i) = certT T and (t', j) = cert t
    1.39 -          in (Abs (a, T', t'), Int.max (i, j)) end
    1.40 -      | cert (t $ u) =
    1.41 -          let val (t', i) = cert t and (u', j) =  cert u
    1.42 -          in (t' $ u', Int.max (i, j)) end;
    1.43 -  in cert end;
    1.44 -
    1.45  (*compute and check type of the term*)
    1.46  fun type_check pp sg tm =
    1.47    let
    1.48 @@ -797,7 +781,7 @@
    1.49    let
    1.50      val _ = check_stale sg;
    1.51  
    1.52 -    val (tm', maxidx) = cert_term_types (Type.cert_typ (tsig_of sg)) tm;
    1.53 +    val tm' = map_term_types (Type.cert_typ (tsig_of sg)) tm;
    1.54      val tm' = if tm = tm' then tm else tm';  (*avoid copying of already normal term*)
    1.55  
    1.56      fun err msg = raise TYPE (msg, [], [tm']);
    1.57 @@ -818,7 +802,7 @@
    1.58    in
    1.59      check_atoms tm';
    1.60      nodup_vars tm';
    1.61 -    (tm', type_check pp sg tm', maxidx)
    1.62 +    (tm', type_check pp sg tm', maxidx_of_term tm')
    1.63    end;
    1.64  
    1.65  end;
    1.66 @@ -1001,8 +985,7 @@
    1.67      raw_consts =
    1.68    let
    1.69      val prep_typ = compress_type o Type.varifyT o Type.no_tvars o
    1.70 -     (if syn_only then #1 o Type.cert_typ_syntax tsig
    1.71 -      else Term.no_dummyT o #1 o Type.cert_typ tsig);
    1.72 +     (if syn_only then Type.cert_typ_syntax tsig else Term.no_dummyT o Type.cert_typ tsig);
    1.73      fun prep_const (c, ty, mx) = (c, prep_typ ty, mx) handle TYPE (msg, _, _) =>
    1.74        (error_msg msg; err_in_const (const_name path c mx));
    1.75  
     2.1 --- a/src/Pure/type.ML	Tue Jun 22 09:51:23 2004 +0200
     2.2 +++ b/src/Pure/type.ML	Tue Jun 22 09:51:39 2004 +0200
     2.3 @@ -32,9 +32,9 @@
     2.4    val cert_class: tsig -> class -> class
     2.5    val cert_sort: tsig -> sort -> sort
     2.6    val witness_sorts: tsig -> sort list -> sort list -> (typ * sort) list
     2.7 -  val cert_typ: tsig -> typ -> typ * int
     2.8 -  val cert_typ_syntax: tsig -> typ -> typ * int
     2.9 -  val cert_typ_raw: tsig -> typ -> typ * int
    2.10 +  val cert_typ: tsig -> typ -> typ
    2.11 +  val cert_typ_syntax: tsig -> typ -> typ
    2.12 +  val cert_typ_raw: tsig -> typ -> typ
    2.13  
    2.14    (*special treatment of type vars*)
    2.15    val strip_sorts: typ -> typ
    2.16 @@ -144,20 +144,15 @@
    2.17  fun bad_nargs t = "Bad number of arguments for type constructor: " ^ quote t;
    2.18  fun undecl_type c = "Undeclared type constructor: " ^ quote c;
    2.19  
    2.20 -local
    2.21 -
    2.22 -fun inst_typ env = Term.map_type_tvar (fn (var as (v, _)) =>
    2.23 -  (case Library.assoc_string_int (env, v) of
    2.24 -    Some U => inst_typ env U
    2.25 -  | None => TVar var));
    2.26 -
    2.27  fun certify_typ normalize syntax tsig ty =
    2.28    let
    2.29      val TSig {classes, types, ...} = tsig;
    2.30      fun err msg = raise TYPE (msg, [ty], []);
    2.31  
    2.32 -    val maxidx = Term.maxidx_of_typ ty;
    2.33 -    val idx = maxidx + 1;
    2.34 +    fun inst_typ env (Type (c, Ts)) = Type (c, map (inst_typ env) Ts)
    2.35 +      | inst_typ env (T as TFree (x, _)) = if_none (Library.assoc_string (env, x)) T
    2.36 +      | inst_typ _ T = T;
    2.37 +
    2.38  
    2.39      val check_syntax =
    2.40        if syntax then K ()
    2.41 @@ -172,28 +167,24 @@
    2.42                Some (LogicalType n, _) => (nargs n; Type (c, Ts'))
    2.43              | Some (Abbreviation (vs, U, syn), _) => (nargs (length vs);
    2.44                  if syn then check_syntax c else ();
    2.45 -                if normalize then
    2.46 -                  inst_typ (map (rpair idx) vs ~~ Ts') (Term.incr_tvar idx U)
    2.47 +                if normalize then inst_typ (vs ~~ Ts') U
    2.48                  else Type (c, Ts'))
    2.49              | Some (Nonterminal, _) => (nargs 0; check_syntax c; T)
    2.50              | None => err (undecl_type c))
    2.51            end
    2.52        | cert (TFree (x, S)) = TFree (x, Sorts.certify_sort classes S)
    2.53        | cert (TVar (xi as (_, i), S)) =
    2.54 -          if i < 0 then err ("Malformed type variable: " ^ quote (Term.string_of_vname xi))
    2.55 +          if i < 0 then
    2.56 +            err ("Malformed type variable: " ^ quote (Term.string_of_vname xi))
    2.57            else TVar (xi, Sorts.certify_sort classes S);
    2.58  
    2.59      val ty' = cert ty;
    2.60 -    val ty' = if ty = ty' then ty else ty';  (*avoid copying of already normal type*)
    2.61 -  in (ty', maxidx) end;  
    2.62 -
    2.63 -in
    2.64 +  in if ty = ty' then ty else ty' end;  (*avoid copying of already normal type*)
    2.65  
    2.66  val cert_typ         = certify_typ true false;
    2.67  val cert_typ_syntax  = certify_typ true true;
    2.68  val cert_typ_raw     = certify_typ false true;
    2.69  
    2.70 -end;
    2.71  
    2.72  
    2.73  (** special treatment of type vars **)
    2.74 @@ -279,15 +270,13 @@
    2.75  
    2.76  (* instantiation *)
    2.77  
    2.78 -fun type_of_sort pp tsig (T, S) =
    2.79 -  if of_sort tsig (T, S) then T
    2.80 -  else raise TYPE ("Type not of sort " ^ Pretty.string_of_sort pp S, [T], []);
    2.81 -
    2.82  fun inst_typ_tvars pp tsig tye =
    2.83    let
    2.84      fun inst (var as (v, S)) =
    2.85        (case assoc_string_int (tye, v) of
    2.86 -        Some U => type_of_sort pp tsig (U, S)
    2.87 +        Some U =>
    2.88 +          if of_sort tsig (U, S) then U
    2.89 +          else raise TYPE ("Type not of sort " ^ Pretty.string_of_sort pp S, [U], [])
    2.90        | None => TVar var);
    2.91    in map_type_tvar inst end;
    2.92  
    2.93 @@ -303,8 +292,9 @@
    2.94    let
    2.95      fun match (subs, (TVar (v, S), T)) =
    2.96            (case Vartab.lookup (subs, v) of
    2.97 -            None => (Vartab.update_new ((v, type_of_sort Pretty.pp_undef tsig (T, S)), subs)
    2.98 -              handle TYPE _ => raise TYPE_MATCH)
    2.99 +            None =>
   2.100 +              if of_sort tsig (T, S) then Vartab.update ((v, T), subs)
   2.101 +              else raise TYPE_MATCH
   2.102            | Some U => if U = T then subs else raise TYPE_MATCH)
   2.103        | match (subs, (Type (a, Ts), Type (b, Us))) =
   2.104            if a <> b then raise TYPE_MATCH
   2.105 @@ -552,7 +542,7 @@
   2.106    let
   2.107      fun err msg =
   2.108        error (msg ^ "\nThe error(s) above occurred in type abbreviation: " ^ quote a);
   2.109 -    val rhs' = strip_sorts (varifyT (no_tvars (#1 (cert_typ_syntax tsig rhs))))
   2.110 +    val rhs' = strip_sorts (no_tvars (cert_typ_syntax tsig rhs))
   2.111        handle TYPE (msg, _, _) => err msg;
   2.112    in
   2.113      (case duplicates vs of
     3.1 --- a/src/Pure/type_infer.ML	Tue Jun 22 09:51:23 2004 +0200
     3.2 +++ b/src/Pure/type_infer.ML	Tue Jun 22 09:51:39 2004 +0200
     3.3 @@ -477,7 +477,7 @@
     3.4      val raw_env = Syntax.raw_term_sorts tm;
     3.5      val sort_of = get_sort tsig def_sort map_sort raw_env;
     3.6  
     3.7 -    val certT = #1 o Type.cert_typ tsig o map_type;
     3.8 +    val certT = Type.cert_typ tsig o map_type;
     3.9      fun decodeT t = certT (Syntax.typ_of_term sort_of map_sort t);
    3.10  
    3.11      fun decode (Const ("_constrain", _) $ t $ typ) =
    3.12 @@ -518,7 +518,7 @@
    3.13      map_const map_type map_sort used freeze pat_Ts raw_ts =
    3.14    let
    3.15      val {classes, arities, ...} = Type.rep_tsig tsig;
    3.16 -    val pat_Ts' = map (#1 o Type.cert_typ tsig) pat_Ts;
    3.17 +    val pat_Ts' = map (Type.cert_typ tsig) pat_Ts;
    3.18      val is_const = is_some o const_type;
    3.19      val raw_ts' =
    3.20        map (decode_types tsig is_const def_type def_sort map_const map_type map_sort) raw_ts;