allow name space entries to be "concealed" -- via binding/naming/local_theory;
authorwenzelm
Sun Oct 25 12:27:21 2009 +0100 (2009-10-25 ago)
changeset 3315756f836b9414f
parent 33156 57222d336c86
child 33158 6e3dc0ba2b06
allow name space entries to be "concealed" -- via binding/naming/local_theory;
src/Pure/General/binding.ML
src/Pure/General/name_space.ML
src/Pure/Isar/local_theory.ML
src/Pure/Isar/proof_context.ML
src/Pure/sign.ML
     1.1 --- a/src/Pure/General/binding.ML	Sun Oct 25 11:58:11 2009 +0100
     1.2 +++ b/src/Pure/General/binding.ML	Sun Oct 25 12:27:21 2009 +0100
     1.3 @@ -10,7 +10,7 @@
     1.4  signature BINDING =
     1.5  sig
     1.6    type binding
     1.7 -  val dest: binding -> (string * bool) list * bstring
     1.8 +  val dest: binding -> bool * (string * bool) list * bstring
     1.9    val make: bstring * Position.T -> binding
    1.10    val pos_of: binding -> Position.T
    1.11    val name: bstring -> binding
    1.12 @@ -27,6 +27,7 @@
    1.13    val prefix_of: binding -> (string * bool) list
    1.14    val map_prefix: ((string * bool) list -> (string * bool) list) -> binding -> binding
    1.15    val prefix: bool -> string -> binding -> binding
    1.16 +  val conceal: binding -> binding
    1.17    val str_of: binding -> string
    1.18  end;
    1.19  
    1.20 @@ -38,19 +39,21 @@
    1.21  (* datatype *)
    1.22  
    1.23  abstype binding = Binding of
    1.24 - {prefix: (string * bool) list,     (*system prefix*)
    1.25 + {conceal: bool,                    (*internal -- for foundational purposes only*)
    1.26 +  prefix: (string * bool) list,     (*system prefix*)
    1.27    qualifier: (string * bool) list,  (*user qualifier*)
    1.28    name: bstring,                    (*base name*)
    1.29    pos: Position.T}                  (*source position*)
    1.30  with
    1.31  
    1.32 -fun make_binding (prefix, qualifier, name, pos) =
    1.33 -  Binding {prefix = prefix, qualifier = qualifier, name = name, pos = pos};
    1.34 +fun make_binding (conceal, prefix, qualifier, name, pos) =
    1.35 +  Binding {conceal = conceal, prefix = prefix, qualifier = qualifier, name = name, pos = pos};
    1.36  
    1.37 -fun map_binding f (Binding {prefix, qualifier, name, pos}) =
    1.38 -  make_binding (f (prefix, qualifier, name, pos));
    1.39 +fun map_binding f (Binding {conceal, prefix, qualifier, name, pos}) =
    1.40 +  make_binding (f (conceal, prefix, qualifier, name, pos));
    1.41  
    1.42 -fun dest (Binding {prefix, qualifier, name, ...}) = (prefix @ qualifier, name);
    1.43 +fun dest (Binding {conceal, prefix, qualifier, name, ...}) =
    1.44 +  (conceal, prefix @ qualifier, name);
    1.45  
    1.46  
    1.47  
    1.48 @@ -58,7 +61,7 @@
    1.49  
    1.50  (* name and position *)
    1.51  
    1.52 -fun make (name, pos) = make_binding ([], [], name, pos);
    1.53 +fun make (name, pos) = make_binding (false, [], [], name, pos);
    1.54  fun name name = make (name, Position.none);
    1.55  
    1.56  fun pos_of (Binding {pos, ...}) = pos;
    1.57 @@ -66,7 +69,10 @@
    1.58  
    1.59  fun eq_name (b, b') = name_of b = name_of b';
    1.60  
    1.61 -fun map_name f = map_binding (fn (prefix, qualifier, name, pos) => (prefix, qualifier, f name, pos));
    1.62 +fun map_name f =
    1.63 +  map_binding (fn (conceal, prefix, qualifier, name, pos) =>
    1.64 +    (conceal, prefix, qualifier, f name, pos));
    1.65 +
    1.66  val prefix_name = map_name o prefix;
    1.67  val suffix_name = map_name o suffix;
    1.68  
    1.69 @@ -77,13 +83,14 @@
    1.70  (* user qualifier *)
    1.71  
    1.72  fun qualify _ "" = I
    1.73 -  | qualify mandatory qual = map_binding (fn (prefix, qualifier, name, pos) =>
    1.74 -      (prefix, (qual, mandatory) :: qualifier, name, pos));
    1.75 +  | qualify mandatory qual =
    1.76 +      map_binding (fn (conceal, prefix, qualifier, name, pos) =>
    1.77 +        (conceal, prefix, (qual, mandatory) :: qualifier, name, pos));
    1.78  
    1.79  fun qualified_name "" = empty
    1.80    | qualified_name s =
    1.81        let val (qualifier, name) = split_last (Long_Name.explode s)
    1.82 -      in make_binding ([], map (rpair false) qualifier, name, Position.none) end;
    1.83 +      in make_binding (false, [], map (rpair false) qualifier, name, Position.none) end;
    1.84  
    1.85  fun qualified_name_of (b as Binding {qualifier, name, ...}) =
    1.86    if is_empty b then ""
    1.87 @@ -94,13 +101,21 @@
    1.88  
    1.89  fun prefix_of (Binding {prefix, ...}) = prefix;
    1.90  
    1.91 -fun map_prefix f = map_binding (fn (prefix, qualifier, name, pos) =>
    1.92 -  (f prefix, qualifier, name, pos));
    1.93 +fun map_prefix f =
    1.94 +  map_binding (fn (conceal, prefix, qualifier, name, pos) =>
    1.95 +    (conceal, f prefix, qualifier, name, pos));
    1.96  
    1.97  fun prefix _ "" = I
    1.98    | prefix mandatory prfx = map_prefix (cons (prfx, mandatory));
    1.99  
   1.100  
   1.101 +(* conceal *)
   1.102 +
   1.103 +val conceal =
   1.104 +  map_binding (fn (_, prefix, qualifier, name, pos) =>
   1.105 +    (true, prefix, qualifier, name, pos));
   1.106 +
   1.107 +
   1.108  (* str_of *)
   1.109  
   1.110  fun str_of binding =
     2.1 --- a/src/Pure/General/name_space.ML	Sun Oct 25 11:58:11 2009 +0100
     2.2 +++ b/src/Pure/General/name_space.ML	Sun Oct 25 12:27:21 2009 +0100
     2.3 @@ -22,22 +22,24 @@
     2.4    type T
     2.5    val empty: string -> T
     2.6    val kind_of: T -> string
     2.7 -  val the_entry: T -> string -> {is_system: bool, pos: Position.T, id: serial}
     2.8 +  val the_entry: T -> string -> {concealed: bool, pos: Position.T, id: serial}
     2.9 +  val is_concealed: T -> string -> bool
    2.10    val intern: T -> xstring -> string
    2.11 -  val extern: T -> string -> xstring
    2.12    val extern_flags: {long_names: bool, short_names: bool, unique_names: bool} ->
    2.13      T -> string -> xstring
    2.14 +  val extern: T -> string -> xstring
    2.15    val hide: bool -> string -> T -> T
    2.16    val merge: T * T -> T
    2.17    type naming
    2.18    val default_naming: naming
    2.19 -  val declare: bool -> naming -> binding -> T -> string * T
    2.20 -  val full_name: naming -> binding -> string
    2.21 -  val external_names: naming -> string -> string list
    2.22    val add_path: string -> naming -> naming
    2.23    val root_path: naming -> naming
    2.24    val parent_path: naming -> naming
    2.25    val mandatory_path: string -> naming -> naming
    2.26 +  val conceal: naming -> naming
    2.27 +  val full_name: naming -> binding -> string
    2.28 +  val external_names: naming -> string -> string list
    2.29 +  val declare: bool -> naming -> binding -> T -> string * T
    2.30    type 'a table = T * 'a Symtab.table
    2.31    val define: bool -> naming -> binding * 'a -> 'a table -> string * 'a table
    2.32    val empty_table: string -> 'a table
    2.33 @@ -64,7 +66,7 @@
    2.34  
    2.35  type entry =
    2.36   {externals: xstring list,
    2.37 -  is_system: bool,
    2.38 +  concealed: bool,
    2.39    pos: Position.T,
    2.40    id: serial};
    2.41  
    2.42 @@ -104,7 +106,9 @@
    2.43  fun the_entry (Name_Space {kind, entries, ...}) name =
    2.44    (case Symtab.lookup entries name of
    2.45      NONE => error ("Unknown " ^ kind ^ " " ^ quote name)
    2.46 -  | SOME {is_system, pos, id, ...} => {is_system = is_system, pos = pos, id = id});
    2.47 +  | SOME {concealed, pos, id, ...} => {concealed = concealed, pos = pos, id = id});
    2.48 +
    2.49 +fun is_concealed space name = #concealed (the_entry space name);
    2.50  
    2.51  
    2.52  (* name accesses *)
    2.53 @@ -209,36 +213,41 @@
    2.54  
    2.55  (* datatype naming *)
    2.56  
    2.57 -datatype naming = Naming of (string * bool) list;
    2.58 -fun map_naming f (Naming path) = Naming (f path);
    2.59 +datatype naming = Naming of bool * (string * bool) list;
    2.60  
    2.61 -val default_naming = Naming [];
    2.62 +fun map_naming f (Naming (conceal, path)) = Naming (f (conceal, path));
    2.63 +fun map_path f = map_naming (apsnd f);
    2.64 +
    2.65 +val default_naming = Naming (false, []);
    2.66  
    2.67 -fun add_path elems = map_naming (fn path => path @ [(elems, false)]);
    2.68 -val root_path = map_naming (fn _ => []);
    2.69 -val parent_path = map_naming (perhaps (try (#1 o split_last)));
    2.70 -fun mandatory_path elems = map_naming (fn path => path @ [(elems, true)]);
    2.71 +fun add_path elems = map_path (fn path => path @ [(elems, false)]);
    2.72 +val root_path = map_path (fn _ => []);
    2.73 +val parent_path = map_path (perhaps (try (#1 o split_last)));
    2.74 +fun mandatory_path elems = map_path (fn path => path @ [(elems, true)]);
    2.75 +
    2.76 +val conceal = map_naming (fn (_, path) => (true, path));
    2.77  
    2.78  
    2.79  (* full name *)
    2.80  
    2.81  fun err_bad binding = error ("Bad name binding " ^ quote (Binding.str_of binding));
    2.82  
    2.83 -fun name_spec (Naming path) binding =
    2.84 +fun name_spec (Naming (conceal1, path)) binding =
    2.85    let
    2.86 -    val (prefix, name) = Binding.dest binding;
    2.87 +    val (conceal2, prefix, name) = Binding.dest binding;
    2.88      val _ = Long_Name.is_qualified name andalso err_bad binding;
    2.89  
    2.90 +    val concealed = conceal1 orelse conceal2;
    2.91      val spec1 = maps (fn (a, b) => map (rpair b) (Long_Name.explode a)) (path @ prefix);
    2.92      val spec2 = if name = "" then [] else [(name, true)];
    2.93      val spec = spec1 @ spec2;
    2.94      val _ =
    2.95        exists (fn (a, _) => a = "" orelse a = "??" orelse exists_string (fn s => s = "\"") a) spec
    2.96        andalso err_bad binding;
    2.97 -  in if null spec2 then [] else spec end;
    2.98 +  in (concealed, if null spec2 then [] else spec) end;
    2.99  
   2.100 -fun full naming = name_spec naming #> map fst;
   2.101 -fun full_name naming = full naming #> Long_Name.implode;
   2.102 +fun full_name naming =
   2.103 +  name_spec naming #> snd #> map fst #> Long_Name.implode;
   2.104  
   2.105  
   2.106  (* accesses *)
   2.107 @@ -254,7 +263,7 @@
   2.108  
   2.109  fun accesses naming binding =
   2.110    let
   2.111 -    val spec = name_spec naming binding;
   2.112 +    val spec = #2 (name_spec naming binding);
   2.113      val sfxs = mandatory_suffixes spec;
   2.114      val pfxs = mandatory_prefixes spec;
   2.115    in pairself (map Long_Name.implode) (sfxs @ pfxs, sfxs) end;
   2.116 @@ -275,13 +284,15 @@
   2.117  
   2.118  fun declare strict naming binding space =
   2.119    let
   2.120 -    val names = full naming binding;
   2.121 -    val name = Long_Name.implode names;
   2.122 +    val (concealed, spec) = name_spec naming binding;
   2.123 +    val (accs, accs') = accesses naming binding;
   2.124 +
   2.125 +    val name = Long_Name.implode (map fst spec);
   2.126      val _ = name = "" andalso err_bad binding;
   2.127 -    val (accs, accs') = accesses naming binding;
   2.128 +
   2.129      val entry =
   2.130       {externals = accs',
   2.131 -      is_system = false,
   2.132 +      concealed = concealed,
   2.133        pos = Position.default (Binding.pos_of binding),
   2.134        id = serial ()};
   2.135      val space' = space |> fold (add_name name) accs |> new_entry strict (name, entry);
     3.1 --- a/src/Pure/Isar/local_theory.ML	Sun Oct 25 11:58:11 2009 +0100
     3.2 +++ b/src/Pure/Isar/local_theory.ML	Sun Oct 25 12:27:21 2009 +0100
     3.3 @@ -72,12 +72,14 @@
     3.4  
     3.5  datatype lthy = LThy of
     3.6   {group: string,
     3.7 +  conceal: bool,
     3.8    theory_prefix: string,
     3.9    operations: operations,
    3.10    target: Proof.context};
    3.11  
    3.12 -fun make_lthy (group, theory_prefix, operations, target) =
    3.13 -  LThy {group = group, theory_prefix = theory_prefix, operations = operations, target = target};
    3.14 +fun make_lthy (group, conceal, theory_prefix, operations, target) =
    3.15 +  LThy {group = group, conceal = conceal, theory_prefix = theory_prefix,
    3.16 +    operations = operations, target = target};
    3.17  
    3.18  
    3.19  (* context data *)
    3.20 @@ -94,8 +96,8 @@
    3.21    | SOME (LThy data) => data);
    3.22  
    3.23  fun map_lthy f lthy =
    3.24 -  let val {group, theory_prefix, operations, target} = get_lthy lthy
    3.25 -  in Data.put (SOME (make_lthy (f (group, theory_prefix, operations, target)))) lthy end;
    3.26 +  let val {group, conceal, theory_prefix, operations, target} = get_lthy lthy
    3.27 +  in Data.put (SOME (make_lthy (f (group, conceal, theory_prefix, operations, target)))) lthy end;
    3.28  
    3.29  
    3.30  (* group *)
    3.31 @@ -110,8 +112,8 @@
    3.32  fun group_position_of lthy =
    3.33    group_properties_of lthy @ Position.properties_of (Position.thread_data ());
    3.34  
    3.35 -fun set_group group = map_lthy (fn (_, theory_prefix, operations, target) =>
    3.36 -  (group, theory_prefix, operations, target));
    3.37 +fun set_group group = map_lthy (fn (_, conceal, theory_prefix, operations, target) =>
    3.38 +  (group, conceal, theory_prefix, operations, target));
    3.39  
    3.40  
    3.41  (* target *)
    3.42 @@ -119,8 +121,8 @@
    3.43  val target_of = #target o get_lthy;
    3.44  val affirm = tap target_of;
    3.45  
    3.46 -fun map_target f = map_lthy (fn (group, theory_prefix, operations, target) =>
    3.47 -  (group, theory_prefix, operations, f target));
    3.48 +fun map_target f = map_lthy (fn (group, conceal, theory_prefix, operations, target) =>
    3.49 +  (group, conceal, theory_prefix, operations, f target));
    3.50  
    3.51  
    3.52  (* substructure mappings *)
    3.53 @@ -138,15 +140,22 @@
    3.54  val checkpoint = raw_theory Theory.checkpoint;
    3.55  
    3.56  fun full_naming lthy =
    3.57 -  Sign.naming_of (ProofContext.theory_of lthy)
    3.58 -  |> Name_Space.mandatory_path (#theory_prefix (get_lthy lthy));
    3.59 +  let val {conceal, theory_prefix, ...} = get_lthy lthy in
    3.60 +    Sign.naming_of (ProofContext.theory_of lthy)
    3.61 +    |> Name_Space.mandatory_path theory_prefix
    3.62 +    |> conceal ? Name_Space.conceal
    3.63 +  end;
    3.64  
    3.65  fun full_name naming = Name_Space.full_name (full_naming naming);
    3.66  
    3.67 -fun theory_result f lthy = lthy |> raw_theory_result (fn thy => thy
    3.68 -  |> Sign.mandatory_path (#theory_prefix (get_lthy lthy))
    3.69 -  |> f
    3.70 -  ||> Sign.restore_naming thy);
    3.71 +fun theory_result f lthy = lthy |> raw_theory_result (fn thy =>
    3.72 +  let val {conceal, theory_prefix, ...} = get_lthy lthy in
    3.73 +    thy
    3.74 +    |> Sign.mandatory_path theory_prefix
    3.75 +    |> conceal ? Sign.conceal
    3.76 +    |> f
    3.77 +    ||> Sign.restore_naming thy
    3.78 +  end);
    3.79  
    3.80  fun theory f = #2 o theory_result (f #> pair ());
    3.81  
    3.82 @@ -197,12 +206,12 @@
    3.83  (* init *)
    3.84  
    3.85  fun init theory_prefix operations target = target |> Data.map
    3.86 -  (fn NONE => SOME (make_lthy ("", theory_prefix, operations, target))
    3.87 +  (fn NONE => SOME (make_lthy ("", false, theory_prefix, operations, target))
    3.88      | SOME _ => error "Local theory already initialized")
    3.89    |> checkpoint;
    3.90  
    3.91  fun restore lthy =
    3.92 -  let val {group = _, theory_prefix, operations, target} = get_lthy lthy
    3.93 +  let val {theory_prefix, operations, target, ...} = get_lthy lthy
    3.94    in init theory_prefix operations target end;
    3.95  
    3.96  val reinit = checkpoint o operation #reinit;
     4.1 --- a/src/Pure/Isar/proof_context.ML	Sun Oct 25 11:58:11 2009 +0100
     4.2 +++ b/src/Pure/Isar/proof_context.ML	Sun Oct 25 12:27:21 2009 +0100
     4.3 @@ -94,6 +94,7 @@
     4.4    val get_thm: Proof.context -> xstring -> thm
     4.5    val add_path: string -> Proof.context -> Proof.context
     4.6    val mandatory_path: string -> Proof.context -> Proof.context
     4.7 +  val conceal: Proof.context -> Proof.context
     4.8    val restore_naming: Proof.context -> Proof.context -> Proof.context
     4.9    val reset_naming: Proof.context -> Proof.context
    4.10    val note_thmss: string -> (Thm.binding * (thm list * attribute list) list) list ->
    4.11 @@ -926,6 +927,7 @@
    4.12  
    4.13  val add_path = map_naming o Name_Space.add_path;
    4.14  val mandatory_path = map_naming o Name_Space.mandatory_path;
    4.15 +val conceal = map_naming Name_Space.conceal;
    4.16  val restore_naming = map_naming o K o naming_of;
    4.17  val reset_naming = map_naming (K local_naming);
    4.18  
     5.1 --- a/src/Pure/sign.ML	Sun Oct 25 11:58:11 2009 +0100
     5.2 +++ b/src/Pure/sign.ML	Sun Oct 25 12:27:21 2009 +0100
     5.3 @@ -125,6 +125,7 @@
     5.4    val parent_path: theory -> theory
     5.5    val mandatory_path: string -> theory -> theory
     5.6    val local_path: theory -> theory
     5.7 +  val conceal: theory -> theory
     5.8    val restore_naming: theory -> theory -> theory
     5.9    val hide_class: bool -> string -> theory -> theory
    5.10    val hide_type: bool -> string -> theory -> theory
    5.11 @@ -618,6 +619,8 @@
    5.12  
    5.13  fun local_path thy = thy |> root_path |> add_path (Context.theory_name thy);
    5.14  
    5.15 +val conceal = map_naming Name_Space.conceal;
    5.16 +
    5.17  val restore_naming = map_naming o K o naming_of;
    5.18  
    5.19