--- a/src/Doc/Implementation/Logic.thy Sat Jun 08 14:57:14 2024 +0200
+++ b/src/Doc/Implementation/Logic.thy Sun Jun 09 22:40:13 2024 +0200
@@ -1293,7 +1293,7 @@
@{define_ML Proofterm.reconstruct_proof:
"theory -> term -> proof -> proof"} \\
@{define_ML Proofterm.expand_proof: "theory ->
- (Proofterm.thm_header -> string option) -> proof -> proof"} \\
+ (Proofterm.thm_header -> Thm_Name.T option) -> proof -> proof"} \\
@{define_ML Proof_Checker.thm_of_proof: "theory -> proof -> thm"} \\
@{define_ML Proof_Syntax.read_proof: "theory -> bool -> bool -> string -> proof"} \\
@{define_ML Proof_Syntax.pretty_proof: "Proof.context -> proof -> Pretty.T"} \\
--- a/src/HOL/Mutabelle/mutabelle_extra.ML Sat Jun 08 14:57:14 2024 +0200
+++ b/src/HOL/Mutabelle/mutabelle_extra.ML Sun Jun 09 22:40:13 2024 +0200
@@ -235,7 +235,7 @@
val forbidden_consts = [\<^const_name>\<open>Pure.type\<close>]
-fun is_forbidden_theorem (s, th) =
+fun is_forbidden_theorem ((s, _): Thm_Name.T, th) =
let val consts = Term.add_const_names (Thm.prop_of th) [] in
exists (member (op =) (Long_Name.explode s)) forbidden_thms orelse
exists (member (op =) forbidden_consts) consts orelse
@@ -421,13 +421,13 @@
^ "(" ^ space_implode "; " (map (fn (s, t) => (s ^ ": " ^ string_of_int t)) timing) ^ ")"
(*^ "\n" ^ string_of_reports reports*)
in
- "mutant of " ^ thm_name ^ ":\n" ^
+ "mutant of " ^ Thm_Name.short thm_name ^ ":\n" ^
YXML.content_of (Syntax.string_of_term_global thy t) ^ "\n" ^
space_implode "; " (map string_of_mtd_result results)
end
fun string_of_detailed_entry thy (thm_name, exec, t, mutant_subentries) =
- thm_name ^ " " ^ (if exec then "[exe]" else "[noexe]") ^ ": " ^
+ Thm_Name.short thm_name ^ " " ^ (if exec then "[exe]" else "[noexe]") ^ ": " ^
Syntax.string_of_term_global thy t ^ "\n" ^
cat_lines (map (string_of_mutant_subentry' thy thm_name) mutant_subentries) ^ "\n"
--- a/src/HOL/Nitpick_Examples/Mono_Nits.thy Sat Jun 08 14:57:14 2024 +0200
+++ b/src/HOL/Nitpick_Examples/Mono_Nits.thy Sun Jun 09 22:40:13 2024 +0200
@@ -151,7 +151,7 @@
String.isSuffix "_raw" name
fun theorems_of thy =
- filter (fn (name, th) =>
+ filter (fn ((name, _), th) =>
not (is_forbidden_theorem name) andalso
Thm.theory_long_name th = Context.theory_long_name thy)
(Global_Theory.all_thms_of thy true)
@@ -186,7 +186,7 @@
val (nondef_ts, def_ts, _, _, _, _) =
Timeout.apply preproc_timeout (preprocess_formulas hol_ctxt [])
neg_t
- val res = name ^ ": " ^ check_formulas (nondef_ts, def_ts)
+ val res = Thm_Name.print name ^ ": " ^ check_formulas (nondef_ts, def_ts)
in File.append path (res ^ "\n"); writeln res end
handle Timeout.TIMEOUT _ => ()
in thy |> theorems_of |> List.app check_theorem end
--- a/src/HOL/Proofs/ex/Proof_Terms.thy Sat Jun 08 14:57:14 2024 +0200
+++ b/src/HOL/Proofs/ex/Proof_Terms.thy Sun Jun 09 22:40:13 2024 +0200
@@ -35,7 +35,7 @@
(*all theorems used in the graph of nested proofs*)
val all_thms =
Proofterm.fold_body_thms
- (fn {name, ...} => insert (op =) name) [body] [];
+ (fn {thm_name, ...} => insert (op =) thm_name) [body] [];
\<close>
text \<open>
--- a/src/HOL/TPTP/atp_problem_import.ML Sat Jun 08 14:57:14 2024 +0200
+++ b/src/HOL/TPTP/atp_problem_import.ML Sun Jun 09 22:40:13 2024 +0200
@@ -187,7 +187,7 @@
|> Config.put Sledgehammer_Prover_ATP.atp_completish (if completeness > 0 then 3 else 0)
|> Local_Theory.note ((\<^binding>\<open>thms\<close>, []), assm_ths0)
- fun ref_of th = (Facts.named (Thm.derivation_name th), [])
+ fun ref_of th = (Facts.named (Thm_Name.short (Thm.derivation_name th)), [])
val ref_of_assms = (Facts.named assm_name, [])
in
Sledgehammer_Tactics.sledgehammer_as_oracle_tac lthy
--- a/src/HOL/TPTP/atp_theory_export.ML Sat Jun 08 14:57:14 2024 +0200
+++ b/src/HOL/TPTP/atp_theory_export.ML Sun Jun 09 22:40:13 2024 +0200
@@ -164,19 +164,19 @@
val problem =
facts
|> map (fn ((_, loc), th) =>
- ((Thm.get_name_hint th, loc), th |> Thm.prop_of |> mono ? monomorphize_term ctxt))
+ ((Thm_Name.short (Thm.get_name_hint th), loc), th |> Thm.prop_of |> mono ? monomorphize_term ctxt))
|> generate_atp_problem ctxt true format Axiom type_enc Exporter combsN false false true []
\<^prop>\<open>False\<close>
|> #1 |> sort_by (heading_sort_key o fst)
val prelude = fst (split_last problem)
- val name_tabs = Sledgehammer_Fact.build_name_tables Thm.get_name_hint facts
+ val name_tabs = Sledgehammer_Fact.build_name_tables (Thm_Name.short o Thm.get_name_hint) facts
val infers =
if infer_policy = No_Inferences then
[]
else
facts
|> map (fn (_, th) =>
- (fact_name_of (Thm.get_name_hint th),
+ (fact_name_of (Thm_Name.short (Thm.get_name_hint th)),
th |> Sledgehammer_Util.thms_in_proof max_dependencies (SOME name_tabs)
|> these |> map fact_name_of))
val all_problem_names =
@@ -295,7 +295,7 @@
#> chop_maximal_groups (op = o apply2 theory_name_of_fact)
#> map (`(include_base_name_of_fact o hd)))
- val fact_tab = Symtab.make (map (fn fact as (_, th) => (Thm.get_name_hint th, fact)) facts)
+ val fact_tab = Symtab.make (map (fn fact as (_, th) => (Thm_Name.short (Thm.get_name_hint th), fact)) facts)
fun write_prelude () =
let val ss = lines_of_atp_problem format (K []) prelude in
@@ -318,7 +318,7 @@
val mepo = Sledgehammer_MePo.mepo_suggested_facts ctxt
(Sledgehammer_Commands.default_params thy []) max_facts NONE hyp_ts conj_t facts
in
- map (suffix "\n" o fact_name_of o Thm.get_name_hint o snd) mepo
+ map (suffix "\n" o fact_name_of o Thm_Name.short o Thm.get_name_hint o snd) mepo
end
fun write_problem_files _ _ _ _ [] = ()
--- a/src/HOL/TPTP/mash_export.ML Sat Jun 08 14:57:14 2024 +0200
+++ b/src/HOL/TPTP/mash_export.ML Sun Jun 09 22:40:13 2024 +0200
@@ -172,7 +172,7 @@
j mod step <> 0 orelse
Thm.legacy_get_kind th = "" orelse
null (the_list isar_deps) orelse
- is_blacklisted_or_something (Thm.get_name_hint th)
+ is_blacklisted_or_something (Thm_Name.short (Thm.get_name_hint th))
fun generate_isar_or_prover_commands ctxt prover params_opt (range, step) thys max_suggs file_name =
let
--- a/src/HOL/Tools/ATP/atp_util.ML Sat Jun 08 14:57:14 2024 +0200
+++ b/src/HOL/Tools/ATP/atp_util.ML Sun Jun 09 22:40:13 2024 +0200
@@ -417,7 +417,7 @@
fun short_thm_name ctxt th =
let
- val long = Thm.get_name_hint th
+ val long = Thm_Name.short (Thm.get_name_hint th)
val short = Long_Name.base_name long
in
(case try (singleton (Attrib.eval_thms ctxt)) (Facts.named short, []) of
--- a/src/HOL/Tools/Ctr_Sugar/ctr_sugar_util.ML Sat Jun 08 14:57:14 2024 +0200
+++ b/src/HOL/Tools/Ctr_Sugar/ctr_sugar_util.ML Sun Jun 09 22:40:13 2024 +0200
@@ -222,10 +222,9 @@
| name_noted_thms qualifier base ((local_name, thms) :: noted) =
if Long_Name.base_name local_name = base then
let
- val thms' = thms |> map_index (uncurry (fn j =>
- Thm.name_derivation
- (((Long_Name.append qualifier base ^
- (if can the_single thms then "" else "_" ^ string_of_int (j + 1))), \<^here>))))
+ val name = Long_Name.append qualifier base;
+ val pos = Position.thread_data ();
+ val thms' = Thm_Name.list (name, pos) thms |> map (uncurry Thm.name_derivation);
in (local_name, thms') :: noted end
else ((local_name, thms) :: name_noted_thms qualifier base noted);
--- a/src/HOL/Tools/Meson/meson.ML Sat Jun 08 14:57:14 2024 +0200
+++ b/src/HOL/Tools/Meson/meson.ML Sun Jun 09 22:40:13 2024 +0200
@@ -459,7 +459,7 @@
(*Use "theorem naming" to label the clauses*)
fun name_thms label =
let fun name1 th (k, ths) =
- (k-1, Thm.put_name_hint (label ^ string_of_int k) th :: ths)
+ (k-1, Thm.put_name_hint (label ^ string_of_int k, 0) th :: ths)
in fn ths => #2 (fold_rev name1 ths (length ths, [])) end;
(*Is the given disjunction an all-negative support clause?*)
--- a/src/HOL/Tools/Metis/metis_tactic.ML Sat Jun 08 14:57:14 2024 +0200
+++ b/src/HOL/Tools/Metis/metis_tactic.ML Sun Jun 09 22:40:13 2024 +0200
@@ -214,7 +214,8 @@
val _ = unused := maps (#2 o #2) unused_th_cls_pairs;
val _ =
if not (null unused_th_cls_pairs) then
- verbose_warning ctxt ("Unused theorems: " ^ commas_quote (map #1 unused_th_cls_pairs))
+ verbose_warning ctxt ("Unused theorems: " ^
+ commas_quote (map (Proof_Context.print_thm_name ctxt o #1) unused_th_cls_pairs))
else ();
val _ =
if not (null cls) andalso not (have_common_thm ctxt used cls) then
--- a/src/HOL/Tools/Mirabelle/mirabelle.ML Sat Jun 08 14:57:14 2024 +0200
+++ b/src/HOL/Tools/Mirabelle/mirabelle.ML Sun Jun 09 22:40:13 2024 +0200
@@ -309,7 +309,7 @@
val prop = Proofterm.thm_node_prop thm_node;
val body = Future.join (Proofterm.thm_node_body thm_node);
val (x', seen') =
- app (n + (if name = "" then 0 else 1)) body
+ app (n + (if Thm_Name.is_empty name then 0 else 1)) body
(x, Inttab.update (i, ()) seen);
in (x' |> n = 0 ? f (name, prop, body), seen') end);
in fn bodies => fn x => #1 (fold (app 0) bodies (x, Inttab.empty)) end;
@@ -319,7 +319,7 @@
fun theorems_in_proof_term thy thm =
let
val all_thms = Global_Theory.all_thms_of thy true;
- fun collect (s, _, _) = if s <> "" then insert (op =) s else I;
+ fun collect (name, _, _) = if Thm_Name.is_empty name then I else insert (op =) name;
fun member_of xs (x, y) = if member (op =) xs x then SOME y else NONE;
fun resolve_thms names = map_filter (member_of names) all_thms;
in resolve_thms (fold_body_thms collect [Thm.proof_body_of thm] []) end;
--- a/src/HOL/Tools/Mirabelle/mirabelle_metis.ML Sat Jun 08 14:57:14 2024 +0200
+++ b/src/HOL/Tools/Mirabelle/mirabelle_metis.ML Sun Jun 09 22:40:13 2024 +0200
@@ -19,7 +19,7 @@
fun metis ctxt = Metis_Tactic.metis_tac [] ATP_Problem_Generate.liftingN ctxt (thms @ facts);
in
(if Mirabelle.can_apply timeout metis pre then "succeeded" else "failed")
- |> not (null names) ? suffix (":\n" ^ commas names)
+ |> not (null names) ? suffix (":\n" ^ commas (map Thm_Name.short names))
end
in ("", {run = run, finalize = K ""}) end
--- a/src/HOL/Tools/Quickcheck/find_unused_assms.ML Sat Jun 08 14:57:14 2024 +0200
+++ b/src/HOL/Tools/Quickcheck/find_unused_assms.ML Sun Jun 09 22:40:13 2024 +0200
@@ -7,7 +7,7 @@
signature FIND_UNUSED_ASSMS =
sig
val check_unused_assms: Proof.context -> string * thm -> string * int list list option
- val find_unused_assms: Proof.context -> string -> (string * int list list option) list
+ val find_unused_assms: Proof.context -> string -> (Thm_Name.T * int list list option) list
val print_unused_assms: Proof.context -> string option -> unit
end
@@ -71,8 +71,8 @@
val thy = Proof_Context.theory_of ctxt
val all_thms =
thms_of thy thy_name
- |> filter (fn (name, _) => Long_Name.count name = 2) (* FIXME !? *)
- |> sort_by #1
+ |> filter (fn ((name, _), _) => Long_Name.count name = 2) (* FIXME !? *)
+ |> sort (Thm_Name.ord o apply2 #1)
val check = check_unused_assms ctxt
in rev (Par_List.map check all_thms) end
@@ -86,8 +86,8 @@
(flat (separate [Pretty.str " and", Pretty.brk 1]
(map (fn i => [Pretty.str (string_of_int (i + 1))]) (sort int_ord is))))
-fun pretty_thm (name, set_of_indexes) =
- Pretty.block (Pretty.str name :: Pretty.str ":" :: Pretty.brk 1 ::
+fun pretty_thm ctxt (name, set_of_indexes) =
+ Pretty.block (Proof_Context.pretty_thm_name ctxt name :: Pretty.str ":" :: Pretty.brk 1 ::
Pretty.str "unnecessary assumption " ::
separate (Pretty.str " or ") (map pretty_indexes set_of_indexes))
@@ -112,7 +112,7 @@
string_of_int total ^ " total) in the theory " ^ quote thy_name
in
[Pretty.str (msg ^ ":"), Pretty.str ""] @
- map pretty_thm with_superfluous_assumptions @
+ map (pretty_thm ctxt) with_superfluous_assumptions @
[Pretty.str "", Pretty.str end_msg]
end |> Pretty.writeln_chunks
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML Sat Jun 08 14:57:14 2024 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML Sun Jun 09 22:40:13 2024 +0200
@@ -223,7 +223,7 @@
fun is_that_fact th =
exists_subterm (fn Free (s, _) => s = skolem_thesis | _ => false) (Thm.prop_of th)
- andalso String.isSuffix sep_that (Thm.get_name_hint th)
+ andalso String.isSuffix sep_that (Thm_Name.short (Thm.get_name_hint th))
datatype interest = Deal_Breaker | Interesting | Boring
@@ -359,7 +359,7 @@
let
fun cons_thm (_, th) = Termtab.cons_list (normalize_vars (normalize_eq (Thm.prop_of th)), th)
fun add_plain canon alias =
- Symtab.update (Thm.get_name_hint alias, name_of (if_thm_before canon alias))
+ Symtab.update (Thm_Name.short (Thm.get_name_hint alias), name_of (if_thm_before canon alias))
fun add_plains (_, aliases as canon :: _) = fold (add_plain canon) aliases
fun add_inclass (name, target) = fold (fn s => Symtab.update (s, target)) (un_class_ify name)
val prop_tab = fold cons_thm facts Termtab.empty
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar_proof.ML Sat Jun 08 14:57:14 2024 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar_proof.ML Sun Jun 09 22:40:13 2024 +0200
@@ -424,7 +424,7 @@
end
fun of_free (s, T) =
- Proof_Context.print_name ctxt s ^ " :: " ^
+ Thy_Header.print_name' ctxt s ^ " :: " ^
maybe_quote ctxt (simplify_spaces (Print_Mode.setmp [] (Syntax.string_of_typ ctxt) T))
fun add_frees xs (s, ctxt) =
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML Sat Jun 08 14:57:14 2024 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML Sun Jun 09 22:40:13 2024 +0200
@@ -789,7 +789,7 @@
fun nickname_of_thm th =
if Thm.has_name_hint th then
- let val hint = Thm.get_name_hint th in
+ let val hint = Thm_Name.short (Thm.get_name_hint th) in
(* There must be a better way to detect local facts. *)
(case Long_Name.dest_local hint of
SOME suf =>
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML Sat Jun 08 14:57:14 2024 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML Sun Jun 09 22:40:13 2024 +0200
@@ -76,7 +76,7 @@
let
fun app_thm map_name (_, thm_node) (accum as (num_thms, names)) =
let
- val name = Proofterm.thm_node_name thm_node
+ val name = Thm_Name.short (Proofterm.thm_node_name thm_node)
val body = Proofterm.thm_node_body thm_node
val (anonymous, enter_class) =
(* The "name = outer_name" case caters for the uncommon case where the proved theorem
@@ -108,7 +108,8 @@
NONE => NONE
| SOME body =>
let val map_names = (case name_tabs of SOME p => apply2 Symtab.lookup p | NONE => `I SOME) in
- SOME (fold_body_thm max_thms (Thm.get_name_hint th) map_names (Proofterm.strip_thm_body body))
+ SOME (fold_body_thm max_thms (Thm_Name.short (Thm.get_name_hint th)) map_names
+ (Proofterm.strip_thm_body body))
handle TOO_MANY () => NONE
end)
--- a/src/HOL/Tools/datatype_realizer.ML Sat Jun 08 14:57:14 2024 +0200
+++ b/src/HOL/Tools/datatype_realizer.ML Sun Jun 09 22:40:13 2024 +0200
@@ -127,7 +127,8 @@
val (thm', thy') = thy
|> Sign.root_path
|> Global_Theory.store_thm
- (Binding.qualified_name (space_implode "_" (ind_name :: vs @ ["correctness"])), thm)
+ (Binding.qualified_name
+ (space_implode "_" (Thm_Name.short ind_name :: vs @ ["correctness"])), thm)
||> Sign.restore_naming thy;
val ivs = rev (Term.add_vars (Logic.varify_global (Old_Datatype_Prop.make_ind [descr])) []);
@@ -201,7 +202,8 @@
val exh_name = Thm.derivation_name exhaust;
val (thm', thy') = thy
|> Sign.root_path
- |> Global_Theory.store_thm (Binding.qualified_name (exh_name ^ "_P_correctness"), thm)
+ |> Global_Theory.store_thm
+ (Binding.qualified_name (Thm_Name.short exh_name ^ "_P_correctness"), thm)
||> Sign.restore_naming thy;
val P = Var (("P", 0), rT' --> HOLogic.boolT);
--- a/src/HOL/Tools/inductive_realizer.ML Sat Jun 08 14:57:14 2024 +0200
+++ b/src/HOL/Tools/inductive_realizer.ML Sun Jun 09 22:40:13 2024 +0200
@@ -13,11 +13,13 @@
structure InductiveRealizer : INDUCTIVE_REALIZER =
struct
-fun name_of_thm thm =
- (case Proofterm.fold_proof_atoms false (fn PThm ({name, ...}, _) => cons name | _ => I)
+fun thm_name_of thm =
+ (case Proofterm.fold_proof_atoms false (fn PThm ({thm_name, ...}, _) => cons thm_name | _ => I)
[Thm.proof_of thm] [] of
- [name] => name
- | _ => raise THM ("name_of_thm: bad proof of theorem", 0, [thm]));
+ [thm_name] => thm_name
+ | _ => raise THM ("thm_name_of: bad proof of theorem", 0, [thm]));
+
+val short_name_of = Thm_Name.short o thm_name_of;
fun prf_of thy =
Thm.transfer thy #>
@@ -61,7 +63,7 @@
(Logic.strip_imp_concl (Thm.prop_of (hd intrs))));
val params = map dest_Var (take nparms ts);
val tname = Binding.name (space_implode "_" (Long_Name.base_name s ^ "T" :: vs));
- fun constr_of_intr intr = (Binding.name (Long_Name.base_name (name_of_thm intr)),
+ fun constr_of_intr intr = (Binding.name (Long_Name.base_name (short_name_of intr)),
map (Logic.unvarifyT_global o snd)
(subtract (op =) params (rev (Term.add_vars (Thm.prop_of intr) []))) @
filter_out (equal Extraction.nullT)
@@ -193,7 +195,7 @@
then fold_rev (absfree o dest_Free) xs HOLogic.unit
else fold_rev (absfree o dest_Free) xs
(list_comb
- (Free ("r" ^ Long_Name.base_name (name_of_thm intr),
+ (Free ("r" ^ Long_Name.base_name (short_name_of intr),
map fastype_of (rev args) ---> conclT), rev args))
end
@@ -216,7 +218,7 @@
end) (premss ~~ dummies);
val frees = fold Term.add_frees fs [];
val Ts = map fastype_of fs;
- fun name_of_fn intr = "r" ^ Long_Name.base_name (name_of_thm intr)
+ fun name_of_fn intr = "r" ^ Long_Name.base_name (short_name_of intr)
in
fst (fold_map (fn concl => fn names =>
let val T = Extraction.etype_of thy vs [] concl
@@ -273,7 +275,7 @@
fun add_ind_realizer rsets intrs induct raw_induct elims vs thy =
let
- val qualifier = Long_Name.qualifier (name_of_thm induct);
+ val qualifier = Long_Name.qualifier (short_name_of induct);
val inducts = Global_Theory.get_thms thy (Long_Name.qualify qualifier "inducts");
val iTs = rev (Term.add_tvars (Thm.prop_of (hd intrs)) []);
val ar = length vs + length iTs;
@@ -354,11 +356,11 @@
{quiet_mode = false, verbose = false, alt_name = Binding.empty, coind = false,
no_elim = false, no_ind = false, skip_mono = false}
rlzpreds rlzparams (map (fn (rintr, intr) =>
- ((Binding.name (Long_Name.base_name (name_of_thm intr)), []),
+ ((Binding.name (Long_Name.base_name (short_name_of intr)), []),
subst_atomic rlzpreds' (Logic.unvarify_global rintr)))
(rintrs ~~ maps snd rss)) []) ||>
Sign.root_path;
- val thy3 = fold (Global_Theory.hide_fact false o name_of_thm) (#intrs ind_info) thy3';
+ val thy3 = fold (Global_Theory.hide_fact false o short_name_of) (#intrs ind_info) thy3';
(** realizer for induction rule **)
@@ -413,7 +415,7 @@
mk_realizer thy'' (vs' @ Ps) (Thm.derivation_name ind, ind, corr, rlz, r))
realizers @ (case realizers of
[(((ind, corr), rlz), r)] =>
- [mk_realizer thy'' (vs' @ Ps) (Long_Name.qualify qualifier "induct",
+ [mk_realizer thy'' (vs' @ Ps) ((Long_Name.qualify qualifier "induct", 0),
ind, corr, rlz, r)]
| _ => [])) thy''
end;
@@ -463,10 +465,10 @@
DEPTH_SOLVE_1 o
FIRST' [assume_tac ctxt, eresolve_tac ctxt [allE], eresolve_tac ctxt [impE]])) 1)]);
val (thm', thy') = Global_Theory.store_thm (Binding.qualified_name (space_implode "_"
- (name_of_thm elim :: vs @ Ps @ ["correctness"])), thm) thy
+ (short_name_of elim :: vs @ Ps @ ["correctness"])), thm) thy
in
Extraction.add_realizers_i
- [mk_realizer thy' (vs @ Ps) (name_of_thm elim, elim, thm', rlz, r)] thy'
+ [mk_realizer thy' (vs @ Ps) (thm_name_of elim, elim, thm', rlz, r)] thy'
end;
(** add realizers to theory **)
@@ -474,7 +476,7 @@
val thy4 = fold add_ind_realizer (subsets Ps) thy3;
val thy5 = Extraction.add_realizers_i
(map (mk_realizer thy4 vs) (map (fn (((rule, rrule), rlz), c) =>
- (name_of_thm rule, rule, rrule, rlz,
+ (thm_name_of rule, rule, rrule, rlz,
list_comb (c, map Var (subtract (op =) params' (rev (Term.add_vars (Thm.prop_of rule) []))))))
(maps snd rss ~~ #intrs ind_info ~~ rintrs ~~ flat constrss))) thy4;
val elimps = map_filter (fn ((s, intrs), p) =>
--- a/src/HOL/Tools/rewrite_hol_proof.ML Sat Jun 08 14:57:14 2024 +0200
+++ b/src/HOL/Tools/rewrite_hol_proof.ML Sun Jun 09 22:40:13 2024 +0200
@@ -305,9 +305,9 @@
(** Replace congruence rules by substitution rules **)
-fun strip_cong ps (PThm ({name = "HOL.cong", ...}, _) % _ % _ % SOME x % SOME y %%
+fun strip_cong ps (PThm ({thm_name = ("HOL.cong", 0), ...}, _) % _ % _ % SOME x % SOME y %%
prfa %% prfT %% prf1 %% prf2) = strip_cong (((x, y), (prf2, prfa)) :: ps) prf1
- | strip_cong ps (PThm ({name = "HOL.refl", ...}, _) % SOME f %% _) = SOME (f, ps)
+ | strip_cong ps (PThm ({thm_name = ("HOL.refl", 0), ...}, _) % SOME f %% _) = SOME (f, ps)
| strip_cong _ _ = NONE;
val subst_prf = Proofterm.any_head_of (Thm.proof_of @{thm subst});
@@ -330,15 +330,15 @@
fun mk_AbsP P t = AbsP ("H", Option.map HOLogic.mk_Trueprop P, t);
-fun elim_cong_aux Ts (PThm ({name = "HOL.iffD1", ...}, _) % _ % _ %% prf1 %% prf2) =
+fun elim_cong_aux Ts (PThm ({thm_name = ("HOL.iffD1", 0), ...}, _) % _ % _ %% prf1 %% prf2) =
Option.map (make_subst Ts prf2 []) (strip_cong [] prf1)
- | elim_cong_aux Ts (PThm ({name = "HOL.iffD1", ...}, _) % P % _ %% prf) =
+ | elim_cong_aux Ts (PThm ({thm_name = ("HOL.iffD1", 0), ...}, _) % P % _ %% prf) =
Option.map (mk_AbsP P o make_subst Ts (PBound 0) [])
(strip_cong [] (Proofterm.incr_boundvars 1 0 prf))
- | elim_cong_aux Ts (PThm ({name = "HOL.iffD2", ...}, _) % _ % _ %% prf1 %% prf2) =
+ | elim_cong_aux Ts (PThm ({thm_name = ("HOL.iffD2", 0), ...}, _) % _ % _ %% prf1 %% prf2) =
Option.map (make_subst Ts prf2 [] o
apsnd (map (make_sym Ts))) (strip_cong [] prf1)
- | elim_cong_aux Ts (PThm ({name = "HOL.iffD2", ...}, _) % _ % P %% prf) =
+ | elim_cong_aux Ts (PThm ({thm_name = ("HOL.iffD2", 0), ...}, _) % _ % P %% prf) =
Option.map (mk_AbsP P o make_subst Ts (PBound 0) [] o
apsnd (map (make_sym Ts))) (strip_cong [] (Proofterm.incr_boundvars 1 0 prf))
| elim_cong_aux _ _ = NONE;
--- a/src/HOL/ex/Sketch_and_Explore.thy Sat Jun 08 14:57:14 2024 +0200
+++ b/src/HOL/ex/Sketch_and_Explore.thy Sun Jun 09 22:40:13 2024 +0200
@@ -91,7 +91,7 @@
val fixes_s =
if not is_for orelse null fixes then NONE
else SOME ("for " ^ space_implode " "
- (map (fn (v, _) => Proof_Context.print_name ctxt' v) fixes));
+ (map (fn (v, _) => Thy_Header.print_name' ctxt' v) fixes));
val premises_s = if is_prems then SOME "premises prems" else NONE;
val sh_s = if is_sh then SOME "sledgehammer" else NONE;
val subgoal_s = map_filter I [SOME "subgoal", premises_s, fixes_s]
@@ -137,10 +137,7 @@
if is_none some_method_ref then [" .."]
else [" by" ^ method_text]
else print ctxt_print method_text clauses;
- val message = Active.sendback_markup_command (cat_lines lines);
- in
- (state |> tap (fn _ => Output.information message))
- end
+ in Output.information (Active.sendback_markup_command (cat_lines lines)) end;
val sketch = print_proof_text_from_state print_sketch;
@@ -157,10 +154,10 @@
end;
fun sketch_cmd some_method_text =
- Toplevel.keep_proof (K () o sketch some_method_text o Toplevel.proof_of)
+ Toplevel.keep_proof (fn state => sketch some_method_text (Toplevel.proof_of state));
fun explore_cmd method_text =
- Toplevel.keep_proof (K () o explore method_text o Toplevel.proof_of)
+ Toplevel.keep_proof (fn state => explore method_text (Toplevel.proof_of state));
fun subgoals_cmd (modes, method_ref) =
let
@@ -168,8 +165,9 @@
val is_for = not (member (op =) modes "nofor")
val is_sh = member (op =) modes "sh"
in
- Toplevel.keep_proof (K () o subgoals (is_prems, is_for, is_sh) method_ref o Toplevel.proof_of)
- end
+ Toplevel.keep_proof (fn state =>
+ subgoals (is_prems, is_for, is_sh) method_ref (Toplevel.proof_of state))
+ end;
val _ =
Outer_Syntax.command \<^command_keyword>\<open>sketch\<close>
--- a/src/Pure/Build/export.ML Sat Jun 08 14:57:14 2024 +0200
+++ b/src/Pure/Build/export.ML Sun Jun 09 22:40:13 2024 +0200
@@ -6,10 +6,10 @@
signature EXPORT =
sig
- val report_export: theory -> Path.binding -> unit
+ val report: Context.generic -> string -> Path.binding -> unit
type params =
- {theory: theory, binding: Path.binding, executable: bool, compress: bool, strict: bool}
- val export_params: params -> XML.body -> unit
+ {theory_name: string, binding: Path.binding, executable: bool, compress: bool, strict: bool}
+ val export_params: Context.generic -> params -> XML.body -> unit
val export: theory -> Path.binding -> XML.body -> unit
val export_executable: theory -> Path.binding -> XML.body -> unit
val export_file: theory -> Path.binding -> Path.T -> unit
@@ -23,34 +23,35 @@
(* export *)
-fun report_export thy binding =
+fun report context theory_name binding =
let
- val theory_name = Context.theory_long_name thy;
val (path, pos) = Path.dest_binding binding;
val markup = Markup.export_path (Path.implode (Path.basic theory_name + path));
- in Context_Position.report_generic (Context.Theory thy) pos markup end;
+ in Context_Position.report_generic context pos markup end;
type params =
- {theory: theory, binding: Path.binding, executable: bool, compress: bool, strict: bool};
+ {theory_name: string, binding: Path.binding, executable: bool, compress: bool, strict: bool};
-fun export_params ({theory = thy, binding, executable, compress, strict}: params) body =
- (report_export thy binding;
+fun export_params context ({theory_name, binding, executable, compress, strict}: params) body =
+ (report context theory_name binding;
(Output.try_protocol_message o Markup.export)
{id = Position.id_of (Position.thread_data ()),
serial = serial (),
- theory_name = Context.theory_long_name thy,
+ theory_name = theory_name,
name = Path.implode_binding (tap Path.proper_binding binding),
executable = executable,
compress = compress,
strict = strict} [body]);
fun export thy binding body =
- export_params
- {theory = thy, binding = binding, executable = false, compress = true, strict = true} body;
+ export_params (Context.Theory thy)
+ {theory_name = Context.theory_long_name thy, binding = binding,
+ executable = false, compress = true, strict = true} body;
fun export_executable thy binding body =
- export_params
- {theory = thy, binding = binding, executable = true, compress = true, strict = true} body;
+ export_params (Context.Theory thy)
+ {theory_name = Context.theory_long_name thy, binding = binding,
+ executable = true, compress = true, strict = true} body;
fun export_file thy binding file =
export thy binding (Bytes.contents_blob (Bytes.read file));
--- a/src/Pure/Build/export.scala Sat Jun 08 14:57:14 2024 +0200
+++ b/src/Pure/Build/export.scala Sun Jun 09 22:40:13 2024 +0200
@@ -88,22 +88,20 @@
{ res =>
val executable = res.bool(Base.executable)
val compressed = res.bool(Base.compressed)
- val bytes = res.bytes(Base.body)
- val body = Future.value(compressed, bytes)
- Entry(entry_name, executable, body, cache)
+ val body = res.bytes(Base.body)
+ Entry(entry_name, executable, compressed, body, cache)
}
)
def write_entries(db: SQL.Database, entries: List[Entry]): Unit =
db.execute_batch_statement(Base.table.insert(), batch =
for (entry <- entries) yield { (stmt: SQL.Statement) =>
- val (compressed, bs) = entry.body.join
stmt.string(1) = entry.session_name
stmt.string(2) = entry.theory_name
stmt.string(3) = entry.name
stmt.bool(4) = entry.executable
- stmt.bool(5) = compressed
- stmt.bytes(6) = bs
+ stmt.bool(5) = entry.compressed
+ stmt.bytes(6) = entry.body
})
def read_theory_names(db: SQL.Database, session_name: String): List[String] =
@@ -147,13 +145,14 @@
def apply(
entry_name: Entry_Name,
executable: Boolean,
- body: Future[(Boolean, Bytes)],
+ compressed: Boolean,
+ body: Bytes,
cache: XML.Cache
- ): Entry = new Entry(entry_name, executable, body, cache)
+ ): Entry = new Entry(entry_name, executable, compressed, body, cache)
def empty(theory_name: String, name: String): Entry =
Entry(Entry_Name(theory = theory_name, name = name),
- false, Future.value(false, Bytes.empty), XML.Cache.none)
+ false, false, Bytes.empty, XML.Cache.none)
def make(
session_name: String,
@@ -161,19 +160,20 @@
bytes: Bytes,
cache: XML.Cache
): Entry = {
- val body =
- if (args.compress) Future.fork(bytes.maybe_compress(cache = cache.compress))
- else Future.value((false, bytes))
+ val (compressed, body) =
+ if (args.compress) bytes.maybe_compress(cache = cache.compress)
+ else (false, bytes)
val entry_name =
Entry_Name(session = session_name, theory = args.theory_name, name = args.name)
- Entry(entry_name, args.executable, body, cache)
+ Entry(entry_name, args.executable, compressed, body, cache)
}
}
final class Entry private(
val entry_name: Entry_Name,
val executable: Boolean,
- val body: Future[(Boolean, Bytes)],
+ val compressed: Boolean,
+ val body: Bytes,
val cache: XML.Cache
) {
def session_name: String = entry_name.session
@@ -181,9 +181,6 @@
def name: String = entry_name.name
override def toString: String = name
- def is_finished: Boolean = body.is_finished
- def cancel(): Unit = body.cancel()
-
def compound_name: String = entry_name.compound_name
def name_has_prefix(s: String): Boolean = name.startsWith(s)
@@ -192,10 +189,8 @@
def name_extends(elems: List[String]): Boolean =
name_elems.startsWith(elems) && name_elems != elems
- def bytes: Bytes = {
- val (compressed, bs) = body.join
- if (compressed) bs.uncompress(cache = cache.compress) else bs
- }
+ def bytes: Bytes =
+ if (compressed) body.uncompress(cache = cache.compress) else body
def text: String = bytes.text
@@ -254,9 +249,6 @@
private val errors = Synchronized[List[String]](Nil)
private def consume(args: List[(Entry, Boolean)]): List[Exn.Result[Unit]] = {
- for ((entry, _) <- args) {
- if (progress.stopped) entry.cancel() else entry.body.join
- }
private_data.transaction_lock(db, label = "Export.consumer(" + args.length + ")") {
var known = private_data.known_entries(db, args.map(p => p._1.entry_name))
val buffer = new mutable.ListBuffer[Option[Entry]]
@@ -291,7 +283,7 @@
private val consumer =
Consumer_Thread.fork_bulk[(Entry, Boolean)](name = "export")(
- bulk = { case (entry, _) => entry.is_finished },
+ bulk = _ => true,
consume = args => (args.grouped(20).toList.flatMap(consume), true))
def make_entry(session_name: String, args: Protocol.Export.Args, body: Bytes): Unit = {
--- a/src/Pure/Build/export_theory.ML Sat Jun 08 14:57:14 2024 +0200
+++ b/src/Pure/Build/export_theory.ML Sun Jun 09 22:40:13 2024 +0200
@@ -283,11 +283,8 @@
val lookup_thm_id = Global_Theory.lookup_thm_id thy;
fun expand_name thm_id (header: Proofterm.thm_header) =
- if #serial header = #serial thm_id then ""
- else
- (case lookup_thm_id (Proofterm.thm_header_id header) of
- NONE => ""
- | SOME thm_name => Thm_Name.print thm_name);
+ if #serial header = #serial thm_id then Thm_Name.empty
+ else the_default Thm_Name.empty (lookup_thm_id (Proofterm.thm_header_id header));
fun entity_markup_thm (serial, (name, i)) =
let
@@ -298,7 +295,7 @@
fun encode_thm thm_id raw_thm =
let
- val deps = map (Thm_Name.print o #2) (Thm_Deps.thm_deps thy [raw_thm]);
+ val deps = map #2 (Thm_Deps.thm_deps thy [raw_thm]);
val thm = prep_thm raw_thm;
val proof0 =
@@ -314,7 +311,7 @@
let
open XML.Encode Term_XML.Encode;
val encode_proof = Proofterm.encode_standard_proof consts;
- in triple encode_prop (list string) encode_proof end
+ in triple encode_prop (list Thm_Name.encode) encode_proof end
end;
fun export_thm (thm_id, thm_name) =
--- a/src/Pure/Build/export_theory.scala Sat Jun 08 14:57:14 2024 +0200
+++ b/src/Pure/Build/export_theory.scala Sun Jun 09 22:40:13 2024 +0200
@@ -346,13 +346,13 @@
sealed case class Thm(
prop: Prop,
- deps: List[String],
+ deps: List[Thm_Name],
proof: Term.Proof)
extends Content[Thm] {
override def cache(cache: Term.Cache): Thm =
Thm(
prop.cache(cache),
- deps.map(cache.string),
+ deps.map(cache.thm_name),
cache.proof(proof))
}
@@ -361,7 +361,7 @@
{ body =>
import XML.Decode._
import Term_XML.Decode._
- val (prop, deps, prf) = triple(decode_prop, list(string), proof)(body)
+ val (prop, deps, prf) = triple(decode_prop, list(Thm_Name.decode), proof)(body)
Thm(prop, deps, prf)
})
--- a/src/Pure/Concurrent/consumer_thread.scala Sat Jun 08 14:57:14 2024 +0200
+++ b/src/Pure/Concurrent/consumer_thread.scala Sun Jun 09 22:40:13 2024 +0200
@@ -57,7 +57,7 @@
private def failure(exn: Throwable): Unit =
Output.error_message(
- "Consumer thread failure: " + quote(thread.getName) + "\n" + Exn.message(exn))
+ "Consumer thread failure: " + quote(thread.getName) + "\n" + Exn.print(exn))
private def robust_finish(): Unit =
try { finish() } catch { case exn: Throwable => failure(exn) }
--- a/src/Pure/General/name_space.ML Sat Jun 08 14:57:14 2024 +0200
+++ b/src/Pure/General/name_space.ML Sun Jun 09 22:40:13 2024 +0200
@@ -28,6 +28,7 @@
val names_long: bool Config.T
val names_short: bool Config.T
val names_unique: bool Config.T
+ val extern_generic: Context.generic -> T -> string -> xstring
val extern: Proof.context -> T -> string -> xstring
val extern_ord: Proof.context -> T -> string ord
val extern_shortest: Proof.context -> T -> string -> xstring
@@ -291,11 +292,11 @@
val names_short = Config.declare_option_bool ("names_short", \<^here>);
val names_unique = Config.declare_option_bool ("names_unique", \<^here>);
-fun extern ctxt space name =
+fun extern_generic context space name =
let
- val names_long = Config.get ctxt names_long;
- val names_short = Config.get ctxt names_short;
- val names_unique = Config.get ctxt names_unique;
+ val names_long = Config.get_generic context names_long;
+ val names_short = Config.get_generic context names_short;
+ val names_unique = Config.get_generic context names_unique;
fun extern_chunks require_unique a chunks =
let val {full_name = c, unique, ...} = intern_chunks space chunks in
@@ -321,6 +322,8 @@
else extern_names (get_aliases space name)
end;
+val extern = extern_generic o Context.Proof;
+
fun extern_ord ctxt space = string_ord o apply2 (extern ctxt space);
fun extern_shortest ctxt =
--- a/src/Pure/Isar/element.ML Sat Jun 08 14:57:14 2024 +0200
+++ b/src/Pure/Isar/element.ML Sun Jun 09 22:40:13 2024 +0200
@@ -141,7 +141,7 @@
val prt_term = Pretty.quote o Syntax.pretty_term ctxt;
val prt_terms = separate (Pretty.keyword2 "and") o map prt_term;
val prt_binding = Attrib.pretty_binding ctxt;
- val prt_name = Proof_Context.pretty_name ctxt;
+ val prt_name = Thy_Header.pretty_name' ctxt;
fun prt_show (a, ts) =
Pretty.block (Pretty.breaks (prt_binding a ":" @ prt_terms (map fst ts)));
@@ -167,7 +167,7 @@
val prt_typ = Pretty.quote o Syntax.pretty_typ ctxt;
val prt_term = Pretty.quote o Syntax.pretty_term ctxt;
val prt_thm = Pretty.cartouche o Thm.pretty_thm ctxt;
- val prt_name = Proof_Context.pretty_name ctxt;
+ val prt_name = Thy_Header.pretty_name' ctxt;
fun prt_binding (b, atts) =
Attrib.pretty_binding ctxt (b, if show_attribs then atts else []);
@@ -226,10 +226,12 @@
fun thm_name ctxt kind th prts =
let val head =
- if Thm.has_name_hint th then
- Pretty.block [Pretty.keyword1 kind, Pretty.brk 1,
- Proof_Context.pretty_name ctxt (Long_Name.base_name (Thm.get_name_hint th)), Pretty.str ":"]
- else Pretty.keyword1 kind
+ (case try Thm.the_name_hint th of
+ SOME (name, _) =>
+ Pretty.block [Pretty.keyword1 kind, Pretty.brk 1,
+ Thy_Header.pretty_name' ctxt (Long_Name.base_name name),
+ Pretty.str ":"]
+ | NONE => Pretty.keyword1 kind)
in Pretty.block (Pretty.fbreaks (head :: prts)) end;
fun obtain prop ctxt =
--- a/src/Pure/Isar/generic_target.ML Sat Jun 08 14:57:14 2024 +0200
+++ b/src/Pure/Isar/generic_target.ML Sun Jun 09 22:40:13 2024 +0200
@@ -296,8 +296,8 @@
local
-val name_thm1 = Global_Theory.name_thm Global_Theory.official1 o Thm_Name.short;
-val name_thm2 = Global_Theory.name_thm Global_Theory.unofficial2 o Thm_Name.short;
+val name_thm1 = Global_Theory.name_thm Global_Theory.official1;
+val name_thm2 = Global_Theory.name_thm Global_Theory.unofficial2;
fun thm_def (name, pos) thm lthy =
if #1 name <> "" andalso Proofterm.zproof_enabled (Proofterm.get_proofs_level ()) then
--- a/src/Pure/Isar/locale.ML Sat Jun 08 14:57:14 2024 +0200
+++ b/src/Pure/Isar/locale.ML Sun Jun 09 22:40:13 2024 +0200
@@ -199,7 +199,8 @@
(Args.theory -- Scan.lift Parse.embedded_position >>
(ML_Syntax.print_string o uncurry check)));
-fun extern thy = Name_Space.extern (Proof_Context.init_global thy) (locale_space thy);
+fun extern thy =
+ Name_Space.extern_generic (Context.Theory thy) (locale_space thy);
fun markup_extern ctxt =
Name_Space.markup_extern ctxt (locale_space (Proof_Context.theory_of ctxt));
--- a/src/Pure/Isar/proof_context.ML Sat Jun 08 14:57:14 2024 +0200
+++ b/src/Pure/Isar/proof_context.ML Sun Jun 09 22:40:13 2024 +0200
@@ -62,9 +62,9 @@
val facts_of: Proof.context -> Facts.T
val facts_of_fact: Proof.context -> string -> Facts.T
val markup_extern_fact: Proof.context -> string -> Markup.T list * xstring
+ val pretty_thm_name: Proof.context -> Thm_Name.T -> Pretty.T
+ val print_thm_name: Proof.context -> Thm_Name.T -> string
val augment: term -> Proof.context -> Proof.context
- val print_name: Proof.context -> string -> string
- val pretty_name: Proof.context -> string -> Pretty.T
val pretty_term_abbrev: Proof.context -> term -> Pretty.T
val pretty_fact: Proof.context -> string * thm list -> Pretty.T
val check_class: Proof.context -> xstring * Position.T -> class * Position.report list
@@ -423,6 +423,11 @@
else [markup];
in (markups, xname) end;
+fun pretty_thm_name ctxt (name, i) =
+ Facts.pretty_thm_name (Context.Proof ctxt) (facts_of_fact ctxt name) (name, i);
+
+val print_thm_name = Pretty.string_of oo pretty_thm_name;
+
(* augment context by implicit term declarations *)
@@ -435,9 +440,6 @@
(** pretty printing **)
-val print_name = Token.print_name o Thy_Header.get_keywords';
-val pretty_name = Pretty.str oo print_name;
-
fun pretty_term_abbrev ctxt = Syntax.pretty_term (set_mode mode_abbrev ctxt);
fun pretty_fact_name ctxt a =
@@ -1499,7 +1501,7 @@
fun pretty_case (name, (fixes, ((asms, (lets, cs)), ctxt))) =
let
- val prt_name = pretty_name ctxt;
+ val prt_name = Thy_Header.pretty_name' ctxt;
val prt_term = Syntax.pretty_term ctxt;
fun prt_let (xi, t) = Pretty.block
@@ -1546,10 +1548,12 @@
fun trim_name x = if Name.is_internal x then Name.clean x else "_";
val trim_names = map trim_name #> drop_suffix (equal "_");
+ val print_name = Thy_Header.print_name' ctxt;
+
fun print_case name xs =
(case trim_names xs of
- [] => print_name ctxt name
- | xs' => enclose "(" ")" (space_implode " " (map (print_name ctxt) (name :: xs'))));
+ [] => print_name name
+ | xs' => enclose "(" ")" (space_implode " " (map print_name (name :: xs'))));
fun is_case x t =
x = Rule_Cases.case_conclN andalso not (Term.exists_subterm Term.is_Var t);
--- a/src/Pure/PIDE/protocol_handlers.scala Sat Jun 08 14:57:14 2024 +0200
+++ b/src/Pure/PIDE/protocol_handlers.scala Sun Jun 09 22:40:13 2024 +0200
@@ -9,7 +9,7 @@
object Protocol_Handlers {
private def err_handler(exn: Throwable, name: String): Nothing =
- error("Failed to initialize protocol handler: " + quote(name) + "\n" + Exn.message(exn))
+ error("Failed to initialize protocol handler: " + quote(name) + "\n" + Exn.print(exn))
sealed case class State(
session: Session,
@@ -49,7 +49,7 @@
catch {
case exn: Throwable =>
Output.error_message(
- "Failed invocation of protocol function: " + quote(a) + "\n" + Exn.message(exn))
+ "Failed invocation of protocol function: " + quote(a) + "\n" + Exn.print(exn))
false
}
case _ => false
--- a/src/Pure/PIDE/session.scala Sat Jun 08 14:57:14 2024 +0200
+++ b/src/Pure/PIDE/session.scala Sun Jun 09 22:40:13 2024 +0200
@@ -20,7 +20,15 @@
def apply[A](name: String)(consume: A => Unit): Consumer[A] =
new Consumer[A](name, consume)
}
- final class Consumer[-A] private(val name: String, val consume: A => Unit)
+ final class Consumer[-A] private(val name: String, val consume: A => Unit) {
+ private def failure(exn: Throwable): Unit =
+ Output.error_message(
+ "Session consumer failure: " + quote(name) + "\n" + Exn.print(exn))
+
+ def consume_robust(a: A): Unit =
+ try { consume(a) }
+ catch { case exn: Throwable => failure(exn) }
+ }
class Outlet[A](dispatcher: Consumer_Thread[() => Unit]) {
private val consumers = Synchronized[List[Consumer[A]]](Nil)
@@ -30,12 +38,7 @@
def post(a: A): Unit = {
for (c <- consumers.value.iterator) {
- dispatcher.send(() =>
- try { c.consume(a) }
- catch {
- case exn: Throwable =>
- Output.error_message("Consumer failed: " + quote(c.name) + "\n" + Exn.message(exn))
- })
+ dispatcher.send(() => c.consume_robust(a))
}
}
}
--- a/src/Pure/Proof/extraction.ML Sat Jun 08 14:57:14 2024 +0200
+++ b/src/Pure/Proof/extraction.ML Sun Jun 09 22:40:13 2024 +0200
@@ -11,7 +11,7 @@
val add_realizes_eqns : string list -> theory -> theory
val add_typeof_eqns_i : ((term * term) list * (term * term)) list -> theory -> theory
val add_typeof_eqns : string list -> theory -> theory
- val add_realizers_i : (string * (string list * term * Proofterm.proof)) list
+ val add_realizers_i : (Thm_Name.T * (string list * term * Proofterm.proof)) list
-> theory -> theory
val add_realizers : (thm * (string list * string * string)) list
-> theory -> theory
@@ -118,8 +118,11 @@
val change_types = Proofterm.change_types o SOME;
-fun extr_name s vs = Long_Name.append "extr" (space_implode "_" (s :: vs));
-fun corr_name s vs = extr_name s vs ^ "_correctness";
+fun extr_name thm_name vs =
+ Long_Name.append "extr" (space_implode "_" (Thm_Name.short thm_name :: vs));
+
+fun corr_name thm_name vs =
+ extr_name thm_name vs ^ "_correctness";
fun msg d s = writeln (Symbol.spaces d ^ s);
@@ -202,16 +205,16 @@
typeof_eqns : rules,
types : (string * ((term -> term option) list *
(term -> typ -> term -> typ -> term) option)) list,
- realizers : (string list * (term * proof)) list Symtab.table,
+ realizers : (string list * (term * proof)) list Thm_Name.Table.table,
defs : thm list,
- expand : string list,
+ expand : Thm_Name.T list,
prep : (theory -> proof -> proof) option}
val empty =
{realizes_eqns = empty_rules,
typeof_eqns = empty_rules,
types = [],
- realizers = Symtab.empty,
+ realizers = Thm_Name.Table.empty,
defs = [],
expand = [],
prep = NONE};
@@ -224,7 +227,7 @@
{realizes_eqns = merge_rules realizes_eqns1 realizes_eqns2,
typeof_eqns = merge_rules typeof_eqns1 typeof_eqns2,
types = AList.merge (op =) (K true) (types1, types2),
- realizers = Symtab.merge_list (eq_set (op =) o apply2 #1) (realizers1, realizers2),
+ realizers = Thm_Name.Table.merge_list (eq_set (op =) o apply2 #1) (realizers1, realizers2),
defs = Library.merge Thm.eq_thm (defs1, defs2),
expand = Library.merge (op =) (expand1, expand2),
prep = if is_some prep1 then prep1 else prep2};
@@ -319,7 +322,7 @@
in
ExtractionData.put
{realizes_eqns = realizes_eqns, typeof_eqns = typeof_eqns, types = types,
- realizers = fold (Symtab.cons_list o prep_rlz thy) rs realizers,
+ realizers = fold (Thm_Name.Table.cons_list o prep_rlz thy) rs realizers,
defs = defs, expand = expand, prep = prep} thy
end
@@ -335,8 +338,8 @@
val rd = Proof_Syntax.read_proof thy' true false;
in fn (thm, (vs, s1, s2)) =>
let
- val name = Thm.derivation_name thm;
- val _ = name <> "" orelse error "add_realizers: unnamed theorem";
+ val thm_name = Thm.derivation_name thm;
+ val _ = if Thm_Name.is_empty thm_name then error "add_realizers: unnamed theorem" else ();
val prop = Thm.unconstrainT thm |> Thm.prop_of |>
Pattern.rewrite_term thy' (map (Logic.dest_equals o Thm.prop_of) defs) [];
val vars = vars_of prop;
@@ -357,7 +360,7 @@
val r = Logic.list_implies (shyps,
fold_rev Logic.all (map (get_var_type r') vars) r');
val prf = Proofterm.reconstruct_proof thy' r (rd s2);
- in (name, (vs, (t, prf))) end
+ in (thm_name, (vs, (t, prf))) end
end;
val add_realizers_i = gen_add_realizers
@@ -411,8 +414,8 @@
val {realizes_eqns, typeof_eqns, types, realizers,
defs, expand, prep} = ExtractionData.get thy;
- val name = Thm.derivation_name thm;
- val _ = name <> "" orelse error "add_expand_thm: unnamed theorem";
+ val thm_name = Thm.derivation_name thm;
+ val _ = if Thm_Name.is_empty thm_name then error "add_expand_thm: unnamed theorem" else ();
in
thy |> ExtractionData.put
(if is_def then
@@ -425,7 +428,7 @@
else
{realizes_eqns = realizes_eqns, typeof_eqns = typeof_eqns, types = types,
realizers = realizers, defs = defs,
- expand = insert (op =) name expand, prep = prep})
+ expand = insert (op =) thm_name expand, prep = prep})
end;
fun extraction_expand is_def =
@@ -508,8 +511,9 @@
val procs = maps (rev o fst o snd) types;
val rtypes = map fst types;
val typroc = typeof_proc [];
- fun expand_name ({name, ...}: Proofterm.thm_header) =
- if name = "" orelse member (op =) expand name then SOME "" else NONE;
+ fun expand_name ({thm_name, ...}: Proofterm.thm_header) =
+ if Thm_Name.is_empty thm_name orelse member (op =) expand thm_name
+ then SOME Thm_Name.empty else NONE;
val prep = the_default (K I) prep thy' o
Proof_Rewrite_Rules.elim_defs thy' false (map (Thm.transfer thy) defs) o
Proofterm.expand_proof thy' expand_name;
@@ -539,7 +543,8 @@
(T, Sign.defaultS thy)) tye;
fun find (vs: string list) = Option.map snd o find_first (curry (eq_set (op =)) vs o fst);
- fun find' (s: string) = map_filter (fn (s', x) => if s = s' then SOME x else NONE);
+ fun filter_thm_name (a: Thm_Name.T) =
+ map_filter (fn (b, x) => if a = b then SOME x else NONE);
fun app_rlz_rews Ts vs t =
strip_abs (length Ts)
@@ -618,7 +623,7 @@
| corr d vs ts Ts hs cs _ (prf0 as PThm (thm_header as {types = SOME Ts', ...}, thm_body)) _ defs =
let
- val {pos, theory_name, name, prop, ...} = thm_header;
+ val {pos, theory_name, thm_name, prop, ...} = thm_header;
val prf = Proofterm.thm_body_proof_open thm_body;
val (vs', tye) = find_inst prop Ts ts vs;
val shyps = mk_shyps tye;
@@ -629,14 +634,16 @@
else snd (extr d vs ts Ts hs prf0 defs)
in
if T = nullT andalso realizes_null vs' prop aconv prop then (prf0, defs)
- else (case Symtab.lookup realizers name of
- NONE => (case find vs' (find' name defs') of
+ else (case Thm_Name.Table.lookup realizers thm_name of
+ NONE => (case find vs' (filter_thm_name thm_name defs') of
NONE =>
let
val _ = T = nullT orelse error "corr: internal error";
- val _ = msg d ("Building correctness proof for " ^ quote name ^
- (if null vs' then ""
- else " (relevant variables: " ^ commas_quote vs' ^ ")"));
+ val _ =
+ msg d ("Building correctness proof for " ^
+ quote (Global_Theory.print_thm_name thy thm_name) ^
+ (if null vs' then ""
+ else " (relevant variables: " ^ commas_quote vs' ^ ")"));
val prf' = prep (Proofterm.reconstruct_proof thy' prop prf);
val (corr_prf0, defs'') = corr (d + 1) vs' [] [] []
(rev shyps) NONE prf' prf' defs';
@@ -644,7 +651,7 @@
val corr_prop = Proofterm.prop_of corr_prf;
val corr_header =
Proofterm.thm_header (serial ()) pos theory_name
- (corr_name name vs') corr_prop
+ (corr_name thm_name vs', 0) corr_prop
(SOME (map TVar (Term.add_tvars corr_prop [] |> rev)));
val corr_prf' =
Proofterm.proof_combP
@@ -656,15 +663,16 @@
mkabsp shyps
in
(Proofterm.proof_combP (prf_subst_TVars tye' corr_prf', sprfs),
- (name, (vs', ((nullt, nullt), (corr_prf, corr_prf')))) :: defs'')
+ (thm_name, (vs', ((nullt, nullt), (corr_prf, corr_prf')))) :: defs'')
end
| SOME (_, (_, prf')) =>
(Proofterm.proof_combP (prf_subst_TVars tye' prf', sprfs), defs'))
| SOME rs => (case find vs' rs of
SOME (_, prf') => (Proofterm.proof_combP (prf_subst_TVars tye' prf', sprfs), defs')
| NONE => error ("corr: no realizer for instance of theorem " ^
- quote name ^ ":\n" ^ Syntax.string_of_term_global thy' (Envir.beta_norm
- (Proofterm.prop_of (Proofterm.proof_combt (prf0, ts)))))))
+ quote (Global_Theory.print_thm_name thy' thm_name) ^ ":\n" ^
+ Syntax.string_of_term_global thy'
+ (Envir.beta_norm (Proofterm.prop_of (Proofterm.proof_combt (prf0, ts)))))))
end
| corr d vs ts Ts hs cs _ (prf0 as PAxm (s, prop, SOME Ts')) _ defs =
@@ -674,7 +682,7 @@
in
if etype_of thy' vs' [] prop = nullT andalso
realizes_null vs' prop aconv prop then (prf0, defs)
- else case find vs' (Symtab.lookup_list realizers s) of
+ else case find vs' (Thm_Name.Table.lookup_list realizers (s, 0)) of
SOME (_, prf) => (Proofterm.proof_combP (prf_subst_TVars tye' prf, mk_sprfs cs tye),
defs)
| NONE => error ("corr: no realizer for instance of axiom " ^
@@ -719,19 +727,20 @@
| extr d vs ts Ts hs (prf0 as PThm (thm_header as {types = SOME Ts', ...}, thm_body)) defs =
let
- val {pos, theory_name, name = s, prop, ...} = thm_header;
+ val {pos, theory_name, thm_name, prop, ...} = thm_header;
val prf = Proofterm.thm_body_proof_open thm_body;
val (vs', tye) = find_inst prop Ts ts vs;
val shyps = mk_shyps tye;
val tye' = (map fst (Term.add_tvars prop [] |> rev) ~~ Ts') @ tye
in
- case Symtab.lookup realizers s of
- NONE => (case find vs' (find' s defs) of
+ case Thm_Name.Table.lookup realizers thm_name of
+ NONE => (case find vs' (filter_thm_name thm_name defs) of
NONE =>
let
- val _ = msg d ("Extracting " ^ quote s ^
- (if null vs' then ""
- else " (relevant variables: " ^ commas_quote vs' ^ ")"));
+ val _ =
+ msg d ("Extracting " ^ quote (Global_Theory.print_thm_name thy' thm_name) ^
+ (if null vs' then ""
+ else " (relevant variables: " ^ commas_quote vs' ^ ")"));
val prf' = prep (Proofterm.reconstruct_proof thy' prop prf);
val (t, defs') = extr (d + 1) vs' [] [] [] prf' defs;
val (corr_prf, defs'') = corr (d + 1) vs' [] [] []
@@ -743,7 +752,7 @@
val args' = filter (fn v => Logic.occs (v, nt)) args;
val t' = mkabs args' nt;
val T = fastype_of t';
- val cname = extr_name s vs';
+ val cname = extr_name thm_name vs';
val c = Const (cname, T);
val u = mkabs args (list_comb (c, args'));
val eqn = Logic.mk_equals (c, t');
@@ -764,7 +773,7 @@
val corr_prop = Proofterm.prop_of corr_prf';
val corr_header =
Proofterm.thm_header (serial ()) pos theory_name
- (corr_name s vs') corr_prop
+ (corr_name thm_name vs', 0) corr_prop
(SOME (map TVar (Term.add_tvars corr_prop [] |> rev)));
val corr_prf'' =
Proofterm.proof_combP (Proofterm.proof_combt
@@ -775,13 +784,14 @@
mkabsp shyps
in
(subst_TVars tye' u,
- (s, (vs', ((t', u), (corr_prf', corr_prf'')))) :: defs'')
+ (thm_name, (vs', ((t', u), (corr_prf', corr_prf'')))) :: defs'')
end
| SOME ((_, u), _) => (subst_TVars tye' u, defs))
| SOME rs => (case find vs' rs of
SOME (t, _) => (subst_TVars tye' t, defs)
| NONE => error ("extr: no realizer for instance of theorem " ^
- quote s ^ ":\n" ^ Syntax.string_of_term_global thy' (Envir.beta_norm
+ quote (Global_Theory.print_thm_name thy' thm_name) ^ ":\n" ^
+ Syntax.string_of_term_global thy' (Envir.beta_norm
(Proofterm.prop_of (Proofterm.proof_combt (prf0, ts))))))
end
@@ -790,7 +800,7 @@
val (vs', tye) = find_inst prop Ts ts vs;
val tye' = (map fst (Term.add_tvars prop [] |> rev) ~~ Ts') @ tye
in
- case find vs' (Symtab.lookup_list realizers s) of
+ case find vs' (Thm_Name.Table.lookup_list realizers (s, 0)) of
SOME (t, _) => (subst_TVars tye' t, defs)
| NONE => error ("extr: no realizer for instance of axiom " ^
quote s ^ ":\n" ^ Syntax.string_of_term_global thy' (Envir.beta_norm
@@ -805,26 +815,27 @@
val prop = Thm.prop_of thm;
val prf = Thm.proof_of thm;
val name = Thm.derivation_name thm;
- val _ = name <> "" orelse error "extraction: unnamed theorem";
+ val _ = if Thm_Name.is_empty name then error "extraction: unnamed theorem" else ();
val _ = etype_of thy' vs [] prop <> nullT orelse error ("theorem " ^
- quote name ^ " has no computational content")
+ quote (Global_Theory.print_thm_name thy' name) ^ " has no computational content")
in Proofterm.reconstruct_proof thy' prop prf end;
val defs =
fold (fn (thm, vs) => snd o (extr 0 vs [] [] [] o prep_thm vs) thm)
thm_vss [];
- fun add_def (s, (vs, ((t, u)))) thy =
+ fun add_def (name, (vs, ((t, u)))) thy =
let
val ft = Type.legacy_freeze t;
val fu = Type.legacy_freeze u;
val head = head_of (strip_abs_body fu);
- val b = Binding.qualified_name (extr_name s vs);
+ val b = Binding.qualified_name (extr_name name vs);
in
thy
|> Sign.add_consts [(b, fastype_of ft, NoSyn)]
|> Global_Theory.add_def
- (Binding.qualified_name (Thm.def_name (extr_name s vs)), Logic.mk_equals (head, ft))
+ (Binding.qualified_name (Thm.def_name (extr_name name vs)),
+ Logic.mk_equals (head, ft))
|-> (fn def_thm =>
Spec_Rules.add_global b Spec_Rules.equational
[Thm.term_of (Thm.lhs_of def_thm)] [def_thm]
--- a/src/Pure/Proof/proof_checker.ML Sat Jun 08 14:57:14 2024 +0200
+++ b/src/Pure/Proof/proof_checker.ML Sun Jun 09 22:40:13 2024 +0200
@@ -16,10 +16,13 @@
(***** construct a theorem out of a proof term *****)
fun lookup_thm thy =
- let val tab = Symtab.build (Global_Theory.all_thms_of thy true |> fold_rev Symtab.update) in
- fn s =>
- (case Symtab.lookup tab s of
- NONE => error ("Unknown theorem " ^ quote s)
+ let
+ val tab =
+ Thm_Name.Table.build (Global_Theory.all_thms_of thy true |> fold_rev Thm_Name.Table.update);
+ in
+ fn name =>
+ (case Thm_Name.Table.lookup tab name of
+ NONE => error ("Unknown theorem " ^ quote (Thm_Name.print name))
| SOME thm => thm)
end;
@@ -85,14 +88,15 @@
(Thm.forall_intr_vars (Thm.forall_intr_frees thm'))
end;
- fun thm_of _ _ (PThm ({name, prop = prop', types = SOME Ts, ...}, _)) =
+ fun thm_of _ _ (PThm ({thm_name, prop = prop', types = SOME Ts, ...}, _)) =
let
- val thm = Thm.unconstrainT (Drule.implies_intr_hyps (lookup name));
+ val thm = Thm.unconstrainT (Drule.implies_intr_hyps (lookup thm_name));
val prop = Thm.prop_of thm;
val _ =
if is_equal prop prop' then ()
else
- error ("Duplicate use of theorem name " ^ quote name ^ "\n" ^
+ error ("Duplicate use of theorem name " ^
+ quote (Global_Theory.print_thm_name thy thm_name) ^ "\n" ^
Syntax.string_of_term_global thy prop ^ "\n\n" ^
Syntax.string_of_term_global thy prop');
in thm_of_atom thm Ts end
--- a/src/Pure/Proof/proof_rewrite_rules.ML Sat Jun 08 14:57:14 2024 +0200
+++ b/src/Pure/Proof/proof_rewrite_rules.ML Sun Jun 09 22:40:13 2024 +0200
@@ -39,12 +39,12 @@
val equal_elim_axm = ax Proofterm.equal_elim_axm [];
val symmetric_axm = ax Proofterm.symmetric_axm [propT];
- fun rew' (PThm ({name = "Pure.protectD", ...}, _) % _ %%
- (PThm ({name = "Pure.protectI", ...}, _) % _ %% prf)) = SOME prf
- | rew' (PThm ({name = "Pure.conjunctionD1", ...}, _) % _ % _ %%
- (PThm ({name = "Pure.conjunctionI", ...}, _) % _ % _ %% prf %% _)) = SOME prf
- | rew' (PThm ({name = "Pure.conjunctionD2", ...}, _) % _ % _ %%
- (PThm ({name = "Pure.conjunctionI", ...}, _) % _ % _ %% _ %% prf)) = SOME prf
+ fun rew' (PThm ({thm_name = ("Pure.protectD", 0), ...}, _) % _ %%
+ (PThm ({thm_name = ("Pure.protectI", 0), ...}, _) % _ %% prf)) = SOME prf
+ | rew' (PThm ({thm_name = ("Pure.conjunctionD1", 0), ...}, _) % _ % _ %%
+ (PThm ({thm_name = ("Pure.conjunctionI", 0), ...}, _) % _ % _ %% prf %% _)) = SOME prf
+ | rew' (PThm ({thm_name = ("Pure.conjunctionD2", 0), ...}, _) % _ % _ %%
+ (PThm ({thm_name = ("Pure.conjunctionI", 0), ...}, _) % _ % _ %% _ %% prf)) = SOME prf
| rew' (PAxm ("Pure.equal_elim", _, _) % _ % _ %%
(PAxm ("Pure.equal_intr", _, _) % _ % _ %% prf %% _)) = SOME prf
| rew' (PAxm ("Pure.symmetric", _, _) % _ % _ %%
@@ -54,14 +54,14 @@
| rew' (PAxm ("Pure.equal_elim", _, _) % SOME (_ $ A) % SOME (_ $ B) %%
(PAxm ("Pure.combination", _, _) % SOME (Const ("Pure.prop", _)) %
_ % _ % _ %% (PAxm ("Pure.reflexive", _, _) % _) %% prf1) %%
- ((tg as PThm ({name = "Pure.protectI", ...}, _)) % _ %% prf2)) =
+ ((tg as PThm ({thm_name = ("Pure.protectI", 0), ...}, _)) % _ %% prf2)) =
SOME (tg %> B %% (equal_elim_axm %> A %> B %% prf1 %% prf2))
| rew' (PAxm ("Pure.equal_elim", _, _) % SOME (_ $ A) % SOME (_ $ B) %%
(PAxm ("Pure.symmetric", _, _) % _ % _ %%
(PAxm ("Pure.combination", _, _) % SOME (Const ("Pure.prop", _)) %
_ % _ % _ %% (PAxm ("Pure.reflexive", _, _) % _) %% prf1)) %%
- ((tg as PThm ({name = "Pure.protectI", ...}, _)) % _ %% prf2)) =
+ ((tg as PThm ({thm_name = ("Pure.protectI", 0), ...}, _)) % _ %% prf2)) =
SOME (tg %> B %% (equal_elim_axm %> A %> B %%
(symmetric_axm % ?? B % ?? A %% prf1) %% prf2))
@@ -245,8 +245,8 @@
(AbsP (s, t, fst (insert_refl defs Ts prf)), false)
| insert_refl defs Ts prf =
(case Proofterm.strip_combt prf of
- (PThm ({name = s, prop, types = SOME Ts, ...}, _), ts) =>
- if member (op =) defs s then
+ (PThm ({thm_name, prop, types = SOME Ts, ...}, _), ts) =>
+ if member (op =) defs thm_name then
let
val vs = vars_of prop;
val tvars = build_rev (Term.add_tvars prop);
@@ -271,11 +271,11 @@
let
val cnames = map (fst o dest_Const o fst) defs';
val expand = Proofterm.fold_proof_atoms true
- (fn PThm ({serial, name, prop, ...}, _) =>
- if member (op =) defnames name orelse
+ (fn PThm ({serial, thm_name, prop, ...}, _) =>
+ if member (op =) defnames thm_name orelse
not (exists_Const (member (op =) cnames o #1) prop)
then I
- else Inttab.update (serial, "")
+ else Inttab.update (serial, Thm_Name.empty)
| _ => I) [prf] Inttab.empty;
in Proofterm.expand_proof thy (Inttab.lookup expand o #serial) prf end
else prf;
--- a/src/Pure/Proof/proof_syntax.ML Sat Jun 08 14:57:14 2024 +0200
+++ b/src/Pure/Proof/proof_syntax.ML Sun Jun 09 22:40:13 2024 +0200
@@ -16,7 +16,7 @@
val pretty_proof: Proof.context -> Proofterm.proof -> Pretty.T
val pretty_proof_boxes_of: Proof.context ->
{full: bool, preproc: theory -> proof -> proof} -> thm -> Pretty.T
- val standard_proof_of: {full: bool, expand_name: Proofterm.thm_header -> string option} ->
+ val standard_proof_of: {full: bool, expand_name: Proofterm.thm_header -> Thm_Name.T option} ->
thm -> Proofterm.proof
val pretty_standard_proof_of: Proof.context -> bool -> thm -> Pretty.T
end;
@@ -104,9 +104,11 @@
let val U = Term.itselfT T --> propT
in Const ("Pure.PClass", U --> proofT) $ Const (Logic.const_of_class c, U) end;
-fun term_of _ (PThm ({serial = i, name, types = Ts, ...}, _)) =
+fun term_of _ (PThm ({serial = i, thm_name = a, types = Ts, ...}, _)) =
fold AppT (these Ts)
- (Const (Long_Name.append "thm" (if name = "" then string_of_int i else name), proofT))
+ (Const
+ (Long_Name.append "thm"
+ (if Thm_Name.is_empty a then string_of_int i else Thm_Name.short a), proofT))
| term_of _ (PAxm (name, _, Ts)) =
fold AppT (these Ts) (Const (Long_Name.append "axm" name, proofT))
| term_of _ (PClass (T, c)) = AppT T (PClasst (T, c))
@@ -141,7 +143,7 @@
fun proof_of_term thy ty =
let
- val thms = Global_Theory.all_thms_of thy true;
+ val thms = Global_Theory.all_thms_of thy true |> map (apfst Thm_Name.short);
val axms = Theory.all_axioms_of thy;
fun mk_term t = (if ty then I else map_types (K dummyT))
@@ -198,7 +200,8 @@
fun read_term thy topsort =
let
- val thm_names = filter_out (fn s => s = "") (map fst (Global_Theory.all_thms_of thy true));
+ val thm_names =
+ filter_out (fn s => s = "") (map (Thm_Name.short o fst) (Global_Theory.all_thms_of thy true));
val axm_names = map fst (Theory.all_axioms_of thy);
val ctxt = thy
|> add_proof_syntax
@@ -224,7 +227,8 @@
fun proof_syntax prf =
let
val thm_names = Symset.dest (Proofterm.fold_proof_atoms true
- (fn PThm ({name, ...}, _) => if name <> "" then Symset.insert name else I
+ (fn PThm ({thm_name, ...}, _) =>
+ if Thm_Name.is_empty thm_name then I else Symset.insert (Thm_Name.short thm_name)
| _ => I) [prf] Symset.empty);
val axm_names = Symset.dest (Proofterm.fold_proof_atoms true
(fn PAxm (name, _, _) => Symset.insert name | _ => I) [prf] Symset.empty);
--- a/src/Pure/Pure.thy Sat Jun 08 14:57:14 2024 +0200
+++ b/src/Pure/Pure.thy Sun Jun 09 22:40:13 2024 +0200
@@ -1378,7 +1378,9 @@
let
val thy = Toplevel.theory_of st;
val ctxt = Toplevel.context_of st;
- fun pretty_thm (a, th) = Proof_Context.pretty_fact ctxt (a, [th]);
+ fun pretty_thm (a, th) =
+ Pretty.block [Pretty.quote (Proof_Context.pretty_thm_name ctxt a),
+ Pretty.str ":", Pretty.brk 1, Thm.pretty_thm ctxt th];
val check = Theory.check {long = false} ctxt;
in
Thm_Deps.unused_thms_cmd
--- a/src/Pure/System/classpath.scala Sat Jun 08 14:57:14 2024 +0200
+++ b/src/Pure/System/classpath.scala Sun Jun 09 22:40:13 2024 +0200
@@ -74,7 +74,7 @@
try { Class.forName(name, true, class_loader).asInstanceOf[Classpath.Service_Class] }
catch {
case _: ClassNotFoundException => err("Class not found")
- case exn: Throwable => err(Exn.message(exn))
+ case exn: Throwable => err(Exn.print(exn))
}
}
}
--- a/src/Pure/Thy/thy_header.ML Sat Jun 08 14:57:14 2024 +0200
+++ b/src/Pure/Thy/thy_header.ML Sun Jun 09 22:40:13 2024 +0200
@@ -17,6 +17,11 @@
val add_keywords: keywords -> theory -> theory
val get_keywords: theory -> Keyword.keywords
val get_keywords': Proof.context -> Keyword.keywords
+ val print_name: theory -> string -> string
+ val print_name': Proof.context -> string -> string
+ val pretty_name: theory -> string -> Pretty.T
+ val pretty_name': Proof.context -> string -> Pretty.T
+
val ml_bootstrapN: string
val ml_roots: string list
val bootstrap_thys: string list
@@ -90,7 +95,7 @@
(("ML", \<^here>), Keyword.command_spec (Keyword.thy_decl, ["ML"]))];
-(* theory data *)
+(* keywords *)
structure Data = Theory_Data
(
@@ -104,6 +109,12 @@
val get_keywords = Data.get;
val get_keywords' = get_keywords o Proof_Context.theory_of;
+val print_name = Token.print_name o get_keywords;
+val print_name' = Token.print_name o get_keywords';
+
+val pretty_name = Pretty.str oo print_name;
+val pretty_name' = Pretty.str oo print_name';
+
(** concrete syntax **)
--- a/src/Pure/Tools/generated_files.ML Sat Jun 08 14:57:14 2024 +0200
+++ b/src/Pure/Tools/generated_files.ML Sun Jun 09 22:40:13 2024 +0200
@@ -349,7 +349,8 @@
(case try Bytes.read (dir + path) of
SOME bytes => Bytes.contents_blob bytes
| NONE => error ("Missing result file " ^ Path.print path ^ Position.here pos));
- val _ = Export.report_export thy export_prefix;
+ val _ =
+ Export.report (Context.Theory thy) (Context.theory_long_name thy) export_prefix;
val binding' =
Path.map_binding (Path.append (Path.path_of_binding export_prefix)) binding;
in
--- a/src/Pure/Tools/simplifier_trace.ML Sat Jun 08 14:57:14 2024 +0200
+++ b/src/Pure/Tools/simplifier_trace.ML Sun Jun 09 22:40:13 2024 +0200
@@ -230,7 +230,7 @@
let
(* FIXME pretty printing via Proof_Context.pretty_fact *)
val pretty_thm = Pretty.block
- [Pretty.str ("Instance of " ^ name ^ ":"),
+ [Pretty.str ("Instance of " ^ Proof_Context.print_thm_name ctxt name ^ ":"),
Pretty.brk 1,
Syntax.pretty_term ctxt (Thm.prop_of thm)]
@@ -319,7 +319,7 @@
val pretty_thm =
(* FIXME pretty printing via Proof_Context.pretty_fact *)
Pretty.block
- [Pretty.str ("In an instance of " ^ name ^ ":"),
+ [Pretty.str ("In an instance of " ^ Proof_Context.print_thm_name ctxt name ^ ":"),
Pretty.brk 1,
Syntax.pretty_term ctxt (Thm.prop_of thm)]
--- a/src/Pure/facts.ML Sat Jun 08 14:57:14 2024 +0200
+++ b/src/Pure/facts.ML Sun Jun 09 22:40:13 2024 +0200
@@ -30,6 +30,7 @@
val intern: T -> xstring -> string
val extern: Proof.context -> T -> string -> xstring
val markup_extern: Proof.context -> T -> string -> Markup.T * xstring
+ val pretty_thm_name: Context.generic -> T -> Thm_Name.T -> Pretty.T
val defined: T -> string -> bool
val is_dynamic: T -> string -> bool
val lookup: Context.generic -> T -> string -> {dynamic: bool, thms: thm list} option
@@ -173,6 +174,12 @@
fun extern ctxt = Name_Space.extern ctxt o space_of;
fun markup_extern ctxt = Name_Space.markup_extern ctxt o space_of;
+fun pretty_thm_name context facts thm_name =
+ let
+ val prfx = Thm_Name.print_prefix context (space_of facts) thm_name;
+ val sffx = Thm_Name.print_suffix thm_name;
+ in Pretty.block [Pretty.mark_str prfx, Pretty.str sffx] end;
+
(* retrieve *)
--- a/src/Pure/global_theory.ML Sat Jun 08 14:57:14 2024 +0200
+++ b/src/Pure/global_theory.ML Sun Jun 09 22:40:13 2024 +0200
@@ -14,6 +14,8 @@
val alias_fact: binding -> string -> theory -> theory
val hide_fact: bool -> string -> theory -> theory
val dest_thms: bool -> theory list -> theory -> (Thm_Name.T * thm) list
+ val pretty_thm_name: theory -> Thm_Name.T -> Pretty.T
+ val print_thm_name: theory -> Thm_Name.T -> string
val get_thm_names: theory -> Thm_Name.T Inttab.table
val dest_thm_names: theory -> (Proofterm.thm_id * Thm_Name.T) list
val lookup_thm_id: theory -> Proofterm.thm_id -> Thm_Name.T option
@@ -21,7 +23,7 @@
val get_thms: theory -> xstring -> thm list
val get_thm: theory -> xstring -> thm
val transfer_theories: theory -> thm -> thm
- val all_thms_of: theory -> bool -> (string * thm) list
+ val all_thms_of: theory -> bool -> (Thm_Name.T * thm) list
val get_thm_name: theory -> Thm_Name.T * Position.T -> thm
type name_flags
val unnamed: name_flags
@@ -29,7 +31,7 @@
val official2: name_flags
val unofficial1: name_flags
val unofficial2: name_flags
- val name_thm: name_flags -> string * Position.T -> thm -> thm
+ val name_thm: name_flags -> Thm_Name.P -> thm -> thm
val name_thms: name_flags -> string * Position.T -> thm list -> thm list
val name_facts: name_flags -> string * Position.T -> (thm list * 'a) list -> (thm list * 'a) list
val check_thms_lazy: thm list lazy -> thm list lazy
@@ -67,7 +69,7 @@
);
-(* facts *)
+(* global facts *)
val facts_of = #1 o Data.get;
val map_facts = Data.map o apfst;
@@ -86,6 +88,9 @@
Facts.dest_static verbose (map facts_of prev_thys) (facts_of thy)
|> maps (fn (name, thms) => Thm_Name.list (name, Position.none) thms |> map (apfst fst));
+fun pretty_thm_name thy = Facts.pretty_thm_name (Context.Theory thy) (facts_of thy);
+val print_thm_name = Pretty.string_of oo pretty_thm_name;
+
(* thm_name vs. derivation_id *)
@@ -104,8 +109,8 @@
(case Inttab.lookup thm_names serial of
SOME thm_name' =>
raise THM ("Duplicate use of derivation identity for " ^
- Thm_Name.print thm_name ^ " vs. " ^
- Thm_Name.print thm_name', 0, [thm])
+ print_thm_name thy thm_name ^ " vs. " ^
+ print_thm_name thy thm_name', 0, [thm])
| NONE => Inttab.update (serial, thm_name) thm_names)));
fun lazy_thm_names thy =
@@ -251,21 +256,18 @@
No_Name_Flags => thm
| Name_Flags {post, official} =>
thm
- |> (official andalso (post orelse Thm.raw_derivation_name thm = "")) ?
+ |> (official andalso (post orelse Thm_Name.is_empty (Thm.raw_derivation_name thm))) ?
Thm.name_derivation (name, pos)
- |> (name <> "" andalso (post orelse not (Thm.has_name_hint thm))) ?
+ |> (not (Thm_Name.is_empty name) andalso (post orelse not (Thm.has_name_hint thm))) ?
Thm.put_name_hint name));
end;
-fun name_thm_short name_flags name =
- name_thm name_flags (Thm_Name.short name);
-
fun name_thms name_flags name_pos thms =
- Thm_Name.list name_pos thms |> map (uncurry (name_thm_short name_flags));
+ Thm_Name.list name_pos thms |> map (uncurry (name_thm name_flags));
fun name_facts name_flags name_pos facts =
- Thm_Name.expr name_pos facts |> (map o apfst o map) (uncurry (name_thm_short name_flags));
+ Thm_Name.expr name_pos facts |> (map o apfst o map) (uncurry (name_thm name_flags));
(* store theorems and proofs *)
@@ -319,7 +321,7 @@
in ((thms', atts), thy2) end);
val unnamed = #1 name = "";
- val name_thm1 = if unnamed then #2 else uncurry (name_thm_short name_flags1);
+ val name_thm1 = if unnamed then #2 else uncurry (name_thm name_flags1);
val app_facts =
fold_maps (fn (named_thms, atts) => fn thy =>
--- a/src/Pure/logic.ML Sat Jun 08 14:57:14 2024 +0200
+++ b/src/Pure/logic.ML Sun Jun 09 22:40:13 2024 +0200
@@ -48,6 +48,7 @@
val const_of_class: class -> string
val class_of_const: string -> class
val mk_of_class: typ * class -> term
+ val match_of_class: term -> typ * string (*exception Match*)
val dest_of_class: term -> typ * class
val mk_of_sort: typ * sort -> term list
val name_classrel: string * string -> string
@@ -303,6 +304,9 @@
fun mk_of_class (ty, c) =
Const (const_of_class c, Term.itselfT ty --> propT) $ mk_type ty;
+fun match_of_class (Const (c, _) $ Const ("Pure.type", Type ("itself", [ty]))) =
+ if String.isSuffix class_suffix c then (ty, class_of_const c) else raise Match;
+
fun dest_of_class (Const (c_class, _) $ ty) = (dest_type ty, class_of_const c_class)
| dest_of_class t = raise TERM ("dest_of_class", [t]);
--- a/src/Pure/more_thm.ML Sat Jun 08 14:57:14 2024 +0200
+++ b/src/Pure/more_thm.ML Sun Jun 09 22:40:13 2024 +0200
@@ -87,9 +87,10 @@
val def_binding: Binding.binding -> Binding.binding
val def_binding_optional: Binding.binding -> Binding.binding -> Binding.binding
val make_def_binding: bool -> Binding.binding -> Binding.binding
+ val the_name_hint: thm -> Thm_Name.T (*exception THM*)
val has_name_hint: thm -> bool
- val get_name_hint: thm -> string
- val put_name_hint: string -> thm -> thm
+ val get_name_hint: thm -> Thm_Name.T
+ val put_name_hint: Thm_Name.T -> thm -> thm
val theoremK: string
val legacy_get_kind: thm -> string
val kind_rule: string -> thm -> thm
@@ -606,11 +607,18 @@
(* unofficial theorem names *)
-fun has_name_hint thm = AList.defined (op =) (Thm.get_tags thm) Markup.nameN;
-fun the_name_hint thm = the (AList.lookup (op =) (Thm.get_tags thm) Markup.nameN);
-fun get_name_hint thm = if has_name_hint thm then the_name_hint thm else "??.unknown";
+fun the_name_hint thm =
+ let val thm_name = Thm_Name.parse (Properties.get_string (Thm.get_tags thm) Markup.nameN)
+ in
+ if Thm_Name.is_empty thm_name
+ then raise THM ("Thm.the_name_hint: missing name", 0, [thm])
+ else thm_name
+ end;
-fun put_name_hint name = untag_rule Markup.nameN #> tag_rule (Markup.nameN, name);
+fun has_name_hint thm = can the_name_hint thm;
+fun get_name_hint thm = try the_name_hint thm |> the_default ("??.unknown", 0);
+
+fun put_name_hint name = untag_rule Markup.nameN #> tag_rule (Markup.nameN, Thm_Name.print name);
(* theorem kinds *)
--- a/src/Pure/proofterm.ML Sat Jun 08 14:57:14 2024 +0200
+++ b/src/Pure/proofterm.ML Sun Jun 09 22:40:13 2024 +0200
@@ -9,7 +9,7 @@
signature PROOFTERM =
sig
type thm_header =
- {serial: serial, pos: Position.T list, theory_name: string, name: string,
+ {serial: serial, pos: Position.T list, theory_name: string, thm_name: Thm_Name.T,
prop: term, types: typ list option}
type thm_body
type thm_node
@@ -38,13 +38,13 @@
val proof_of: proof_body -> proof
val join_proof: proof_body future -> proof
val map_proof_of: (proof -> proof) -> proof_body -> proof_body
- val thm_header: serial -> Position.T list -> string -> string -> term -> typ list option ->
+ val thm_header: serial -> Position.T list -> string -> Thm_Name.T -> term -> typ list option ->
thm_header
val thm_body: proof_body -> thm_body
val thm_body_proof_raw: thm_body -> proof
val thm_body_proof_open: thm_body -> proof
val thm_node_theory_name: thm_node -> string
- val thm_node_name: thm_node -> string
+ val thm_node_name: thm_node -> Thm_Name.T
val thm_node_prop: thm_node -> term
val thm_node_body: thm_node -> proof_body future
val thm_node_thms: thm_node -> thm list
@@ -52,7 +52,7 @@
val make_thm: thm_header -> thm_body -> thm
val fold_proof_atoms: bool -> (proof -> 'a -> 'a) -> proof list -> 'a -> 'a
val fold_body_thms:
- ({serial: serial, name: string, prop: term, body: proof_body} -> 'a -> 'a) ->
+ ({serial: serial, thm_name: Thm_Name.T, prop: term, body: proof_body} -> 'a -> 'a) ->
proof_body list -> 'a -> 'a
val oracle_ord: oracle ord
val thm_ord: thm ord
@@ -170,8 +170,8 @@
val reconstruct_proof: theory -> term -> proof -> proof
val prop_of': term list -> proof -> term
val prop_of: proof -> term
- val expand_name_empty: thm_header -> string option
- val expand_proof: theory -> (thm_header -> string option) -> proof -> proof
+ val expand_name_empty: thm_header -> Thm_Name.T option
+ val expand_proof: theory -> (thm_header -> Thm_Name.T option) -> proof -> proof
val standard_vars: Name.context -> term * proof option -> term * proof option
val standard_vars_term: Name.context -> term -> term
@@ -183,13 +183,13 @@
val export_proof_boxes_required: theory -> bool
val export_proof_boxes: proof_body list -> unit
val fulfill_norm_proof: theory -> (serial * proof_body) list -> proof_body -> proof_body
- val thm_proof: theory -> sorts_proof -> string * Position.T -> sort list -> term list ->
+ val thm_proof: theory -> sorts_proof -> Thm_Name.P -> sort list -> term list ->
term -> (serial * proof_body future) list -> proof_body -> proof_body
val unconstrain_thm_proof: theory -> sorts_proof -> sort list ->
term -> (serial * proof_body future) list -> proof_body -> term * proof_body
val get_identity: sort list -> term list -> term -> proof ->
- {serial: serial, theory_name: string, name: string} option
- val get_approximative_name: sort list -> term list -> term -> proof -> string
+ {serial: serial, theory_name: string, thm_name: Thm_Name.T} option
+ val get_approximative_name: sort list -> term list -> term -> proof -> Thm_Name.T
type thm_id = {serial: serial, theory_name: string}
val make_thm_id: serial * string -> thm_id
val thm_header_id: thm_header -> thm_id
@@ -206,7 +206,7 @@
(** datatype proof **)
type thm_header =
- {serial: serial, pos: Position.T list, theory_name: string, name: string,
+ {serial: serial, pos: Position.T list, theory_name: string, thm_name: Thm_Name.T,
prop: term, types: typ list option};
datatype proof =
@@ -230,7 +230,7 @@
and thm_body =
Thm_Body of {open_proof: proof -> proof, body: proof_body future}
and thm_node =
- Thm_Node of {theory_name: string, name: string, prop: term,
+ Thm_Node of {theory_name: string, thm_name: Thm_Name.T, prop: term,
body: proof_body future, export: unit lazy, consolidate: unit lazy};
type oracle = (string * Position.T) * term option;
@@ -253,8 +253,9 @@
fun no_proof (PBody {oracles, thms, zboxes, zproof, ...}) =
PBody {oracles = oracles, thms = thms, zboxes = zboxes, zproof = zproof, proof = MinProof};
-fun thm_header serial pos theory_name name prop types : thm_header =
- {serial = serial, pos = pos, theory_name = theory_name, name = name, prop = prop, types = types};
+fun thm_header serial pos theory_name thm_name prop types : thm_header =
+ {serial = serial, pos = pos, theory_name = theory_name, thm_name = thm_name,
+ prop = prop, types = types};
fun thm_body body = Thm_Body {open_proof = I, body = Future.value body};
fun thm_body_proof_raw (Thm_Body {body, ...}) = join_proof body;
@@ -262,7 +263,7 @@
fun rep_thm_node (Thm_Node args) = args;
val thm_node_theory_name = #theory_name o rep_thm_node;
-val thm_node_name = #name o rep_thm_node;
+val thm_node_name = #thm_name o rep_thm_node;
val thm_node_prop = #prop o rep_thm_node;
val thm_node_body = #body o rep_thm_node;
val thm_node_thms = thm_node_body #> Future.join #> (fn PBody {thms, ...} => thms);
@@ -276,21 +277,21 @@
maps (fn PBody {thms, ...} => map (thm_node_consolidate o #2) thms)
#> Lazy.consolidate #> map Lazy.force #> ignore;
-fun make_thm_node theory_name name prop body export =
+fun make_thm_node theory_name thm_name prop body export =
let
val consolidate =
Lazy.lazy_name "Proofterm.make_thm_node" (fn () =>
let val PBody {thms, ...} = Future.join body
in consolidate_bodies (join_thms thms) end);
in
- Thm_Node {theory_name = theory_name, name = name, prop = prop, body = body,
+ Thm_Node {theory_name = theory_name, thm_name = thm_name, prop = prop, body = body,
export = export, consolidate = consolidate}
end;
val no_export = Lazy.value ();
-fun make_thm ({serial, theory_name, name, prop, ...}: thm_header) (Thm_Body {body, ...}) =
- (serial, make_thm_node theory_name name prop body no_export);
+fun make_thm ({serial, theory_name, thm_name, prop, ...}: thm_header) (Thm_Body {body, ...}) =
+ (serial, make_thm_node theory_name thm_name prop body no_export);
(* proof atoms *)
@@ -317,11 +318,11 @@
if Intset.member seen i then (x, seen)
else
let
- val name = thm_node_name thm_node;
+ val thm_name = thm_node_name thm_node;
val prop = thm_node_prop thm_node;
val body = Future.join (thm_node_body thm_node);
val (x', seen') = app body (x, Intset.insert i seen);
- in (f {serial = i, name = name, prop = prop, body = body} x', seen') end);
+ in (f {serial = i, thm_name = thm_name, prop = prop, body = body} x', seen') end);
in fn bodies => fn x => #1 (fold app bodies (x, Intset.empty)) end;
@@ -341,8 +342,8 @@
| no_thm_names (AbsP (x, t, prf)) = AbsP (x, t, no_thm_names prf)
| no_thm_names (prf % t) = no_thm_names prf % t
| no_thm_names (prf1 %% prf2) = no_thm_names prf1 %% no_thm_names prf2
- | no_thm_names (PThm ({serial, pos, theory_name, name = _, prop, types}, thm_body)) =
- PThm (thm_header serial pos theory_name "" prop types, thm_body)
+ | no_thm_names (PThm ({serial, pos, theory_name, thm_name = _, prop, types}, thm_body)) =
+ PThm (thm_header serial pos theory_name Thm_Name.empty prop types, thm_body)
| no_thm_names a = a;
fun no_thm_proofs (Abst (x, T, prf)) = Abst (x, T, no_thm_proofs prf)
@@ -385,8 +386,8 @@
fn PAxm (a, b, c) => ([a], pair (term consts) (option (list typ)) (b, c)),
fn PClass (a, b) => ([b], typ a),
fn Oracle (a, b, c) => ([a], pair (term consts) (option (list typ)) (b, c)),
- fn PThm ({serial, pos, theory_name, name, prop, types}, Thm_Body {open_proof, body, ...}) =>
- ([int_atom serial, theory_name, name],
+ fn PThm ({serial, pos, theory_name, thm_name, prop, types}, Thm_Body {open_proof, body, ...}) =>
+ ([int_atom serial, theory_name, #1 thm_name, int_atom (#2 thm_name)],
pair (list properties) (pair (term consts) (pair (option (list typ)) (proof_body consts)))
(map Position.properties_of pos,
(prop, (types, map_proof_of open_proof (Future.join body)))))]
@@ -394,7 +395,7 @@
triple (list (pair (pair string (properties o Position.properties_of))
(option (term consts)))) (list (thm consts)) (proof consts) (oracles, thms, prf)
and thm consts (a, thm_node) =
- pair int (pair string (pair string (pair (term consts) (proof_body consts))))
+ pair int (pair string (pair Thm_Name.encode (pair (term consts) (proof_body consts))))
(a, (thm_node_theory_name thm_node, (thm_node_name thm_node, (thm_node_prop thm_node,
(Future.join (thm_node_body thm_node))))));
@@ -417,8 +418,8 @@
fn PAxm (name, _, SOME Ts) => ([name], list typ Ts),
fn PClass (T, c) => ([c], typ T),
fn Oracle (name, prop, SOME Ts) => ([name], pair (standard_term consts) (list typ) (prop, Ts)),
- fn PThm ({serial, theory_name, name, types = SOME Ts, ...}, _) =>
- ([int_atom serial, theory_name, name], list typ Ts)];
+ fn PThm ({serial, theory_name, thm_name, types = SOME Ts, ...}, _) =>
+ ([int_atom serial, theory_name, #1 thm_name, int_atom (#2 thm_name)], list typ Ts)];
in
@@ -447,12 +448,12 @@
fn ([a], b) => let val (c, d) = pair (term consts) (option (list typ)) b in PAxm (a, c, d) end,
fn ([b], a) => PClass (typ a, b),
fn ([a], b) => let val (c, d) = pair (term consts) (option (list typ)) b in Oracle (a, c, d) end,
- fn ([a, b, c], d) =>
+ fn ([a, b, c, d], e) =>
let
- val ((e, (f, (g, h)))) =
- pair (list properties) (pair (term consts) (pair (option (list typ)) (proof_body consts))) d;
- val header = thm_header (int_atom a) (map Position.of_properties e) b c f g;
- in PThm (header, thm_body h) end]
+ val ((x, (y, (z, w)))) =
+ pair (list properties) (pair (term consts) (pair (option (list typ)) (proof_body consts))) e;
+ val header = thm_header (int_atom a) (map Position.of_properties x) b (c, int_atom d) y z;
+ in PThm (header, thm_body w) end]
and proof_body consts x =
let
val (a, b, c) =
@@ -462,7 +463,7 @@
and thm consts x =
let
val (a, (b, (c, (d, e)))) =
- pair int (pair string (pair string (pair (term consts) (proof_body consts)))) x
+ pair int (pair string (pair Thm_Name.decode (pair (term consts) (proof_body consts)))) x
in (a, make_thm_node b c d (Future.value e) no_export) end;
in
@@ -556,8 +557,8 @@
| proof (PAxm (a, prop, SOME Ts)) = PAxm (a, prop, SOME (typs Ts))
| proof (PClass C) = ofclass C
| proof (Oracle (a, prop, SOME Ts)) = Oracle (a, prop, SOME (typs Ts))
- | proof (PThm ({serial, pos, theory_name, name, prop, types = SOME Ts}, thm_body)) =
- PThm (thm_header serial pos theory_name name prop (SOME (typs Ts)), thm_body)
+ | proof (PThm ({serial, pos, theory_name, thm_name, prop, types = SOME Ts}, thm_body)) =
+ PThm (thm_header serial pos theory_name thm_name prop (SOME (typs Ts)), thm_body)
| proof _ = raise Same.SAME;
in proof end;
@@ -597,8 +598,8 @@
fun change_types types (PAxm (name, prop, _)) = PAxm (name, prop, types)
| change_types (SOME [T]) (PClass (_, c)) = PClass (T, c)
| change_types types (Oracle (name, prop, _)) = Oracle (name, prop, types)
- | change_types types (PThm ({serial, pos, theory_name, name, prop, types = _}, thm_body)) =
- PThm (thm_header serial pos theory_name name prop types, thm_body)
+ | change_types types (PThm ({serial, pos, theory_name, thm_name, prop, types = _}, thm_body)) =
+ PThm (thm_header serial pos theory_name thm_name prop types, thm_body)
| change_types _ prf = prf;
@@ -762,8 +763,8 @@
PClass (norm_type_same T, c)
| norm (Oracle (a, prop, Ts)) =
Oracle (a, prop, Same.map_option norm_types_same Ts)
- | norm (PThm ({serial = i, pos = p, theory_name, name = a, prop = t, types = Ts}, thm_body)) =
- PThm (thm_header i p theory_name a t
+ | norm (PThm ({serial = i, pos = p, theory_name, thm_name, prop = t, types = Ts}, thm_body)) =
+ PThm (thm_header i p theory_name thm_name t
(Same.map_option norm_types_same Ts), thm_body)
| norm _ = raise Same.SAME;
in Same.commit norm end;
@@ -1023,8 +1024,8 @@
| proof _ _ (PAxm (a, prop, Ts)) = PAxm (a, prop, typs Ts)
| proof _ _ (PClass (T, c)) = PClass (typ T, c)
| proof _ _ (Oracle (a, prop, Ts)) = Oracle (a, prop, typs Ts)
- | proof _ _ (PThm ({serial, pos, theory_name, name, prop, types}, thm_body)) =
- PThm (thm_header serial pos theory_name name prop (typs types), thm_body)
+ | proof _ _ (PThm ({serial, pos, theory_name, thm_name, prop, types}, thm_body)) =
+ PThm (thm_header serial pos theory_name thm_name prop (typs types), thm_body)
| proof _ _ _ = raise Same.SAME;
val k = length prems;
@@ -1399,8 +1400,8 @@
if c1 = c2 then matchT inst (T1, T2)
else raise PMatch
| mtch Ts i j inst
- (PThm ({name = name1, prop = prop1, types = types1, ...}, _),
- PThm ({name = name2, prop = prop2, types = types2, ...}, _)) =
+ (PThm ({thm_name = name1, prop = prop1, types = types1, ...}, _),
+ PThm ({thm_name = name2, prop = prop2, types = types2, ...}, _)) =
if name1 = name2 andalso prop1 = prop2
then optmatch matchTs inst (types1, types2)
else raise PMatch
@@ -1446,8 +1447,8 @@
| subst _ _ (PAxm (id, prop, Ts)) = PAxm (id, prop, Same.map_option substTs Ts)
| subst _ _ (PClass (T, c)) = PClass (substT T, c)
| subst _ _ (Oracle (id, prop, Ts)) = Oracle (id, prop, Same.map_option substTs Ts)
- | subst _ _ (PThm ({serial = i, pos = p, theory_name, name = id, prop, types}, thm_body)) =
- PThm (thm_header i p theory_name id prop (Same.map_option substTs types), thm_body)
+ | subst _ _ (PThm ({serial = i, pos = p, theory_name, thm_name, prop, types}, thm_body)) =
+ PThm (thm_header i p theory_name thm_name prop (Same.map_option substTs types), thm_body)
| subst _ _ _ = raise Same.SAME;
in fn t => subst 0 0 t handle Same.SAME => t end;
@@ -1466,7 +1467,7 @@
| (Hyp (Var _), _) => true
| (PAxm (a, _, _), PAxm (b, _, _)) => a = b andalso matchrands prf1 prf2
| (PClass (_, c), PClass (_, d)) => c = d andalso matchrands prf1 prf2
- | (PThm ({name = a, prop = propa, ...}, _), PThm ({name = b, prop = propb, ...}, _)) =>
+ | (PThm ({thm_name = a, prop = propa, ...}, _), PThm ({thm_name = b, prop = propb, ...}, _)) =>
a = b andalso propa = propb andalso matchrands prf1 prf2
| (PBound i, PBound j) => i = j andalso matchrands prf1 prf2
| (AbsP _, _) => true (*because of possible eta equality*)
@@ -1616,12 +1617,12 @@
(fn TVar ((a, i), S) => subst_same (TVar ((a, i - shift), S)) | A => subst_same A);
in Same.commit (map_proof_types_same subst_type_same) prf end;
-fun guess_name (PThm ({name, ...}, _)) = name
+fun guess_name (PThm ({thm_name, ...}, _)) = thm_name
| guess_name (prf %% Hyp _) = guess_name prf
| guess_name (prf %% PClass _) = guess_name prf
| guess_name (prf % NONE) = guess_name prf
| guess_name (prf % SOME (Var _)) = guess_name prf
- | guess_name _ = "";
+ | guess_name _ = Thm_Name.empty;
(* generate constraints for proof term *)
@@ -1733,7 +1734,7 @@
| SOME Ts => (Ts, env));
val prop' = subst_atomic_types (prop_types ~~ Ts)
(forall_intr_variables_term prop) handle ListPair.UnequalLengths =>
- error ("Wrong number of type arguments for " ^ quote (guess_name prf))
+ error ("Wrong number of type arguments for " ^ quote (Thm_Name.print (guess_name prf)))
in (prop', change_types (SOME Ts) prf, [], env', vTs) end;
fun head_norm (prop, prf, cnstrts, env, vTs) =
@@ -1920,7 +1921,8 @@
(* expand and reconstruct subproofs *)
-fun expand_name_empty (header: thm_header) = if #name header = "" then SOME "" else NONE;
+fun expand_name_empty (header: thm_header) =
+ if Thm_Name.is_empty (#thm_name header) then SOME Thm_Name.empty else NONE;
fun expand_proof thy expand_name prf =
let
@@ -1939,10 +1941,10 @@
let val (seen', maxidx', prf') = expand seen maxidx prf
in (seen', maxidx', prf' % t) end
| expand seen maxidx (prf as PThm (header, thm_body)) =
- let val {serial, pos, theory_name, name, prop, types} = header in
+ let val {serial, pos, theory_name, thm_name, prop, types} = header in
(case expand_name header of
- SOME name' =>
- if name' = "" andalso is_some types then
+ SOME thm_name' =>
+ if #1 thm_name' = "" andalso is_some types then
let
val (seen', maxidx', prf') =
(case Inttab.lookup seen serial of
@@ -1959,8 +1961,9 @@
val prf'' = prf'
|> incr_indexes (maxidx + 1) |> app_types (maxidx + 1) prop (the types);
in (seen', maxidx' + maxidx + 1, prf'') end
- else if name' <> name then
- (seen, maxidx, PThm (thm_header serial pos theory_name name' prop types, thm_body))
+ else if thm_name' <> thm_name then
+ (seen, maxidx,
+ PThm (thm_header serial pos theory_name thm_name' prop types, thm_body))
else (seen, maxidx, prf)
| NONE => (seen, maxidx, prf))
end
@@ -2146,11 +2149,8 @@
local
-fun export_proof thy i prop prf0 =
+fun export_proof thy i prop prf =
let
- val prf = prf0
- |> reconstruct_proof thy prop
- |> apply_preproc thy;
val (prop', SOME prf') = (prop, SOME prf) |> standard_vars Name.context;
val args = [] |> add_standard_vars_term prop' |> add_standard_vars prf' |> rev;
val typargs = [] |> Term.add_tfrees prop' |> fold_proof_terms Term.add_tfrees prf' |> rev;
@@ -2164,8 +2164,8 @@
val encode_proof = encode_standard_proof consts;
in pair (list (pair string sort)) (pair encode_vars (pair encode_term encode_proof)) end;
in
- Export.export_params
- {theory = thy,
+ Export.export_params (Context.Theory thy)
+ {theory_name = Context.theory_long_name thy,
binding = Path.binding0 (Path.make ["proofs", string_of_int i]),
executable = false,
compress = true,
@@ -2176,7 +2176,7 @@
(name, pos) shyps hyps concl promises
(PBody {oracles = oracles0, thms = thms0, zboxes = zboxes0, zproof = zproof0, proof = proof0}) =
let
- val named = name <> "";
+ val named = not (Thm_Name.is_empty name);
val prop = Logic.list_implies (hyps, concl);
val args = prop_args prop;
@@ -2206,18 +2206,23 @@
if export_enabled () then new_prf ()
else
(case strip_combt (proof_head_of proof0) of
- (PThm ({serial = ser, name = a, prop = prop', types = NONE, ...}, thm_body'), args') =>
- if (a = "" orelse a = name) andalso prop' = prop1 andalso args' = args then
+ (PThm ({serial = ser, thm_name = a, prop = prop', types = NONE, ...}, thm_body'), args') =>
+ if (#1 a = "" orelse a = name) andalso prop' = prop1 andalso args' = args then
let
val Thm_Body {body = body', ...} = thm_body';
- val i = if a = "" andalso named then serial () else ser;
+ val i = if #1 a = "" andalso named then serial () else ser;
in (i, body' |> ser <> i ? Future.map (map_proof_of (rew_proof thy))) end
else new_prf ()
| _ => new_prf ());
val exp_proof = Future.map proof_of body';
val open_proof = not named ? rew_proof thy;
- fun export_body () = Future.join exp_proof |> open_proof |> export_proof thy i prop1;
+ fun export_body () =
+ Future.join exp_proof
+ |> open_proof
+ |> reconstruct_proof thy prop1
+ |> apply_preproc thy
+ |> export_proof thy i prop1;
val export =
if export_enabled () then
@@ -2255,7 +2260,7 @@
prepare_thm_proof false thy sorts_proof name shyps hyps concl promises #> #2;
fun unconstrain_thm_proof thy sorts_proof shyps concl promises body =
- prepare_thm_proof true thy sorts_proof ("", Position.none)
+ prepare_thm_proof true thy sorts_proof Thm_Name.none
shyps [] concl promises body;
end;
@@ -2266,14 +2271,14 @@
fun get_identity shyps hyps prop prf =
let val (_, prop) = Logic.unconstrainT shyps (Logic.list_implies (hyps, prop)) in
(case term_head_of (proof_head_of prf) of
- PThm ({serial, theory_name, name, prop = prop', ...}, _) =>
+ PThm ({serial, theory_name, thm_name, prop = prop', ...}, _) =>
if prop = prop'
- then SOME {serial = serial, theory_name = theory_name, name = name} else NONE
+ then SOME {serial = serial, theory_name = theory_name, thm_name = thm_name} else NONE
| _ => NONE)
end;
fun get_approximative_name shyps hyps prop prf =
- Option.map #name (get_identity shyps hyps prop prf) |> the_default "";
+ Option.map #thm_name (get_identity shyps hyps prop prf) |> the_default Thm_Name.empty;
(* thm_id *)
@@ -2292,8 +2297,8 @@
fun get_id shyps hyps prop prf : thm_id option =
(case get_identity shyps hyps prop prf of
NONE => NONE
- | SOME {name = "", ...} => NONE
- | SOME {serial, theory_name, ...} => SOME (make_thm_id (serial, theory_name)));
+ | SOME {serial, theory_name, thm_name, ...} =>
+ if Thm_Name.is_empty thm_name then NONE else SOME (make_thm_id (serial, theory_name)));
fun this_id NONE _ = false
| this_id (SOME (thm_id: thm_id)) (thm_id': thm_id) = #serial thm_id = #serial thm_id';
--- a/src/Pure/raw_simplifier.ML Sat Jun 08 14:57:14 2024 +0200
+++ b/src/Pure/raw_simplifier.ML Sun Jun 09 22:40:13 2024 +0200
@@ -27,7 +27,7 @@
val empty_ss: simpset
val merge_ss: simpset * simpset -> simpset
val dest_ss: simpset ->
- {simps: (string * thm) list,
+ {simps: (Thm_Name.T * thm) list,
procs: (string * term list) list,
congs: (cong_name * thm) list,
weak_congs: cong_name list,
@@ -133,7 +133,7 @@
type rrule =
{thm: thm, (*the rewrite rule*)
- name: string, (*name of theorem from which rewrite rule was extracted*)
+ name: Thm_Name.T, (*name of theorem from which rewrite rule was extracted*)
lhs: term, (*the left-hand side*)
elhs: cterm, (*the eta-contracted lhs*)
extra: bool, (*extra variables outside of elhs*)
@@ -443,8 +443,15 @@
fun print_term ctxt s t =
s ^ "\n" ^ Syntax.string_of_term ctxt t;
-fun print_thm ctxt s (name, th) =
- print_term ctxt (if name = "" then s else s ^ " " ^ quote name ^ ":") (Thm.full_prop_of th);
+fun print_thm ctxt msg (name, th) =
+ let
+ val thy = Proof_Context.theory_of ctxt;
+ val sffx =
+ if Thm_Name.is_empty name then ""
+ else " " ^ quote (Global_Theory.print_thm_name thy name) ^ ":";
+ in print_term ctxt (msg ^ sffx) (Thm.full_prop_of th) end;
+
+fun print_thm0 ctxt msg th = print_thm ctxt msg (Thm_Name.empty, th);
@@ -466,8 +473,7 @@
(Net.delete_term eq_rrule (Thm.term_of elhs, rrule) rules, prems, depth))
handle Net.DELETE =>
(if not loud then ()
- else cond_warning ctxt
- (fn () => print_thm ctxt "Rewrite rule not in simpset:" ("", thm));
+ else cond_warning ctxt (fn () => print_thm0 ctxt "Rewrite rule not in simpset:" thm);
ctxt);
fun insert_rrule (rrule as {thm, name, ...}) ctxt =
@@ -478,8 +484,7 @@
val rules' = Net.insert_term eq_rrule (Thm.term_of elhs, trim_context_rrule rrule2) rules;
in (rules', prems, depth) end)
handle Net.INSERT =>
- (cond_warning ctxt (fn () => print_thm ctxt "Ignoring duplicate rewrite rule:" ("", thm));
- ctxt));
+ (cond_warning ctxt (fn () => print_thm0 ctxt "Ignoring duplicate rewrite rule:" thm); ctxt));
val vars_set = Vars.build o Vars.add_vars;
@@ -603,7 +608,7 @@
false)
handle Net.INSERT =>
(cond_warning ctxt
- (fn () => print_thm ctxt "Symmetric rewrite rule already in simpset:" ("", thm));
+ (fn () => print_thm0 ctxt "Symmetric rewrite rule already in simpset:" thm);
true);
fun sym_present ctxt thms =
@@ -631,7 +636,7 @@
(*
with check for presence of symmetric version:
if sym_present ctxt [thm]
- then (cond_warning ctxt (fn () => print_thm ctxt "Ignoring rewrite rule:" ("", thm)); ctxt)
+ then (cond_warning ctxt (fn () => print_thm0 ctxt "Ignoring rewrite rule:" thm); ctxt)
else ctxt addsimps [thm];
*)
fun del_simp thm ctxt = ctxt delsimps [thm];
@@ -910,16 +915,14 @@
Thm.transitive thm (Drule.beta_eta_conversion (Thm.rhs_of thm))
in Thm.transitive nthm nthm' end
end
- val _ =
- if msg then cond_tracing ctxt (fn () => print_thm ctxt "SUCCEEDED" ("", thm'))
- else ();
+ val _ = if msg then cond_tracing ctxt (fn () => print_thm0 ctxt "SUCCEEDED" thm') else ();
in SOME thm'' end
handle THM _ =>
let
val _ $ _ $ prop0 = Thm.prop_of thm;
val _ =
cond_tracing ctxt (fn () =>
- print_thm ctxt "Proved wrong theorem (bad subgoaler?)" ("", thm') ^ "\n" ^
+ print_thm0 ctxt "Proved wrong theorem (bad subgoaler?)" thm' ^ "\n" ^
print_term ctxt "Should have proved:" prop0);
in NONE end;
@@ -932,8 +935,8 @@
val thm' = Thm.close_derivation \<^here> thm;
in
if rewrite_rule_extra_vars prems lhs rhs
- then (cond_warning ctxt (fn () => print_thm ctxt "Extra vars on rhs:" ("", thm)); [])
- else [mk_rrule2 {thm = thm', name = "", lhs = lhs, elhs = elhs, perm = false}]
+ then (cond_warning ctxt (fn () => print_thm0 ctxt "Extra vars on rhs:" thm); [])
+ else [mk_rrule2 {thm = thm', name = Thm_Name.empty, lhs = lhs, elhs = elhs, perm = false}]
end;
@@ -1007,27 +1010,27 @@
then
(cond_tracing ctxt (fn () =>
print_thm ctxt "Cannot apply permutative rewrite rule" (name, thm) ^ "\n" ^
- print_thm ctxt "Term does not become smaller:" ("", thm'));
+ print_thm0 ctxt "Term does not become smaller:" thm');
NONE)
else
(cond_tracing ctxt (fn () =>
print_thm ctxt "Applying instance of rewrite rule" (name, thm));
if unconditional
then
- (cond_tracing ctxt (fn () => print_thm ctxt "Rewriting:" ("", thm'));
+ (cond_tracing ctxt (fn () => print_thm0 ctxt "Rewriting:" thm');
trace_rrule trace_args ctxt (fn ctxt' =>
let
val lr = Logic.dest_equals prop;
val SOME thm'' = check_conv ctxt' false eta_thm thm';
in SOME (thm'', uncond_skel (congs, lr)) end))
else
- (cond_tracing ctxt (fn () => print_thm ctxt "Trying to rewrite:" ("", thm'));
+ (cond_tracing ctxt (fn () => print_thm0 ctxt "Trying to rewrite:" thm');
if simp_depth ctxt > Config.get ctxt simp_depth_limit
then (cond_tracing ctxt (fn () => "simp_depth_limit exceeded - giving up"); NONE)
else
trace_rrule trace_args ctxt (fn ctxt' =>
(case prover ctxt' thm' of
- NONE => (cond_tracing ctxt' (fn () => print_thm ctxt' "FAILED" ("", thm')); NONE)
+ NONE => (cond_tracing ctxt' (fn () => print_thm0 ctxt' "FAILED" thm'); NONE)
| SOME thm2 =>
(case check_conv ctxt' true eta_thm thm2 of
NONE => NONE
@@ -1069,8 +1072,7 @@
NONE => (cond_tracing' ctxt simp_debug (fn () => "FAILED"); proc_rews ps)
| SOME raw_thm =>
(cond_tracing ctxt (fn () =>
- print_thm ctxt ("Procedure " ^ quote name ^ " produced rewrite rule:")
- ("", raw_thm));
+ print_thm0 ctxt ("Procedure " ^ quote name ^ " produced rewrite rule:") raw_thm);
(case rews (mk_procrule ctxt raw_thm) of
NONE =>
(cond_tracing ctxt (fn () =>
@@ -1101,9 +1103,8 @@
is handled when congc is called *)
val thm' =
Thm.instantiate insts (Thm.rename_boundvars (Thm.term_of rlhs) (Thm.term_of t) rthm);
- val _ =
- cond_tracing ctxt (fn () => print_thm ctxt "Applying congruence rule:" ("", thm'));
- fun err (msg, thm) = (cond_tracing ctxt (fn () => print_thm ctxt msg ("", thm)); NONE);
+ val _ = cond_tracing ctxt (fn () => print_thm0 ctxt "Applying congruence rule:" thm');
+ fun err (msg, thm) = (cond_tracing ctxt (fn () => print_thm0 ctxt msg thm); NONE);
in
(case prover thm' of
NONE => err ("Congruence proof failed. Could not prove", thm')
--- a/src/Pure/term.scala Sat Jun 08 14:57:14 2024 +0200
+++ b/src/Pure/term.scala Sun Jun 09 22:40:13 2024 +0200
@@ -142,8 +142,8 @@
private lazy val hash: Int = ("Oracle", name, prop, types).hashCode()
override def hashCode(): Int = hash
}
- case class PThm(serial: Long, theory_name: String, name: String, types: List[Typ]) extends Proof {
- private lazy val hash: Int = ("PThm", serial, theory_name, name, types).hashCode()
+ case class PThm(serial: Long, theory_name: String, thm_name: Thm_Name, types: List[Typ]) extends Proof {
+ private lazy val hash: Int = ("PThm", serial, theory_name, thm_name, types).hashCode()
override def hashCode(): Int = hash
}
@@ -234,6 +234,10 @@
}
}
+ protected def cache_thm_name(x: Thm_Name): Thm_Name =
+ if (x == Thm_Name.empty) Thm_Name.empty
+ else lookup(x) getOrElse store(Thm_Name(cache_string(x.name), x.index))
+
protected def cache_proof(x: Proof): Proof = {
if (x == MinProof) MinProof
else {
@@ -253,8 +257,9 @@
case PClass(typ, cls) => store(PClass(cache_typ(typ), cache_string(cls)))
case Oracle(name, prop, types) =>
store(Oracle(cache_string(name), cache_term(prop), cache_typs(types)))
- case PThm(serial, theory_name, name, types) =>
- store(PThm(serial, cache_string(theory_name), cache_string(name), cache_typs(types)))
+ case PThm(serial, theory_name, thm_name, types) =>
+ store(PThm(serial, cache_string(theory_name), cache_thm_name(thm_name),
+ cache_typs(types)))
}
}
}
@@ -269,6 +274,8 @@
if (no_cache) x else synchronized { cache_typ(x) }
def term(x: Term): Term =
if (no_cache) x else synchronized { cache_term(x) }
+ def thm_name(x: Thm_Name): Thm_Name =
+ if (no_cache) x else synchronized { cache_thm_name(x) }
def proof(x: Proof): Proof =
if (no_cache) x else synchronized { cache_proof(x) }
--- a/src/Pure/term_xml.scala Sat Jun 08 14:57:14 2024 +0200
+++ b/src/Pure/term_xml.scala Sun Jun 09 22:40:13 2024 +0200
@@ -92,7 +92,9 @@
{ case (List(a), b) => PAxm(a, list(typ)(b)) },
{ case (List(a), b) => PClass(typ(b), a) },
{ case (List(a), b) => val (c, d) = pair(term, list(typ))(b); Oracle(a, c, d) },
- { case (List(a, b, c), d) => PThm(long_atom(a), b, c, list(typ)(d)) }))
+ { case (List(a, b, c, d), e) =>
+ PThm(long_atom(a), b, Thm_Name(c, int_atom(d)), list(typ)(e))
+ }))
proof
}
--- a/src/Pure/thm.ML Sat Jun 08 14:57:14 2024 +0200
+++ b/src/Pure/thm.ML Sun Jun 09 22:40:13 2024 +0200
@@ -118,11 +118,11 @@
val extra_shyps: thm -> sort list
val strip_shyps: thm -> thm
val derivation_closed: thm -> bool
- val derivation_name: thm -> string
+ val derivation_name: thm -> Thm_Name.T
val derivation_id: thm -> Proofterm.thm_id option
- val raw_derivation_name: thm -> string
- val expand_name: thm -> Proofterm.thm_header -> string option
- val name_derivation: string * Position.T -> thm -> thm
+ val raw_derivation_name: thm -> Thm_Name.T
+ val expand_name: thm -> Proofterm.thm_header -> Thm_Name.T option
+ val name_derivation: Thm_Name.P -> thm -> thm
val close_derivation: Position.T -> thm -> thm
val trim_context: thm -> thm
val axiom: theory -> string -> thm
@@ -176,8 +176,8 @@
val plain_prop_of: thm -> term
val get_zproof_serials: theory -> serial list
val get_zproof: theory -> serial ->
- {name: Thm_Name.T * Position.T, thm: thm, zboxes: ZTerm.zboxes, zproof: zproof} option
- val store_zproof: Thm_Name.T * Position.T -> thm -> theory -> thm * theory
+ {name: Thm_Name.P, thm: thm, zboxes: ZTerm.zboxes, zproof: zproof} option
+ val store_zproof: Thm_Name.P -> thm -> theory -> thm * theory
val dest_state: thm * int -> (term * term) list * term list * term * term
val lift_rule: cterm -> thm -> thm
val incr_indexes: int -> thm -> thm
@@ -951,7 +951,7 @@
structure Data = Theory_Data
(
type T =
- {name: Thm_Name.T * Position.T, thm: thm} Inttab.table * (*stored zproof thms*)
+ {name: Thm_Name.P, thm: thm} Inttab.table * (*stored zproof thms*)
unit Name_Space.table * (*oracles: authentic derivation names*)
classes; (*type classes within the logic*)
@@ -1130,7 +1130,9 @@
(case Proofterm.get_identity shyps hyps prop (Proofterm.proof_of body) of
NONE => K false
| SOME {serial, ...} => fn (header: Proofterm.thm_header) => serial = #serial header);
- fun expand header = if self_id header orelse #name header = "" then SOME "" else NONE;
+ fun expand header =
+ if self_id header orelse Thm_Name.is_empty (#thm_name header)
+ then SOME Thm_Name.empty else NONE;
in expand end;
(*deterministic name of finished proof*)
@@ -1166,7 +1168,7 @@
fun close_derivation pos =
solve_constraints #> (fn thm =>
if not (null (tpairs_of thm)) orelse derivation_closed thm then thm
- else name_derivation ("", pos) thm);
+ else name_derivation (Thm_Name.empty, pos) thm);
val trim_context = solve_constraints #> trim_context_thm;
--- a/src/Pure/thm_deps.ML Sat Jun 08 14:57:14 2024 +0200
+++ b/src/Pure/thm_deps.ML Sun Jun 09 22:40:13 2024 +0200
@@ -12,7 +12,7 @@
val pretty_thm_oracles: Proof.context -> thm list -> Pretty.T
val thm_deps: theory -> thm list -> (Proofterm.thm_id * Thm_Name.T) list
val pretty_thm_deps: theory -> thm list -> Pretty.T
- val unused_thms_cmd: theory list * theory list -> (string * thm) list
+ val unused_thms_cmd: theory list * theory list -> (Thm_Name.T * thm) list
end;
structure Thm_Deps: THM_DEPS =
@@ -73,17 +73,17 @@
fun pretty_thm_deps thy thms =
let
- val ctxt = Proof_Context.init_global thy;
+ val facts = Global_Theory.facts_of thy;
+ val extern_fact = Name_Space.extern_generic (Context.Theory thy) (Facts.space_of facts);
val deps =
(case try (thm_deps thy) thms of
SOME deps => deps
| NONE => error "Malformed proofs");
val items =
- map #2 deps
- |> map (fn (name, i) => (Proof_Context.markup_extern_fact ctxt name, i))
- |> sort_by (#2 o #1)
- |> map (fn ((marks, xname), i) =>
- Pretty.item [Pretty.marks_str (marks, Thm_Name.print (xname, i))]);
+ deps
+ |> map (fn (_, thm_name as (name, _)) => (extern_fact name, thm_name))
+ |> sort_by #1
+ |> map (fn (_, thm_name) => Pretty.item [Global_Theory.pretty_thm_name thy thm_name])
in Pretty.big_list ("dependencies: " ^ string_of_int (length items)) items end;
@@ -96,9 +96,8 @@
else
let val {concealed, group, ...} = Name_Space.the_entry space name in
fold_rev (transfer #> (fn th =>
- (case Thm.derivation_name th of
- "" => I
- | a => cons (a, (th, concealed, group))))) ths
+ let val a = Thm.derivation_name th
+ in if Thm_Name.is_empty a then I else cons (a, (th, concealed, group)) end)) ths
end;
fun add_facts thy =
let
@@ -108,15 +107,15 @@
val new_thms =
fold add_facts thys []
- |> sort_distinct (string_ord o apply2 #1);
+ |> sort_distinct (Thm_Name.ord o apply2 #1);
val used =
Proofterm.fold_body_thms
- (fn {name = a, ...} => a <> "" ? Symset.insert a)
+ (fn {thm_name = a, ...} => not (Thm_Name.is_empty a) ? Thm_Name.Set.insert a)
(map Proofterm.strip_thm_body (Thm.proof_bodies_of (map (#1 o #2) new_thms)))
- Symset.empty;
+ Thm_Name.Set.empty;
- fun is_unused a = not (Symset.member used a);
+ fun is_unused a = not (Thm_Name.Set.member used a);
(*groups containing at least one used theorem*)
val used_groups =
--- a/src/Pure/thm_name.ML Sat Jun 08 14:57:14 2024 +0200
+++ b/src/Pure/thm_name.ML Sun Jun 09 22:40:13 2024 +0200
@@ -11,29 +11,105 @@
sig
type T = string * int
val ord: T ord
+ structure Set: SET
+ structure Table: TABLE
+ val empty: T
+ val is_empty: T -> bool
+
+ type P = T * Position.T
+ val none: P
+ val list: string * Position.T -> 'a list -> (P * 'a) list
+ val expr: string * Position.T -> ('a list * 'b) list -> ((P * 'a) list * 'b) list
+
+ val parse: string -> T
+ val print_prefix: Context.generic -> Name_Space.T -> T -> Markup.T * string
+ val print_suffix: T -> string
val print: T -> string
- val short: T * Position.T -> string * Position.T
- val list: string * Position.T -> 'a list -> ((T * Position.T) * 'a) list
- val expr: string * Position.T -> ('a list * 'b) list -> (((T * Position.T) * 'a) list * 'b) list
+ val short: T -> string
+ val encode: T XML.Encode.T
+ val decode: T XML.Decode.T
end;
structure Thm_Name: THM_NAME =
struct
+(* type T *)
+
type T = string * int;
val ord = prod_ord string_ord int_ord;
-fun print (name, index) =
- if name = "" orelse index = 0 then name
- else name ^ enclose "(" ")" (string_of_int index);
+structure Set = Set(type key = T val ord = ord);
+structure Table = Table(Set.Key);
+
+val empty: T = ("", 0);
+fun is_empty ((a, _): T) = a = "";
+
-fun short ((name, index), pos: Position.T) =
- if name = "" orelse index = 0 then (name, pos)
- else (name ^ "_" ^ string_of_int index, pos);
+(* type P *)
+
+type P = T * Position.T;
-fun list (name, pos: Position.T) [thm] = [(((name, 0): T, pos), thm)]
- | list (name, pos) thms = map_index (fn (i, thm) => (((name, i + 1), pos), thm)) thms;
+val none: P = (empty, Position.none);
+
+fun list (name, pos) [x] = [(((name, 0), pos): P, x)]
+ | list ("", pos) xs = map (fn thm => ((empty, pos), thm)) xs
+ | list (name, pos) xs = map_index (fn (i, thm) => (((name, i + 1), pos), thm)) xs;
fun expr name = burrow_fst (burrow (list name));
+
+(* parse *)
+
+local
+
+fun is_bg c = c = #"(";
+fun is_en c = c = #")";
+fun is_digit c = #"0" <= c andalso c <= #"9";
+fun get_digit c = Char.ord c - Char.ord #"0";
+
+in
+
+fun parse string =
+ let
+ val n = size string;
+ fun char i = if 0 <= i andalso i < n then String.nth string i else #"\000";
+ fun test pred i = pred (char i);
+
+ fun scan i k m =
+ let val c = char i in
+ if is_digit c then scan (i - 1) (k * 10) (m + k * get_digit c)
+ else if is_bg c then (String.substring (string, 0, i), m)
+ else (string, 0)
+ end;
+ in
+ if test is_en (n - 1) andalso test is_digit (n - 2)
+ then scan (n - 2) 1 0
+ else (string, 0)
+ end;
+
end;
+
+
+(* print *)
+
+fun print_prefix context space ((name, _): T) =
+ if name = "" then (Markup.empty, "")
+ else (Name_Space.markup space name, Name_Space.extern_generic context space name);
+
+fun print_suffix (name, index) =
+ if name = "" orelse index = 0 then ""
+ else enclose "(" ")" (string_of_int index);
+
+fun print (name, index) = name ^ print_suffix (name, index);
+
+fun short (name, index) =
+ if name = "" orelse index = 0 then name
+ else name ^ "_" ^ string_of_int index;
+
+
+(* XML data representation *)
+
+val encode = let open XML.Encode in pair string int end;
+val decode = let open XML.Decode in pair string int end;
+
+end;
--- a/src/Pure/thm_name.scala Sat Jun 08 14:57:14 2024 +0200
+++ b/src/Pure/thm_name.scala Sun Jun 09 22:40:13 2024 +0200
@@ -23,14 +23,32 @@
private val Thm_Name_Regex = """^(.)+\((\d+)\)$""".r
+ val empty: Thm_Name = Thm_Name("", 0)
+
def parse(s: String): Thm_Name =
s match {
case Thm_Name_Regex(name, Value.Nat(index)) => Thm_Name(name, index)
case _ => Thm_Name(s, 0)
}
+
+
+ /* XML data representation */
+
+ def encode: XML.Encode.T[Thm_Name] = { (thm_name: Thm_Name) =>
+ import XML.Encode._
+ pair(string, int)((thm_name.name, thm_name.index))
+ }
+
+ def decode: XML.Decode.T[Thm_Name] = { (body: XML.Body) =>
+ import XML.Decode._
+ val (name, index) = pair(string, int)(body)
+ Thm_Name(name, index)
+ }
}
sealed case class Thm_Name(name: String, index: Int) {
+ def is_empty: Boolean = name.isEmpty
+
def print: String =
if (name == "" || index == 0) name
else name + "(" + index + ")"
--- a/src/Pure/zterm.ML Sat Jun 08 14:57:14 2024 +0200
+++ b/src/Pure/zterm.ML Sun Jun 09 22:40:13 2024 +0200
@@ -24,7 +24,7 @@
| ZConst of string * ztyp list (*polymorphic constant: >= 2 type arguments*)
| ZAbs of string * ztyp * zterm
| ZApp of zterm * zterm
- | ZClass of ztyp * class (*OFCLASS proposition*)
+ | OFCLASS of ztyp * class
structure ZTerm =
struct
@@ -48,7 +48,7 @@
| fold_types f (ZConst (_, As)) = fold f As
| fold_types f (ZAbs (_, T, b)) = f T #> fold_types f b
| fold_types f (ZApp (t, u)) = fold_types f t #> fold_types f u
- | fold_types f (ZClass (T, _)) = f T
+ | fold_types f (OFCLASS (T, _)) = f T
| fold_types _ _ = I;
@@ -98,7 +98,7 @@
| cons_nr (ZConst _) = 4
| cons_nr (ZAbs _) = 5
| cons_nr (ZApp _) = 6
- | cons_nr (ZClass _) = 7;
+ | cons_nr (OFCLASS _) = 7;
fun struct_ord tu =
if pointer_eq tu then EQUAL
@@ -121,7 +121,7 @@
| (ZConst (a, _), ZConst (b, _)) => fast_string_ord (a, b)
| (ZVar (xi, _), ZVar (yj, _)) => Term_Ord.fast_indexname_ord (xi, yj)
| (ZBound i, ZBound j) => int_ord (i, j)
- | (ZClass (_, a), ZClass (_, b)) => fast_string_ord (a, b)
+ | (OFCLASS (_, a), OFCLASS (_, b)) => fast_string_ord (a, b)
| _ => EQUAL);
fun types_ord tu =
@@ -135,7 +135,7 @@
| (ZConst1 (_, T), ZConst1 (_, U)) => ztyp_ord (T, U)
| (ZConst (_, Ts), ZConst (_, Us)) => dict_ord ztyp_ord (Ts, Us)
| (ZVar (_, T), ZVar (_, U)) => ztyp_ord (T, U)
- | (ZClass (T, _), ZClass (U, _)) => ztyp_ord (T, U)
+ | (OFCLASS (T, _), OFCLASS (U, _)) => ztyp_ord (T, U)
| _ => EQUAL);
in
@@ -195,8 +195,7 @@
datatype zproof_name =
ZAxiom of string
| ZOracle of string
- | ZBox of {theory_name: string, serial: serial}
- | ZThm of {theory_name: string, thm_name: Thm_Name.T * Position.T, serial: serial};
+ | ZThm of {theory_name: string, thm_name: Thm_Name.P, serial: serial};
type zproof_const = (zproof_name * zterm) * (ztyp ZTVars.table * zterm ZVars.table);
@@ -209,7 +208,7 @@
| ZAppt of zproof * zterm
| ZAppp of zproof * zproof
| ZHyp of zterm
- | ZClassp of ztyp * class; (*OFCLASS proof from sorts algebra*)
+ | OFCLASSp of ztyp * class; (*OFCLASS proof from sorts algebra*)
@@ -275,7 +274,7 @@
val unions_zboxes: zboxes list -> zboxes
val add_box_proof: {unconstrain: bool} -> theory ->
term list -> term -> zproof -> zboxes -> zproof * zboxes
- val thm_proof: theory -> Thm_Name.T * Position.T -> term list -> term -> zproof -> zbox * zproof
+ val thm_proof: theory -> Thm_Name.P -> term list -> term -> zproof -> zbox * zproof
val axiom_proof: theory -> string -> term -> zproof
val oracle_proof: theory -> string -> term -> zproof
val assume_proof: theory -> term -> zproof
@@ -466,7 +465,7 @@
| term (ZApp (t, u)) =
(ZApp (term t, Same.commit term u)
handle Same.SAME => ZApp (t, term u))
- | term (ZClass (T, c)) = ZClass (typ T, c);
+ | term (OFCLASS (T, c)) = OFCLASS (typ T, c);
in term end;
fun instantiate_type_same instT =
@@ -490,7 +489,7 @@
| proof (ZAppt (p, t)) = proof p #> term t
| proof (ZAppp (p, q)) = proof p #> proof q
| proof (ZHyp h) = hyps ? term h
- | proof (ZClassp (T, _)) = hyps ? typ T;
+ | proof (OFCLASSp (T, _)) = hyps ? typ T;
in proof end;
fun fold_proof_types hyps typ =
@@ -556,7 +555,7 @@
(ZAppp (proof p, Same.commit proof q)
handle Same.SAME => ZAppp (p, proof q))
| proof (ZHyp h) = if hyps then ZHyp (term h) else raise Same.SAME
- | proof (ZClassp (T, c)) = if hyps then ZClassp (typ T, c) else raise Same.SAME;
+ | proof (OFCLASSp (T, c)) = if hyps then OFCLASSp (typ T, c) else raise Same.SAME;
in proof end;
fun map_proof hyps typ term = Same.commit (map_proof_same hyps typ term);
@@ -567,7 +566,7 @@
fun map_class_proof class =
let
- fun proof (ZClassp C) = class C
+ fun proof (OFCLASSp C) = class C
| proof (ZAbst (a, T, p)) = ZAbst (a, T, proof p)
| proof (ZAbsp (a, t, p)) = ZAbsp (a, t, proof p)
| proof (ZAppt (p, t)) = ZAppt (proof p, t)
@@ -605,11 +604,10 @@
| [T] => ZConst1 (c, ztyp T)
| Ts => ZConst (c, map ztyp Ts))
| zterm (Abs (a, T, b)) = ZAbs (a, ztyp T, zterm b)
- | zterm ((t as Const (c, _)) $ (u as Const ("Pure.type", _))) =
- if String.isSuffix Logic.class_suffix c then
- ZClass (ztyp (Logic.dest_type u), Logic.class_of_const c)
- else ZApp (zterm t, zterm u)
- | zterm (t $ u) = ZApp (zterm t, zterm u);
+ | zterm (tm as t $ u) =
+ (case try Logic.match_of_class tm of
+ SOME (T, c) => OFCLASS (ztyp T, c)
+ | NONE => ZApp (zterm t, zterm u));
in {ztyp = ztyp, zterm = zterm} end;
val zterm_of = #zterm o zterm_cache;
@@ -640,7 +638,7 @@
| term (ZConst (c, Ts)) = const (c, map typ_of Ts)
| term (ZAbs (a, T, b)) = Abs (a, typ_of T, term b)
| term (ZApp (t, u)) = term t $ term u
- | term (ZClass (T, c)) = Logic.mk_of_class (typ_of T, c);
+ | term (OFCLASS (T, c)) = Logic.mk_of_class (typ_of T, c);
in term end;
@@ -844,8 +842,8 @@
(case get_bound lev t of
SOME p => p
| NONE => raise ZTERM ("Loose bound in proof term", [], [t], [prf]))
- | proof lev (ZClassp C) =
- (case get_bound lev (ZClass C) of
+ | proof lev (OFCLASSp C) =
+ (case get_bound lev (OFCLASS C) of
SOME p => p
| NONE => raise Same.SAME)
| proof lev (ZAbst (x, T, p)) = ZAbst (x, T, proof lev p)
@@ -857,7 +855,7 @@
| proof _ _ = raise Same.SAME;
in ZAbsps prems (Same.commit (proof 0) prf) end;
-fun box_proof {unconstrain} zproof_name thy hyps concl prf =
+fun box_proof {unconstrain} thy thm_name hyps concl prf =
let
val {zterm, ...} = zterm_cache thy;
@@ -898,26 +896,23 @@
val i = serial ();
val zbox: zbox = (i, (prop', prf'));
- val const = constrain_proof (ZConstp (zproof_const (zproof_name i, prop')));
+ val proof_name =
+ ZThm {theory_name = Context.theory_long_name thy, thm_name = thm_name, serial = i};
+
+ val const = constrain_proof (ZConstp (zproof_const (proof_name, prop')));
val args1 =
outer_constraints |> map (fn (T, c) =>
- ZClassp (ztyp_of (if unconstrain then unconstrain_typ T else T), c));
+ OFCLASSp (ztyp_of (if unconstrain then unconstrain_typ T else T), c));
val args2 = if unconstrain then map ZHyp hyps' else map (ZHyp o zterm) hyps;
in (zbox, ZAppps (ZAppps (const, args1), args2)) end;
in
-fun thm_proof thy thm_name =
- let
- val thy_name = Context.theory_long_name thy;
- fun zproof_name i = ZThm {theory_name = thy_name, thm_name = thm_name, serial = i};
- in box_proof {unconstrain = false} zproof_name thy end;
+val thm_proof = box_proof {unconstrain = false};
fun add_box_proof unconstrain thy hyps concl prf zboxes =
let
- val thy_name = Context.theory_long_name thy;
- fun zproof_name i = ZBox {theory_name = thy_name, serial = i};
- val (zbox, prf') = box_proof unconstrain zproof_name thy hyps concl prf;
+ val (zbox, prf') = box_proof unconstrain thy Thm_Name.none hyps concl prf;
val zboxes' = add_zboxes zbox zboxes;
in (prf', zboxes') end;
@@ -984,7 +979,7 @@
fun forall_elim_proof thy t p = ZAppt (p, zterm_of thy t);
-fun of_class_proof (T, c) = ZClassp (ztyp_of T, c);
+fun of_class_proof (T, c) = OFCLASSp (ztyp_of T, c);
(* equality *)
@@ -1196,7 +1191,7 @@
| incr lev (ZApp (t, u)) =
(ZApp (incr lev t, Same.commit (incr lev) u)
handle Same.SAME => ZApp (t, incr lev u))
- | incr _ (ZClass (T, c)) = ZClass (typ T, c);
+ | incr _ (OFCLASS (T, c)) = OFCLASS (typ T, c);
in incr lev end;
fun proof Ts lev (ZAbst (a, T, p)) =
@@ -1213,7 +1208,7 @@
handle Same.SAME => ZAppp (p, proof Ts lev q))
| proof Ts lev (ZConstp (a, insts)) =
ZConstp (a, map_insts_same typ (term Ts lev) insts)
- | proof _ _ (ZClassp (T, c)) = ZClassp (typ T, c)
+ | proof _ _ (OFCLASSp (T, c)) = OFCLASSp (typ T, c)
| proof _ _ _ = raise Same.SAME;
val k = length prems;