tuned certify_typ;
authorwenzelm
Mon Jun 21 16:40:55 2004 +0200 (2004-06-21)
changeset 149895a5d076a9863
parent 14988 973ced82812d
child 14990 582b655da757
tuned certify_typ;
src/Pure/type.ML
     1.1 --- a/src/Pure/type.ML	Mon Jun 21 16:40:44 2004 +0200
     1.2 +++ b/src/Pure/type.ML	Mon Jun 21 16:40:55 2004 +0200
     1.3 @@ -11,7 +11,7 @@
     1.4    (*type signatures and certified types*)
     1.5    datatype decl =
     1.6      LogicalType of int |
     1.7 -    Abbreviation of string list * typ |
     1.8 +    Abbreviation of string list * typ * bool |
     1.9      Nonterminal
    1.10    type tsig
    1.11    val rep_tsig: tsig ->
    1.12 @@ -32,9 +32,9 @@
    1.13    val cert_class: tsig -> class -> class
    1.14    val cert_sort: tsig -> sort -> sort
    1.15    val witness_sorts: tsig -> sort list -> sort list -> (typ * sort) list
    1.16 -  val cert_typ: tsig -> typ -> typ
    1.17 -  val cert_typ_syntax: tsig -> typ -> typ
    1.18 -  val cert_typ_raw: tsig -> typ -> typ
    1.19 +  val cert_typ: tsig -> typ -> typ * int
    1.20 +  val cert_typ_syntax: tsig -> typ -> typ * int
    1.21 +  val cert_typ_raw: tsig -> typ -> typ * int
    1.22  
    1.23    (*special treatment of type vars*)
    1.24    val strip_sorts: typ -> typ
    1.25 @@ -75,7 +75,7 @@
    1.26  
    1.27  datatype decl =
    1.28    LogicalType of int |
    1.29 -  Abbreviation of string list * typ |
    1.30 +  Abbreviation of string list * typ * bool |
    1.31    Nonterminal;
    1.32  
    1.33  fun str_of_decl (LogicalType _) = "logical type constructor"
    1.34 @@ -131,13 +131,9 @@
    1.35  fun eq_sort (TSig {classes, ...}) = Sorts.sort_eq classes;
    1.36  fun subsort (TSig {classes, ...}) = Sorts.sort_le classes;
    1.37  fun of_sort (TSig {classes, arities, ...}) = Sorts.of_sort (classes, arities);
    1.38 -fun norm_sort (TSig {classes, ...}) = Sorts.norm_sort classes;
    1.39  
    1.40 -fun cert_class (TSig {classes, ...}) c =
    1.41 -  if can (Graph.get_node classes) c then c
    1.42 -  else raise TYPE ("Undeclared class: " ^ quote c, [], []);
    1.43 -
    1.44 -fun cert_sort tsig = norm_sort tsig o map (cert_class tsig);
    1.45 +fun cert_class (TSig {classes, ...}) = Sorts.certify_class classes;
    1.46 +fun cert_sort (TSig {classes, ...}) = Sorts.certify_sort classes;
    1.47  
    1.48  fun witness_sorts (tsig as TSig {classes, arities, log_types, ...}) =
    1.49    Sorts.witness_sorts (classes, arities) log_types;
    1.50 @@ -150,61 +146,46 @@
    1.51  
    1.52  local
    1.53  
    1.54 -fun inst_typ tye =
    1.55 -  let
    1.56 -    fun inst (var as (v, _)) =
    1.57 -      (case assoc_string_int (tye, v) of
    1.58 -        Some U => inst_typ tye U
    1.59 -      | None => TVar var);
    1.60 -  in map_type_tvar inst end;
    1.61 -
    1.62 -fun norm_typ (tsig as TSig {types, ...}) ty =
    1.63 -  let
    1.64 -    val idx = Term.maxidx_of_typ ty + 1;
    1.65 -
    1.66 -    fun norm (Type (a, Ts)) =
    1.67 -          (case Symtab.lookup (types, a) of
    1.68 -            Some (Abbreviation (vs, U), _) =>
    1.69 -              norm (inst_typ (map (rpair idx) vs ~~ Ts) (incr_tvar idx U))
    1.70 -          | _ => Type (a, map norm Ts))
    1.71 -      | norm (TFree (x, S)) = TFree (x, norm_sort tsig S)
    1.72 -      | norm (TVar (xi, S)) = TVar (xi, norm_sort tsig S);
    1.73 -
    1.74 -    val ty' = norm ty;
    1.75 -  in if ty = ty' then ty else ty' end;  (*avoid copying of already normal type*)
    1.76 +fun inst_typ env = Term.map_type_tvar (fn (var as (v, _)) =>
    1.77 +  (case Library.assoc_string_int (env, v) of
    1.78 +    Some U => inst_typ env U
    1.79 +  | None => TVar var));
    1.80  
    1.81  fun certify_typ normalize syntax tsig ty =
    1.82    let
    1.83 -    val TSig {types, ...} = tsig;
    1.84 +    val TSig {classes, types, ...} = tsig;
    1.85      fun err msg = raise TYPE (msg, [ty], []);
    1.86  
    1.87 -    fun check_sort S = (map (cert_class tsig) S; ());
    1.88 +    val maxidx = Term.maxidx_of_typ ty;
    1.89 +    val idx = maxidx + 1;
    1.90  
    1.91 -    fun check_typ (Type (c, Ts)) =
    1.92 -          let fun nargs n = if length Ts <> n then err (bad_nargs c) else () in
    1.93 +    val check_syntax =
    1.94 +      if syntax then K ()
    1.95 +      else fn c => err ("Illegal occurrence of syntactic type: " ^ quote c);
    1.96 +
    1.97 +    fun cert (T as Type (c, Ts)) =
    1.98 +          let
    1.99 +            val Ts' = map cert Ts;
   1.100 +            fun nargs n = if length Ts <> n then err (bad_nargs c) else ();
   1.101 +          in
   1.102              (case Symtab.lookup (types, c) of
   1.103 -              Some (LogicalType n, _) => nargs n
   1.104 -            | Some (Abbreviation (vs, _), _) => nargs (length vs)
   1.105 -            | Some (Nonterminal, _) => nargs 0
   1.106 -            | None => err (undecl_type c));
   1.107 -            seq check_typ Ts
   1.108 +              Some (LogicalType n, _) => (nargs n; Type (c, Ts'))
   1.109 +            | Some (Abbreviation (vs, U, syn), _) => (nargs (length vs);
   1.110 +                if syn then check_syntax c else ();
   1.111 +                if normalize then
   1.112 +                  inst_typ (map (rpair idx) vs ~~ Ts') (Term.incr_tvar idx U)
   1.113 +                else Type (c, Ts'))
   1.114 +            | Some (Nonterminal, _) => (nargs 0; check_syntax c; T)
   1.115 +            | None => err (undecl_type c))
   1.116            end
   1.117 -    | check_typ (TFree (_, S)) = check_sort S
   1.118 -    | check_typ (TVar ((x, i), S)) =
   1.119 -        if i < 0 then err ("Malformed type variable: " ^ quote (Term.string_of_vname (x, i)))
   1.120 -        else check_sort S;
   1.121 +      | cert (TFree (x, S)) = TFree (x, Sorts.certify_sort classes S)
   1.122 +      | cert (TVar (xi as (_, i), S)) =
   1.123 +          if i < 0 then err ("Malformed type variable: " ^ quote (Term.string_of_vname xi))
   1.124 +          else TVar (xi, Sorts.certify_sort classes S);
   1.125  
   1.126 -    fun no_syntax (Type (c, Ts)) =
   1.127 -          (case Symtab.lookup (types, c) of
   1.128 -            Some (Nonterminal, _) =>
   1.129 -              err ("Illegal occurrence of syntactic type: " ^ quote c)
   1.130 -          | _ => seq no_syntax Ts)
   1.131 -      | no_syntax _ = ();
   1.132 -
   1.133 -    val _ = check_typ ty;
   1.134 -    val ty' = if normalize orelse not syntax then norm_typ tsig ty else ty;
   1.135 -    val _ = if not syntax then no_syntax ty' else ();
   1.136 -  in ty' end;
   1.137 +    val ty' = cert ty;
   1.138 +    val ty' = if ty = ty' then ty else ty';  (*avoid copying of already normal type*)
   1.139 +  in (ty', maxidx) end;  
   1.140  
   1.141  in
   1.142  
   1.143 @@ -562,11 +543,16 @@
   1.144  fun change_types f = change_tsig (fn (classes, default, types, arities) =>
   1.145    (classes, default, f types, arities));
   1.146  
   1.147 +fun syntactic types (Type (c, Ts)) =
   1.148 +      (case Symtab.lookup (types, c) of Some (Nonterminal, _) => true | _ => false)
   1.149 +        orelse exists (syntactic types) Ts
   1.150 +  | syntactic _ _ = false;
   1.151 +
   1.152  fun add_abbr (a, vs, rhs) tsig = tsig |> change_types (fn types =>
   1.153    let
   1.154      fun err msg =
   1.155        error (msg ^ "\nThe error(s) above occurred in type abbreviation: " ^ quote a);
   1.156 -    val rhs' = strip_sorts (varifyT (no_tvars (cert_typ_syntax tsig rhs)))
   1.157 +    val rhs' = strip_sorts (varifyT (no_tvars (#1 (cert_typ_syntax tsig rhs))))
   1.158        handle TYPE (msg, _, _) => err msg;
   1.159    in
   1.160      (case duplicates vs of
   1.161 @@ -575,7 +561,7 @@
   1.162      (case gen_rems (op =) (map (#1 o #1) (typ_tvars rhs'), vs) of
   1.163        [] => []
   1.164      | extras => err ("Extra variables on rhs: " ^ commas_quote extras));
   1.165 -    types |> new_decl (a, Abbreviation (vs, rhs'))
   1.166 +    types |> new_decl (a, Abbreviation (vs, rhs', syntactic types rhs'))
   1.167    end);
   1.168  
   1.169  in