src/Pure/type.ML
changeset 14993 802f3732a54e
parent 14989 5a5d076a9863
child 14998 9606c6224933
     1.1 --- a/src/Pure/type.ML	Tue Jun 22 09:51:23 2004 +0200
     1.2 +++ b/src/Pure/type.ML	Tue Jun 22 09:51:39 2004 +0200
     1.3 @@ -32,9 +32,9 @@
     1.4    val cert_class: tsig -> class -> class
     1.5    val cert_sort: tsig -> sort -> sort
     1.6    val witness_sorts: tsig -> sort list -> sort list -> (typ * sort) list
     1.7 -  val cert_typ: tsig -> typ -> typ * int
     1.8 -  val cert_typ_syntax: tsig -> typ -> typ * int
     1.9 -  val cert_typ_raw: tsig -> typ -> typ * int
    1.10 +  val cert_typ: tsig -> typ -> typ
    1.11 +  val cert_typ_syntax: tsig -> typ -> typ
    1.12 +  val cert_typ_raw: tsig -> typ -> typ
    1.13  
    1.14    (*special treatment of type vars*)
    1.15    val strip_sorts: typ -> typ
    1.16 @@ -144,20 +144,15 @@
    1.17  fun bad_nargs t = "Bad number of arguments for type constructor: " ^ quote t;
    1.18  fun undecl_type c = "Undeclared type constructor: " ^ quote c;
    1.19  
    1.20 -local
    1.21 -
    1.22 -fun inst_typ env = Term.map_type_tvar (fn (var as (v, _)) =>
    1.23 -  (case Library.assoc_string_int (env, v) of
    1.24 -    Some U => inst_typ env U
    1.25 -  | None => TVar var));
    1.26 -
    1.27  fun certify_typ normalize syntax tsig ty =
    1.28    let
    1.29      val TSig {classes, types, ...} = tsig;
    1.30      fun err msg = raise TYPE (msg, [ty], []);
    1.31  
    1.32 -    val maxidx = Term.maxidx_of_typ ty;
    1.33 -    val idx = maxidx + 1;
    1.34 +    fun inst_typ env (Type (c, Ts)) = Type (c, map (inst_typ env) Ts)
    1.35 +      | inst_typ env (T as TFree (x, _)) = if_none (Library.assoc_string (env, x)) T
    1.36 +      | inst_typ _ T = T;
    1.37 +
    1.38  
    1.39      val check_syntax =
    1.40        if syntax then K ()
    1.41 @@ -172,28 +167,24 @@
    1.42                Some (LogicalType n, _) => (nargs n; Type (c, Ts'))
    1.43              | Some (Abbreviation (vs, U, syn), _) => (nargs (length vs);
    1.44                  if syn then check_syntax c else ();
    1.45 -                if normalize then
    1.46 -                  inst_typ (map (rpair idx) vs ~~ Ts') (Term.incr_tvar idx U)
    1.47 +                if normalize then inst_typ (vs ~~ Ts') U
    1.48                  else Type (c, Ts'))
    1.49              | Some (Nonterminal, _) => (nargs 0; check_syntax c; T)
    1.50              | None => err (undecl_type c))
    1.51            end
    1.52        | cert (TFree (x, S)) = TFree (x, Sorts.certify_sort classes S)
    1.53        | cert (TVar (xi as (_, i), S)) =
    1.54 -          if i < 0 then err ("Malformed type variable: " ^ quote (Term.string_of_vname xi))
    1.55 +          if i < 0 then
    1.56 +            err ("Malformed type variable: " ^ quote (Term.string_of_vname xi))
    1.57            else TVar (xi, Sorts.certify_sort classes S);
    1.58  
    1.59      val ty' = cert ty;
    1.60 -    val ty' = if ty = ty' then ty else ty';  (*avoid copying of already normal type*)
    1.61 -  in (ty', maxidx) end;  
    1.62 -
    1.63 -in
    1.64 +  in if ty = ty' then ty else ty' end;  (*avoid copying of already normal type*)
    1.65  
    1.66  val cert_typ         = certify_typ true false;
    1.67  val cert_typ_syntax  = certify_typ true true;
    1.68  val cert_typ_raw     = certify_typ false true;
    1.69  
    1.70 -end;
    1.71  
    1.72  
    1.73  (** special treatment of type vars **)
    1.74 @@ -279,15 +270,13 @@
    1.75  
    1.76  (* instantiation *)
    1.77  
    1.78 -fun type_of_sort pp tsig (T, S) =
    1.79 -  if of_sort tsig (T, S) then T
    1.80 -  else raise TYPE ("Type not of sort " ^ Pretty.string_of_sort pp S, [T], []);
    1.81 -
    1.82  fun inst_typ_tvars pp tsig tye =
    1.83    let
    1.84      fun inst (var as (v, S)) =
    1.85        (case assoc_string_int (tye, v) of
    1.86 -        Some U => type_of_sort pp tsig (U, S)
    1.87 +        Some U =>
    1.88 +          if of_sort tsig (U, S) then U
    1.89 +          else raise TYPE ("Type not of sort " ^ Pretty.string_of_sort pp S, [U], [])
    1.90        | None => TVar var);
    1.91    in map_type_tvar inst end;
    1.92  
    1.93 @@ -303,8 +292,9 @@
    1.94    let
    1.95      fun match (subs, (TVar (v, S), T)) =
    1.96            (case Vartab.lookup (subs, v) of
    1.97 -            None => (Vartab.update_new ((v, type_of_sort Pretty.pp_undef tsig (T, S)), subs)
    1.98 -              handle TYPE _ => raise TYPE_MATCH)
    1.99 +            None =>
   1.100 +              if of_sort tsig (T, S) then Vartab.update ((v, T), subs)
   1.101 +              else raise TYPE_MATCH
   1.102            | Some U => if U = T then subs else raise TYPE_MATCH)
   1.103        | match (subs, (Type (a, Ts), Type (b, Us))) =
   1.104            if a <> b then raise TYPE_MATCH
   1.105 @@ -552,7 +542,7 @@
   1.106    let
   1.107      fun err msg =
   1.108        error (msg ^ "\nThe error(s) above occurred in type abbreviation: " ^ quote a);
   1.109 -    val rhs' = strip_sorts (varifyT (no_tvars (#1 (cert_typ_syntax tsig rhs))))
   1.110 +    val rhs' = strip_sorts (no_tvars (cert_typ_syntax tsig rhs))
   1.111        handle TYPE (msg, _, _) => err msg;
   1.112    in
   1.113      (case duplicates vs of