# HG changeset patch
# User wenzelm
# Date 1427747699 -7200
# Node ID 890b68e1e8b65787d646d2a0768e5aa802add820
# Parent  49b975c5f58d68d200e41d369c51e61c0672e6a9
support for strictly private name space entries;
tuned signature;

diff -r 49b975c5f58d -r 890b68e1e8b6 src/HOL/TPTP/TPTP_Parser/tptp_reconstruct.ML
--- 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
diff -r 49b975c5f58d -r 890b68e1e8b6 src/HOL/TPTP/TPTP_Proof_Reconstruction.thy
--- 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
diff -r 49b975c5f58d -r 890b68e1e8b6 src/HOL/Tools/BNF/bnf_def.ML
--- 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) =
diff -r 49b975c5f58d -r 890b68e1e8b6 src/HOL/Tools/BNF/bnf_fp_util.ML
--- 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)])
diff -r 49b975c5f58d -r 890b68e1e8b6 src/HOL/Tools/BNF/bnf_util.ML
--- 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
diff -r 49b975c5f58d -r 890b68e1e8b6 src/Pure/General/binding.ML
--- 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;
-
diff -r 49b975c5f58d -r 890b68e1e8b6 src/Pure/General/name_space.ML
--- 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;
-