--- a/src/HOL/TPTP/TPTP_Parser/tptp_reconstruct.ML Mon Mar 30 20:51:11 2015 +0200
+++ b/src/HOL/TPTP/TPTP_Parser/tptp_reconstruct.ML Mon Mar 30 22:34:59 2015 +0200
@@ -1006,10 +1006,7 @@
val def_thm =
case AList.lookup (op =) (#defs pannot) n of
NONE => error ("Did not find definition: " ^ n)
- | SOME binding =>
- Binding.dest binding
- |> #3
- |> Global_Theory.get_thm thy
+ | SOME binding => Global_Theory.get_thm thy (Binding.name_of binding)
in
rtac def_thm 1 THEN rest (tl skel) memo
end
@@ -1018,10 +1015,7 @@
val ax_thm =
case AList.lookup (op =) (#axs pannot) n of
NONE => error ("Did not find axiom: " ^ n)
- | SOME binding =>
- Binding.dest binding
- |> #3
- |> Global_Theory.get_thm thy
+ | SOME binding => Global_Theory.get_thm thy (Binding.name_of binding)
in
rtac ax_thm 1 THEN rest (tl skel) memo
end
@@ -1184,10 +1178,7 @@
fun def_thm thy =
case AList.lookup (op =) (#defs pannot) n of
NONE => error ("Did not find definition: " ^ n)
- | SOME binding =>
- Binding.dest binding
- |> #3
- |> Global_Theory.get_thm thy
+ | SOME binding => Global_Theory.get_thm thy (Binding.name_of binding)
in
(hd skel,
Thm.prop_of (def_thm thy)
@@ -1200,10 +1191,7 @@
val ax_thm =
case AList.lookup (op =) (#axs pannot) n of
NONE => error ("Did not find axiom: " ^ n)
- | SOME binding =>
- Binding.dest binding
- |> #3
- |> Global_Theory.get_thm thy
+ | SOME binding => Global_Theory.get_thm thy (Binding.name_of binding)
in
(hd skel,
Thm.prop_of ax_thm
--- a/src/HOL/TPTP/TPTP_Proof_Reconstruction.thy Mon Mar 30 20:51:11 2015 +0200
+++ b/src/HOL/TPTP/TPTP_Proof_Reconstruction.thy Mon Mar 30 22:34:59 2015 +0200
@@ -2057,9 +2057,9 @@
fun values () =
case role of
TPTP_Syntax.Role_Definition =>
- map (apsnd Binding.dest) (#defs pannot)
+ map (apsnd Binding.name_of) (#defs pannot)
| TPTP_Syntax.Role_Axiom =>
- map (apsnd Binding.dest) (#axs pannot)
+ map (apsnd Binding.name_of) (#axs pannot)
| _ => raise UNSUPPORTED_ROLE
in
if is_none (source_inf_opt node) then []
@@ -2075,7 +2075,7 @@
use the ones in the proof annotation.*)
(fn x =>
if role = TPTP_Syntax.Role_Definition then
- let fun values () = map (apsnd Binding.dest) (#defs pannot)
+ let fun values () = map (apsnd Binding.name_of) (#defs pannot)
in
map snd (values ())
end
@@ -2086,7 +2086,7 @@
val roled_dependencies =
roled_dependencies_names
- #> map (#3 #> Global_Theory.get_thm thy)
+ #> map (Global_Theory.get_thm thy)
in
val depends_on_defs = roled_dependencies TPTP_Syntax.Role_Definition
val depends_on_axs = roled_dependencies TPTP_Syntax.Role_Axiom
--- a/src/HOL/Tools/BNF/bnf_def.ML Mon Mar 30 20:51:11 2015 +0200
+++ b/src/HOL/Tools/BNF/bnf_def.ML Mon Mar 30 22:34:59 2015 +0200
@@ -689,7 +689,7 @@
val facts = facts_of_bnf bnf;
val wits = wits_of_bnf bnf;
val qualify =
- let val (_, qs, _) = Binding.dest bnf_b;
+ let val qs = Binding.path_of bnf_b;
in fold_rev (fn (s, mand) => Binding.qualify mand s) qs #> qualify0 end;
fun note_if_note_all (noted0, lthy0) =
--- a/src/HOL/Tools/BNF/bnf_fp_util.ML Mon Mar 30 20:51:11 2015 +0200
+++ b/src/HOL/Tools/BNF/bnf_fp_util.ML Mon Mar 30 22:34:59 2015 +0200
@@ -613,7 +613,9 @@
subtract (op =) Xs (filter (fn T => exists (fn Ts => member (op =) Ts T) Ass) resBs) @ Xs;
fun raw_qualify base_b =
- let val (_, qs, n) = Binding.dest base_b;
+ let
+ val qs = Binding.path_of base_b;
+ val n = Binding.name_of base_b;
in
Binding.prefix_name rawN
#> fold_rev (fn (s, mand) => Binding.qualify mand s) (qs @ [(n, true)])
--- a/src/HOL/Tools/BNF/bnf_util.ML Mon Mar 30 20:51:11 2015 +0200
+++ b/src/HOL/Tools/BNF/bnf_util.ML Mon Mar 30 22:34:59 2015 +0200
@@ -142,7 +142,7 @@
fun typedef (b, Ts, mx) set opt_morphs tac lthy =
let
(*Work around loss of qualification in "typedef" axioms by replicating it in the name*)
- val b' = fold_rev Binding.prefix_name (map (suffix "_" o fst) (#2 (Binding.dest b))) b;
+ val b' = fold_rev Binding.prefix_name (map (suffix "_" o fst) (Binding.path_of b)) b;
val ((name, info), (lthy, lthy_old)) =
lthy
|> Local_Theory.conceal
--- a/src/Pure/General/binding.ML Mon Mar 30 20:51:11 2015 +0200
+++ b/src/Pure/General/binding.ML Mon Mar 30 22:34:59 2015 +0200
@@ -10,7 +10,8 @@
signature BINDING =
sig
eqtype binding
- val dest: binding -> bool * (string * bool) list * bstring
+ val dest: binding -> {private: bool, conceal: bool, path: (string * bool) list, name: bstring}
+ val path_of: binding -> (string * bool) list
val make: bstring * Position.T -> binding
val pos_of: binding -> Position.T
val set_pos: Position.T -> binding -> binding
@@ -28,6 +29,7 @@
val prefix_of: binding -> (string * bool) list
val map_prefix: ((string * bool) list -> (string * bool) list) -> binding -> binding
val prefix: bool -> string -> binding -> binding
+ val private: binding -> binding
val conceal: binding -> binding
val pretty: binding -> Pretty.T
val print: binding -> string
@@ -44,20 +46,24 @@
(* datatype *)
datatype binding = Binding of
- {conceal: bool, (*internal -- for foundational purposes only*)
+ {private: bool, (*entry is strictly private -- no name space accesses*)
+ conceal: bool, (*entry is for foundational purposes -- please ignore*)
prefix: (string * bool) list, (*system prefix*)
qualifier: (string * bool) list, (*user qualifier*)
name: bstring, (*base name*)
pos: Position.T}; (*source position*)
-fun make_binding (conceal, prefix, qualifier, name, pos) =
- Binding {conceal = conceal, prefix = prefix, qualifier = qualifier, name = name, pos = pos};
+fun make_binding (private, conceal, prefix, qualifier, name, pos) =
+ Binding {private = private, conceal = conceal, prefix = prefix,
+ qualifier = qualifier, name = name, pos = pos};
-fun map_binding f (Binding {conceal, prefix, qualifier, name, pos}) =
- make_binding (f (conceal, prefix, qualifier, name, pos));
+fun map_binding f (Binding {private, conceal, prefix, qualifier, name, pos}) =
+ make_binding (f (private, conceal, prefix, qualifier, name, pos));
-fun dest (Binding {conceal, prefix, qualifier, name, ...}) =
- (conceal, prefix @ qualifier, name);
+fun dest (Binding {private, conceal, prefix, qualifier, name, ...}) =
+ {private = private, conceal = conceal, path = prefix @ qualifier, name = name};
+
+val path_of = #path o dest;
@@ -65,11 +71,12 @@
(* name and position *)
-fun make (name, pos) = make_binding (false, [], [], name, pos);
+fun make (name, pos) = make_binding (false, false, [], [], name, pos);
fun pos_of (Binding {pos, ...}) = pos;
fun set_pos pos =
- map_binding (fn (conceal, prefix, qualifier, name, _) => (conceal, prefix, qualifier, name, pos));
+ map_binding (fn (private, conceal, prefix, qualifier, name, _) =>
+ (private, conceal, prefix, qualifier, name, pos));
fun name name = make (name, Position.none);
fun name_of (Binding {name, ...}) = name;
@@ -77,8 +84,8 @@
fun eq_name (b, b') = name_of b = name_of b';
fun map_name f =
- map_binding (fn (conceal, prefix, qualifier, name, pos) =>
- (conceal, prefix, qualifier, f name, pos));
+ map_binding (fn (private, conceal, prefix, qualifier, name, pos) =>
+ (private, conceal, prefix, qualifier, f name, pos));
val prefix_name = map_name o prefix;
val suffix_name = map_name o suffix;
@@ -91,17 +98,18 @@
fun qualify _ "" = I
| qualify mandatory qual =
- map_binding (fn (conceal, prefix, qualifier, name, pos) =>
- (conceal, prefix, (qual, mandatory) :: qualifier, name, pos));
+ map_binding (fn (private, conceal, prefix, qualifier, name, pos) =>
+ (private, conceal, prefix, (qual, mandatory) :: qualifier, name, pos));
-fun qualified mandatory name' = map_binding (fn (conceal, prefix, qualifier, name, pos) =>
- let val qualifier' = if name = "" then qualifier else qualifier @ [(name, mandatory)]
- in (conceal, prefix, qualifier', name', pos) end);
+fun qualified mandatory name' =
+ map_binding (fn (private, conceal, prefix, qualifier, name, pos) =>
+ let val qualifier' = if name = "" then qualifier else qualifier @ [(name, mandatory)]
+ in (private, conceal, prefix, qualifier', name', pos) end);
fun qualified_name "" = empty
| qualified_name s =
let val (qualifier, name) = split_last (Long_Name.explode s)
- in make_binding (false, [], map (rpair false) qualifier, name, Position.none) end;
+ in make_binding (false, false, [], map (rpair false) qualifier, name, Position.none) end;
(* system prefix *)
@@ -109,18 +117,22 @@
fun prefix_of (Binding {prefix, ...}) = prefix;
fun map_prefix f =
- map_binding (fn (conceal, prefix, qualifier, name, pos) =>
- (conceal, f prefix, qualifier, name, pos));
+ map_binding (fn (private, conceal, prefix, qualifier, name, pos) =>
+ (private, conceal, f prefix, qualifier, name, pos));
fun prefix _ "" = I
| prefix mandatory prfx = map_prefix (cons (prfx, mandatory));
-(* conceal *)
+(* visibility flags *)
+
+val private =
+ map_binding (fn (_, conceal, prefix, qualifier, name, pos) =>
+ (true, conceal, prefix, qualifier, name, pos));
val conceal =
- map_binding (fn (_, prefix, qualifier, name, pos) =>
- (true, prefix, qualifier, name, pos));
+ map_binding (fn (private, _, prefix, qualifier, name, pos) =>
+ (private, true, prefix, qualifier, name, pos));
(* print *)
@@ -148,4 +160,3 @@
end;
type binding = Binding.binding;
-
--- a/src/Pure/General/name_space.ML Mon Mar 30 20:51:11 2015 +0200
+++ b/src/Pure/General/name_space.ML Mon Mar 30 22:34:59 2015 +0200
@@ -33,6 +33,7 @@
val completion: Context.generic -> T -> xstring * Position.T -> Completion.T
val merge: T * T -> T
type naming
+ val private: naming -> naming
val conceal: naming -> naming
val get_group: naming -> serial option
val set_group: serial option -> naming -> naming
@@ -283,32 +284,37 @@
(* datatype naming *)
datatype naming = Naming of
- {conceal: bool,
+ {private: bool,
+ conceal: bool,
group: serial option,
theory_name: string,
path: (string * bool) list};
-fun make_naming (conceal, group, theory_name, path) =
- Naming {conceal = conceal, group = group, theory_name = theory_name, path = path};
+fun make_naming (private, conceal, group, theory_name, path) =
+ Naming {private = private, conceal = conceal, group = group,
+ theory_name = theory_name, path = path};
-fun map_naming f (Naming {conceal, group, theory_name, path}) =
- make_naming (f (conceal, group, theory_name, path));
+fun map_naming f (Naming {private, conceal, group, theory_name, path}) =
+ make_naming (f (private, conceal, group, theory_name, path));
-fun map_path f = map_naming (fn (conceal, group, theory_name, path) =>
- (conceal, group, theory_name, f path));
+fun map_path f = map_naming (fn (private, conceal, group, theory_name, path) =>
+ (private, conceal, group, theory_name, f path));
-val conceal = map_naming (fn (_, group, theory_name, path) =>
- (true, group, theory_name, path));
+val private = map_naming (fn (_, conceal, group, theory_name, path) =>
+ (true, conceal, group, theory_name, path));
-fun set_theory_name theory_name = map_naming (fn (conceal, group, _, path) =>
- (conceal, group, theory_name, path));
+val conceal = map_naming (fn (private, _, group, theory_name, path) =>
+ (private, true, group, theory_name, path));
+
+fun set_theory_name theory_name = map_naming (fn (private, conceal, group, _, path) =>
+ (private, conceal, group, theory_name, path));
fun get_group (Naming {group, ...}) = group;
-fun set_group group = map_naming (fn (conceal, _, theory_name, path) =>
- (conceal, group, theory_name, path));
+fun set_group group = map_naming (fn (private, conceal, _, theory_name, path) =>
+ (private, conceal, group, theory_name, path));
fun new_group naming = set_group (SOME (serial ())) naming;
val reset_group = set_group NONE;
@@ -319,9 +325,9 @@
fun mandatory_path elems = map_path (fn path => path @ [(elems, true)]);
fun qualified_path mandatory binding = map_path (fn path =>
- path @ #2 (Binding.dest (Binding.qualified mandatory "" binding)));
+ path @ Binding.path_of (Binding.qualified mandatory "" binding));
-val global_naming = make_naming (false, NONE, "", []);
+val global_naming = make_naming (false, false, NONE, "", []);
val local_naming = global_naming |> add_path Long_Name.localN;
@@ -329,27 +335,28 @@
fun err_bad binding = error (Binding.bad binding);
-fun transform_binding (Naming {conceal = true, ...}) = Binding.conceal
- | transform_binding _ = I;
+fun transform_binding (Naming {private, conceal, ...}) =
+ private ? Binding.private #>
+ conceal ? Binding.conceal;
val bad_specs = ["", "??", "__"];
-fun name_spec (naming as Naming {path, ...}) raw_binding =
+fun name_spec (naming as Naming {path = path1, ...}) raw_binding =
let
val binding = transform_binding naming raw_binding;
- val (concealed, prefix, name) = Binding.dest binding;
+ val {private, conceal, path = path2, name} = Binding.dest binding;
val _ = Long_Name.is_qualified name andalso err_bad binding;
- val spec1 = maps (fn (a, b) => map (rpair b) (Long_Name.explode a)) (path @ prefix);
+ val spec1 = maps (fn (a, b) => map (rpair b) (Long_Name.explode a)) (path1 @ path2);
val spec2 = if name = "" then [] else [(name, true)];
val spec = spec1 @ spec2;
val _ =
exists (fn (a, _) => member (op =) bad_specs a orelse exists_string (fn s => s = "\"") a) spec
andalso err_bad binding;
- in (concealed, if null spec2 then [] else spec) end;
+ in {private = private, conceal = conceal, spec = if null spec2 then [] else spec} end;
fun full_name naming =
- name_spec naming #> #2 #> map #1 #> Long_Name.implode;
+ name_spec naming #> #spec #> map #1 #> Long_Name.implode;
val base_name = full_name global_naming #> Long_Name.base_name;
@@ -366,11 +373,13 @@
fun mandatory_suffixes xs = map rev (mandatory_prefixes (rev xs));
fun accesses naming binding =
- let
- val spec = #2 (name_spec naming binding);
- val sfxs = mandatory_suffixes spec;
- val pfxs = mandatory_prefixes spec;
- in apply2 (map Long_Name.implode) (sfxs @ pfxs, sfxs) end;
+ (case name_spec naming binding of
+ {private = true, ...} => ([], [])
+ | {spec, ...} =>
+ let
+ val sfxs = mandatory_suffixes spec;
+ val pfxs = mandatory_prefixes spec;
+ in apply2 (map Long_Name.implode) (sfxs @ pfxs, sfxs) end);
(* hide *)
@@ -433,7 +442,7 @@
let
val naming = naming_of context;
val Naming {group, theory_name, ...} = naming;
- val (concealed, spec) = name_spec naming binding;
+ val {conceal, spec, ...} = name_spec naming binding;
val (accs, accs') = accesses naming binding;
val name = Long_Name.implode (map fst spec);
@@ -441,7 +450,7 @@
val (proper_pos, pos) = Position.default (Binding.pos_of binding);
val entry =
- {concealed = concealed,
+ {concealed = conceal,
group = group,
theory_name = theory_name,
pos = pos,
@@ -556,4 +565,3 @@
fun markup_table ctxt (Table (space, tab)) = markup_entries ctxt space (Change_Table.dest tab);
end;
-