export facts with reconstructed proof term (if possible), but its PThm boxes need to be collected separately;
authorwenzelm
Thu Aug 15 16:06:57 2019 +0200 (2 months ago)
changeset 70534fb876ebbf5a7
parent 70533 031620901fcd
child 70535 de6062ac70b6
export facts with reconstructed proof term (if possible), but its PThm boxes need to be collected separately;
src/Pure/Thy/export_theory.ML
src/Pure/Thy/export_theory.scala
src/Pure/proofterm.ML
     1.1 --- a/src/Pure/Thy/export_theory.ML	Thu Aug 15 16:02:47 2019 +0200
     1.2 +++ b/src/Pure/Thy/export_theory.ML	Thu Aug 15 16:06:57 2019 +0200
     1.3 @@ -220,40 +220,43 @@
     1.4  
     1.5      (* axioms and facts *)
     1.6  
     1.7 -    fun prop_of raw_thm =
     1.8 +    fun standard_prop used extra_shyps raw_prop raw_proof =
     1.9        let
    1.10 -        val thm = raw_thm
    1.11 -          |> Thm.transfer thy
    1.12 -          |> Thm.check_hyps (Context.Theory thy)
    1.13 -          |> Thm.strip_shyps;
    1.14 -        val prop = thm
    1.15 -          |> Thm.full_prop_of;
    1.16 -      in (Thm.extra_shyps thm, prop) end;
    1.17 +        val raw_proofs = the_list raw_proof;
    1.18 +        val used_proofs = used |> fold Proofterm.used_frees_proof raw_proofs;
    1.19 +        val ([prop], proofs) = ([raw_prop], raw_proofs) |> Proofterm.standard_vars used_proofs;
    1.20  
    1.21 -    fun encode_prop used (Ss, raw_prop) =
    1.22 -      let
    1.23 -        val prop = Proofterm.standard_vars_term used raw_prop;
    1.24          val args = rev (add_frees used prop []);
    1.25          val typargs = rev (add_tfrees used prop []);
    1.26 -        val used' = fold (Name.declare o #1) typargs used;
    1.27 -        val sorts = Name.invent used' Name.aT (length Ss) ~~ Ss;
    1.28 -      in
    1.29 -        (sorts @ typargs, args, prop) |>
    1.30 -          let open XML.Encode Term_XML.Encode
    1.31 -          in triple (list (pair string sort)) (list (pair string typ)) term end
    1.32 -      end;
    1.33 +        val used_typargs = fold (Name.declare o #1) typargs used;
    1.34 +        val sorts = Name.invent used_typargs Name.aT (length extra_shyps) ~~ extra_shyps;
    1.35 +      in ((sorts @ typargs, args, prop), try hd proofs) end;
    1.36 +
    1.37 +    val encode_prop =
    1.38 +      let open XML.Encode Term_XML.Encode
    1.39 +      in triple (list (pair string sort)) (list (pair string typ)) term end;
    1.40 +
    1.41 +    fun encode_axiom used prop =
    1.42 +      encode_prop (#1 (standard_prop used [] prop NONE));
    1.43  
    1.44 -    fun encode_axiom used t = encode_prop used ([], t);
    1.45 +    val clean_thm =
    1.46 +      Thm.transfer thy
    1.47 +      #> Thm.check_hyps (Context.Theory thy)
    1.48 +      #> Thm.strip_shyps;
    1.49  
    1.50 -    val encode_fact = encode_prop Name.context;
    1.51 -    val encode_fact_single = encode_fact o prop_of;
    1.52 -    val encode_fact_multi = XML.Encode.list encode_fact o map prop_of;
    1.53 +    val encode_fact = clean_thm #> (fn thm =>
    1.54 +      standard_prop Name.context
    1.55 +        (Thm.extra_shyps thm)
    1.56 +        (Thm.full_prop_of thm)
    1.57 +        (try Thm.reconstruct_proof_of thm) |>
    1.58 +      let open XML.Encode Term_XML.Encode
    1.59 +      in pair encode_prop (option Proofterm.encode_full) end);
    1.60  
    1.61      val _ =
    1.62        export_entities "axioms" (fn _ => fn t => SOME (encode_axiom Name.context t))
    1.63          Theory.axiom_space (Theory.axioms_of thy);
    1.64      val _ =
    1.65 -      export_entities "facts" (K (SOME o encode_fact_multi))
    1.66 +      export_entities "facts" (K (SOME o XML.Encode.list encode_fact))
    1.67          (Facts.space_of o Global_Theory.facts_of)
    1.68          (Facts.dest_static true [] (Global_Theory.facts_of thy));
    1.69  
    1.70 @@ -262,12 +265,12 @@
    1.71  
    1.72      val encode_class =
    1.73        let open XML.Encode Term_XML.Encode
    1.74 -      in pair (list (pair string typ)) (list encode_fact_single) end;
    1.75 +      in pair (list (pair string typ)) (list (encode_axiom Name.context)) end;
    1.76  
    1.77      fun export_class name =
    1.78        (case try (Axclass.get_info thy) name of
    1.79          NONE => ([], [])
    1.80 -      | SOME {params, axioms, ...} => (params, axioms))
    1.81 +      | SOME {params, axioms, ...} => (params, map (Thm.plain_prop_of o clean_thm) axioms))
    1.82        |> encode_class |> SOME;
    1.83  
    1.84      val _ =
     2.1 --- a/src/Pure/Thy/export_theory.scala	Thu Aug 15 16:02:47 2019 +0200
     2.2 +++ b/src/Pure/Thy/export_theory.scala	Thu Aug 15 16:06:57 2019 +0200
     2.3 @@ -284,7 +284,7 @@
     2.4        })
     2.5  
     2.6  
     2.7 -  /* facts */
     2.8 +  /* axioms and facts */
     2.9  
    2.10    sealed case class Prop(
    2.11      typargs: List[(String, Term.Sort)],
    2.12 @@ -309,23 +309,45 @@
    2.13      Prop(typargs, args, t)
    2.14    }
    2.15  
    2.16 -  sealed case class Fact_Single(entity: Entity, prop: Prop)
    2.17 +
    2.18 +  sealed case class Fact(prop: Prop, proof: Option[Term.Proof])
    2.19 +  {
    2.20 +    def cache(cache: Term.Cache): Fact =
    2.21 +      Fact(prop.cache(cache), proof.map(cache.proof _))
    2.22 +  }
    2.23 +
    2.24 +  def decode_fact(body: XML.Body): Fact =
    2.25 +  {
    2.26 +    val (prop, proof) =
    2.27 +    {
    2.28 +      import XML.Decode._
    2.29 +      pair(decode_prop _, option(Term_XML.Decode.proof))(body)
    2.30 +    }
    2.31 +    Fact(prop, proof)
    2.32 +  }
    2.33 +
    2.34 +  sealed case class Fact_Single(entity: Entity, fact: Fact)
    2.35    {
    2.36      def cache(cache: Term.Cache): Fact_Single =
    2.37 -      Fact_Single(entity.cache(cache), prop.cache(cache))
    2.38 +      Fact_Single(entity.cache(cache), fact.cache(cache))
    2.39 +
    2.40 +    def prop: Prop = fact.prop
    2.41 +    def proof: Option[Term.Proof] = fact.proof
    2.42    }
    2.43  
    2.44 -  sealed case class Fact_Multi(entity: Entity, props: List[Prop])
    2.45 +  sealed case class Fact_Multi(entity: Entity, facts: List[Fact])
    2.46    {
    2.47      def cache(cache: Term.Cache): Fact_Multi =
    2.48 -      Fact_Multi(entity.cache(cache), props.map(_.cache(cache)))
    2.49 +      Fact_Multi(entity.cache(cache), facts.map(_.cache(cache)))
    2.50 +
    2.51 +    def props: List[Prop] = facts.map(_.prop)
    2.52  
    2.53      def split: List[Fact_Single] =
    2.54 -      props match {
    2.55 -        case List(prop) => List(Fact_Single(entity, prop))
    2.56 +      facts match {
    2.57 +        case List(fact) => List(Fact_Single(entity, fact))
    2.58          case _ =>
    2.59 -          for ((prop, i) <- props.zipWithIndex)
    2.60 -          yield Fact_Single(entity.copy(name = entity.name + "(" + (i + 1) + ")"), prop)
    2.61 +          for ((fact, i) <- facts.zipWithIndex)
    2.62 +          yield Fact_Single(entity.copy(name = entity.name + "(" + (i + 1) + ")"), fact)
    2.63        }
    2.64    }
    2.65  
    2.66 @@ -334,15 +356,15 @@
    2.67        {
    2.68          val (entity, body) = decode_entity(Kind.AXIOM, tree)
    2.69          val prop = decode_prop(body)
    2.70 -        Fact_Single(entity, prop)
    2.71 +        Fact_Single(entity, Fact(prop, None))
    2.72        })
    2.73  
    2.74    def read_facts(provider: Export.Provider): List[Fact_Multi] =
    2.75      provider.uncompressed_yxml(export_prefix + "facts").map((tree: XML.Tree) =>
    2.76        {
    2.77          val (entity, body) = decode_entity(Kind.FACT, tree)
    2.78 -        val props = XML.Decode.list(decode_prop)(body)
    2.79 -        Fact_Multi(entity, props)
    2.80 +        val facts = XML.Decode.list(decode_fact)(body)
    2.81 +        Fact_Multi(entity, facts)
    2.82        })
    2.83  
    2.84  
     3.1 --- a/src/Pure/proofterm.ML	Thu Aug 15 16:02:47 2019 +0200
     3.2 +++ b/src/Pure/proofterm.ML	Thu Aug 15 16:06:57 2019 +0200
     3.3 @@ -67,6 +67,7 @@
     3.4  
     3.5    val encode: proof XML.Encode.T
     3.6    val encode_body: proof_body XML.Encode.T
     3.7 +  val encode_full: proof XML.Encode.T
     3.8    val decode: proof XML.Decode.T
     3.9    val decode_body: proof_body XML.Decode.T
    3.10  
    3.11 @@ -165,6 +166,9 @@
    3.12    val standard_vars: Name.context -> term list * proof list -> term list * proof list
    3.13    val standard_vars_term: Name.context -> term -> term
    3.14    val standard_vars_proof: Name.context -> proof -> proof
    3.15 +  val used_frees_type: typ -> Name.context -> Name.context
    3.16 +  val used_frees_term: term -> Name.context -> Name.context
    3.17 +  val used_frees_proof: proof -> Name.context -> Name.context
    3.18  
    3.19    val proof_serial: unit -> proof_serial
    3.20    val fulfill_norm_proof: theory -> (serial * proof_body) list -> proof_body -> proof_body
    3.21 @@ -389,10 +393,24 @@
    3.22    pair int (triple string term proof_body)
    3.23      (a, (thm_node_name thm_node, thm_node_prop thm_node, Future.join (thm_node_body thm_node)));
    3.24  
    3.25 +fun full_proof prf = prf |> variant
    3.26 + [fn MinProof => ([], []),
    3.27 +  fn PBound a => ([int_atom a], []),
    3.28 +  fn Abst (a, SOME b, c) => ([a], pair typ full_proof (b, c)),
    3.29 +  fn AbsP (a, SOME b, c) => ([a], pair term full_proof (b, c)),
    3.30 +  fn a % SOME b => ([], pair full_proof term (a, b)),
    3.31 +  fn a %% b => ([], pair full_proof full_proof (a, b)),
    3.32 +  fn Hyp a => ([], term a),
    3.33 +  fn PAxm (name, _, SOME Ts) => ([name], list typ Ts),
    3.34 +  fn OfClass (T, c) => ([c], typ T),
    3.35 +  fn Oracle (name, prop, SOME Ts) => ([name], pair term (list typ) (prop, Ts)),
    3.36 +  fn PThm ({serial, name, types = SOME Ts, ...}, _) => ([int_atom serial, name], list typ Ts)];
    3.37 +
    3.38  in
    3.39  
    3.40  val encode = proof;
    3.41  val encode_body = proof_body;
    3.42 +val encode_full = full_proof;
    3.43  
    3.44  end;
    3.45  
    3.46 @@ -2051,6 +2069,10 @@
    3.47  
    3.48  end;
    3.49  
    3.50 +val used_frees_type = fold_atyps (fn TFree (a, _) => Name.declare a | _ => I);
    3.51 +fun used_frees_term t = fold_types used_frees_type t #> Term.declare_term_frees t;
    3.52 +val used_frees_proof = fold_proof_terms used_frees_term used_frees_type;
    3.53 +
    3.54  
    3.55  (* PThm nodes *)
    3.56  
    3.57 @@ -2076,30 +2098,9 @@
    3.58  
    3.59  fun clean_proof thy = rew_proof thy #> shrink_proof;
    3.60  
    3.61 -
    3.62 -local open XML.Encode Term_XML.Encode in
    3.63 -
    3.64 -fun proof prf = prf |> variant
    3.65 - [fn MinProof => ([], []),
    3.66 -  fn PBound a => ([int_atom a], []),
    3.67 -  fn Abst (a, SOME b, c) => ([a], pair typ proof (b, c)),
    3.68 -  fn AbsP (a, SOME b, c) => ([a], pair term proof (b, c)),
    3.69 -  fn a % SOME b => ([], pair proof term (a, b)),
    3.70 -  fn a %% b => ([], pair proof proof (a, b)),
    3.71 -  fn Hyp a => ([], term a),
    3.72 -  fn PAxm (name, b, SOME Ts) => ([name], list typ Ts),
    3.73 -  fn OfClass (T, c) => ([c], typ T),
    3.74 -  fn Oracle (name, prop, SOME Ts) => ([name], pair term (list typ) (prop, Ts)),
    3.75 -  fn PThm ({serial, name, types = SOME Ts, ...}, _) => ([int_atom serial, name], list typ Ts)];
    3.76 -
    3.77 -fun encode_export prop prf = pair term proof (prop, prf);
    3.78 -
    3.79 -
    3.80 -val used_frees_type = fold_atyps (fn TFree (a, _) => Name.declare a | _ => I);
    3.81 -fun used_frees_term t = fold_types used_frees_type t #> Term.declare_term_frees t;
    3.82 -val used_frees_proof = fold_proof_terms used_frees_term used_frees_type;
    3.83 -
    3.84 -end;
    3.85 +fun encode_export prop prf =
    3.86 +  let open XML.Encode Term_XML.Encode
    3.87 +  in pair term encode_full (prop, prf) end;
    3.88  
    3.89  fun export_proof thy i prop prf =
    3.90    let