clarified signature: explicitly distinguish theory_base_name vs. theory_long_name;
--- a/src/HOL/Mutabelle/mutabelle_extra.ML Wed Apr 19 23:27:55 2023 +0200
+++ b/src/HOL/Mutabelle/mutabelle_extra.ML Thu Apr 20 11:57:34 2023 +0200
@@ -331,7 +331,7 @@
fun thms_of all thy =
filter
- (fn th => (all orelse Thm.theory_name th = Context.theory_name thy)
+ (fn th => (all orelse Thm.theory_base_name th = Context.theory_base_name thy)
(* andalso is_executable_thm thy th *))
(map snd (filter_out is_forbidden_theorem (Global_Theory.all_thms_of thy false)))
--- a/src/HOL/Nitpick_Examples/Mono_Nits.thy Wed Apr 19 23:27:55 2023 +0200
+++ b/src/HOL/Nitpick_Examples/Mono_Nits.thy Thu Apr 20 11:57:34 2023 +0200
@@ -153,7 +153,7 @@
fun theorems_of thy =
filter (fn (name, th) =>
not (is_forbidden_theorem name) andalso
- Thm.theory_name th = Context.theory_name thy)
+ Thm.theory_base_name th = Context.theory_base_name thy)
(Global_Theory.all_thms_of thy true)
fun check_formulas tsp =
@@ -175,7 +175,7 @@
fun check_theory thy =
let
- val path = File.tmp_path (Context.theory_name thy ^ ".out" |> Path.explode)
+ val path = File.tmp_path (Context.theory_base_name thy ^ ".out" |> Path.explode)
val _ = File.write path ""
fun check_theorem (name, th) =
let
--- a/src/HOL/TPTP/mash_export.ML Wed Apr 19 23:27:55 2023 +0200
+++ b/src/HOL/TPTP/mash_export.ML Thu Apr 20 11:57:34 2023 +0200
@@ -58,7 +58,7 @@
| _ => ("", []))
fun has_thm_thy th thy =
- Context.theory_name thy = Thm.theory_name th
+ Context.theory_base_name thy = Thm.theory_base_name th
fun has_thys thys th = exists (has_thm_thy th) thys
@@ -98,7 +98,7 @@
fun do_fact ((_, stature), th) =
let
val name = nickname_of_thm th
- val feats = features_of ctxt (Thm.theory_name th) stature [Thm.prop_of th]
+ val feats = features_of ctxt (Thm.theory_base_name th) stature [Thm.prop_of th]
val s = encode_str name ^ ": " ^ encode_strs (sort string_ord feats) ^ "\n"
in
File.append path s
@@ -187,14 +187,14 @@
val _ = tracing ("Fact " ^ string_of_int j ^ ": " ^ name)
val isar_deps = isar_dependencies_of name_tabs th
val do_query = not (is_bad_query ctxt step j th isar_deps)
- val goal_feats = features_of ctxt (Thm.theory_name th) stature [Thm.prop_of th]
+ val goal_feats = features_of ctxt (Thm.theory_base_name th) stature [Thm.prop_of th]
val access_facts = filter_accessible_from th new_facts @ old_facts
val (marker, deps) =
smart_dependencies_of ctxt params_opt access_facts name_tabs th isar_deps
fun extra_features_of (((_, stature), th), weight) =
[Thm.prop_of th]
- |> features_of ctxt (Thm.theory_name th) stature
+ |> features_of ctxt (Thm.theory_base_name th) stature
|> map (rpair (weight * extra_feature_factor))
val query =
@@ -261,7 +261,7 @@
val suggs =
old_facts
|> filter_accessible_from th
- |> mepo_or_mash_suggested_facts ctxt (Thm.theory_name th)
+ |> mepo_or_mash_suggested_facts ctxt (Thm.theory_base_name th)
params max_suggs hyp_ts concl_t
|> map (nickname_of_thm o snd)
in
--- a/src/HOL/Tools/Quickcheck/find_unused_assms.ML Wed Apr 19 23:27:55 2023 +0200
+++ b/src/HOL/Tools/Quickcheck/find_unused_assms.ML Thu Apr 20 11:57:34 2023 +0200
@@ -16,7 +16,7 @@
fun thms_of thy thy_name =
Global_Theory.all_thms_of thy false
- |> filter (fn (_, th) => Thm.theory_name th = thy_name)
+ |> filter (fn (_, th) => Thm.theory_base_name th = thy_name)
fun do_while P f s list =
if P s then
@@ -95,7 +95,8 @@
fun print_unused_assms ctxt opt_thy_name =
let
- val thy_name = the_default (Context.theory_name (Proof_Context.theory_of ctxt)) opt_thy_name
+ val thy_name =
+ the_default (Context.theory_base_name (Proof_Context.theory_of ctxt)) opt_thy_name
val results = find_unused_assms ctxt thy_name
val total = length results
val with_assumptions = length (filter (is_some o snd) results)
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML Wed Apr 19 23:27:55 2023 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML Thu Apr 20 11:57:34 2023 +0200
@@ -796,7 +796,7 @@
(* There must be a better way to detect local facts. *)
(case Long_Name.dest_local hint of
SOME suf =>
- Long_Name.implode [Thm.theory_name th, suf, crude_printed_term 25 (Thm.prop_of th)]
+ Long_Name.implode [Thm.theory_base_name th, suf, crude_printed_term 25 (Thm.prop_of th)]
| NONE => hint)
end
else
@@ -820,9 +820,9 @@
fun crude_thm_ord ctxt =
let
val ancestor_lengths =
- fold (fn thy => Symtab.update (Context.theory_name thy, length (Context.ancestors_of thy)))
+ fold (fn thy => Symtab.update (Context.theory_base_name thy, length (Context.ancestors_of thy)))
(Theory.nodes_of (Proof_Context.theory_of ctxt)) Symtab.empty
- val ancestor_length = Symtab.lookup ancestor_lengths o Context.theory_id_name
+ val ancestor_length = Symtab.lookup ancestor_lengths o Context.theory_id_name {long = false}
fun crude_theory_ord p =
if Context.eq_thy_id p then EQUAL
@@ -832,9 +832,9 @@
(case apply2 ancestor_length p of
(SOME m, SOME n) =>
(case int_ord (m, n) of
- EQUAL => string_ord (apply2 Context.theory_id_name p)
+ EQUAL => string_ord (apply2 (Context.theory_id_name {long = false}) p)
| ord => ord)
- | _ => string_ord (apply2 Context.theory_id_name p))
+ | _ => string_ord (apply2 (Context.theory_id_name {long = false}) p))
in
fn p =>
(case crude_theory_ord (apply2 Thm.theory_id p) of
@@ -1125,7 +1125,7 @@
val chunks = app_hd (cons th) chunks
val chunks_and_parents' =
if thm_less_eq (th, th') andalso
- Thm.theory_name th = Thm.theory_name th'
+ Thm.theory_base_name th = Thm.theory_base_name th'
then (chunks, [nickname_of_thm th])
else chunks_and_parents_for chunks th'
in
@@ -1172,11 +1172,11 @@
val chained = filter (fn ((_, (scope, _)), _) => scope = Chained) facts
- fun fact_has_right_theory (_, th) = thy_name = Thm.theory_name th
+ fun fact_has_right_theory (_, th) = thy_name = Thm.theory_base_name th
fun chained_or_extra_features_of factor (((_, stature), th), weight) =
[Thm.prop_of th]
- |> features_of ctxt (Thm.theory_name th) stature
+ |> features_of ctxt (Thm.theory_base_name th) stature
|> map (rpair (weight * factor))
in
(case get_state ctxt of
@@ -1283,7 +1283,7 @@
launch_thread timeout (fn () =>
let
val thy = Proof_Context.theory_of ctxt
- val feats = features_of ctxt (Context.theory_name thy) (Local, General) [t]
+ val feats = features_of ctxt (Context.theory_base_name thy) (Local, General) [t]
in
map_state ctxt
(fn {access_G, xtabs as ((num_facts0, _), _), ffds, freqs, dirty_facts} =>
@@ -1395,7 +1395,7 @@
(learns, (num_nontrivial, next_commit, _)) =
let
val name = nickname_of_thm th
- val feats = features_of ctxt (Thm.theory_name th) stature [Thm.prop_of th]
+ val feats = features_of ctxt (Thm.theory_base_name th) stature [Thm.prop_of th]
val deps = these (deps_of status th)
val num_nontrivial = num_nontrivial |> not (null deps) ? Integer.add 1
val learns = (name, parents, feats, deps) :: learns
@@ -1544,7 +1544,7 @@
[("", [])]
else
let
- val thy_name = Context.theory_name (Proof_Context.theory_of ctxt)
+ val thy_name = Context.theory_base_name (Proof_Context.theory_of ctxt)
fun maybe_launch_thread exact min_num_facts_to_learn =
if not (Async_Manager_Legacy.has_running_threads MaShN) andalso
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_mepo.ML Wed Apr 19 23:27:55 2023 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mepo.ML Thu Apr 20 11:57:34 2023 +0200
@@ -220,7 +220,7 @@
t
fun theory_const_prop_of fudge th =
- theory_constify fudge (Thm.theory_name th) (Thm.prop_of th)
+ theory_constify fudge (Thm.theory_base_name th) (Thm.prop_of th)
fun pair_consts_fact thy fudge fact =
(case fact |> snd |> theory_const_prop_of fudge |> pconsts_in_fact thy of
@@ -546,7 +546,7 @@
[]
else
relevance_filter ctxt thres0 decay max_facts fudge facts hyp_ts
- (concl_t |> theory_constify fudge (Context.theory_name thy)))
+ (concl_t |> theory_constify fudge (Context.theory_base_name thy)))
|> map fact_of_lazy_fact
end
--- a/src/Pure/Isar/named_target.ML Wed Apr 19 23:27:55 2023 +0200
+++ b/src/Pure/Isar/named_target.ML Thu Apr 20 11:57:34 2023 +0200
@@ -97,7 +97,7 @@
theory_registration = Generic_Target.theory_registration,
locale_dependency = fn _ => error "Not possible in theory target",
pretty = fn ctxt => [Pretty.block [Pretty.keyword1 "theory", Pretty.brk 1,
- Pretty.str (Context.theory_name (Proof_Context.theory_of ctxt))]]}
+ Pretty.str (Context.theory_base_name (Proof_Context.theory_of ctxt))]]}
| operations (Locale locale) =
{define = Generic_Target.define (locale_foundation locale),
notes = Generic_Target.notes (Generic_Target.locale_target_notes locale),
--- a/src/Pure/Isar/outer_syntax.ML Wed Apr 19 23:27:55 2023 +0200
+++ b/src/Pure/Isar/outer_syntax.ML Thu Apr 20 11:57:34 2023 +0200
@@ -112,7 +112,7 @@
(* maintain commands *)
fun add_command name cmd thy =
- if member (op =) Thy_Header.bootstrap_thys (Context.theory_name thy) then thy
+ if member (op =) Thy_Header.bootstrap_thys (Context.theory_base_name thy) then thy
else
let
val _ =
--- a/src/Pure/Isar/proof_context.ML Wed Apr 19 23:27:55 2023 +0200
+++ b/src/Pure/Isar/proof_context.ML Thu Apr 20 11:57:34 2023 +0200
@@ -10,7 +10,7 @@
sig
val theory_of: Proof.context -> theory
val init_global: theory -> Proof.context
- val get_global: theory -> string -> Proof.context
+ val get_global: {long: bool} -> theory -> string -> Proof.context
type mode
val mode_default: mode
val mode_pattern: mode
--- a/src/Pure/Isar/toplevel.ML Wed Apr 19 23:27:55 2023 +0200
+++ b/src/Pure/Isar/toplevel.ML Thu Apr 20 11:57:34 2023 +0200
@@ -162,7 +162,7 @@
Toplevel =>
(case previous_theory_of state of
NONE => "at top level"
- | SOME thy => "at top level, result theory " ^ quote (Context.theory_name thy))
+ | SOME thy => "at top level, result theory " ^ quote (Context.theory_base_name thy))
| Theory (Context.Theory _) => "in theory mode"
| Theory (Context.Proof _) => "in local theory mode"
| Proof _ => "in proof mode"
--- a/src/Pure/ML/ml_antiquotations.ML Wed Apr 19 23:27:55 2023 +0200
+++ b/src/Pure/ML/ml_antiquotations.ML Thu Apr 20 11:57:34 2023 +0200
@@ -65,7 +65,7 @@
ML_Antiquotation.value_embedded \<^binding>\<open>theory_context\<close>
(Args.context -- Scan.lift Parse.embedded_position >> (fn (ctxt, (name, pos)) =>
(Theory.check {long = false} ctxt (name, pos);
- "Proof_Context.get_global (Proof_Context.theory_of ML_context) " ^
+ "Proof_Context.get_global {long = false} (Proof_Context.theory_of ML_context) " ^
ML_Syntax.print_string name))) #>
ML_Antiquotation.inline \<^binding>\<open>context\<close>
--- a/src/Pure/Thy/export_theory.ML Wed Apr 19 23:27:55 2023 +0200
+++ b/src/Pure/Thy/export_theory.ML Thu Apr 20 11:57:34 2023 +0200
@@ -414,7 +414,7 @@
get_dependencies parents thy |> map_index (fn (i, dep) =>
let
val xname = string_of_int (i + 1);
- val name = Long_Name.implode [Context.theory_name thy, xname];
+ val name = Long_Name.implode [Context.theory_base_name thy, xname];
val markup = make_entity_markup name xname (#pos (#1 dep)) (#serial (#1 dep));
val body = encode_locale_dependency dep;
in XML.Elem (markup, body) end)
--- a/src/Pure/Thy/thy_info.ML Wed Apr 19 23:27:55 2023 +0200
+++ b/src/Pure/Thy/thy_info.ML Thu Apr 20 11:57:34 2023 +0200
@@ -65,7 +65,7 @@
else
let
val keywords = Thy_Header.get_keywords thy;
- val thy_name = Context.theory_name thy;
+ val thy_name = Context.theory_base_name thy;
val latex = Document_Output.present_thy options keywords thy_name segments;
in
if Options.string options "document" = "false" then ()
--- a/src/Pure/Tools/thy_deps.ML Wed Apr 19 23:27:55 2023 +0200
+++ b/src/Pure/Tools/thy_deps.ML Thu Apr 20 11:57:34 2023 +0200
@@ -27,8 +27,8 @@
SOME Bs => (fn thy => exists (fn B => rel (B, thy)) Bs)
| NONE => K true);
fun node thy =
- ((Context.theory_name thy, Graph_Display.content_node (Context.theory_name thy) []),
- map Context.theory_name (filter pred (Theory.parents_of thy)));
+ ((Context.theory_base_name thy, Graph_Display.content_node (Context.theory_base_name thy) []),
+ map Context.theory_base_name (filter pred (Theory.parents_of thy)));
in map node (filter pred (Theory.nodes_of (Proof_Context.theory_of ctxt))) end;
val thy_deps =
--- a/src/Pure/context.ML Wed Apr 19 23:27:55 2023 +0200
+++ b/src/Pure/context.ML Thu Apr 20 11:57:34 2023 +0200
@@ -20,7 +20,7 @@
sig
val theory_of: Proof.context -> theory
val init_global: theory -> Proof.context
- val get_global: theory -> string -> Proof.context
+ val get_global: {long: bool} -> theory -> string -> Proof.context
end
end;
@@ -34,11 +34,10 @@
val parents_of: theory -> theory list
val ancestors_of: theory -> theory list
val theory_id_ord: theory_id ord
- val theory_id_long_name: theory_id -> string
- val theory_id_name: theory_id -> string
+ val theory_id_name: {long: bool} -> theory_id -> string
val theory_long_name: theory -> string
- val theory_name: theory -> string
- val theory_name': {long: bool} -> theory -> string
+ val theory_base_name: theory -> string
+ val theory_name: {long: bool} -> theory -> string
val theory_identifier: theory -> serial
val PureN: string
val pretty_thy: theory -> Pretty.T
@@ -166,12 +165,13 @@
val theory_id_stage = #stage o rep_theory_id;
val theory_id_final = stage_final o theory_id_stage;
val theory_id_ord = int_ord o apply2 (#id o rep_theory_id);
-val theory_id_long_name = #name o rep_theory_id;
-val theory_id_name = Long_Name.base_name o theory_id_long_name;
+fun theory_id_name {long} thy_id =
+ let val name = #name (rep_theory_id thy_id)
+ in if long then name else Long_Name.base_name name end;
val theory_long_name = #name o identity_of;
-val theory_name = Long_Name.base_name o theory_long_name;
-fun theory_name' {long} = if long then theory_long_name else theory_name;
+val theory_base_name = Long_Name.base_name o theory_long_name;
+fun theory_name {long} = if long then theory_long_name else theory_base_name;
val theory_identifier = #id o identity_of;
val parents_of = #parents o ancestry_of;
@@ -183,8 +183,10 @@
val PureN = "Pure";
fun display_name thy_id =
- if theory_id_final thy_id then theory_id_name thy_id
- else theory_id_name thy_id ^ ":" ^ string_of_int (theory_id_stage thy_id);
+ let
+ val name = theory_id_name {long = false} thy_id;
+ val final = theory_id_final thy_id;
+ in if final then name else name ^ ":" ^ string_of_int (theory_id_stage thy_id) end;
fun display_names thy =
let
@@ -204,8 +206,8 @@
in Pretty.str_list "{" "}" abbrev end;
fun get_theory long thy name =
- if theory_name' long thy <> name then
- (case find_first (fn thy' => theory_name' long thy' = name) (ancestors_of thy) of
+ if theory_name long thy <> name then
+ (case find_first (fn thy' => theory_name long thy' = name) (ancestors_of thy) of
SOME thy' => thy'
| NONE => error ("Unknown ancestor theory " ^ quote name))
else if theory_id_final (theory_id thy) then thy
@@ -238,7 +240,7 @@
fun eq_thy_consistent (thy1, thy2) =
eq_thy (thy1, thy2) orelse
- (theory_name thy1 = theory_name thy2 andalso
+ (theory_base_name thy1 = theory_base_name thy2 andalso
raise THEORY ("Duplicate theory name", [thy1, thy2]));
fun extend_ancestors thy thys =
@@ -513,7 +515,7 @@
struct
fun theory_of (Proof.Context (_, thy)) = thy;
fun init_global thy = Proof.Context (init_data thy, thy);
- fun get_global thy name = init_global (get_theory {long = false} thy name);
+ fun get_global long thy name = init_global (get_theory long thy name);
end;
structure Proof_Data =
--- a/src/Pure/global_theory.ML Wed Apr 19 23:27:55 2023 +0200
+++ b/src/Pure/global_theory.ML Thu Apr 20 11:57:34 2023 +0200
@@ -172,9 +172,9 @@
let
val theories =
Symtab.build (Theory.nodes_of thy |> fold (fn thy' =>
- Symtab.update (Context.theory_name thy', thy')));
+ Symtab.update (Context.theory_base_name thy', thy')));
fun transfer th =
- Thm.transfer (the_default thy (Symtab.lookup theories (Thm.theory_name th))) th;
+ Thm.transfer (the_default thy (Symtab.lookup theories (Thm.theory_base_name th))) th;
in transfer end;
fun all_thms_of thy verbose =
--- a/src/Pure/proofterm.ML Wed Apr 19 23:27:55 2023 +0200
+++ b/src/Pure/proofterm.ML Thu Apr 20 11:57:34 2023 +0200
@@ -2137,7 +2137,7 @@
fun export_standard_enabled () = Options.default_bool "export_standard_proofs";
fun export_proof_boxes_required thy =
- Context.theory_name thy = Context.PureN orelse
+ Context.theory_base_name thy = Context.PureN orelse
(export_enabled () andalso not (export_standard_enabled ()));
fun export_proof_boxes bodies =
--- a/src/Pure/sign.ML Wed Apr 19 23:27:55 2023 +0200
+++ b/src/Pure/sign.ML Thu Apr 20 11:57:34 2023 +0200
@@ -514,7 +514,7 @@
val mandatory_path = map_naming o Name_Space.mandatory_path;
val qualified_path = map_naming oo Name_Space.qualified_path;
-fun local_path thy = thy |> root_path |> add_path (Context.theory_name thy);
+fun local_path thy = thy |> root_path |> add_path (Context.theory_base_name thy);
fun init_naming thy =
let
--- a/src/Pure/theory.ML Wed Apr 19 23:27:55 2023 +0200
+++ b/src/Pure/theory.ML Thu Apr 20 11:57:34 2023 +0200
@@ -143,7 +143,7 @@
val completion_report =
Completion.make_report (name, pos)
(fn completed =>
- map (Context.theory_name' long) (ancestors_of thy)
+ map (Context.theory_name long) (ancestors_of thy)
|> filter (completed o Long_Name.base_name)
|> sort_strings
|> map (fn a => (a, (Markup.theoryN, a))));
--- a/src/Pure/thm.ML Wed Apr 19 23:27:55 2023 +0200
+++ b/src/Pure/thm.ML Thu Apr 20 11:57:34 2023 +0200
@@ -66,7 +66,9 @@
val terms_of_tpairs: (term * term) list -> term list
val full_prop_of: thm -> term
val theory_id: thm -> Context.theory_id
- val theory_name: thm -> string
+ val theory_name: {long: bool} -> thm -> string
+ val theory_long_name: thm -> string
+ val theory_base_name: thm -> string
val maxidx_of: thm -> int
val maxidx_thm: thm -> int -> int
val shyps_of: thm -> sort Ord_List.T
@@ -494,7 +496,10 @@
val cert_of = #cert o rep_thm;
val theory_id = Context.certificate_theory_id o cert_of;
-val theory_name = Context.theory_id_name o theory_id;
+
+fun theory_name long = Context.theory_id_name long o theory_id;
+val theory_long_name = theory_name {long = true};
+val theory_base_name = theory_name {long = false};
val maxidx_of = #maxidx o rep_thm;
fun maxidx_thm th i = Int.max (maxidx_of th, i);
@@ -2399,7 +2404,7 @@
val th' = th |> unconstrainT |> tap (expose_proof thy) |> trim_context;
val prop = plain_prop_of th;
val (t, Ss, c) = Logic.dest_arity prop;
- val ar = ((t, Ss, c), (th', Context.theory_name thy, serial ()));
+ val ar = ((t, Ss, c), (th', Context.theory_base_name thy, serial ()));
in
thy
|> Sign.primitive_arity (t, Ss, [c])
--- a/src/Tools/Code/code_runtime.ML Wed Apr 19 23:27:55 2023 +0200
+++ b/src/Tools/Code/code_runtime.ML Thu Apr 20 11:57:34 2023 +0200
@@ -718,7 +718,7 @@
val code_binding = Path.map_binding Code_Target.code_path binding;
val preamble =
"(* Generated from " ^
- Path.implode (Resources.thy_path (Path.basic (Context.theory_name thy))) ^
+ Path.implode (Resources.thy_path (Path.basic (Context.theory_base_name thy))) ^
"; DO NOT EDIT! *)";
val thy' = Code_Target.export code_binding (Bytes.string (preamble ^ "\n\n" ^ code)) thy;
val _ = Code_Target.code_export_message thy';
--- a/src/Tools/Code/code_thingol.ML Wed Apr 19 23:27:55 2023 +0200
+++ b/src/Tools/Code/code_thingol.ML Thu Apr 20 11:57:34 2023 +0200
@@ -1009,7 +1009,7 @@
let
val thy = Proof_Context.theory_of ctxt;
fun this_theory name =
- if Context.theory_name thy = name then thy
+ if Context.theory_base_name thy = name then thy
else Context.get_theory {long = false} thy name;
fun consts_of thy' =