support for explicit scope of private entries;
authorwenzelm
Tue Mar 31 22:31:05 2015 +0200 (2015-03-31)
changeset 59886e0dc738eb08c
parent 59885 3470a265d404
child 59887 43dc3c660f41
support for explicit scope of private entries;
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	Tue Mar 31 21:12:22 2015 +0200
     1.2 +++ b/src/Pure/General/binding.ML	Tue Mar 31 22:31:05 2015 +0200
     1.3 @@ -9,6 +9,8 @@
     1.4  
     1.5  signature BINDING =
     1.6  sig
     1.7 +  eqtype scope
     1.8 +  val new_scope: unit -> scope
     1.9    eqtype binding
    1.10    val path_of: binding -> (string * bool) list
    1.11    val make: bstring * Position.T -> binding
    1.12 @@ -28,15 +30,16 @@
    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 private: binding -> binding
    1.17 +  val private: scope -> binding -> binding
    1.18 +  val private_default: scope option -> binding -> binding
    1.19    val concealed: binding -> binding
    1.20    val pretty: binding -> Pretty.T
    1.21    val print: binding -> string
    1.22    val pp: binding -> Pretty.T
    1.23    val bad: binding -> string
    1.24    val check: binding -> unit
    1.25 -  val name_spec: (string * bool) list -> binding ->
    1.26 -    {private: bool, concealed: bool, spec: (string * bool) list}
    1.27 +  val name_spec: scope list -> (string * bool) list -> binding ->
    1.28 +    {accessible: bool, concealed: bool, spec: (string * bool) list}
    1.29  end;
    1.30  
    1.31  structure Binding: BINDING =
    1.32 @@ -44,10 +47,17 @@
    1.33  
    1.34  (** representation **)
    1.35  
    1.36 -(* datatype *)
    1.37 +(* scope of private entries *)
    1.38 +
    1.39 +datatype scope = Scope of serial;
    1.40 +
    1.41 +fun new_scope () = Scope (serial ());
    1.42 +
    1.43 +
    1.44 +(* binding *)
    1.45  
    1.46  datatype binding = Binding of
    1.47 - {private: bool,                    (*entry is strictly private -- no name space accesses*)
    1.48 + {private: scope option,            (*entry is strictly private within its scope*)
    1.49    concealed: bool,                  (*entry is for foundational purposes -- please ignore*)
    1.50    prefix: (string * bool) list,     (*system prefix*)
    1.51    qualifier: (string * bool) list,  (*user qualifier*)
    1.52 @@ -69,7 +79,7 @@
    1.53  
    1.54  (* name and position *)
    1.55  
    1.56 -fun make (name, pos) = make_binding (false, false, [], [], name, pos);
    1.57 +fun make (name, pos) = make_binding (NONE, false, [], [], name, pos);
    1.58  
    1.59  fun pos_of (Binding {pos, ...}) = pos;
    1.60  fun set_pos pos =
    1.61 @@ -107,7 +117,7 @@
    1.62  fun qualified_name "" = empty
    1.63    | qualified_name s =
    1.64        let val (qualifier, name) = split_last (Long_Name.explode s)
    1.65 -      in make_binding (false, false, [], map (rpair false) qualifier, name, Position.none) end;
    1.66 +      in make_binding (NONE, false, [], map (rpair false) qualifier, name, Position.none) end;
    1.67  
    1.68  
    1.69  (* system prefix *)
    1.70 @@ -124,9 +134,13 @@
    1.71  
    1.72  (* visibility flags *)
    1.73  
    1.74 -val private =
    1.75 +fun private scope =
    1.76    map_binding (fn (_, concealed, prefix, qualifier, name, pos) =>
    1.77 -    (true, concealed, prefix, qualifier, name, pos));
    1.78 +    (SOME scope, concealed, prefix, qualifier, name, pos));
    1.79 +
    1.80 +fun private_default private' =
    1.81 +  map_binding (fn (private, concealed, prefix, qualifier, name, pos) =>
    1.82 +    (if is_some private then private else private', concealed, prefix, qualifier, name, pos));
    1.83  
    1.84  val concealed =
    1.85    map_binding (fn (private, _, prefix, qualifier, name, pos) =>
    1.86 @@ -161,11 +175,16 @@
    1.87  
    1.88  val bad_specs = ["", "??", "__"];
    1.89  
    1.90 -fun name_spec path binding =
    1.91 +fun name_spec scopes path binding =
    1.92    let
    1.93      val Binding {private, concealed, prefix, qualifier, name, ...} = binding;
    1.94      val _ = Long_Name.is_qualified name andalso error (bad binding);
    1.95  
    1.96 +    val accessible =
    1.97 +      (case private of
    1.98 +        NONE => true
    1.99 +      | SOME scope => member (op =) scopes scope);
   1.100 +
   1.101      val spec1 =
   1.102        maps (fn (a, b) => map (rpair b) (Long_Name.explode a)) (path @ prefix @ qualifier);
   1.103      val spec2 = if name = "" then [] else [(name, true)];
   1.104 @@ -173,7 +192,7 @@
   1.105      val _ =
   1.106        exists (fn (a, _) => member (op =) bad_specs a orelse exists_string (fn s => s = "\"") a) spec
   1.107        andalso error (bad binding);
   1.108 -  in {private = private, concealed = concealed, spec = if null spec2 then [] else spec} end;
   1.109 +  in {accessible = accessible, concealed = concealed, spec = if null spec2 then [] else spec} end;
   1.110  
   1.111  end;
   1.112  
     2.1 --- a/src/Pure/General/name_space.ML	Tue Mar 31 21:12:22 2015 +0200
     2.2 +++ b/src/Pure/General/name_space.ML	Tue Mar 31 22:31:05 2015 +0200
     2.3 @@ -32,7 +32,9 @@
     2.4    val completion: Context.generic -> T -> xstring * Position.T -> Completion.T
     2.5    val merge: T * T -> T
     2.6    type naming
     2.7 -  val private: naming -> naming
     2.8 +  val get_scope: naming -> Binding.scope option
     2.9 +  val new_scope: naming -> Binding.scope * naming
    2.10 +  val private: Binding.scope -> naming -> naming
    2.11    val concealed: naming -> naming
    2.12    val get_group: naming -> serial option
    2.13    val set_group: serial option -> naming -> naming
    2.14 @@ -280,37 +282,48 @@
    2.15  (* datatype naming *)
    2.16  
    2.17  datatype naming = Naming of
    2.18 - {private: bool,
    2.19 + {scopes: Binding.scope list,
    2.20 +  private: Binding.scope option,
    2.21    concealed: bool,
    2.22    group: serial option,
    2.23    theory_name: string,
    2.24    path: (string * bool) list};
    2.25  
    2.26 -fun make_naming (private, concealed, group, theory_name, path) =
    2.27 -  Naming {private = private, concealed = concealed, group = group,
    2.28 -    theory_name = theory_name, path = path};
    2.29 +fun make_naming (scopes, private, concealed, group, theory_name, path) =
    2.30 +  Naming {scopes = scopes, private = private, concealed = concealed,
    2.31 +    group = group, theory_name = theory_name, path = path};
    2.32  
    2.33 -fun map_naming f (Naming {private, concealed, group, theory_name, path}) =
    2.34 -  make_naming (f (private, concealed, group, theory_name, path));
    2.35 +fun map_naming f (Naming {scopes, private, concealed, group, theory_name, path}) =
    2.36 +  make_naming (f (scopes, private, concealed, group, theory_name, path));
    2.37  
    2.38 -fun map_path f = map_naming (fn (private, concealed, group, theory_name, path) =>
    2.39 -  (private, concealed, group, theory_name, f path));
    2.40 +fun map_path f = map_naming (fn (scopes, private, concealed, group, theory_name, path) =>
    2.41 +  (scopes, private, concealed, group, theory_name, f path));
    2.42  
    2.43  
    2.44 -val private = map_naming (fn (_, concealed, group, theory_name, path) =>
    2.45 -  (true, concealed, group, theory_name, path));
    2.46 +fun get_scopes (Naming {scopes, ...}) = scopes;
    2.47 +val get_scope = try hd o get_scopes;
    2.48  
    2.49 -val concealed = map_naming (fn (private, _, group, theory_name, path) =>
    2.50 -  (private, true, group, theory_name, path));
    2.51 +fun new_scope naming =
    2.52 +  let
    2.53 +    val scope = Binding.new_scope ();
    2.54 +    val naming' =
    2.55 +      naming |> map_naming (fn (scopes, private, concealed, group, theory_name, path) =>
    2.56 +        (scope :: scopes, private, concealed, group, theory_name, path));
    2.57 +  in (scope, naming') end;
    2.58  
    2.59 -fun set_theory_name theory_name = map_naming (fn (private, concealed, group, _, path) =>
    2.60 -  (private, concealed, group, theory_name, path));
    2.61 +fun private scope = map_naming (fn (scopes, _, concealed, group, theory_name, path) =>
    2.62 +  (scopes, SOME scope, concealed, group, theory_name, path));
    2.63  
    2.64 +val concealed = map_naming (fn (scopes, private, _, group, theory_name, path) =>
    2.65 +  (scopes, private, true, group, theory_name, path));
    2.66 +
    2.67 +fun set_theory_name theory_name = map_naming (fn (scopes, private, concealed, group, _, path) =>
    2.68 +  (scopes, private, concealed, group, theory_name, path));
    2.69  
    2.70  fun get_group (Naming {group, ...}) = group;
    2.71  
    2.72 -fun set_group group = map_naming (fn (private, concealed, _, theory_name, path) =>
    2.73 -  (private, concealed, group, theory_name, path));
    2.74 +fun set_group group = map_naming (fn (scopes, private, concealed, _, theory_name, path) =>
    2.75 +  (scopes, private, concealed, group, theory_name, path));
    2.76  
    2.77  fun new_group naming = set_group (SOME (serial ())) naming;
    2.78  val reset_group = set_group NONE;
    2.79 @@ -325,18 +338,18 @@
    2.80  fun qualified_path mandatory binding = map_path (fn path =>
    2.81    path @ Binding.path_of (Binding.qualified mandatory "" binding));
    2.82  
    2.83 -val global_naming = make_naming (false, false, NONE, "", []);
    2.84 +val global_naming = make_naming ([], NONE, false, NONE, "", []);
    2.85  val local_naming = global_naming |> add_path Long_Name.localN;
    2.86  
    2.87  
    2.88  (* full name *)
    2.89  
    2.90  fun transform_binding (Naming {private, concealed, ...}) =
    2.91 -  private ? Binding.private #>
    2.92 +  Binding.private_default private #>
    2.93    concealed ? Binding.concealed;
    2.94  
    2.95  fun name_spec naming binding =
    2.96 -  Binding.name_spec (get_path naming) (transform_binding naming binding);
    2.97 +  Binding.name_spec (get_scopes naming) (get_path naming) (transform_binding naming binding);
    2.98  
    2.99  fun full_name naming =
   2.100    name_spec naming #> #spec #> map #1 #> Long_Name.implode;
   2.101 @@ -357,7 +370,7 @@
   2.102  
   2.103  fun accesses naming binding =
   2.104    (case name_spec naming binding of
   2.105 -    {private = true, ...} => ([], [])
   2.106 +    {accessible = false, ...} => ([], [])
   2.107    | {spec, ...} =>
   2.108        let
   2.109          val sfxs = mandatory_suffixes spec;
     3.1 --- a/src/Pure/Isar/local_theory.ML	Tue Mar 31 21:12:22 2015 +0200
     3.2 +++ b/src/Pure/Isar/local_theory.ML	Tue Mar 31 22:31:05 2015 +0200
     3.3 @@ -144,9 +144,13 @@
     3.4      else lthy
     3.5    end;
     3.6  
     3.7 -fun open_target background_naming operations after_close target =
     3.8 -  assert target
     3.9 -  |> Data.map (cons (make_lthy (background_naming, operations, after_close, true, target)));
    3.10 +fun open_target background_naming operations after_close lthy =
    3.11 +  let
    3.12 +    val _ = assert lthy;
    3.13 +    val (_, target) = Proof_Context.new_scope lthy;
    3.14 +  in
    3.15 +    target |> Data.map (cons (make_lthy (background_naming, operations, after_close, true, target)))
    3.16 +  end;
    3.17  
    3.18  fun close_target lthy =
    3.19    let
     4.1 --- a/src/Pure/Isar/proof_context.ML	Tue Mar 31 21:12:22 2015 +0200
     4.2 +++ b/src/Pure/Isar/proof_context.ML	Tue Mar 31 22:31:05 2015 +0200
     4.3 @@ -34,6 +34,8 @@
     4.4    val naming_of: Proof.context -> Name_Space.naming
     4.5    val restore_naming: Proof.context -> Proof.context -> Proof.context
     4.6    val full_name: Proof.context -> binding -> string
     4.7 +  val get_scope: Proof.context -> Binding.scope option
     4.8 +  val new_scope: Proof.context -> Binding.scope * Proof.context
     4.9    val concealed: Proof.context -> Proof.context
    4.10    val class_space: Proof.context -> Name_Space.T
    4.11    val type_space: Proof.context -> Name_Space.T
    4.12 @@ -305,6 +307,14 @@
    4.13  
    4.14  val full_name = Name_Space.full_name o naming_of;
    4.15  
    4.16 +val get_scope = Name_Space.get_scope o naming_of;
    4.17 +
    4.18 +fun new_scope ctxt =
    4.19 +  let
    4.20 +    val (scope, naming') = Name_Space.new_scope (naming_of ctxt);
    4.21 +    val ctxt' = map_naming (K naming') ctxt;
    4.22 +  in (scope, ctxt') end;
    4.23 +
    4.24  val concealed = map_naming Name_Space.concealed;
    4.25  
    4.26  
     5.1 --- a/src/Pure/sign.ML	Tue Mar 31 21:12:22 2015 +0200
     5.2 +++ b/src/Pure/sign.ML	Tue Mar 31 22:31:05 2015 +0200
     5.3 @@ -101,6 +101,8 @@
     5.4      (string * (Proof.context -> Ast.ast list -> Ast.ast)) list -> theory -> theory
     5.5    val add_trrules: Ast.ast Syntax.trrule list -> theory -> theory
     5.6    val del_trrules: Ast.ast Syntax.trrule list -> theory -> theory
     5.7 +  val get_scope: theory -> Binding.scope option
     5.8 +  val new_scope: theory -> Binding.scope * theory
     5.9    val new_group: theory -> theory
    5.10    val reset_group: theory -> theory
    5.11    val add_path: string -> theory -> theory
    5.12 @@ -500,6 +502,14 @@
    5.13  
    5.14  (* naming *)
    5.15  
    5.16 +val get_scope = Name_Space.get_scope o naming_of;
    5.17 +
    5.18 +fun new_scope thy =
    5.19 +  let
    5.20 +    val (scope, naming') = Name_Space.new_scope (naming_of thy);
    5.21 +    val thy' = map_naming (K naming') thy;
    5.22 +  in (scope, thy') end;
    5.23 +
    5.24  val new_group = map_naming Name_Space.new_group;
    5.25  val reset_group = map_naming Name_Space.reset_group;
    5.26