export spec rules;

--- 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 *)

--- 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 _ =

--- 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)
+  }
 }