tsig: removed unnecessary universal witness;
authorwenzelm
Sun Apr 13 16:40:07 2008 +0200 (2008-04-13)
changeset 26641cf67665296c2
parent 26640 92e6d3ec91bd
child 26642 454d11701fa4
tsig: removed unnecessary universal witness;
Sorts.class_error: produce message only (formerly msg_class_error);
src/Pure/type.ML
     1.1 --- a/src/Pure/type.ML	Sun Apr 13 16:40:06 2008 +0200
     1.2 +++ b/src/Pure/type.ML	Sun Apr 13 16:40:07 2008 +0200
     1.3 @@ -18,12 +18,10 @@
     1.4     {classes: NameSpace.T * Sorts.algebra,
     1.5      default: sort,
     1.6      types: (decl * serial) NameSpace.table,
     1.7 -    log_types: string list,
     1.8 -    witness: (typ * sort) option}
     1.9 +    log_types: string list}
    1.10    val empty_tsig: tsig
    1.11    val defaultS: tsig -> sort
    1.12    val logical_types: tsig -> string list
    1.13 -  val universal_witness: tsig -> (typ * sort) option
    1.14    val eq_sort: tsig -> sort * sort -> bool
    1.15    val subsort: tsig -> sort * sort -> bool
    1.16    val of_sort: tsig -> typ * sort -> bool
    1.17 @@ -107,26 +105,21 @@
    1.18      classes: NameSpace.T * Sorts.algebra,   (*order-sorted algebra of type classes*)
    1.19      default: sort,                          (*default sort on input*)
    1.20      types: (decl * serial) NameSpace.table, (*declared types*)
    1.21 -    log_types: string list,                 (*logical types sorted by number of arguments*)
    1.22 -    witness: (typ * sort) option};          (*witness for non-emptiness of strictest sort*)
    1.23 +    log_types: string list};                (*logical types sorted by number of arguments*)
    1.24  
    1.25  fun rep_tsig (TSig comps) = comps;
    1.26  
    1.27 -fun make_tsig (classes, default, types, log_types, witness) =
    1.28 -  TSig {classes = classes, default = default, types = types,
    1.29 -    log_types = log_types, witness = witness};
    1.30 +fun make_tsig (classes, default, types, log_types) =
    1.31 +  TSig {classes = classes, default = default, types = types, log_types = log_types};
    1.32  
    1.33  fun build_tsig ((space, classes), default, types) =
    1.34    let
    1.35      val log_types =
    1.36        Symtab.fold (fn (c, (LogicalType n, _)) => cons (c, n) | _ => I) (snd types) []
    1.37        |> Library.sort (Library.int_ord o pairself snd) |> map fst;
    1.38 -    val witness =
    1.39 -      (case Sorts.witness_sorts classes log_types [] [Sorts.minimal_classes classes] of
    1.40 -        [w] => SOME w | _ => NONE);
    1.41 -  in make_tsig ((space, classes), default, types, log_types, witness) end;
    1.42 +  in make_tsig ((space, classes), default, types, log_types) end;
    1.43  
    1.44 -fun map_tsig f (TSig {classes, default, types, log_types = _, witness = _}) =
    1.45 +fun map_tsig f (TSig {classes, default, types, log_types = _}) =
    1.46    build_tsig (f (classes, default, types));
    1.47  
    1.48  val empty_tsig =
    1.49 @@ -137,7 +130,6 @@
    1.50  
    1.51  fun defaultS (TSig {default, ...}) = default;
    1.52  fun logical_types (TSig {log_types, ...}) = log_types;
    1.53 -fun universal_witness (TSig {witness, ...}) = witness;
    1.54  
    1.55  fun eq_sort (TSig {classes, ...}) = Sorts.sort_eq (#2 classes);
    1.56  fun subsort (TSig {classes, ...}) = Sorts.sort_le (#2 classes);
    1.57 @@ -230,7 +222,7 @@
    1.58  
    1.59  fun arity_sorts _ tsig a [] = replicate (arity_number tsig a) []
    1.60    | arity_sorts pp (TSig {classes, ...}) a S = Sorts.mg_domain (#2 classes) a S
    1.61 -      handle Sorts.CLASS_ERROR err => Sorts.class_error pp err;
    1.62 +      handle Sorts.CLASS_ERROR err => error (Sorts.class_error pp err);
    1.63  
    1.64  
    1.65  
    1.66 @@ -391,7 +383,7 @@
    1.67  
    1.68  exception TUNIFY;
    1.69  
    1.70 -(*occurs_check*)
    1.71 +(*occurs check*)
    1.72  fun occurs v tye =
    1.73    let
    1.74      fun occ (Type (_, Ts)) = exists occ Ts
    1.75 @@ -625,9 +617,9 @@
    1.76  fun merge_tsigs pp (tsig1, tsig2) =
    1.77    let
    1.78      val (TSig {classes = (space1, classes1), default = default1, types = types1,
    1.79 -      log_types = _, witness = _}) = tsig1;
    1.80 +      log_types = _}) = tsig1;
    1.81      val (TSig {classes = (space2, classes2), default = default2, types = types2,
    1.82 -      log_types = _, witness = _}) = tsig2;
    1.83 +      log_types = _}) = tsig2;
    1.84  
    1.85      val space' = NameSpace.merge (space1, space2);
    1.86      val classes' = Sorts.merge_algebra pp (classes1, classes2);