eliminated qualified_names naming policy: qualified names are only permitted via explicit Binding.qualify/qualified_name etc. (NB: user-level outer syntax should never do this);
authorwenzelm
Wed Mar 11 16:36:27 2009 +0100 (2009-03-11)
changeset 30438c2d49315b93b
parent 30437 910a7aeb8dec
child 30444 62139eb64bfe
eliminated qualified_names naming policy: qualified names are only permitted via explicit Binding.qualify/qualified_name etc. (NB: user-level outer syntax should never do this);
src/Pure/General/name_space.ML
src/Pure/Isar/element.ML
src/Pure/Isar/local_theory.ML
src/Pure/Isar/locale.ML
src/Pure/Isar/proof_context.ML
src/Pure/Isar/theory_target.ML
src/Pure/sign.ML
     1.1 --- a/src/Pure/General/name_space.ML	Wed Mar 11 15:45:40 2009 +0100
     1.2 +++ b/src/Pure/General/name_space.ML	Wed Mar 11 16:36:27 2009 +0100
     1.3 @@ -36,7 +36,6 @@
     1.4    val root_path: naming -> naming
     1.5    val parent_path: naming -> naming
     1.6    val no_base_names: naming -> naming
     1.7 -  val qualified_names: naming -> naming
     1.8    val sticky_prefix: string -> naming -> naming
     1.9    type 'a table = T * 'a Symtab.table
    1.10    val bind: naming -> binding * 'a -> 'a table -> string * 'a table       (*exception Symtab.DUP*)
    1.11 @@ -174,53 +173,44 @@
    1.12  
    1.13  datatype naming = Naming of
    1.14   {path: (string * bool) list,
    1.15 -  no_base_names: bool,
    1.16 -  qualified_names: bool};
    1.17 +  no_base_names: bool};
    1.18  
    1.19 -fun make_naming (path, no_base_names, qualified_names) =
    1.20 -  Naming {path = path, no_base_names = no_base_names, qualified_names = qualified_names};
    1.21 +fun make_naming (path, no_base_names) =
    1.22 +  Naming {path = path, no_base_names = no_base_names};
    1.23  
    1.24 -fun map_naming f (Naming {path, no_base_names, qualified_names}) =
    1.25 -  make_naming (f (path, no_base_names, qualified_names));
    1.26 -
    1.27 -fun path_of (Naming {path, ...}) = path;
    1.28 +fun map_naming f (Naming {path, no_base_names}) =
    1.29 +  make_naming (f (path, no_base_names));
    1.30  
    1.31  
    1.32  (* configure naming *)
    1.33  
    1.34 -val default_naming = make_naming ([], false, false);
    1.35 +val default_naming = make_naming ([], false);
    1.36  
    1.37 -fun add_path elems = map_naming (fn (path, no_base_names, qualified_names) =>
    1.38 -  (path @ map (rpair false) (Long_Name.explode elems), no_base_names, qualified_names));
    1.39 +fun add_path elems = map_naming (fn (path, no_base_names) =>
    1.40 +  (path @ map (rpair false) (Long_Name.explode elems), no_base_names));
    1.41  
    1.42 -val root_path = map_naming (fn (_, no_base_names, qualified_names) =>
    1.43 -  ([], no_base_names, qualified_names));
    1.44 +val root_path = map_naming (fn (_, no_base_names) => ([], no_base_names));
    1.45  
    1.46 -val parent_path = map_naming (fn (path, no_base_names, qualified_names) =>
    1.47 -  (perhaps (try (#1 o split_last)) path, no_base_names, qualified_names));
    1.48 +val parent_path = map_naming (fn (path, no_base_names) =>
    1.49 +  (perhaps (try (#1 o split_last)) path, no_base_names));
    1.50  
    1.51 -fun sticky_prefix elems = map_naming (fn (path, no_base_names, qualified_names) =>
    1.52 -  (path @ map (rpair true) (Long_Name.explode elems), no_base_names, qualified_names));
    1.53 +fun sticky_prefix elems = map_naming (fn (path, no_base_names) =>
    1.54 +  (path @ map (rpair true) (Long_Name.explode elems), no_base_names));
    1.55  
    1.56 -val no_base_names = map_naming (fn (path, _, qualified_names) => (path, true, qualified_names));
    1.57 -val qualified_names = map_naming (fn (path, no_base_names, _) => (path, no_base_names, true));
    1.58 +val no_base_names = map_naming (fn (path, _) => (path, true));
    1.59  
    1.60  
    1.61  (* full name *)
    1.62  
    1.63  fun err_bad binding = error ("Bad name declaration " ^ quote (Binding.str_of binding));
    1.64  
    1.65 -fun name_spec (Naming {path, qualified_names, ...}) binding =
    1.66 +fun name_spec (Naming {path, ...}) binding =
    1.67    let
    1.68      val (prefix, name) = Binding.dest binding;
    1.69 -    val _ = not qualified_names andalso Long_Name.is_qualified name andalso err_bad binding;
    1.70 +    val _ = Long_Name.is_qualified name andalso err_bad binding;
    1.71  
    1.72      val spec1 = maps (fn (a, b) => map (rpair b) (Long_Name.explode a)) (path @ prefix);
    1.73 -    val spec2 =
    1.74 -      (case try split_last (Long_Name.explode name) of
    1.75 -        NONE => []
    1.76 -      | SOME (qual, base) => map (rpair false) qual @ [(base, true)]);
    1.77 -
    1.78 +    val spec2 = if name = "" then [] else [(name, true)];
    1.79      val spec = spec1 @ spec2;
    1.80      val _ =
    1.81        exists (fn (a, _) => a = "" orelse a = "??" orelse exists_string (fn s => s = "\"") a) spec
     2.1 --- a/src/Pure/Isar/element.ML	Wed Mar 11 15:45:40 2009 +0100
     2.2 +++ b/src/Pure/Isar/element.ML	Wed Mar 11 16:36:27 2009 +0100
     2.3 @@ -518,8 +518,8 @@
     2.4      fun activate elem ctxt =
     2.5        let val elem' = (map_ctxt_attrib Args.assignable o prep_facts ctxt) elem
     2.6        in (elem', activate_elem elem' ctxt) end
     2.7 -    val (elems, ctxt') = fold_map activate raw_elems (ProofContext.qualified_names ctxt);
     2.8 -  in (elems |> map (map_ctxt_attrib Args.closure), ProofContext.restore_naming ctxt ctxt') end;
     2.9 +    val (elems, ctxt') = fold_map activate raw_elems ctxt;
    2.10 +  in (elems |> map (map_ctxt_attrib Args.closure), ctxt') end;
    2.11  
    2.12  fun check_name name =
    2.13    if Long_Name.is_qualified name then error ("Illegal qualified name: " ^ quote name)
     3.1 --- a/src/Pure/Isar/local_theory.ML	Wed Mar 11 15:45:40 2009 +0100
     3.2 +++ b/src/Pure/Isar/local_theory.ML	Wed Mar 11 16:36:27 2009 +0100
     3.3 @@ -138,14 +138,12 @@
     3.4  
     3.5  fun full_naming lthy =
     3.6    Sign.naming_of (ProofContext.theory_of lthy)
     3.7 -  |> NameSpace.sticky_prefix (#theory_prefix (get_lthy lthy))
     3.8 -  |> NameSpace.qualified_names;
     3.9 +  |> NameSpace.sticky_prefix (#theory_prefix (get_lthy lthy));
    3.10  
    3.11  fun full_name naming = NameSpace.full_name (full_naming naming);
    3.12  
    3.13  fun theory_result f lthy = lthy |> raw_theory_result (fn thy => thy
    3.14    |> Sign.sticky_prefix (#theory_prefix (get_lthy lthy))
    3.15 -  |> Sign.qualified_names
    3.16    |> f
    3.17    ||> Sign.restore_naming thy);
    3.18  
     4.1 --- a/src/Pure/Isar/locale.ML	Wed Mar 11 15:45:40 2009 +0100
     4.2 +++ b/src/Pure/Isar/locale.ML	Wed Mar 11 16:36:27 2009 +0100
     4.3 @@ -107,19 +107,6 @@
     4.4  
     4.5  datatype ctxt = datatype Element.ctxt;
     4.6  
     4.7 -fun global_note_qualified kind facts thy = (*FIXME*)
     4.8 -  thy
     4.9 -  |> Sign.qualified_names
    4.10 -  |> PureThy.note_thmss kind facts
    4.11 -  ||> Sign.restore_naming thy;
    4.12 -
    4.13 -fun local_note_qualified kind facts ctxt = (*FIXME*)
    4.14 -  ctxt
    4.15 -  |> ProofContext.qualified_names
    4.16 -  |> ProofContext.note_thmss_i kind facts
    4.17 -  ||> ProofContext.restore_naming ctxt;
    4.18 -
    4.19 -
    4.20  
    4.21  (*** Theory data ***)
    4.22  
    4.23 @@ -337,7 +324,7 @@
    4.24  fun init_global_elem (Notes (kind, facts)) thy =
    4.25    let
    4.26      val facts' = Attrib.map_facts (Attrib.attribute_i thy) facts
    4.27 -  in global_note_qualified kind facts' thy |> snd end
    4.28 +  in PureThy.note_thmss kind facts' thy |> snd end
    4.29  
    4.30  fun init_local_elem (Fixes fixes) ctxt = ctxt |>
    4.31        ProofContext.add_fixes_i fixes |> snd
    4.32 @@ -359,7 +346,7 @@
    4.33    | init_local_elem (Notes (kind, facts)) ctxt =
    4.34        let
    4.35          val facts' = Attrib.map_facts (Attrib.attribute_i (ProofContext.theory_of ctxt)) facts
    4.36 -      in local_note_qualified kind facts' ctxt |> snd end
    4.37 +      in ProofContext.note_thmss_i kind facts' ctxt |> snd end
    4.38  
    4.39  fun cons_elem false (Notes notes) elems = elems
    4.40    | cons_elem _ elem elems = elem :: elems
    4.41 @@ -452,7 +439,7 @@
    4.42              let
    4.43                val args'' = snd args' |> Element.facts_map (Element.morph_ctxt morph) |>
    4.44                  Attrib.map_facts (Attrib.attribute_i thy)
    4.45 -            in global_note_qualified kind args'' #> snd end)
    4.46 +            in PureThy.note_thmss kind args'' #> snd end)
    4.47          (get_registrations thy |> filter (fn (name, _) => name = loc)) thy))
    4.48    in ctxt'' end;
    4.49  
     5.1 --- a/src/Pure/Isar/proof_context.ML	Wed Mar 11 15:45:40 2009 +0100
     5.2 +++ b/src/Pure/Isar/proof_context.ML	Wed Mar 11 16:36:27 2009 +0100
     5.3 @@ -98,7 +98,6 @@
     5.4    val get_thm: Proof.context -> xstring -> thm
     5.5    val add_path: string -> Proof.context -> Proof.context
     5.6    val sticky_prefix: string -> Proof.context -> Proof.context
     5.7 -  val qualified_names: Proof.context -> Proof.context
     5.8    val restore_naming: Proof.context -> Proof.context -> Proof.context
     5.9    val reset_naming: Proof.context -> Proof.context
    5.10    val note_thmss: string -> (Thm.binding * (Facts.ref * attribute list) list) list ->
    5.11 @@ -947,7 +946,6 @@
    5.12  
    5.13  val add_path        = map_naming o NameSpace.add_path;
    5.14  val sticky_prefix   = map_naming o NameSpace.sticky_prefix;
    5.15 -val qualified_names = map_naming NameSpace.qualified_names;
    5.16  val restore_naming  = map_naming o K o naming_of;
    5.17  val reset_naming    = map_naming (K local_naming);
    5.18  
     6.1 --- a/src/Pure/Isar/theory_target.ML	Wed Mar 11 15:45:40 2009 +0100
     6.2 +++ b/src/Pure/Isar/theory_target.ML	Wed Mar 11 16:36:27 2009 +0100
     6.3 @@ -144,12 +144,6 @@
     6.4  
     6.5    in (result'', result) end;
     6.6  
     6.7 -fun note_local kind facts ctxt =
     6.8 -  ctxt
     6.9 -  |> ProofContext.qualified_names
    6.10 -  |> ProofContext.note_thmss_i kind facts
    6.11 -  ||> ProofContext.restore_naming ctxt;
    6.12 -
    6.13  fun notes (Target {target, is_locale, ...}) kind facts lthy =
    6.14    let
    6.15      val thy = ProofContext.theory_of lthy;
    6.16 @@ -165,12 +159,10 @@
    6.17        |> Attrib.map_facts (if is_locale then K I else Attrib.attribute_i thy);
    6.18    in
    6.19      lthy |> LocalTheory.theory
    6.20 -      (Sign.qualified_names
    6.21 -        #> PureThy.note_thmss_grouped kind (LocalTheory.group_of lthy) global_facts #> snd
    6.22 -        #> Sign.restore_naming thy)
    6.23 -    |> not is_locale ? LocalTheory.target (note_local kind global_facts #> snd)
    6.24 +      (PureThy.note_thmss_grouped kind (LocalTheory.group_of lthy) global_facts #> snd)
    6.25 +    |> not is_locale ? LocalTheory.target (ProofContext.note_thmss_i kind global_facts #> snd)
    6.26      |> is_locale ? LocalTheory.target (Locale.add_thmss target kind target_facts)
    6.27 -    |> note_local kind local_facts
    6.28 +    |> ProofContext.note_thmss_i kind local_facts
    6.29    end;
    6.30  
    6.31  
     7.1 --- a/src/Pure/sign.ML	Wed Mar 11 15:45:40 2009 +0100
     7.2 +++ b/src/Pure/sign.ML	Wed Mar 11 16:36:27 2009 +0100
     7.3 @@ -126,7 +126,6 @@
     7.4    val parent_path: theory -> theory
     7.5    val sticky_prefix: string -> theory -> theory
     7.6    val no_base_names: theory -> theory
     7.7 -  val qualified_names: theory -> theory
     7.8    val local_path: theory -> theory
     7.9    val restore_naming: theory -> theory -> theory
    7.10    val hide_class: bool -> string -> theory -> theory
    7.11 @@ -622,7 +621,6 @@
    7.12  val parent_path     = map_naming NameSpace.parent_path;
    7.13  val sticky_prefix   = map_naming o NameSpace.sticky_prefix;
    7.14  val no_base_names   = map_naming NameSpace.no_base_names;
    7.15 -val qualified_names = map_naming NameSpace.qualified_names;
    7.16  
    7.17  fun local_path thy = thy |> root_path |> add_path (Context.theory_name thy);
    7.18