# HG changeset patch # User wenzelm # Date 1572803735 -3600 # Node ID bb49abc2ecbb3afd254d3a2f805f63e56bbf6a40 # Parent 58022ee70b3576163b700e4cf10f77663355d6fa determine proof boxes from exported proof (NB: thm_boxes is not sufficient due to OfClass proofs); diff -r 58022ee70b35 -r bb49abc2ecbb src/Pure/Thy/export_theory.ML --- a/src/Pure/Thy/export_theory.ML Sun Nov 03 18:53:48 2019 +0100 +++ b/src/Pure/Thy/export_theory.ML Sun Nov 03 18:55:35 2019 +0100 @@ -249,16 +249,6 @@ val lookup_thm_id = Global_Theory.lookup_thm_id thy; - fun proof_boxes thm thm_id = - let - val selection = - {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]) - handle Proofterm.MIN_PROOF () => Thm_Deps.thm_boxes selection [thm] - in boxes @ [thm_id] end; - fun expand_name thm_id (header: Proofterm.thm_header) = if #serial header = #serial thm_id then "" else @@ -277,7 +267,6 @@ let val deps = map (Thm_Name.print o #2) (Thm_Deps.thm_deps thy [raw_thm]); val thm = clean_thm (Thm.unconstrainT raw_thm); - val boxes = proof_boxes thm thm_id; val proof0 = if Proofterm.export_standard_enabled () then @@ -290,12 +279,11 @@ if Proofterm.export_proof_boxes_required thy then Proofterm.export_proof_boxes [proof] else (); in - (prop, (deps, (boxes, proof))) |> + (prop, deps, proof) |> let open XML.Encode Term_XML.Encode; - fun encode_box {serial, theory_name} = pair int string (serial, theory_name); val encode_proof = Proofterm.encode_standard_proof consts; - in pair encode_prop (pair (list string) (pair (list encode_box) encode_proof)) end + in triple encode_prop (list string) encode_proof end end; fun export_thm (thm_id, thm_name) = diff -r 58022ee70b35 -r bb49abc2ecbb src/Pure/Thy/export_theory.scala --- a/src/Pure/Thy/export_theory.scala Sun Nov 03 18:53:48 2019 +0100 +++ b/src/Pure/Thy/export_theory.scala Sun Nov 03 18:55:35 2019 +0100 @@ -7,6 +7,9 @@ package isabelle +import scala.collection.immutable.SortedMap + + object Export_Theory { /** session content **/ @@ -352,16 +355,12 @@ sealed case class Thm_Id(serial: Long, theory_name: String) { def pure: Boolean = theory_name == Thy_Header.PURE - - def cache(cache: Term.Cache): Thm_Id = - Thm_Id(serial, cache.string(theory_name)) } sealed case class Thm( entity: Entity, prop: Prop, deps: List[String], - proof_boxes: List[Thm_Id], proof: Term.Proof) { def cache(cache: Term.Cache): Thm = @@ -369,7 +368,6 @@ entity.cache(cache), prop.cache(cache), deps.map(cache.string _), - proof_boxes.map(_.cache(cache)), cache.proof(proof)) } @@ -377,18 +375,13 @@ provider.uncompressed_yxml(export_prefix + "thms").map((tree: XML.Tree) => { val (entity, body) = decode_entity(Kind.THM, tree) - val (prop, (deps, (prf_boxes, prf))) = + val (prop, deps, prf) = { import XML.Decode._ import Term_XML.Decode._ - def thm_id(body: XML.Body): Thm_Id = - { - val (serial, theory_name) = pair(long, string)(body) - Thm_Id(serial, theory_name) - } - pair(decode_prop _, pair(list(string), pair(list(thm_id), proof)))(body) + triple(decode_prop, list(string), proof)(body) } - Thm(entity, prop, deps, prf_boxes, prf) + Thm(entity, prop, deps, prf) }) sealed case class Proof( @@ -428,6 +421,46 @@ } } + def read_proof_boxes( + store: Sessions.Store, + provider: Export.Provider, + proof: Term.Proof, + suppress: Thm_Id => Boolean = _ => false, + cache: Option[Term.Cache] = None): List[(Thm_Id, Proof)] = + { + var seen = Set.empty[Long] + var result = SortedMap.empty[Long, (Thm_Id, Proof)] + + def boxes(prf: Term.Proof) + { + prf match { + case Term.Abst(_, _, p) => boxes(p) + case Term.AbsP(_, _, p) => boxes(p) + case Term.Appt(p, _) => boxes(p) + case Term.AppP(p, q) => boxes(p); boxes(q) + case thm: Term.PThm if !seen(thm.serial) => + seen += thm.serial + val id = Thm_Id(thm.serial, thm.theory_name) + if (!suppress(id)) { + val read = + if (id.pure) Export_Theory.read_pure_proof(store, id, cache = cache) + else Export_Theory.read_proof(provider, id, cache = cache) + read match { + case Some(p) => + result += (thm.serial -> (id -> p)) + boxes(p.proof) + case None => + error("Missing proof " + thm.serial + " (theory " + quote (thm.theory_name) + ")") + } + } + case _ => + } + } + + boxes(proof) + result.iterator.map(_._2).toList + } + /* type classes */ diff -r 58022ee70b35 -r bb49abc2ecbb src/Pure/thm_deps.ML --- a/src/Pure/thm_deps.ML Sun Nov 03 18:53:48 2019 +0100 +++ b/src/Pure/thm_deps.ML Sun Nov 03 18:55:35 2019 +0100 @@ -12,8 +12,6 @@ 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 thm_boxes: {included: Proofterm.thm_id -> bool, excluded: Proofterm.thm_id -> bool} -> - thm list -> Proofterm.thm_id list val unused_thms_cmd: theory list * theory list -> (string * thm) list end; @@ -81,21 +79,6 @@ in Pretty.big_list ("dependencies: " ^ string_of_int (length items)) items end; -(* thm boxes: intermediate PThm nodes *) - -fun thm_boxes {included, excluded} thms = - let - fun boxes (i, thm_node) res = - let val thm_id = Proofterm.thm_id (i, thm_node) in - if Inttab.defined res i orelse (excluded thm_id andalso not (included thm_id)) - then res - else - Inttab.update (i, thm_id) res - |> fold boxes (Proofterm.thm_node_thms thm_node) - end; - in Inttab.fold_rev (cons o #2) (fold (fold boxes o Thm.thm_deps) thms Inttab.empty) [] end; - - (* unused_thms_cmd *) fun unused_thms_cmd (base_thys, thys) =