# HG changeset patch # User wenzelm # Date 1717856807 -7200 # Node ID a397fd0c451ae2dc9d51920309eb4bddb953e2b4 # Parent f3bfec3b02f0b6d7b0e897ba210d34b442af252b more accurate output of Thm_Name.T wrt. facts name space; diff -r f3bfec3b02f0 -r a397fd0c451a src/Pure/Isar/proof_context.ML --- a/src/Pure/Isar/proof_context.ML Sat Jun 08 11:47:48 2024 +0200 +++ b/src/Pure/Isar/proof_context.ML Sat Jun 08 16:26:47 2024 +0200 @@ -62,6 +62,8 @@ 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 @@ -423,6 +425,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 *) diff -r f3bfec3b02f0 -r a397fd0c451a src/Pure/Proof/extraction.ML --- a/src/Pure/Proof/extraction.ML Sat Jun 08 11:47:48 2024 +0200 +++ b/src/Pure/Proof/extraction.ML Sat Jun 08 16:26:47 2024 +0200 @@ -641,7 +641,7 @@ val _ = T = nullT orelse error "corr: internal error"; val _ = msg d ("Building correctness proof for " ^ - quote (Thm_Name.short thm_name) ^ + 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); @@ -670,7 +670,7 @@ | 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 (Thm_Name.short thm_name) ^ ":\n" ^ + 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 @@ -738,7 +738,7 @@ NONE => let val _ = - msg d ("Extracting " ^ quote (Thm_Name.short thm_name) ^ + 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); @@ -790,7 +790,7 @@ | SOME rs => (case find vs' rs of SOME (t, _) => (subst_TVars tye' t, defs) | NONE => error ("extr: no realizer for instance of theorem " ^ - quote (Thm_Name.short thm_name) ^ ":\n" ^ + 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 @@ -817,7 +817,7 @@ val name = Thm.derivation_name thm; val _ = if Thm_Name.is_empty name then error "extraction: unnamed theorem" else (); val _ = etype_of thy' vs [] prop <> nullT orelse error ("theorem " ^ - quote (Thm_Name.short 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 = diff -r f3bfec3b02f0 -r a397fd0c451a src/Pure/Proof/proof_checker.ML --- a/src/Pure/Proof/proof_checker.ML Sat Jun 08 11:47:48 2024 +0200 +++ b/src/Pure/Proof/proof_checker.ML Sat Jun 08 16:26:47 2024 +0200 @@ -93,7 +93,8 @@ 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 f3bfec3b02f0 -r a397fd0c451a src/Pure/Pure.thy --- a/src/Pure/Pure.thy Sat Jun 08 11:47:48 2024 +0200 +++ b/src/Pure/Pure.thy Sat Jun 08 16:26:47 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 @@ -1386,7 +1388,7 @@ NONE => (Theory.parents_of thy, [thy]) | SOME (xs, NONE) => (map check xs, [thy]) | SOME (xs, SOME ys) => (map check xs, map check ys)) - |> map (apfst Thm_Name.short #> pretty_thm) |> Pretty.writeln_chunks + |> map pretty_thm |> Pretty.writeln_chunks end))); in end\ diff -r f3bfec3b02f0 -r a397fd0c451a src/Pure/facts.ML --- a/src/Pure/facts.ML Sat Jun 08 11:47:48 2024 +0200 +++ b/src/Pure/facts.ML Sat Jun 08 16:26:47 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 f3bfec3b02f0 -r a397fd0c451a src/Pure/global_theory.ML --- a/src/Pure/global_theory.ML Sat Jun 08 11:47:48 2024 +0200 +++ b/src/Pure/global_theory.ML Sat Jun 08 16:26:47 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 @@ -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 = diff -r f3bfec3b02f0 -r a397fd0c451a src/Pure/proofterm.ML --- a/src/Pure/proofterm.ML Sat Jun 08 11:47:48 2024 +0200 +++ b/src/Pure/proofterm.ML Sat Jun 08 16:26:47 2024 +0200 @@ -1734,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 (Thm_Name.short (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) = diff -r f3bfec3b02f0 -r a397fd0c451a src/Pure/thm_deps.ML --- a/src/Pure/thm_deps.ML Sat Jun 08 11:47:48 2024 +0200 +++ b/src/Pure/thm_deps.ML Sat Jun 08 16:26:47 2024 +0200 @@ -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; diff -r f3bfec3b02f0 -r a397fd0c451a src/Pure/thm_name.ML --- a/src/Pure/thm_name.ML Sat Jun 08 11:47:48 2024 +0200 +++ b/src/Pure/thm_name.ML Sat Jun 08 16:26:47 2024 +0200 @@ -21,6 +21,8 @@ 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 print_prefix: Context.generic -> Name_Space.T -> T -> Markup.T * string + val print_suffix: T -> string val print: T -> string val short: T -> string end; @@ -55,9 +57,15 @@ (* output *) -fun print (name, index) = - if name = "" orelse index = 0 then name - else name ^ enclose "(" ")" (string_of_int index); +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