--- a/src/Pure/type.ML Sat Jun 11 22:15:54 2005 +0200
+++ b/src/Pure/type.ML Sat Jun 11 22:15:55 2005 +0200
@@ -15,9 +15,9 @@
Nonterminal
type tsig
val rep_tsig: tsig ->
- {classes: Sorts.classes,
+ {classes: NameSpace.T * Sorts.classes,
default: sort,
- types: (decl * stamp) Symtab.table,
+ types: (decl * stamp) NameSpace.table,
arities: Sorts.arities,
log_types: string list,
witness: (typ * sort) option}
@@ -58,12 +58,14 @@
val raw_unify: typ * typ -> bool
(*extend and merge type signatures*)
- val add_classes: Pretty.pp -> (class * class list) list -> tsig -> tsig
+ val add_classes: Pretty.pp -> NameSpace.naming -> (bstring * class list) list -> tsig -> tsig
+ val hide_classes: bool -> string list -> tsig -> tsig
val add_classrel: Pretty.pp -> (class * class) list -> tsig -> tsig
val set_defsort: sort -> tsig -> tsig
- val add_types: (string * int) list -> tsig -> tsig
- val add_abbrevs: (string * string list * typ) list -> tsig -> tsig
- val add_nonterminals: string list -> tsig -> tsig
+ val add_types: NameSpace.naming -> (bstring * int) list -> tsig -> tsig
+ val add_abbrevs: NameSpace.naming -> (string * string list * typ) list -> tsig -> tsig
+ val add_nonterminals: NameSpace.naming -> string list -> tsig -> tsig
+ val hide_types: bool -> string list -> tsig -> tsig
val add_arities: Pretty.pp -> arity list -> tsig -> tsig
val merge_tsigs: Pretty.pp -> tsig * tsig -> tsig
end;
@@ -89,12 +91,12 @@
datatype tsig =
TSig of {
- classes: Sorts.classes, (*declared classes with proper subclass relation*)
- default: sort, (*default sort on input*)
- types: (decl * stamp) Symtab.table, (*declared types*)
- arities: Sorts.arities, (*image specification of types wrt. sorts*)
- log_types: string list, (*logical types sorted by number of arguments*)
- witness: (typ * sort) option}; (*witness for non-emptiness of strictest sort*)
+ classes: NameSpace.T * Sorts.classes, (*declared classes with proper subclass relation*)
+ default: sort, (*default sort on input*)
+ types: (decl * stamp) NameSpace.table, (*declared types*)
+ arities: Sorts.arities, (*image specification of types wrt. sorts*)
+ log_types: string list, (*logical types sorted by number of arguments*)
+ witness: (typ * sort) option}; (*witness for non-emptiness of strictest sort*)
fun rep_tsig (TSig comps) = comps;
@@ -102,43 +104,41 @@
TSig {classes = classes, default = default, types = types, arities = arities,
log_types = log_types, witness = witness};
-fun map_tsig f (TSig {classes, default, types, arities, log_types, witness}) =
- make_tsig (f (classes, default, types, arities, log_types, witness));
-
fun build_tsig (classes, default, types, arities) =
let
fun add_log_type (ts, (c, (LogicalType n, _))) = (c, n) :: ts
| add_log_type (ts, _) = ts;
val log_types =
- Symtab.foldl add_log_type ([], types)
+ Symtab.foldl add_log_type ([], #2 types)
|> Library.sort (Library.int_ord o pairself #2) |> map #1;
val witness =
- (case Sorts.witness_sorts (classes, arities) log_types [] [Graph.keys classes] of
+ (case Sorts.witness_sorts (#2 classes, arities) log_types [] [Graph.keys (#2 classes)] of
[w] => SOME w | _ => NONE);
in make_tsig (classes, default, types, arities, log_types, witness) end;
-fun change_tsig f (TSig {classes, default, types, arities, log_types = _, witness = _}) =
+fun map_tsig f (TSig {classes, default, types, arities, log_types = _, witness = _}) =
build_tsig (f (classes, default, types, arities));
-val empty_tsig = build_tsig (Graph.empty, [], Symtab.empty, Symtab.empty);
+val empty_tsig =
+ build_tsig ((NameSpace.empty, Graph.empty), [], NameSpace.empty_table, Symtab.empty);
(* classes and sorts *)
-fun classes (TSig {classes = C, ...}) = Graph.keys C;
+fun classes (TSig {classes = (_, C), ...}) = Graph.keys C;
fun defaultS (TSig {default, ...}) = default;
fun logical_types (TSig {log_types, ...}) = log_types;
fun universal_witness (TSig {witness, ...}) = witness;
-fun eq_sort (TSig {classes, ...}) = Sorts.sort_eq classes;
-fun subsort (TSig {classes, ...}) = Sorts.sort_le classes;
-fun of_sort (TSig {classes, arities, ...}) = Sorts.of_sort (classes, arities);
+fun eq_sort (TSig {classes, ...}) = Sorts.sort_eq (#2 classes);
+fun subsort (TSig {classes, ...}) = Sorts.sort_le (#2 classes);
+fun of_sort (TSig {classes, arities, ...}) = Sorts.of_sort (#2 classes, arities);
-fun cert_class (TSig {classes, ...}) = Sorts.certify_class classes;
-fun cert_sort (TSig {classes, ...}) = Sorts.certify_sort classes;
+fun cert_class (TSig {classes, ...}) = Sorts.certify_class (#2 classes);
+fun cert_sort (TSig {classes, ...}) = Sorts.certify_sort (#2 classes);
fun witness_sorts (tsig as TSig {classes, arities, log_types, ...}) =
- Sorts.witness_sorts (classes, arities) log_types;
+ Sorts.witness_sorts (#2 classes, arities) log_types;
(* certified types *)
@@ -154,7 +154,7 @@
fun certify_typ normalize syntax tsig ty =
let
- val TSig {classes, types, ...} = tsig;
+ val TSig {classes = (_, classes), types = (_, types), ...} = tsig;
fun err msg = raise TYPE (msg, [ty], []);
val check_syntax =
@@ -338,7 +338,7 @@
| NONE => T)
| devar (T, tye) = T;
-fun unify (tsig as TSig {classes, arities, ...}) (tyenv, maxidx) TU =
+fun unify (tsig as TSig {classes = (_, classes), arities, ...}) (tyenv, maxidx) TU =
let
val tyvar_count = ref maxidx;
fun gen_tyvar S = TVar (("'a", inc tyvar_count), S);
@@ -445,10 +445,10 @@
in
-fun add_arities pp decls tsig = tsig |> change_tsig (fn (classes, default, types, arities) =>
+fun add_arities pp decls tsig = tsig |> map_tsig (fn (classes, default, types, arities) =>
let
fun prep (t, Ss, S) =
- (case Symtab.lookup (types, t) of
+ (case Symtab.lookup (#2 types, t) of
SOME (LogicalType n, _) =>
if length Ss = n then
(t, map (cert_sort tsig) Ss, cert_sort tsig S)
@@ -458,7 +458,7 @@
| NONE => error (undecl_type t));
val ars = decls |> map ((fn (t, Ss, S) => (t, map (fn c => (c, Ss)) S)) o prep);
- val arities' = fold (insert_arities pp classes) ars arities;
+ val arities' = fold (insert_arities pp (#2 classes)) ars arities;
in (classes, default, types, arities') end);
fun rebuild_arities pp classes arities =
@@ -481,40 +481,52 @@
error (cat_lines (map (fn cs =>
"Cycle in class relation: " ^ Pretty.string_of_classrel pp cs) css));
-fun add_class pp (c, cs) tsig = tsig |> change_tsig (fn (classes, default, types, arities) =>
- let
- val cs' = map (cert_class tsig) cs
- handle TYPE (msg, _, _) => error msg;
- val classes' = classes |> Graph.new_node (c, stamp ())
- handle Graph.DUP d => err_dup_classes [d];
- val classes'' = classes' |> fold Graph.add_edge_trans_acyclic (map (pair c) cs')
- handle Graph.CYCLES css => err_cyclic_classes pp css;
- in (classes'', default, types, arities) end);
+fun add_class pp naming (c, cs) tsig =
+ tsig |> map_tsig (fn ((space, classes), default, types, arities) =>
+ let
+ val c' = NameSpace.full naming c;
+ val cs' = map (cert_class tsig) cs
+ handle TYPE (msg, _, _) => error msg;
+ val space' = space |> NameSpace.declare naming c';
+ val classes' = classes |> Graph.new_node (c', stamp ())
+ handle Graph.DUP dup => err_dup_classes [dup];
+ val classes'' = classes' |> fold Graph.add_edge_trans_acyclic (map (pair c') cs')
+ handle Graph.CYCLES css => err_cyclic_classes pp css;
+ in ((space', classes''), default, types, arities) end);
in
-val add_classes = fold o add_class;
+val add_classes = fold oo add_class;
-fun add_classrel pp ps tsig = tsig |> change_tsig (fn (classes, default, types, arities) =>
+fun add_classrel pp ps tsig =
+ tsig |> map_tsig (fn ((space, classes), default, types, arities) =>
+ let
+ val ps' = map (pairself (cert_class tsig)) ps
+ handle TYPE (msg, _, _) => error msg;
+ val classes' = classes |> fold Graph.add_edge_trans_acyclic ps'
+ handle Graph.CYCLES css => err_cyclic_classes pp css;
+ val default' = default |> Sorts.norm_sort classes';
+ val arities' = arities |> rebuild_arities pp classes';
+ in ((space, classes'), default', types, arities') end);
+
+fun merge_classes pp ((space1, classes1), (space2, classes2)) =
let
- val ps' = map (pairself (cert_class tsig)) ps
- handle TYPE (msg, _, _) => error msg;
- val classes' = classes |> fold Graph.add_edge_trans_acyclic ps'
- handle Graph.CYCLES css => err_cyclic_classes pp css;
- val default' = default |> Sorts.norm_sort classes';
- val arities' = arities |> rebuild_arities pp classes';
- in (classes', default', types, arities') end);
-
-fun merge_classes pp CC = Graph.merge_trans_acyclic (op =) CC
- handle Graph.DUPS cs => err_dup_classes cs
- | Graph.CYCLES css => err_cyclic_classes pp css;
+ val space = NameSpace.merge (space1, space2);
+ val classes =
+ Graph.merge_trans_acyclic (op =) (classes1, classes2)
+ handle Graph.DUPS cs => err_dup_classes cs
+ | Graph.CYCLES css => err_cyclic_classes pp css;
+ in (space, classes) end;
end;
+fun hide_classes fully cs = map_tsig (fn ((space, classes), default, types, arities) =>
+ ((fold (NameSpace.hide fully) cs space, classes), default, types, arities));
+
(* default sort *)
-fun set_defsort S tsig = tsig |> change_tsig (fn (classes, _, types, arities) =>
+fun set_defsort S tsig = tsig |> map_tsig (fn (classes, _, types, arities) =>
(classes, cert_sort tsig S handle TYPE (msg, _, _) => error msg, types, arities));
@@ -531,14 +543,19 @@
else error ("Conflict of " ^ s ^ " with " ^ s' ^ ": " ^ quote c)
end;
-fun new_decl (c, decl) types =
- (case Symtab.lookup (types, c) of
- SOME (decl', _) => err_in_decls c decl decl'
- | NONE => Symtab.update ((c, (decl, stamp ())), types));
+fun new_decl naming (c, decl) (space, types) =
+ let
+ val c' = NameSpace.full naming c;
+ val space' = NameSpace.declare naming c' space;
+ val types' =
+ (case Symtab.lookup (types, c') of
+ SOME (decl', _) => err_in_decls c' decl decl'
+ | NONE => Symtab.update ((c', (decl, stamp ())), types));
+ in (space', types') end;
-fun the_decl types c = fst (the (Symtab.lookup (types, c)));
+fun the_decl (_, types) c = fst (the (Symtab.lookup (types, c)));
-fun change_types f = change_tsig (fn (classes, default, types, arities) =>
+fun change_types f = map_tsig (fn (classes, default, types, arities) =>
(classes, default, f types, arities));
fun syntactic types (Type (c, Ts)) =
@@ -546,7 +563,7 @@
orelse exists (syntactic types) Ts
| syntactic _ _ = false;
-fun add_abbrev (a, vs, rhs) tsig = tsig |> change_types (fn types =>
+fun add_abbrev naming (a, vs, rhs) tsig = tsig |> change_types (fn types =>
let
fun err msg =
error (msg ^ "\nThe error(s) above occurred in type abbreviation: " ^ quote a);
@@ -559,23 +576,27 @@
(case gen_rems (op =) (map (#1 o #1) (typ_tvars rhs'), vs) of
[] => []
| extras => err ("Extra variables on rhs: " ^ commas_quote extras));
- types |> new_decl (a, Abbreviation (vs, rhs', syntactic types rhs'))
+ types |> new_decl naming (a, Abbreviation (vs, rhs', syntactic (#2 types) rhs'))
end);
in
-fun add_types ps = change_types (fold new_decl (ps |> map (fn (c, n) =>
+fun add_types naming ps = change_types (fold (new_decl naming) (ps |> map (fn (c, n) =>
if n < 0 then err_neg_args c else (c, LogicalType n))));
-val add_abbrevs = fold add_abbrev;
-val add_nonterminals = change_types o fold new_decl o map (rpair Nonterminal);
+val add_abbrevs = fold o add_abbrev;
+
+fun add_nonterminals naming = change_types o fold (new_decl naming) o map (rpair Nonterminal);
fun merge_types (types1, types2) =
- Symtab.merge Library.eq_snd (types1, types2) handle Symtab.DUPS (d :: _) =>
+ NameSpace.merge_tables Library.eq_snd (types1, types2) handle Symtab.DUPS (d :: _) =>
err_in_decls d (the_decl types1 d) (the_decl types2 d);
end;
+fun hide_types fully cs = map_tsig (fn (classes, default, (space, types), arities) =>
+ (classes, default, (fold (NameSpace.hide fully) cs space, types), arities));
+
(* merge type signatures *)
@@ -587,9 +608,9 @@
log_types = _, witness = _}) = tsig2;
val classes' = merge_classes pp (classes1, classes2);
- val default' = Sorts.inter_sort classes' (default1, default2);
+ val default' = Sorts.inter_sort (#2 classes') (default1, default2);
val types' = merge_types (types1, types2);
- val arities' = merge_arities pp classes' (arities1, arities2);
+ val arities' = merge_arities pp (#2 classes') (arities1, arities2);
in build_tsig (classes', default', types', arities') end;
end;