--- a/src/Pure/General/name_space.ML Thu Dec 04 18:37:46 2008 -0800
+++ b/src/Pure/General/name_space.ML Fri Dec 05 08:05:14 2008 +0100
@@ -33,7 +33,6 @@
val default_naming: naming
val declare: naming -> Binding.T -> T -> string * T
val full_name: naming -> Binding.T -> string
- val declare_base: naming -> string -> T -> T
val external_names: naming -> string -> string list
val path_of: naming -> string
val add_path: string -> naming -> naming
@@ -45,6 +44,8 @@
val bind: naming -> Binding.T * 'a
-> 'a table -> string * 'a table (*exception Symtab.DUP*)
val merge_tables: ('a * 'a -> bool) -> 'a table * 'a table -> 'a table
+ val join_tables: (string -> 'a * 'a -> 'a)
+ -> 'a table * 'a table -> 'a table
val dest_table: 'a table -> (string * 'a) list
val extern_table: 'a table -> (xstring * 'a) list
val extend_table: naming -> (bstring * 'a) list -> 'a table -> 'a table
@@ -264,13 +265,9 @@
(* declarations *)
-fun full (Naming (path, (qualify, _))) = qualify path;
+fun full_internal (Naming (path, (qualify, _))) = qualify path;
-fun full_name naming b =
- let val (prefix, bname) = Binding.dest b
- in full (apply_prefix prefix naming) bname end;
-
-fun declare_base naming name space =
+fun declare_internal naming name space =
if is_hidden name then
error ("Attempt to declare hidden name " ^ quote name)
else
@@ -282,12 +279,16 @@
val (accs, accs') = pairself (map implode_name) (accesses naming names);
in space |> fold (add_name name) accs |> put_accesses name accs' end;
+fun full_name naming b =
+ let val (prefix, bname) = Binding.dest b
+ in full_internal (apply_prefix prefix naming) bname end;
+
fun declare bnaming b =
let
val (prefix, bname) = Binding.dest b;
val naming = apply_prefix prefix bnaming;
- val name = full naming bname;
- in declare_base naming name #> pair name end;
+ val name = full_internal naming bname;
+ in declare_internal naming name #> pair name end;
@@ -303,12 +304,15 @@
in (name, (space', Symtab.update_new (name, x) tab)) end;
fun extend_table naming bentries (space, tab) =
- let val entries = map (apfst (full naming)) bentries
- in (fold (declare_base naming o #1) entries space, Symtab.extend (tab, entries)) end;
+ let val entries = map (apfst (full_internal naming)) bentries
+ in (fold (declare_internal naming o #1) entries space, Symtab.extend (tab, entries)) end;
fun merge_tables eq ((space1, tab1), (space2, tab2)) =
(merge (space1, space2), Symtab.merge eq (tab1, tab2));
+fun join_tables f ((space1, tab1), (space2, tab2)) =
+ (merge (space1, space2), Symtab.join f (tab1, tab2));
+
fun ext_table (space, tab) =
Symtab.fold (fn (name, x) => cons ((name, extern space name), x)) tab []
|> Library.sort_wrt (#2 o #1);
--- a/src/Pure/Isar/expression.ML Thu Dec 04 18:37:46 2008 -0800
+++ b/src/Pure/Isar/expression.ML Fri Dec 05 08:05:14 2008 +0100
@@ -772,7 +772,7 @@
val deps' = map (fn (l, morph) => (l, morph $> satisfy)) deps;
val loc_ctxt = thy' |>
- NewLocale.register_locale name (extraTs, params)
+ NewLocale.register_locale bname (extraTs, params)
(asm, map prop_of defs) ([], [])
(map (fn n => (n, stamp ())) notes |> rev) (map (fn d => (d, stamp ())) deps' |> rev) |>
NewLocale.init name
--- a/src/Pure/Isar/local_theory.ML Thu Dec 04 18:37:46 2008 -0800
+++ b/src/Pure/Isar/local_theory.ML Fri Dec 05 08:05:14 2008 +0100
@@ -19,7 +19,7 @@
val raw_theory: (theory -> theory) -> local_theory -> local_theory
val checkpoint: local_theory -> local_theory
val full_naming: local_theory -> NameSpace.naming
- val full_name: local_theory -> bstring -> string
+ val full_name: local_theory -> Binding.T -> string
val theory_result: (theory -> 'a * theory) -> local_theory -> 'a * local_theory
val theory: (theory -> theory) -> local_theory -> local_theory
val target_result: (Proof.context -> 'a * Proof.context) -> local_theory -> 'a * local_theory
@@ -142,7 +142,7 @@
|> NameSpace.sticky_prefix (#theory_prefix (get_lthy lthy))
|> NameSpace.qualified_names;
-fun full_name naming = NameSpace.full_name (full_naming naming) o Binding.name;
+fun full_name naming = NameSpace.full_name (full_naming naming);
fun theory_result f lthy = lthy |> raw_theory_result (fn thy => thy
|> Sign.sticky_prefix (#theory_prefix (get_lthy lthy))
--- a/src/Pure/Isar/locale.ML Thu Dec 04 18:37:46 2008 -0800
+++ b/src/Pure/Isar/locale.ML Fri Dec 05 08:05:14 2008 +0100
@@ -387,7 +387,7 @@
(* 1st entry: locale namespace,
2nd entry: locales of the theory *)
- val empty = (NameSpace.empty, Symtab.empty);
+ val empty = NameSpace.empty_table;
val copy = I;
val extend = I;
@@ -403,8 +403,7 @@
regs = merge_alists (op =) regs regs',
intros = intros,
dests = dests};
- fun merge _ ((space1, locs1), (space2, locs2)) =
- (NameSpace.merge (space1, space2), Symtab.join join_locales (locs1, locs2));
+ fun merge _ = NameSpace.join_tables join_locales;
);
@@ -431,10 +430,9 @@
of SOME loc => loc
| NONE => error ("Unknown locale " ^ quote name);
-fun register_locale name loc thy =
- thy |> LocalesData.map (fn (space, locs) =>
- (NameSpace.declare_base (Sign.naming_of thy) name space,
- Symtab.update (name, loc) locs));
+fun register_locale bname loc thy =
+ thy |> LocalesData.map (NameSpace.bind (Sign.naming_of thy)
+ (Binding.name bname, loc) #> snd);
fun change_locale name f thy =
let
@@ -1990,7 +1988,7 @@
|> Sign.no_base_names
|> PureThy.note_thmss Thm.assumptionK facts' |> snd
|> Sign.restore_naming thy'
- |> register_locale name {axiom = axs',
+ |> register_locale bname {axiom = axs',
elems = map (fn e => (e, stamp ())) elems'',
params = params_of elemss''' |> map (fn (x, SOME T) => ((x, T), the (Symtab.lookup syn x))),
decls = ([], []),
--- a/src/Pure/Isar/new_locale.ML Thu Dec 04 18:37:46 2008 -0800
+++ b/src/Pure/Isar/new_locale.ML Fri Dec 05 08:05:14 2008 +0100
@@ -10,7 +10,7 @@
val clear_idents: Proof.context -> Proof.context
val test_locale: theory -> string -> bool
- val register_locale: string ->
+ val register_locale: bstring ->
(string * sort) list * (Binding.T * typ option * mixfix) list ->
term option * term list ->
(declaration * stamp) list * (declaration * stamp) list ->
@@ -104,7 +104,7 @@
type T = NameSpace.T * locale Symtab.table;
(* locale namespace and locales of the theory *)
- val empty = (NameSpace.empty, Symtab.empty);
+ val empty = NameSpace.empty_table;
val copy = I;
val extend = I;
@@ -120,8 +120,7 @@
dependencies = s_merge (dependencies, dependencies')
}
end;
- fun merge _ ((space1, locs1), (space2, locs2)) =
- (NameSpace.merge (space1, space2), Symtab.join join_locales (locs1, locs2));
+ fun merge _ = NameSpace.join_tables join_locales;
);
val intern = NameSpace.intern o #1 o LocalesData.get;
@@ -136,11 +135,10 @@
fun test_locale thy name = case get_locale thy name
of SOME _ => true | NONE => false;
-fun register_locale name parameters spec decls notes dependencies thy =
- thy |> LocalesData.map (fn (space, locs) =>
- (NameSpace.declare_base (Sign.naming_of thy) name space, Symtab.update (name,
- Loc {parameters = parameters, spec = spec, decls = decls, notes = notes,
- dependencies = dependencies}) locs));
+fun register_locale bname parameters spec decls notes dependencies thy =
+ thy |> LocalesData.map (NameSpace.bind (Sign.naming_of thy) (Binding.name bname,
+ Loc {parameters = parameters, spec = spec, decls = decls, notes = notes,
+ dependencies = dependencies}) #> snd);
fun change_locale name f thy =
let
--- a/src/Pure/Isar/theory_target.ML Thu Dec 04 18:37:46 2008 -0800
+++ b/src/Pure/Isar/theory_target.ML Fri Dec 05 08:05:14 2008 +0100
@@ -163,11 +163,9 @@
fun notes (Target {target, is_locale, is_class, ...}) kind facts lthy =
let
val thy = ProofContext.theory_of lthy;
- val full = LocalTheory.full_name lthy;
-
val facts' = facts
- |> map (fn (a, bs) =>
- (a, PureThy.burrow_fact (PureThy.name_multi (full (Name.name_of (fst a)))) bs))
+ |> map (fn (a, bs) => (a, PureThy.burrow_fact (PureThy.name_multi
+ (LocalTheory.full_name lthy (fst a))) bs))
|> PureThy.map_facts (import_export_proof lthy);
val local_facts = PureThy.map_facts #1 facts'
|> Attrib.map_facts (Attrib.attribute_i thy);
--- a/src/Pure/simplifier.ML Thu Dec 04 18:37:46 2008 -0800
+++ b/src/Pure/simplifier.ML Fri Dec 05 08:05:14 2008 +0100
@@ -177,9 +177,10 @@
fun gen_simproc prep {name, lhss, proc, identifier} lthy =
let
+ val b = Binding.name name;
val naming = LocalTheory.full_naming lthy;
val simproc = make_simproc
- {name = LocalTheory.full_name lthy name,
+ {name = LocalTheory.full_name lthy b,
lhss =
let
val lhss' = prep lthy lhss;
@@ -194,7 +195,7 @@
in
lthy |> LocalTheory.declaration (fn phi =>
let
- val b' = Morphism.binding phi (Binding.name name);
+ val b' = Morphism.binding phi b;
val simproc' = morph_simproc phi simproc;
in
Simprocs.map (fn simprocs =>
--- a/src/Pure/thm.ML Thu Dec 04 18:37:46 2008 -0800
+++ b/src/Pure/thm.ML Fri Dec 05 08:05:14 2008 +0100
@@ -1703,7 +1703,7 @@
val naming = Sign.naming_of thy;
val name = NameSpace.full_name naming (Binding.name bname);
val thy' = thy |> Oracles.map (fn (space, tab) =>
- (NameSpace.declare_base naming name space,
+ (NameSpace.declare naming (Binding.name bname) space |> snd,
Symtab.update_new (name, stamp ()) tab handle Symtab.DUP dup => err_dup_ora dup));
in ((name, invoke_oracle (Theory.check_thy thy') name oracle), thy') end;
--- a/src/Pure/type.ML Thu Dec 04 18:37:46 2008 -0800
+++ b/src/Pure/type.ML Fri Dec 05 08:05:14 2008 +0100
@@ -509,10 +509,9 @@
fun add_class pp naming (c, cs) tsig =
tsig |> map_tsig (fn ((space, classes), default, types) =>
let
- val c' = NameSpace.full_name naming (Binding.name c);
val cs' = map (cert_class tsig) cs
handle TYPE (msg, _, _) => error msg;
- val space' = space |> NameSpace.declare_base naming c';
+ val (c', space') = space |> NameSpace.declare naming (Binding.name c);
val classes' = classes |> Sorts.add_class pp (c', cs');
in ((space', classes'), default, types) end);
@@ -568,8 +567,7 @@
fun new_decl naming tags (c, decl) (space, types) =
let
val tags' = tags |> Position.default_properties (Position.thread_data ());
- val c' = NameSpace.full_name naming (Binding.name c);
- val space' = NameSpace.declare_base naming c' space;
+ val (c', space') = NameSpace.declare naming (Binding.name c) space;
val types' =
(case Symtab.lookup types c' of
SOME ((decl', _), _) => err_in_decls c' decl decl'