removed is_type_abbr;
authorwenzelm
Sun May 21 14:37:17 2000 +0200 (2000-05-21 ago)
changeset 889999266fe189a1
parent 8898 a1ee54500516
child 8900 e9f1cd37cba4
removed is_type_abbr;
src/Pure/type.ML
     1.1 --- a/src/Pure/type.ML	Sun May 21 14:36:29 2000 +0200
     1.2 +++ b/src/Pure/type.ML	Sun May 21 14:37:17 2000 +0200
     1.3 @@ -29,10 +29,11 @@
     1.4    val defaultS: type_sig -> sort
     1.5    val logical_types: type_sig -> string list
     1.6    val univ_witness: type_sig -> (typ * sort) option
     1.7 -  val is_type_abbr: type_sig -> string -> bool
     1.8    val subsort: type_sig -> sort * sort -> bool
     1.9    val eq_sort: type_sig -> sort * sort -> bool
    1.10    val norm_sort: type_sig -> sort -> sort
    1.11 +  val cert_class: type_sig -> class -> class
    1.12 +  val cert_sort: type_sig -> sort -> sort
    1.13    val witness_sorts: type_sig -> sort list -> sort list -> (typ * sort) list
    1.14    val rem_sorts: typ -> typ
    1.15    val tsig0: type_sig
    1.16 @@ -179,7 +180,30 @@
    1.17  fun defaultS (TySg {default, ...}) = default;
    1.18  fun logical_types (TySg {log_types, ...}) = log_types;
    1.19  fun univ_witness (TySg {univ_witness, ...}) = univ_witness;
    1.20 -fun is_type_abbr (TySg {abbrs, ...}) name = is_some (Symtab.lookup (abbrs, name));
    1.21 +
    1.22 +
    1.23 +(* error messages *)
    1.24 +
    1.25 +fun undeclared_class c = "Undeclared class: " ^ quote c;
    1.26 +fun undeclared_classes cs = "Undeclared class(es): " ^ commas_quote cs;
    1.27 +
    1.28 +fun err_undeclared_class s = error (undeclared_class s);
    1.29 +
    1.30 +fun err_dup_classes cs =
    1.31 +  error ("Duplicate declaration of class(es): " ^ commas_quote cs);
    1.32 +
    1.33 +fun undeclared_type c = "Undeclared type constructor: " ^ quote c;
    1.34 +
    1.35 +fun err_neg_args c =
    1.36 +  error ("Negative number of arguments of type constructor: " ^ quote c);
    1.37 +
    1.38 +fun err_dup_tycon c =
    1.39 +  error ("Duplicate declaration of type constructor: " ^ quote c);
    1.40 +
    1.41 +fun dup_tyabbrs ts =
    1.42 +  "Duplicate declaration of type abbreviation(s): " ^ commas_quote ts;
    1.43 +
    1.44 +fun ty_confl c = "Conflicting type constructor and abbreviation: " ^ quote c;
    1.45  
    1.46  
    1.47  (* sorts *)
    1.48 @@ -188,6 +212,11 @@
    1.49  fun eq_sort (TySg {classrel, ...}) = Sorts.sort_eq classrel;
    1.50  fun norm_sort (TySg {classrel, ...}) = Sorts.norm_sort classrel;
    1.51  
    1.52 +fun cert_class (TySg {classes, ...}) c =
    1.53 +  if c mem_string classes then c else raise TYPE (undeclared_class c, [], []);
    1.54 +
    1.55 +fun cert_sort tsig S = norm_sort tsig (map (cert_class tsig) S);
    1.56 +
    1.57  fun witness_sorts (tsig as TySg {classrel, arities, log_types, ...}) =
    1.58    Sorts.witness_sorts (classrel, arities, log_types);
    1.59  
    1.60 @@ -196,36 +225,14 @@
    1.61    | rem_sorts (TVar (xi, _)) = TVar (xi, []);
    1.62  
    1.63  
    1.64 -(* error messages *)
    1.65 -
    1.66 -fun undcl_class c = "Undeclared class " ^ quote c;
    1.67 -fun err_undcl_class s = error (undcl_class s);
    1.68 -
    1.69 -fun err_dup_classes cs =
    1.70 -  error ("Duplicate declaration of class(es) " ^ commas_quote cs);
    1.71 -
    1.72 -fun undcl_type c = "Undeclared type constructor " ^ quote c;
    1.73 -
    1.74 -fun err_neg_args c =
    1.75 -  error ("Negative number of arguments of type constructor " ^ quote c);
    1.76 -
    1.77 -fun err_dup_tycon c =
    1.78 -  error ("Duplicate declaration of type constructor " ^ quote c);
    1.79 -
    1.80 -fun dup_tyabbrs ts =
    1.81 -  "Duplicate declaration of type abbreviation(s) " ^ commas_quote ts;
    1.82 -
    1.83 -fun ty_confl c = "Conflicting type constructor and abbreviation " ^ quote c;
    1.84 -
    1.85 -
    1.86 -(* FIXME err_undcl_class! *)
    1.87 +(* FIXME err_undeclared_class! *)
    1.88  (* 'leq' checks the partial order on classes according to the
    1.89     statements in classrel 'a'
    1.90  *)
    1.91  
    1.92  fun less a (C, D) = case Symtab.lookup (a, C) of
    1.93       Some ss => D mem_string ss
    1.94 -   | None => err_undcl_class C;
    1.95 +   | None => err_undeclared_class C;
    1.96  
    1.97  fun leq a (C, D)  =  C = D orelse less a (C, D);
    1.98  
    1.99 @@ -317,7 +324,7 @@
   1.100  
   1.101      fun class_err (errs, c) =
   1.102        if c mem_string classes then errs
   1.103 -      else undcl_class c ins_string errs;
   1.104 +      else undeclared_class c ins_string errs;
   1.105  
   1.106      val sort_err = foldl class_err;
   1.107  
   1.108 @@ -333,7 +340,7 @@
   1.109              | None =>
   1.110                  (case Symtab.lookup (abbrs, c) of
   1.111                    Some (vs, _) => nargs (length vs)
   1.112 -                | None => undcl_type c ins_string errs))
   1.113 +                | None => undeclared_type c ins_string errs))
   1.114            end
   1.115      | typ_errs (errs, TFree (_, S)) = sort_err (errs, S)
   1.116      | typ_errs (errs, TVar ((x, i), S)) =
   1.117 @@ -343,9 +350,9 @@
   1.118    in typ_errs (errors, typ) end;
   1.119  
   1.120  
   1.121 -(* cert_typ *)
   1.122 +(* cert_typ *)           (*exception TYPE*)
   1.123  
   1.124 -(*check and normalize typ wrt. tsig*)           (*exception TYPE*)
   1.125 +(*check and normalize type wrt tsig*)
   1.126  fun cert_typ tsig T =
   1.127    (case typ_errors tsig (T, []) of
   1.128      [] => norm_typ tsig T
   1.129 @@ -502,7 +509,7 @@
   1.130                             else Symtab.update ((s, sups union_string ges'), classrel)
   1.131             | None => classrel
   1.132          end
   1.133 -      else err_undcl_class s'
   1.134 +      else err_undeclared_class s'
   1.135    in foldl upd (Symtab.update ((s, ges), classrel), ges) end;
   1.136  
   1.137  
   1.138 @@ -627,7 +634,7 @@
   1.139     the 'arities' association list of the given type signatrure  *)
   1.140  
   1.141  fun coregular (classes, classrel, tycons) =
   1.142 -  let fun ex C = if C mem_string classes then () else err_undcl_class(C);
   1.143 +  let fun ex C = if C mem_string classes then () else err_undeclared_class(C);
   1.144  
   1.145        fun addar(arities, (t, (w, C))) = case Symtab.lookup (tycons, t) of
   1.146              Some(n) => if n <> length w then varying_decls(t) else
   1.147 @@ -635,7 +642,7 @@
   1.148                        let val ars = the (Symtab.lookup (arities, t))
   1.149                            val ars' = add_arity classrel ars (t,(C,w))
   1.150                        in Symtab.update ((t,ars'), arities) end)
   1.151 -          | None => error (undcl_type t);
   1.152 +          | None => error (undeclared_type t);
   1.153  
   1.154    in addar end;
   1.155