src/Pure/type.ML
changeset 19642 ea7162f84677
parent 19579 b802d1804b77
child 19694 08894a78400b
     1.1 --- a/src/Pure/type.ML	Tue May 16 13:01:23 2006 +0200
     1.2 +++ b/src/Pure/type.ML	Tue May 16 13:01:24 2006 +0200
     1.3 @@ -15,14 +15,12 @@
     1.4      Nonterminal
     1.5    type tsig
     1.6    val rep_tsig: tsig ->
     1.7 -   {classes: NameSpace.T * Sorts.classes,
     1.8 +   {classes: NameSpace.T * Sorts.algebra,
     1.9      default: sort,
    1.10      types: (decl * stamp) NameSpace.table,
    1.11 -    arities: Sorts.arities,
    1.12      log_types: string list,
    1.13      witness: (typ * sort) option}
    1.14    val empty_tsig: tsig
    1.15 -  val classes: tsig -> class list
    1.16    val defaultS: tsig -> sort
    1.17    val logical_types: tsig -> string list
    1.18    val universal_witness: tsig -> (typ * sort) option
    1.19 @@ -98,57 +96,51 @@
    1.20  
    1.21  datatype tsig =
    1.22    TSig of {
    1.23 -    classes: NameSpace.T * Sorts.classes,   (*declared classes with proper subclass relation*)
    1.24 +    classes: NameSpace.T * Sorts.algebra,   (*order-sorted algebra of type classes*)
    1.25      default: sort,                          (*default sort on input*)
    1.26      types: (decl * stamp) NameSpace.table,  (*declared types*)
    1.27 -    arities: Sorts.arities,                 (*image specification of types wrt. sorts*)
    1.28      log_types: string list,                 (*logical types sorted by number of arguments*)
    1.29      witness: (typ * sort) option};          (*witness for non-emptiness of strictest sort*)
    1.30  
    1.31  fun rep_tsig (TSig comps) = comps;
    1.32  
    1.33 -fun make_tsig (classes, default, types, arities, log_types, witness) =
    1.34 -  TSig {classes = classes, default = default, types = types, arities = arities,
    1.35 +fun make_tsig (classes, default, types, log_types, witness) =
    1.36 +  TSig {classes = classes, default = default, types = types,
    1.37      log_types = log_types, witness = witness};
    1.38  
    1.39 -fun build_tsig (classes, default, types, arities) =
    1.40 +fun build_tsig ((space, classes), default, types) =
    1.41    let
    1.42      val log_types =
    1.43        Symtab.fold (fn (c, (LogicalType n, _)) => cons (c, n) | _ => I) (snd types) []
    1.44        |> Library.sort (Library.int_ord o pairself snd) |> map fst;
    1.45      val witness =
    1.46 -      (case Sorts.witness_sorts (snd classes, arities) log_types [] [Graph.keys (snd classes)] of
    1.47 +      (case Sorts.witness_sorts classes log_types [] [Sorts.classes classes] of
    1.48          [w] => SOME w | _ => NONE);
    1.49 -  in make_tsig (classes, default, types, arities, log_types, witness) end;
    1.50 +  in make_tsig ((space, classes), default, types, log_types, witness) end;
    1.51  
    1.52 -fun map_tsig f (TSig {classes, default, types, arities, log_types = _, witness = _}) =
    1.53 -  build_tsig (f (classes, default, types, arities));
    1.54 +fun map_tsig f (TSig {classes, default, types, log_types = _, witness = _}) =
    1.55 +  build_tsig (f (classes, default, types));
    1.56  
    1.57  val empty_tsig =
    1.58 -  build_tsig ((NameSpace.empty, Graph.empty), [], NameSpace.empty_table, Symtab.empty);
    1.59 +  build_tsig ((NameSpace.empty, Sorts.empty_algebra), [], NameSpace.empty_table);
    1.60  
    1.61  
    1.62  (* classes and sorts *)
    1.63  
    1.64 -fun classes (TSig {classes = (_, C), ...}) = Graph.keys C;
    1.65  fun defaultS (TSig {default, ...}) = default;
    1.66  fun logical_types (TSig {log_types, ...}) = log_types;
    1.67  fun universal_witness (TSig {witness, ...}) = witness;
    1.68  
    1.69  fun eq_sort (TSig {classes, ...}) = Sorts.sort_eq (#2 classes);
    1.70  fun subsort (TSig {classes, ...}) = Sorts.sort_le (#2 classes);
    1.71 -fun of_sort (TSig {classes, arities, ...}) = Sorts.of_sort (#2 classes, arities);
    1.72 +fun of_sort (TSig {classes, ...}) = Sorts.of_sort (#2 classes);
    1.73  fun inter_sort (TSig {classes, ...}) = Sorts.inter_sort (#2 classes);
    1.74  
    1.75 -fun cert_class (TSig {classes, ...}) c =
    1.76 -  if can (Graph.get_node (#2 classes)) c then c
    1.77 -  else raise TYPE ("Undeclared class: " ^ quote c, [], []);
    1.78 +fun cert_class (TSig {classes, ...}) = Sorts.certify_class (#2 classes);
    1.79 +fun cert_sort (TSig {classes, ...}) = Sorts.certify_sort (#2 classes);
    1.80  
    1.81 -fun cert_sort (tsig as TSig {classes, ...}) =
    1.82 -  Sorts.norm_sort (#2 classes) o map (cert_class tsig);
    1.83 -
    1.84 -fun witness_sorts (tsig as TSig {classes, arities, log_types, ...}) =
    1.85 -  Sorts.witness_sorts (#2 classes, arities) log_types;
    1.86 +fun witness_sorts (tsig as TSig {classes, log_types, ...}) =
    1.87 +  Sorts.witness_sorts (#2 classes) log_types;
    1.88  
    1.89  
    1.90  (* certified types *)
    1.91 @@ -211,9 +203,8 @@
    1.92    | _ => error (undecl_type a));
    1.93  
    1.94  fun arity_sorts _ tsig a [] = replicate (arity_number tsig a) []
    1.95 -  | arity_sorts pp (TSig {classes, arities, ...}) a S =
    1.96 -      Sorts.mg_domain (#2 classes, arities) a S
    1.97 -        handle Sorts.CLASS_ERROR err => Sorts.class_error pp err;
    1.98 +  | arity_sorts pp (TSig {classes, ...}) a S = Sorts.mg_domain (#2 classes) a S
    1.99 +      handle Sorts.CLASS_ERROR err => Sorts.class_error pp err;
   1.100  
   1.101  
   1.102  
   1.103 @@ -379,13 +370,13 @@
   1.104    | devar tye T = T;
   1.105  
   1.106  (*order-sorted unification*)
   1.107 -fun unify (tsig as TSig {classes = (_, classes), arities, ...}) TU (tyenv, maxidx) =
   1.108 +fun unify (tsig as TSig {classes = (_, classes), ...}) TU (tyenv, maxidx) =
   1.109    let
   1.110      val tyvar_count = ref maxidx;
   1.111      fun gen_tyvar S = TVar (("'a", inc tyvar_count), S);
   1.112  
   1.113 -    fun mg_domain a S =
   1.114 -      Sorts.mg_domain (classes, arities) a S handle Sorts.CLASS_ERROR _ => raise TUNIFY;
   1.115 +    fun mg_domain a S = Sorts.mg_domain classes a S
   1.116 +      handle Sorts.CLASS_ERROR _ => raise TUNIFY;
   1.117  
   1.118      fun meet (_, []) tye = tye
   1.119        | meet (TVar (xi, S'), S) tye =
   1.120 @@ -470,22 +461,22 @@
   1.121  (* classes *)
   1.122  
   1.123  fun add_class pp naming (c, cs) tsig =
   1.124 -  tsig |> map_tsig (fn ((space, classes), default, types, arities) =>
   1.125 +  tsig |> map_tsig (fn ((space, classes), default, types) =>
   1.126      let
   1.127        val c' = NameSpace.full naming c;
   1.128        val cs' = map (cert_class tsig) cs
   1.129          handle TYPE (msg, _, _) => error msg;
   1.130        val space' = space |> NameSpace.declare naming c';
   1.131        val classes' = classes |> Sorts.add_class pp (c', cs');
   1.132 -    in ((space', classes'), default, types, arities) end);
   1.133 +    in ((space', classes'), default, types) end);
   1.134  
   1.135 -fun hide_classes fully cs = map_tsig (fn ((space, classes), default, types, arities) =>
   1.136 -  ((fold (NameSpace.hide fully) cs space, classes), default, types, arities));
   1.137 +fun hide_classes fully cs = map_tsig (fn ((space, classes), default, types) =>
   1.138 +  ((fold (NameSpace.hide fully) cs space, classes), default, types));
   1.139  
   1.140  
   1.141  (* arities *)
   1.142  
   1.143 -fun add_arity pp (t, Ss, S) tsig = tsig |> map_tsig (fn (classes, default, types, arities) =>
   1.144 +fun add_arity pp (t, Ss, S) tsig = tsig |> map_tsig (fn ((space, classes), default, types) =>
   1.145    let
   1.146      val _ =
   1.147        (case Symtab.lookup (#2 types) t of
   1.148 @@ -494,27 +485,25 @@
   1.149        | NONE => error (undecl_type t));
   1.150      val (Ss', S') = (map (cert_sort tsig) Ss, cert_sort tsig S)
   1.151        handle TYPE (msg, _, _) => error msg;
   1.152 -    val arities' = arities |> Sorts.add_arities pp (#2 classes) ((t, map (fn c' => (c', Ss')) S'));
   1.153 -  in (classes, default, types, arities') end);
   1.154 +    val classes' = classes |> Sorts.add_arities pp ((t, map (fn c' => (c', Ss')) S'));
   1.155 +  in ((space, classes'), default, types) end);
   1.156  
   1.157  
   1.158  (* classrel *)
   1.159  
   1.160  fun add_classrel pp rel tsig =
   1.161 -  tsig |> map_tsig (fn ((space, classes), default, types, arities) =>
   1.162 +  tsig |> map_tsig (fn ((space, classes), default, types) =>
   1.163      let
   1.164        val rel' = pairself (cert_class tsig) rel
   1.165          handle TYPE (msg, _, _) => error msg;
   1.166        val classes' = classes |> Sorts.add_classrel pp rel;
   1.167 -      val default' = default |> Sorts.norm_sort classes';
   1.168 -      val arities' = arities |> Sorts.rebuild_arities pp classes';
   1.169 -    in ((space, classes'), default', types, arities') end);
   1.170 +    in ((space, classes'), default, types) end);
   1.171  
   1.172  
   1.173  (* default sort *)
   1.174  
   1.175 -fun set_defsort S tsig = tsig |> map_tsig (fn (classes, _, types, arities) =>
   1.176 -  (classes, cert_sort tsig S handle TYPE (msg, _, _) => error msg, types, arities));
   1.177 +fun set_defsort S tsig = tsig |> map_tsig (fn (classes, _, types) =>
   1.178 +  (classes, cert_sort tsig S handle TYPE (msg, _, _) => error msg, types));
   1.179  
   1.180  
   1.181  (* types *)
   1.182 @@ -542,11 +531,11 @@
   1.183  
   1.184  fun the_decl (_, types) = fst o the o Symtab.lookup types;
   1.185  
   1.186 -fun map_types f = map_tsig (fn (classes, default, types, arities) =>
   1.187 +fun map_types f = map_tsig (fn (classes, default, types) =>
   1.188    let
   1.189      val (space', tab') = f types;
   1.190      val _ = assert (NameSpace.intern space' "dummy" = "dummy") "Illegal declaration of dummy type";
   1.191 -  in (classes, default, (space', tab'), arities) end);
   1.192 +  in (classes, default, (space', tab')) end);
   1.193  
   1.194  fun syntactic types (Type (c, Ts)) =
   1.195        (case Symtab.lookup types c of SOME (Nonterminal, _) => true | _ => false)
   1.196 @@ -583,8 +572,8 @@
   1.197  
   1.198  end;
   1.199  
   1.200 -fun hide_types fully cs = map_tsig (fn (classes, default, (space, types), arities) =>
   1.201 -  (classes, default, (fold (NameSpace.hide fully) cs space, types), arities));
   1.202 +fun hide_types fully cs = map_tsig (fn (classes, default, (space, types)) =>
   1.203 +  (classes, default, (fold (NameSpace.hide fully) cs space, types)));
   1.204  
   1.205  
   1.206  (* merge type signatures *)
   1.207 @@ -592,15 +581,14 @@
   1.208  fun merge_tsigs pp (tsig1, tsig2) =
   1.209    let
   1.210      val (TSig {classes = (space1, classes1), default = default1, types = types1,
   1.211 -      arities = arities1, log_types = _, witness = _}) = tsig1;
   1.212 +      log_types = _, witness = _}) = tsig1;
   1.213      val (TSig {classes = (space2, classes2), default = default2, types = types2,
   1.214 -      arities = arities2, log_types = _, witness = _}) = tsig2;
   1.215 +      log_types = _, witness = _}) = tsig2;
   1.216  
   1.217      val space' = NameSpace.merge (space1, space2);
   1.218 -    val classes' = Sorts.merge_classes pp (classes1, classes2);
   1.219 +    val classes' = Sorts.merge_algebra pp (classes1, classes2);
   1.220      val default' = Sorts.inter_sort classes' (default1, default2);
   1.221      val types' = merge_types (types1, types2);
   1.222 -    val arities' = Sorts.merge_arities pp classes' (arities1, arities2);
   1.223 -  in build_tsig ((space', classes'), default', types', arities') end;
   1.224 +  in build_tsig ((space', classes'), default', types') end;
   1.225  
   1.226  end;