# HG changeset patch # User wenzelm # Date 1575123443 -3600 # Node ID 785610ad6bfab8055a68405888ec8e3df308b7aa # Parent 8331063570d6b21b03f3fa62aee67c17fc5e262f export spec rules; diff -r 8331063570d6 -r 785610ad6bfa src/Pure/Isar/spec_rules.ML --- a/src/Pure/Isar/spec_rules.ML Wed Nov 27 16:54:33 2019 +0000 +++ b/src/Pure/Isar/spec_rules.ML Sat Nov 30 15:17:23 2019 +0100 @@ -1,7 +1,9 @@ (* Title: Pure/Isar/spec_rules.ML Author: Makarius -Rules that characterize specifications, with rough classification. +Rules that characterize specifications, with optional name and +rough classification. + NB: In the face of arbitrary morphisms, the original shape of specifications may get lost. *) @@ -11,6 +13,7 @@ datatype recursion = Primrec of string list | Recdef | Primcorec of string list | Corec | Unknown_Recursion val recursion_ord: recursion ord + val encode_recursion: recursion XML.Encode.T datatype rough_classification = Equational of recursion | Inductive | Co_Inductive | Unknown val rough_classification_ord: rough_classification ord val equational_primrec: string list -> rough_classification @@ -23,10 +26,12 @@ val is_co_inductive: rough_classification -> bool val is_relational: rough_classification -> bool val is_unknown: rough_classification -> bool + val encode_rough_classification: rough_classification XML.Encode.T type spec = {name: string, rough_classification: rough_classification, terms: term list, rules: thm list} val get: Proof.context -> spec list val get_global: theory -> spec list + val dest_theory: theory -> spec list val retrieve: Proof.context -> term -> spec list val retrieve_global: theory -> term -> spec list val add: string -> rough_classification -> term list -> thm list -> local_theory -> local_theory @@ -48,6 +53,16 @@ | recursion_ord (Primcorec Ts1, Primcorec Ts2) = list_ord fast_string_ord (Ts1, Ts2) | recursion_ord rs = int_ord (apply2 recursion_index rs); +val encode_recursion = + let open XML.Encode in + variant + [fn Primrec a => ([], list string a), + fn Recdef => ([], []), + fn Primcorec a => ([], list string a), + fn Corec => ([], []), + fn Unknown_Recursion => ([], [])] + end; + (* rough classification *) @@ -69,6 +84,15 @@ val is_relational = is_inductive orf is_co_inductive; val is_unknown = fn Unknown => true | _ => false; +val encode_rough_classification = + let open XML.Encode in + variant + [fn Equational r => ([], encode_recursion r), + fn Inductive => ([], []), + fn Co_Inductive => ([], []), + fn Unknown => ([], [])] + end; + (* rules *) @@ -95,17 +119,22 @@ (* get *) -fun get_generic context = +fun get_generic imports context = let val thy = Context.theory_of context; val transfer = Global_Theory.transfer_theories thy; + fun imported spec = + imports |> exists (fn thy => Item_Net.member (Rules.get (Context.Theory thy)) spec); in Item_Net.content (Rules.get context) + |> filter_out imported |> (map o map_spec_rules) transfer end; -val get = get_generic o Context.Proof; -val get_global = get_generic o Context.Theory; +val get = get_generic [] o Context.Proof; +val get_global = get_generic [] o Context.Theory; + +fun dest_theory thy = rev (get_generic (Theory.parents_of thy) (Context.Theory thy)); (* retrieve *) diff -r 8331063570d6 -r 785610ad6bfa src/Pure/Thy/export_theory.ML --- a/src/Pure/Thy/export_theory.ML Wed Nov 27 16:54:33 2019 +0000 +++ b/src/Pure/Thy/export_theory.ML Sat Nov 30 15:17:23 2019 +0100 @@ -232,6 +232,9 @@ val sorts = Name.invent used_typargs Name.aT (length extra_shyps) ~~ extra_shyps; in ((sorts @ typargs, args, prop), proof) end; + fun standard_prop_of thm = + standard_prop Name.context (Thm.extra_shyps thm) (Thm.full_prop_of thm); + val encode_prop = let open XML.Encode Term_XML.Encode in triple (list (pair string sort)) (list (pair string typ)) encode_term end; @@ -247,6 +250,7 @@ (* theorems and proof terms *) val clean_thm = Thm.check_hyps (Context.Theory thy) #> Thm.strip_shyps; + val prep_thm = clean_thm #> Thm.unconstrainT; val lookup_thm_id = Global_Theory.lookup_thm_id thy; @@ -267,7 +271,7 @@ fun encode_thm thm_id raw_thm = 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 thm = prep_thm raw_thm; val proof0 = if Proofterm.export_standard_enabled () then @@ -275,8 +279,7 @@ {full = true, expand_name = SOME o expand_name thm_id} thm else if Proofterm.export_enabled () then Thm.reconstruct_proof_of thm else MinProof; - val (prop, SOME proof) = - standard_prop Name.context (Thm.extra_shyps thm) (Thm.full_prop_of thm) (SOME proof0); + val (prop, SOME proof) = standard_prop_of thm (SOME proof0); val _ = Thm.expose_proofs thy [thm]; in (prop, deps, proof) |> @@ -397,6 +400,25 @@ if null constdefs then () else export_body thy "constdefs" (encode_constdefs constdefs); + (* spec rules *) + + fun encode_spec {name, rough_classification, terms, rules} = + let + val terms' = map Logic.unvarify_global terms; + val rules' = map (fn rule => #1 (standard_prop_of (prep_thm rule) NONE)) rules; + open XML.Encode; + in + pair string (pair Spec_Rules.encode_rough_classification + (pair (list encode_term) (list encode_prop))) + (name, (rough_classification, (terms', rules'))) + end; + + val _ = + (case Spec_Rules.dest_theory thy of + [] => () + | spec_rules => export_body thy "spec_rules" (XML.Encode.list encode_spec spec_rules)); + + (* parents *) val _ = diff -r 8331063570d6 -r 785610ad6bfa src/Pure/Thy/export_theory.scala --- a/src/Pure/Thy/export_theory.scala Wed Nov 27 16:54:33 2019 +0000 +++ b/src/Pure/Thy/export_theory.scala Sat Nov 30 15:17:23 2019 +0100 @@ -42,6 +42,7 @@ arities: Boolean = true, constdefs: Boolean = true, typedefs: Boolean = true, + spec_rules: Boolean = true, cache: Term.Cache = Term.make_cache()): Session = { val thys = @@ -56,7 +57,8 @@ session, theory, types = types, consts = consts, axioms = axioms, thms = thms, classes = classes, locales = locales, locale_dependencies = locale_dependencies, classrel = classrel, arities = arities, - constdefs = constdefs, typedefs = typedefs, cache = Some(cache)) + constdefs = constdefs, typedefs = typedefs, + spec_rules = spec_rules, cache = Some(cache)) } } })) @@ -90,7 +92,8 @@ classrel: List[Classrel], arities: List[Arity], constdefs: List[Constdef], - typedefs: List[Typedef]) + typedefs: List[Typedef], + spec_rules: List[Spec_Rule]) { override def toString: String = name @@ -116,7 +119,8 @@ classrel.map(_.cache(cache)), arities.map(_.cache(cache)), constdefs.map(_.cache(cache)), - typedefs.map(_.cache(cache))) + typedefs.map(_.cache(cache)), + spec_rules.map(_.cache(cache))) } def read_theory(provider: Export.Provider, session_name: String, theory_name: String, @@ -131,6 +135,7 @@ arities: Boolean = true, constdefs: Boolean = true, typedefs: Boolean = true, + spec_rules: Boolean = true, cache: Option[Term.Cache] = None): Theory = { val parents = @@ -155,7 +160,8 @@ if (classrel) read_classrel(provider) else Nil, if (arities) read_arities(provider) else Nil, if (constdefs) read_constdefs(provider) else Nil, - if (typedefs) read_typedefs(provider) else Nil) + if (typedefs) read_typedefs(provider) else Nil, + if (spec_rules) read_spec_rules(provider) else Nil) if (cache.isDefined) theory.cache(cache.get) else theory } @@ -643,4 +649,92 @@ for { (name, (rep_type, (abs_type, (rep_name, (abs_name, axiom_name))))) <- typedefs } yield Typedef(name, rep_type, abs_type, rep_name, abs_name, axiom_name) } + + + /* Pure spec rules */ + + sealed abstract class Recursion + { + def cache(cache: Term.Cache): Recursion = + this match { + case Primrec(types) => Primrec(types.map(cache.string)) + case Primcorec(types) => Primcorec(types.map(cache.string)) + case _ => this + } + } + case class Primrec(types: List[String]) extends Recursion + case object Recdef extends Recursion + case class Primcorec(types: List[String]) extends Recursion + case object Corec extends Recursion + case object Unknown_Recursion extends Recursion + + val decode_recursion: XML.Decode.T[Recursion] = + { + import XML.Decode._ + variant(List( + { case (Nil, a) => Primrec(list(string)(a)) }, + { case (Nil, Nil) => Recdef }, + { case (Nil, a) => Primcorec(list(string)(a)) }, + { case (Nil, Nil) => Corec }, + { case (Nil, Nil) => Unknown_Recursion })) + } + + + sealed abstract class Rough_Classification + { + def is_equational: Boolean = this.isInstanceOf[Equational] + def is_inductive: Boolean = this == Inductive + def is_co_inductive: Boolean = this == Co_Inductive + def is_relational: Boolean = is_inductive || is_co_inductive + def is_unknown: Boolean = this == Unknown + + def cache(cache: Term.Cache): Rough_Classification = + this match { + case Equational(recursion) => Equational(recursion.cache(cache)) + case _ => this + } + } + case class Equational(recursion: Recursion) extends Rough_Classification + case object Inductive extends Rough_Classification + case object Co_Inductive extends Rough_Classification + case object Unknown extends Rough_Classification + + val decode_rough_classification: XML.Decode.T[Rough_Classification] = + { + import XML.Decode._ + variant(List( + { case (Nil, a) => Equational(decode_recursion(a)) }, + { case (Nil, Nil) => Inductive }, + { case (Nil, Nil) => Co_Inductive }, + { case (Nil, Nil) => Unknown })) + } + + + sealed case class Spec_Rule( + name: String, + rough_classification: Rough_Classification, + terms: List[Term.Term], + rules: List[Prop]) + { + def cache(cache: Term.Cache): Spec_Rule = + Spec_Rule( + cache.string(name), + rough_classification.cache(cache), + terms.map(cache.term(_)), + rules.map(_.cache(cache))) + } + + def read_spec_rules(provider: Export.Provider): List[Spec_Rule] = + { + val body = provider.uncompressed_yxml(export_prefix + "spec_rules") + val spec_rules = + { + import XML.Decode._ + import Term_XML.Decode._ + list(pair(string, pair(decode_rough_classification, pair(list(term), list(decode_prop)))))( + body) + } + for ((name, (rough_classification, (terms, rules))) <- spec_rules) + yield Spec_Rule(name, rough_classification, terms, rules) + } }