diff -r 96d73621fabb -r 033d890fe91f src/Pure/type.ML --- 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;