# HG changeset patch # User wenzelm # Date 1717965613 -7200 # Node ID 594356f1681084df2a44db34dd61172f839eeffc # Parent 8678986d9af564ab1117549b1f431f8fc51b8d31# Parent a828e47c867c669a97ca5ee4d6929d111dc714a6 merged diff -r 8678986d9af5 -r 594356f16810 src/Doc/Implementation/Logic.thy --- 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"} \\ diff -r 8678986d9af5 -r 594356f16810 src/HOL/Mutabelle/mutabelle_extra.ML --- 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>\Pure.type\] -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" diff -r 8678986d9af5 -r 594356f16810 src/HOL/Nitpick_Examples/Mono_Nits.thy --- 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 diff -r 8678986d9af5 -r 594356f16810 src/HOL/Proofs/ex/Proof_Terms.thy --- 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] []; \ text \ diff -r 8678986d9af5 -r 594356f16810 src/HOL/TPTP/atp_problem_import.ML --- 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>\thms\, []), 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 diff -r 8678986d9af5 -r 594356f16810 src/HOL/TPTP/atp_theory_export.ML --- 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>\False\ |> #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 _ _ _ _ [] = () diff -r 8678986d9af5 -r 594356f16810 src/HOL/TPTP/mash_export.ML --- 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 diff -r 8678986d9af5 -r 594356f16810 src/HOL/Tools/ATP/atp_util.ML --- 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 diff -r 8678986d9af5 -r 594356f16810 src/HOL/Tools/Ctr_Sugar/ctr_sugar_util.ML --- 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); diff -r 8678986d9af5 -r 594356f16810 src/HOL/Tools/Meson/meson.ML --- 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?*) diff -r 8678986d9af5 -r 594356f16810 src/HOL/Tools/Metis/metis_tactic.ML --- 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 diff -r 8678986d9af5 -r 594356f16810 src/HOL/Tools/Mirabelle/mirabelle.ML --- 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; diff -r 8678986d9af5 -r 594356f16810 src/HOL/Tools/Mirabelle/mirabelle_metis.ML --- 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 diff -r 8678986d9af5 -r 594356f16810 src/HOL/Tools/Quickcheck/find_unused_assms.ML --- 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 diff -r 8678986d9af5 -r 594356f16810 src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML --- 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 diff -r 8678986d9af5 -r 594356f16810 src/HOL/Tools/Sledgehammer/sledgehammer_isar_proof.ML --- 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) = diff -r 8678986d9af5 -r 594356f16810 src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML --- 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 => diff -r 8678986d9af5 -r 594356f16810 src/HOL/Tools/Sledgehammer/sledgehammer_util.ML --- 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) diff -r 8678986d9af5 -r 594356f16810 src/HOL/Tools/datatype_realizer.ML --- 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); diff -r 8678986d9af5 -r 594356f16810 src/HOL/Tools/inductive_realizer.ML --- 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) => diff -r 8678986d9af5 -r 594356f16810 src/HOL/Tools/rewrite_hol_proof.ML --- 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; diff -r 8678986d9af5 -r 594356f16810 src/HOL/ex/Sketch_and_Explore.thy --- 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>\sketch\ diff -r 8678986d9af5 -r 594356f16810 src/Pure/Build/export.ML --- 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)); diff -r 8678986d9af5 -r 594356f16810 src/Pure/Build/export.scala --- 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 = { diff -r 8678986d9af5 -r 594356f16810 src/Pure/Build/export_theory.ML --- 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) = diff -r 8678986d9af5 -r 594356f16810 src/Pure/Build/export_theory.scala --- 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) }) diff -r 8678986d9af5 -r 594356f16810 src/Pure/Concurrent/consumer_thread.scala --- 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) } diff -r 8678986d9af5 -r 594356f16810 src/Pure/General/name_space.ML --- 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 = diff -r 8678986d9af5 -r 594356f16810 src/Pure/Isar/element.ML --- 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 = diff -r 8678986d9af5 -r 594356f16810 src/Pure/Isar/generic_target.ML --- 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 diff -r 8678986d9af5 -r 594356f16810 src/Pure/Isar/locale.ML --- 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)); diff -r 8678986d9af5 -r 594356f16810 src/Pure/Isar/proof_context.ML --- 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); diff -r 8678986d9af5 -r 594356f16810 src/Pure/PIDE/protocol_handlers.scala --- 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 diff -r 8678986d9af5 -r 594356f16810 src/Pure/PIDE/session.scala --- 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)) } } } diff -r 8678986d9af5 -r 594356f16810 src/Pure/Proof/extraction.ML --- 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] diff -r 8678986d9af5 -r 594356f16810 src/Pure/Proof/proof_checker.ML --- 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 diff -r 8678986d9af5 -r 594356f16810 src/Pure/Proof/proof_rewrite_rules.ML --- 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; diff -r 8678986d9af5 -r 594356f16810 src/Pure/Proof/proof_syntax.ML --- 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); diff -r 8678986d9af5 -r 594356f16810 src/Pure/Pure.thy --- 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 diff -r 8678986d9af5 -r 594356f16810 src/Pure/System/classpath.scala --- 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)) } } } diff -r 8678986d9af5 -r 594356f16810 src/Pure/Thy/thy_header.ML --- 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 **) diff -r 8678986d9af5 -r 594356f16810 src/Pure/Tools/generated_files.ML --- 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 diff -r 8678986d9af5 -r 594356f16810 src/Pure/Tools/simplifier_trace.ML --- 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)] diff -r 8678986d9af5 -r 594356f16810 src/Pure/facts.ML --- 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 *) diff -r 8678986d9af5 -r 594356f16810 src/Pure/global_theory.ML --- 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 => diff -r 8678986d9af5 -r 594356f16810 src/Pure/logic.ML --- 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]); diff -r 8678986d9af5 -r 594356f16810 src/Pure/more_thm.ML --- 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 *) diff -r 8678986d9af5 -r 594356f16810 src/Pure/proofterm.ML --- 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'; diff -r 8678986d9af5 -r 594356f16810 src/Pure/raw_simplifier.ML --- 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') diff -r 8678986d9af5 -r 594356f16810 src/Pure/term.scala --- 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) } diff -r 8678986d9af5 -r 594356f16810 src/Pure/term_xml.scala --- 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 } diff -r 8678986d9af5 -r 594356f16810 src/Pure/thm.ML --- 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; diff -r 8678986d9af5 -r 594356f16810 src/Pure/thm_deps.ML --- 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 = diff -r 8678986d9af5 -r 594356f16810 src/Pure/thm_name.ML --- 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; diff -r 8678986d9af5 -r 594356f16810 src/Pure/thm_name.scala --- 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 + ")" diff -r 8678986d9af5 -r 594356f16810 src/Pure/zterm.ML --- 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;