support for strictly private name space entries;
authorwenzelm
Mon Mar 30 22:34:59 2015 +0200 (2015-03-30)
changeset 59858890b68e1e8b6
parent 59857 49b975c5f58d
child 59859 f9d1442c70f3
support for strictly private name space entries;
tuned signature;
src/HOL/TPTP/TPTP_Parser/tptp_reconstruct.ML
src/HOL/TPTP/TPTP_Proof_Reconstruction.thy
src/HOL/Tools/BNF/bnf_def.ML
src/HOL/Tools/BNF/bnf_fp_util.ML
src/HOL/Tools/BNF/bnf_util.ML
src/Pure/General/binding.ML
src/Pure/General/name_space.ML
     1.1 --- a/src/HOL/TPTP/TPTP_Parser/tptp_reconstruct.ML	Mon Mar 30 20:51:11 2015 +0200
     1.2 +++ b/src/HOL/TPTP/TPTP_Parser/tptp_reconstruct.ML	Mon Mar 30 22:34:59 2015 +0200
     1.3 @@ -1006,10 +1006,7 @@
     1.4                      val def_thm =
     1.5                        case AList.lookup (op =) (#defs pannot) n of
     1.6                            NONE => error ("Did not find definition: " ^ n)
     1.7 -                        | SOME binding =>
     1.8 -                            Binding.dest binding
     1.9 -                            |> #3
    1.10 -                            |> Global_Theory.get_thm thy
    1.11 +                        | SOME binding => Global_Theory.get_thm thy (Binding.name_of binding)
    1.12                    in
    1.13                      rtac def_thm 1 THEN rest (tl skel) memo
    1.14                    end
    1.15 @@ -1018,10 +1015,7 @@
    1.16                      val ax_thm =
    1.17                        case AList.lookup (op =) (#axs pannot) n of
    1.18                            NONE => error ("Did not find axiom: " ^ n)
    1.19 -                        | SOME binding =>
    1.20 -                            Binding.dest binding
    1.21 -                            |> #3
    1.22 -                            |> Global_Theory.get_thm thy
    1.23 +                        | SOME binding => Global_Theory.get_thm thy (Binding.name_of binding)
    1.24                    in
    1.25                      rtac ax_thm 1 THEN rest (tl skel) memo
    1.26                    end
    1.27 @@ -1184,10 +1178,7 @@
    1.28                    fun def_thm thy =
    1.29                      case AList.lookup (op =) (#defs pannot) n of
    1.30                          NONE => error ("Did not find definition: " ^ n)
    1.31 -                      | SOME binding =>
    1.32 -                          Binding.dest binding
    1.33 -                          |> #3
    1.34 -                          |> Global_Theory.get_thm thy
    1.35 +                      | SOME binding => Global_Theory.get_thm thy (Binding.name_of binding)
    1.36                  in
    1.37                    (hd skel,
    1.38                     Thm.prop_of (def_thm thy)
    1.39 @@ -1200,10 +1191,7 @@
    1.40                    val ax_thm =
    1.41                      case AList.lookup (op =) (#axs pannot) n of
    1.42                          NONE => error ("Did not find axiom: " ^ n)
    1.43 -                      | SOME binding =>
    1.44 -                          Binding.dest binding
    1.45 -                          |> #3
    1.46 -                          |> Global_Theory.get_thm thy
    1.47 +                      | SOME binding => Global_Theory.get_thm thy (Binding.name_of binding)
    1.48                  in
    1.49                    (hd skel,
    1.50                     Thm.prop_of ax_thm
     2.1 --- a/src/HOL/TPTP/TPTP_Proof_Reconstruction.thy	Mon Mar 30 20:51:11 2015 +0200
     2.2 +++ b/src/HOL/TPTP/TPTP_Proof_Reconstruction.thy	Mon Mar 30 22:34:59 2015 +0200
     2.3 @@ -2057,9 +2057,9 @@
     2.4            fun values () =
     2.5              case role of
     2.6                  TPTP_Syntax.Role_Definition =>
     2.7 -                  map (apsnd Binding.dest) (#defs pannot)
     2.8 +                  map (apsnd Binding.name_of) (#defs pannot)
     2.9                | TPTP_Syntax.Role_Axiom =>
    2.10 -                  map (apsnd Binding.dest) (#axs pannot)
    2.11 +                  map (apsnd Binding.name_of) (#axs pannot)
    2.12                | _ => raise UNSUPPORTED_ROLE
    2.13            in
    2.14              if is_none (source_inf_opt node) then []
    2.15 @@ -2075,7 +2075,7 @@
    2.16                           use the ones in the proof annotation.*)
    2.17                         (fn x =>
    2.18                           if role = TPTP_Syntax.Role_Definition then
    2.19 -                           let fun values () = map (apsnd Binding.dest) (#defs pannot)
    2.20 +                           let fun values () = map (apsnd Binding.name_of) (#defs pannot)
    2.21                             in
    2.22                               map snd (values ())
    2.23                             end
    2.24 @@ -2086,7 +2086,7 @@
    2.25  
    2.26        val roled_dependencies =
    2.27          roled_dependencies_names
    2.28 -        #> map (#3 #> Global_Theory.get_thm thy)
    2.29 +        #> map (Global_Theory.get_thm thy)
    2.30      in
    2.31        val depends_on_defs = roled_dependencies TPTP_Syntax.Role_Definition
    2.32        val depends_on_axs = roled_dependencies TPTP_Syntax.Role_Axiom
     3.1 --- a/src/HOL/Tools/BNF/bnf_def.ML	Mon Mar 30 20:51:11 2015 +0200
     3.2 +++ b/src/HOL/Tools/BNF/bnf_def.ML	Mon Mar 30 22:34:59 2015 +0200
     3.3 @@ -689,7 +689,7 @@
     3.4      val facts = facts_of_bnf bnf;
     3.5      val wits = wits_of_bnf bnf;
     3.6      val qualify =
     3.7 -      let val (_, qs, _) = Binding.dest bnf_b;
     3.8 +      let val qs = Binding.path_of bnf_b;
     3.9        in fold_rev (fn (s, mand) => Binding.qualify mand s) qs #> qualify0 end;
    3.10  
    3.11      fun note_if_note_all (noted0, lthy0) =
     4.1 --- a/src/HOL/Tools/BNF/bnf_fp_util.ML	Mon Mar 30 20:51:11 2015 +0200
     4.2 +++ b/src/HOL/Tools/BNF/bnf_fp_util.ML	Mon Mar 30 22:34:59 2015 +0200
     4.3 @@ -613,7 +613,9 @@
     4.4        subtract (op =) Xs (filter (fn T => exists (fn Ts => member (op =) Ts T) Ass) resBs) @ Xs;
     4.5  
     4.6      fun raw_qualify base_b =
     4.7 -      let val (_, qs, n) = Binding.dest base_b;
     4.8 +      let
     4.9 +        val qs = Binding.path_of base_b;
    4.10 +        val n = Binding.name_of base_b;
    4.11        in
    4.12          Binding.prefix_name rawN
    4.13          #> fold_rev (fn (s, mand) => Binding.qualify mand s) (qs @ [(n, true)])
     5.1 --- a/src/HOL/Tools/BNF/bnf_util.ML	Mon Mar 30 20:51:11 2015 +0200
     5.2 +++ b/src/HOL/Tools/BNF/bnf_util.ML	Mon Mar 30 22:34:59 2015 +0200
     5.3 @@ -142,7 +142,7 @@
     5.4  fun typedef (b, Ts, mx) set opt_morphs tac lthy =
     5.5    let
     5.6      (*Work around loss of qualification in "typedef" axioms by replicating it in the name*)
     5.7 -    val b' = fold_rev Binding.prefix_name (map (suffix "_" o fst) (#2 (Binding.dest b))) b;
     5.8 +    val b' = fold_rev Binding.prefix_name (map (suffix "_" o fst) (Binding.path_of b)) b;
     5.9      val ((name, info), (lthy, lthy_old)) =
    5.10        lthy
    5.11        |> Local_Theory.conceal
     6.1 --- a/src/Pure/General/binding.ML	Mon Mar 30 20:51:11 2015 +0200
     6.2 +++ b/src/Pure/General/binding.ML	Mon Mar 30 22:34:59 2015 +0200
     6.3 @@ -10,7 +10,8 @@
     6.4  signature BINDING =
     6.5  sig
     6.6    eqtype binding
     6.7 -  val dest: binding -> bool * (string * bool) list * bstring
     6.8 +  val dest: binding -> {private: bool, conceal: bool, path: (string * bool) list, name: bstring}
     6.9 +  val path_of: binding -> (string * bool) list
    6.10    val make: bstring * Position.T -> binding
    6.11    val pos_of: binding -> Position.T
    6.12    val set_pos: Position.T -> binding -> binding
    6.13 @@ -28,6 +29,7 @@
    6.14    val prefix_of: binding -> (string * bool) list
    6.15    val map_prefix: ((string * bool) list -> (string * bool) list) -> binding -> binding
    6.16    val prefix: bool -> string -> binding -> binding
    6.17 +  val private: binding -> binding
    6.18    val conceal: binding -> binding
    6.19    val pretty: binding -> Pretty.T
    6.20    val print: binding -> string
    6.21 @@ -44,20 +46,24 @@
    6.22  (* datatype *)
    6.23  
    6.24  datatype binding = Binding of
    6.25 - {conceal: bool,                    (*internal -- for foundational purposes only*)
    6.26 + {private: bool,                    (*entry is strictly private -- no name space accesses*)
    6.27 +  conceal: bool,                    (*entry is for foundational purposes -- please ignore*)
    6.28    prefix: (string * bool) list,     (*system prefix*)
    6.29    qualifier: (string * bool) list,  (*user qualifier*)
    6.30    name: bstring,                    (*base name*)
    6.31    pos: Position.T};                 (*source position*)
    6.32  
    6.33 -fun make_binding (conceal, prefix, qualifier, name, pos) =
    6.34 -  Binding {conceal = conceal, prefix = prefix, qualifier = qualifier, name = name, pos = pos};
    6.35 +fun make_binding (private, conceal, prefix, qualifier, name, pos) =
    6.36 +  Binding {private = private, conceal = conceal, prefix = prefix,
    6.37 +    qualifier = qualifier, name = name, pos = pos};
    6.38  
    6.39 -fun map_binding f (Binding {conceal, prefix, qualifier, name, pos}) =
    6.40 -  make_binding (f (conceal, prefix, qualifier, name, pos));
    6.41 +fun map_binding f (Binding {private, conceal, prefix, qualifier, name, pos}) =
    6.42 +  make_binding (f (private, conceal, prefix, qualifier, name, pos));
    6.43  
    6.44 -fun dest (Binding {conceal, prefix, qualifier, name, ...}) =
    6.45 -  (conceal, prefix @ qualifier, name);
    6.46 +fun dest (Binding {private, conceal, prefix, qualifier, name, ...}) =
    6.47 +  {private = private, conceal = conceal, path = prefix @ qualifier, name = name};
    6.48 +
    6.49 +val path_of = #path o dest;
    6.50  
    6.51  
    6.52  
    6.53 @@ -65,11 +71,12 @@
    6.54  
    6.55  (* name and position *)
    6.56  
    6.57 -fun make (name, pos) = make_binding (false, [], [], name, pos);
    6.58 +fun make (name, pos) = make_binding (false, false, [], [], name, pos);
    6.59  
    6.60  fun pos_of (Binding {pos, ...}) = pos;
    6.61  fun set_pos pos =
    6.62 -  map_binding (fn (conceal, prefix, qualifier, name, _) => (conceal, prefix, qualifier, name, pos));
    6.63 +  map_binding (fn (private, conceal, prefix, qualifier, name, _) =>
    6.64 +    (private, conceal, prefix, qualifier, name, pos));
    6.65  
    6.66  fun name name = make (name, Position.none);
    6.67  fun name_of (Binding {name, ...}) = name;
    6.68 @@ -77,8 +84,8 @@
    6.69  fun eq_name (b, b') = name_of b = name_of b';
    6.70  
    6.71  fun map_name f =
    6.72 -  map_binding (fn (conceal, prefix, qualifier, name, pos) =>
    6.73 -    (conceal, prefix, qualifier, f name, pos));
    6.74 +  map_binding (fn (private, conceal, prefix, qualifier, name, pos) =>
    6.75 +    (private, conceal, prefix, qualifier, f name, pos));
    6.76  
    6.77  val prefix_name = map_name o prefix;
    6.78  val suffix_name = map_name o suffix;
    6.79 @@ -91,17 +98,18 @@
    6.80  
    6.81  fun qualify _ "" = I
    6.82    | qualify mandatory qual =
    6.83 -      map_binding (fn (conceal, prefix, qualifier, name, pos) =>
    6.84 -        (conceal, prefix, (qual, mandatory) :: qualifier, name, pos));
    6.85 +      map_binding (fn (private, conceal, prefix, qualifier, name, pos) =>
    6.86 +        (private, conceal, prefix, (qual, mandatory) :: qualifier, name, pos));
    6.87  
    6.88 -fun qualified mandatory name' = map_binding (fn (conceal, prefix, qualifier, name, pos) =>
    6.89 -  let val qualifier' = if name = "" then qualifier else qualifier @ [(name, mandatory)]
    6.90 -  in (conceal, prefix, qualifier', name', pos) end);
    6.91 +fun qualified mandatory name' =
    6.92 +  map_binding (fn (private, conceal, prefix, qualifier, name, pos) =>
    6.93 +    let val qualifier' = if name = "" then qualifier else qualifier @ [(name, mandatory)]
    6.94 +    in (private, conceal, prefix, qualifier', name', pos) end);
    6.95  
    6.96  fun qualified_name "" = empty
    6.97    | qualified_name s =
    6.98        let val (qualifier, name) = split_last (Long_Name.explode s)
    6.99 -      in make_binding (false, [], map (rpair false) qualifier, name, Position.none) end;
   6.100 +      in make_binding (false, false, [], map (rpair false) qualifier, name, Position.none) end;
   6.101  
   6.102  
   6.103  (* system prefix *)
   6.104 @@ -109,18 +117,22 @@
   6.105  fun prefix_of (Binding {prefix, ...}) = prefix;
   6.106  
   6.107  fun map_prefix f =
   6.108 -  map_binding (fn (conceal, prefix, qualifier, name, pos) =>
   6.109 -    (conceal, f prefix, qualifier, name, pos));
   6.110 +  map_binding (fn (private, conceal, prefix, qualifier, name, pos) =>
   6.111 +    (private, conceal, f prefix, qualifier, name, pos));
   6.112  
   6.113  fun prefix _ "" = I
   6.114    | prefix mandatory prfx = map_prefix (cons (prfx, mandatory));
   6.115  
   6.116  
   6.117 -(* conceal *)
   6.118 +(* visibility flags *)
   6.119 +
   6.120 +val private =
   6.121 +  map_binding (fn (_, conceal, prefix, qualifier, name, pos) =>
   6.122 +    (true, conceal, prefix, qualifier, name, pos));
   6.123  
   6.124  val conceal =
   6.125 -  map_binding (fn (_, prefix, qualifier, name, pos) =>
   6.126 -    (true, prefix, qualifier, name, pos));
   6.127 +  map_binding (fn (private, _, prefix, qualifier, name, pos) =>
   6.128 +    (private, true, prefix, qualifier, name, pos));
   6.129  
   6.130  
   6.131  (* print *)
   6.132 @@ -148,4 +160,3 @@
   6.133  end;
   6.134  
   6.135  type binding = Binding.binding;
   6.136 -
     7.1 --- a/src/Pure/General/name_space.ML	Mon Mar 30 20:51:11 2015 +0200
     7.2 +++ b/src/Pure/General/name_space.ML	Mon Mar 30 22:34:59 2015 +0200
     7.3 @@ -33,6 +33,7 @@
     7.4    val completion: Context.generic -> T -> xstring * Position.T -> Completion.T
     7.5    val merge: T * T -> T
     7.6    type naming
     7.7 +  val private: naming -> naming
     7.8    val conceal: naming -> naming
     7.9    val get_group: naming -> serial option
    7.10    val set_group: serial option -> naming -> naming
    7.11 @@ -283,32 +284,37 @@
    7.12  (* datatype naming *)
    7.13  
    7.14  datatype naming = Naming of
    7.15 - {conceal: bool,
    7.16 + {private: bool,
    7.17 +  conceal: bool,
    7.18    group: serial option,
    7.19    theory_name: string,
    7.20    path: (string * bool) list};
    7.21  
    7.22 -fun make_naming (conceal, group, theory_name, path) =
    7.23 -  Naming {conceal = conceal, group = group, theory_name = theory_name, path = path};
    7.24 +fun make_naming (private, conceal, group, theory_name, path) =
    7.25 +  Naming {private = private, conceal = conceal, group = group,
    7.26 +    theory_name = theory_name, path = path};
    7.27  
    7.28 -fun map_naming f (Naming {conceal, group, theory_name, path}) =
    7.29 -  make_naming (f (conceal, group, theory_name, path));
    7.30 +fun map_naming f (Naming {private, conceal, group, theory_name, path}) =
    7.31 +  make_naming (f (private, conceal, group, theory_name, path));
    7.32  
    7.33 -fun map_path f = map_naming (fn (conceal, group, theory_name, path) =>
    7.34 -  (conceal, group, theory_name, f path));
    7.35 +fun map_path f = map_naming (fn (private, conceal, group, theory_name, path) =>
    7.36 +  (private, conceal, group, theory_name, f path));
    7.37  
    7.38  
    7.39 -val conceal = map_naming (fn (_, group, theory_name, path) =>
    7.40 -  (true, group, theory_name, path));
    7.41 +val private = map_naming (fn (_, conceal, group, theory_name, path) =>
    7.42 +  (true, conceal, group, theory_name, path));
    7.43  
    7.44 -fun set_theory_name theory_name = map_naming (fn (conceal, group, _, path) =>
    7.45 -  (conceal, group, theory_name, path));
    7.46 +val conceal = map_naming (fn (private, _, group, theory_name, path) =>
    7.47 +  (private, true, group, theory_name, path));
    7.48 +
    7.49 +fun set_theory_name theory_name = map_naming (fn (private, conceal, group, _, path) =>
    7.50 +  (private, conceal, group, theory_name, path));
    7.51  
    7.52  
    7.53  fun get_group (Naming {group, ...}) = group;
    7.54  
    7.55 -fun set_group group = map_naming (fn (conceal, _, theory_name, path) =>
    7.56 -  (conceal, group, theory_name, path));
    7.57 +fun set_group group = map_naming (fn (private, conceal, _, theory_name, path) =>
    7.58 +  (private, conceal, group, theory_name, path));
    7.59  
    7.60  fun new_group naming = set_group (SOME (serial ())) naming;
    7.61  val reset_group = set_group NONE;
    7.62 @@ -319,9 +325,9 @@
    7.63  fun mandatory_path elems = map_path (fn path => path @ [(elems, true)]);
    7.64  
    7.65  fun qualified_path mandatory binding = map_path (fn path =>
    7.66 -  path @ #2 (Binding.dest (Binding.qualified mandatory "" binding)));
    7.67 +  path @ Binding.path_of (Binding.qualified mandatory "" binding));
    7.68  
    7.69 -val global_naming = make_naming (false, NONE, "", []);
    7.70 +val global_naming = make_naming (false, false, NONE, "", []);
    7.71  val local_naming = global_naming |> add_path Long_Name.localN;
    7.72  
    7.73  
    7.74 @@ -329,27 +335,28 @@
    7.75  
    7.76  fun err_bad binding = error (Binding.bad binding);
    7.77  
    7.78 -fun transform_binding (Naming {conceal = true, ...}) = Binding.conceal
    7.79 -  | transform_binding _ = I;
    7.80 +fun transform_binding (Naming {private, conceal, ...}) =
    7.81 +  private ? Binding.private #>
    7.82 +  conceal ? Binding.conceal;
    7.83  
    7.84  val bad_specs = ["", "??", "__"];
    7.85  
    7.86 -fun name_spec (naming as Naming {path, ...}) raw_binding =
    7.87 +fun name_spec (naming as Naming {path = path1, ...}) raw_binding =
    7.88    let
    7.89      val binding = transform_binding naming raw_binding;
    7.90 -    val (concealed, prefix, name) = Binding.dest binding;
    7.91 +    val {private, conceal, path = path2, name} = Binding.dest binding;
    7.92      val _ = Long_Name.is_qualified name andalso err_bad binding;
    7.93  
    7.94 -    val spec1 = maps (fn (a, b) => map (rpair b) (Long_Name.explode a)) (path @ prefix);
    7.95 +    val spec1 = maps (fn (a, b) => map (rpair b) (Long_Name.explode a)) (path1 @ path2);
    7.96      val spec2 = if name = "" then [] else [(name, true)];
    7.97      val spec = spec1 @ spec2;
    7.98      val _ =
    7.99        exists (fn (a, _) => member (op =) bad_specs a orelse exists_string (fn s => s = "\"") a) spec
   7.100        andalso err_bad binding;
   7.101 -  in (concealed, if null spec2 then [] else spec) end;
   7.102 +  in {private = private, conceal = conceal, spec = if null spec2 then [] else spec} end;
   7.103  
   7.104  fun full_name naming =
   7.105 -  name_spec naming #> #2 #> map #1 #> Long_Name.implode;
   7.106 +  name_spec naming #> #spec #> map #1 #> Long_Name.implode;
   7.107  
   7.108  val base_name = full_name global_naming #> Long_Name.base_name;
   7.109  
   7.110 @@ -366,11 +373,13 @@
   7.111  fun mandatory_suffixes xs = map rev (mandatory_prefixes (rev xs));
   7.112  
   7.113  fun accesses naming binding =
   7.114 -  let
   7.115 -    val spec = #2 (name_spec naming binding);
   7.116 -    val sfxs = mandatory_suffixes spec;
   7.117 -    val pfxs = mandatory_prefixes spec;
   7.118 -  in apply2 (map Long_Name.implode) (sfxs @ pfxs, sfxs) end;
   7.119 +  (case name_spec naming binding of
   7.120 +    {private = true, ...} => ([], [])
   7.121 +  | {spec, ...} =>
   7.122 +      let
   7.123 +        val sfxs = mandatory_suffixes spec;
   7.124 +        val pfxs = mandatory_prefixes spec;
   7.125 +      in apply2 (map Long_Name.implode) (sfxs @ pfxs, sfxs) end);
   7.126  
   7.127  
   7.128  (* hide *)
   7.129 @@ -433,7 +442,7 @@
   7.130    let
   7.131      val naming = naming_of context;
   7.132      val Naming {group, theory_name, ...} = naming;
   7.133 -    val (concealed, spec) = name_spec naming binding;
   7.134 +    val {conceal, spec, ...} = name_spec naming binding;
   7.135      val (accs, accs') = accesses naming binding;
   7.136  
   7.137      val name = Long_Name.implode (map fst spec);
   7.138 @@ -441,7 +450,7 @@
   7.139  
   7.140      val (proper_pos, pos) = Position.default (Binding.pos_of binding);
   7.141      val entry =
   7.142 -     {concealed = concealed,
   7.143 +     {concealed = conceal,
   7.144        group = group,
   7.145        theory_name = theory_name,
   7.146        pos = pos,
   7.147 @@ -556,4 +565,3 @@
   7.148  fun markup_table ctxt (Table (space, tab)) = markup_entries ctxt space (Change_Table.dest tab);
   7.149  
   7.150  end;
   7.151 -