# HG changeset patch # User wenzelm # Date 1733134964 -3600 # Node ID c32ebdcbe8ca72131a48349a14f8188d34bbd3f7 # Parent fb49af893986484bb521a61efa4e1023b9d8646a proper context for extern operation: observe local options; more uniform global_ctxt for pretty printing; diff -r fb49af893986 -r c32ebdcbe8ca src/Pure/Proof/extraction.ML --- a/src/Pure/Proof/extraction.ML Mon Dec 02 11:08:36 2024 +0100 +++ b/src/Pure/Proof/extraction.ML Mon Dec 02 11:22:44 2024 +0100 @@ -505,6 +505,8 @@ fun extract thm_vss thy = let val thy' = add_syntax thy; + val global_ctxt = Syntax.init_pretty_global thy'; + val print_thm_name = Global_Theory.print_thm_name global_ctxt; val {realizes_eqns, typeof_eqns, types, realizers, defs, expand, prep} = ExtractionData.get thy; @@ -640,8 +642,7 @@ let val _ = T = nullT orelse error "corr: internal error"; val _ = - msg d ("Building correctness proof for " ^ - quote (Global_Theory.print_thm_name thy thm_name) ^ + msg d ("Building correctness proof for " ^ quote (print_thm_name thm_name) ^ (if null vs' then "" else " (relevant variables: " ^ commas_quote vs' ^ ")")); val prf' = prep (Proofterm.reconstruct_proof thy' prop prf); @@ -670,8 +671,8 @@ | 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 (Global_Theory.print_thm_name thy' thm_name) ^ ":\n" ^ - Syntax.string_of_term_global thy' + quote (print_thm_name thm_name) ^ ":\n" ^ + Syntax.string_of_term global_ctxt (Envir.beta_norm (Proofterm.prop_of (Proofterm.proof_combt (prf0, ts))))))) end @@ -686,7 +687,7 @@ SOME (_, prf) => (Proofterm.proof_combP (prf_subst_TVars tye' prf, mk_sprfs cs tye), defs) | NONE => error ("corr: no realizer for instance of axiom " ^ - quote s ^ ":\n" ^ Syntax.string_of_term_global thy' (Envir.beta_norm + quote s ^ ":\n" ^ Syntax.string_of_term global_ctxt (Envir.beta_norm (Proofterm.prop_of (Proofterm.proof_combt (prf0, ts))))) end @@ -738,7 +739,7 @@ NONE => let val _ = - msg d ("Extracting " ^ quote (Global_Theory.print_thm_name thy' thm_name) ^ + msg d ("Extracting " ^ quote (print_thm_name thm_name) ^ (if null vs' then "" else " (relevant variables: " ^ commas_quote vs' ^ ")")); val prf' = prep (Proofterm.reconstruct_proof thy' prop prf); @@ -790,8 +791,8 @@ | SOME rs => (case find vs' rs of SOME (t, _) => (subst_TVars tye' t, defs) | NONE => error ("extr: no realizer for instance of theorem " ^ - quote (Global_Theory.print_thm_name thy' thm_name) ^ ":\n" ^ - Syntax.string_of_term_global thy' (Envir.beta_norm + quote (print_thm_name thm_name) ^ ":\n" ^ + Syntax.string_of_term global_ctxt (Envir.beta_norm (Proofterm.prop_of (Proofterm.proof_combt (prf0, ts)))))) end @@ -803,7 +804,7 @@ 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 + quote s ^ ":\n" ^ Syntax.string_of_term global_ctxt (Envir.beta_norm (Proofterm.prop_of (Proofterm.proof_combt (prf0, ts))))) end @@ -817,7 +818,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 (Global_Theory.print_thm_name thy' name) ^ " has no computational content") + quote (print_thm_name name) ^ " has no computational content") in Proofterm.reconstruct_proof thy' prop prf end; val defs = diff -r fb49af893986 -r c32ebdcbe8ca src/Pure/Proof/proof_checker.ML --- a/src/Pure/Proof/proof_checker.ML Mon Dec 02 11:08:36 2024 +0100 +++ b/src/Pure/Proof/proof_checker.ML Mon Dec 02 11:22:44 2024 +0100 @@ -72,7 +72,10 @@ end; fun thm_of_proof thy = - let val lookup = lookup_thm thy in + let + val global_ctxt = Syntax.init_pretty_global thy; + val lookup = lookup_thm thy; + in fn prf => let val prf_names = @@ -96,9 +99,9 @@ if is_equal prop prop' then () else error ("Duplicate use of theorem name " ^ - quote (Global_Theory.print_thm_name thy thm_name) ^ Position.here thm_pos - ^ "\n" ^ Syntax.string_of_term_global thy prop - ^ "\n\n" ^ Syntax.string_of_term_global thy prop'); + quote (Global_Theory.print_thm_name global_ctxt thm_name) ^ Position.here thm_pos + ^ "\n" ^ Syntax.string_of_term global_ctxt prop + ^ "\n\n" ^ Syntax.string_of_term global_ctxt prop'); in thm_of_atom thm Ts end | thm_of _ _ (PAxm (name, _, SOME Ts)) = diff -r fb49af893986 -r c32ebdcbe8ca src/Pure/Pure.thy --- a/src/Pure/Pure.thy Mon Dec 02 11:08:36 2024 +0100 +++ b/src/Pure/Pure.thy Mon Dec 02 11:22:44 2024 +0100 @@ -1378,10 +1378,8 @@ "print theorem dependencies (immediate non-transitive)" (Parse.thms1 >> (fn args => Toplevel.keep (fn st => - let - val thy = Toplevel.theory_of st; - val ctxt = Toplevel.context_of st; - in Pretty.writeln (Thm_Deps.pretty_thm_deps thy (Attrib.eval_thms ctxt args)) end))); + let val ctxt = Toplevel.context_of st + in Pretty.writeln (Thm_Deps.pretty_thm_deps ctxt (Attrib.eval_thms ctxt args)) end))); val _ = Outer_Syntax.command \<^command_keyword>\thm_oracles\ diff -r fb49af893986 -r c32ebdcbe8ca src/Pure/global_theory.ML --- a/src/Pure/global_theory.ML Mon Dec 02 11:08:36 2024 +0100 +++ b/src/Pure/global_theory.ML Mon Dec 02 11:22:44 2024 +0100 @@ -14,8 +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.P * thm) list - val pretty_thm_name: theory -> Thm_Name.T -> Pretty.T - val print_thm_name: theory -> Thm_Name.T -> string + val pretty_thm_name: Proof.context -> Thm_Name.T -> Pretty.T + val print_thm_name: Proof.context -> Thm_Name.T -> string val get_thm_names: theory -> Thm_Name.P Inttab.table val dest_thm_names: theory -> (Proofterm.thm_id * Thm_Name.P) list val lookup_thm_id: theory -> Proofterm.thm_id -> Thm_Name.P option @@ -88,7 +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); -fun pretty_thm_name thy = Facts.pretty_thm_name (Context.Theory thy) (facts_of thy); +fun pretty_thm_name ctxt = + Facts.pretty_thm_name (Context.Proof ctxt) (facts_of (Proof_Context.theory_of ctxt)); + val print_thm_name = Pretty.string_of oo pretty_thm_name; @@ -108,9 +110,11 @@ else (case Inttab.lookup thm_names serial of SOME (thm_name', thm_pos') => - raise THM ("Duplicate use of derivation identity for " ^ - print_thm_name thy thm_name ^ Position.here thm_pos ^ " vs. " ^ - print_thm_name thy thm_name' ^ Position.here thm_pos', 0, [thm]) + let val thy_ctxt = Proof_Context.init_global thy in + raise THM ("Duplicate use of derivation identity for " ^ + print_thm_name thy_ctxt thm_name ^ Position.here thm_pos ^ " vs. " ^ + print_thm_name thy_ctxt thm_name' ^ Position.here thm_pos', 0, [thm]) + end | NONE => Inttab.update (serial, (thm_name, thm_pos)) thm_names))); fun lazy_thm_names thy = diff -r fb49af893986 -r c32ebdcbe8ca src/Pure/raw_simplifier.ML --- a/src/Pure/raw_simplifier.ML Mon Dec 02 11:08:36 2024 +0100 +++ b/src/Pure/raw_simplifier.ML Mon Dec 02 11:22:44 2024 +0100 @@ -481,10 +481,9 @@ 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) ^ ":"; + else " " ^ quote (Global_Theory.print_thm_name ctxt 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); diff -r fb49af893986 -r c32ebdcbe8ca src/Pure/thm_deps.ML --- a/src/Pure/thm_deps.ML Mon Dec 02 11:08:36 2024 +0100 +++ b/src/Pure/thm_deps.ML Mon Dec 02 11:22:44 2024 +0100 @@ -11,7 +11,7 @@ val has_skip_proof: thm list -> bool 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 pretty_thm_deps: Proof.context -> thm list -> Pretty.T val unused_thms_cmd: theory list * theory list -> (Thm_Name.T * thm) list end; @@ -71,10 +71,11 @@ |-> Inttab.fold_rev (fn (_, SOME entry) => cons entry | _ => I) end; -fun pretty_thm_deps thy thms = +fun pretty_thm_deps ctxt thms = let + val thy = Proof_Context.theory_of ctxt; val facts = Global_Theory.facts_of thy; - val extern_fact = Name_Space.extern_global thy (Facts.space_of facts); + val extern_fact = Name_Space.extern ctxt (Facts.space_of facts); val deps = (case try (thm_deps thy) thms of SOME deps => deps @@ -83,7 +84,7 @@ 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]) + |> map (fn (_, thm_name) => Pretty.item [Global_Theory.pretty_thm_name ctxt thm_name]) in Pretty.big_list ("dependencies: " ^ string_of_int (length items)) items end;