# HG changeset patch # User wenzelm # Date 1572617395 -3600 # Node ID 7abe5abb4c050da3a66f6cd80a56df6802a332e2 # Parent a1c137961c1273690e507af4d9e946a2191ecbb1 more detailed proof term output; tuned signature; diff -r a1c137961c12 -r 7abe5abb4c05 src/Pure/Proof/proof_syntax.ML --- a/src/Pure/Proof/proof_syntax.ML Fri Nov 01 14:30:22 2019 +0100 +++ b/src/Pure/Proof/proof_syntax.ML Fri Nov 01 15:09:55 2019 +0100 @@ -14,6 +14,7 @@ val proof_of: bool -> thm -> Proofterm.proof val pretty_proof: Proof.context -> Proofterm.proof -> Pretty.T val pretty_standard_proof_of: Proof.context -> bool -> thm -> Pretty.T + val pretty_proof_boxes_of: Proof.context -> bool -> thm -> Pretty.T end; structure Proof_Syntax : PROOF_SYNTAX = @@ -198,4 +199,28 @@ fun pretty_standard_proof_of ctxt full thm = pretty_proof ctxt (Thm.standard_proof_of {full = full, expand_name = Thm.expand_name thm} thm); +fun pretty_proof_boxes_of ctxt full thm = + let + val thy = Proof_Context.theory_of ctxt; + val selection = + {included = Proofterm.this_id (Thm.derivation_id thm), + excluded = is_some o Global_Theory.lookup_thm_id thy} + in + Proofterm.proof_boxes selection [Thm.proof_of thm] + |> map (fn ({serial = i, pos, prop, ...}, proof) => + let + val proof' = proof + |> full ? Proofterm.reconstruct_proof thy prop + |> Proofterm.forall_intr_variables prop; + val prop' = prop + |> Proofterm.forall_intr_variables_term; + val name = Long_Name.append "thm" (string_of_int i); + in + Pretty.item + [Pretty.str (name ^ Position.here_list pos ^ ":"), Pretty.brk 1, + Syntax.pretty_term ctxt prop', Pretty.fbrk, pretty_proof ctxt proof'] + end) + |> Pretty.chunks + end; + end; diff -r a1c137961c12 -r 7abe5abb4c05 src/Pure/Thy/export_theory.ML --- a/src/Pure/Thy/export_theory.ML Fri Nov 01 14:30:22 2019 +0100 +++ b/src/Pure/Thy/export_theory.ML Fri Nov 01 15:09:55 2019 +0100 @@ -257,7 +257,7 @@ fun proof_boxes thm thm_id = let val selection = - {included = fn thm_id' => #serial thm_id = #serial thm_id', + {included = Proofterm.this_id (SOME thm_id), excluded = is_some o lookup_thm_id}; val boxes = map (Proofterm.thm_header_id o #1) (Proofterm.proof_boxes selection [Thm.proof_of thm]) diff -r a1c137961c12 -r 7abe5abb4c05 src/Pure/proofterm.ML --- a/src/Pure/proofterm.ML Fri Nov 01 14:30:22 2019 +0100 +++ b/src/Pure/proofterm.ML Fri Nov 01 15:09:55 2019 +0100 @@ -191,6 +191,7 @@ val thm_header_id: thm_header -> thm_id val thm_id: thm -> thm_id val get_id: sort list -> term list -> term -> proof -> thm_id option + val this_id: thm_id option -> thm_id -> bool val proof_boxes: {excluded: thm_id -> bool, included: thm_id -> bool} -> proof list -> (thm_header * proof) list (*exception MIN_PROOF*) end @@ -853,8 +854,9 @@ let val U = Term.itselfT T --> propT in Const ("Pure.OfClass", U --> proofT) $ Const (Logic.const_of_class c, U) end; -fun term_of _ (PThm ({name, types = Ts, ...}, _)) = - fold AppT (these Ts) (Const (Long_Name.append "thm" name, proofT)) +fun term_of _ (PThm ({serial = i, name, types = Ts, ...}, _)) = + fold AppT (these Ts) + (Const (Long_Name.append "thm" (if name = "" then string_of_int i else name), proofT)) | term_of _ (PAxm (name, _, Ts)) = fold AppT (these Ts) (Const (Long_Name.append "axm" name, proofT)) | term_of _ (OfClass (T, c)) = AppT T (OfClasst (T, c)) @@ -2325,6 +2327,9 @@ | SOME {name = "", ...} => NONE | SOME {serial, theory_name, ...} => 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'; + (* proof boxes: intermediate PThm nodes *)