# HG changeset patch
# User wenzelm
# Date 1553694469 -3600
# Node ID 8f2d3a27aff0ed81f735f7d15de65ca0e06d69ec
# Parent  2d5c313e858258602ef29f7e93e114d88d696d16
more informative Spec_Rules.Equational: support corecursion;

diff -r 2d5c313e8582 -r 8f2d3a27aff0 src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML
--- a/src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML	Wed Mar 27 12:08:08 2019 +0100
+++ b/src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML	Wed Mar 27 14:47:49 2019 +0100
@@ -1059,6 +1059,7 @@
   let
     val (bs, mxs) = map_split (apfst fst) fixes;
     val (arg_Ts, res_Ts) = map (strip_type o snd o fst #>> mk_tupleT_balanced) fixes |> split_list;
+    val primcorec_types = map (#1 o dest_Type) res_Ts;
 
     val _ = check_duplicate_const_names bs;
     val _ = List.app (uncurry (check_top_sort lthy)) (bs ~~ arg_Ts);
@@ -1532,7 +1533,7 @@
         val fun_ts0 = map fst def_infos;
       in
         lthy
-        |> Spec_Rules.add Spec_Rules.equational (fun_ts0, flat sel_thmss)
+        |> Spec_Rules.add (Spec_Rules.equational_primcorec primcorec_types) (fun_ts0, flat sel_thmss)
         |> Spec_Rules.add Spec_Rules.equational (fun_ts0, flat ctr_thmss)
         |> Spec_Rules.add Spec_Rules.equational (fun_ts0, flat code_thmss)
         |> plugins code_plugin ? Code.declare_default_eqns (map (rpair true) (flat code_thmss))
diff -r 2d5c313e8582 -r 8f2d3a27aff0 src/Pure/Isar/spec_rules.ML
--- a/src/Pure/Isar/spec_rules.ML	Wed Mar 27 12:08:08 2019 +0100
+++ b/src/Pure/Isar/spec_rules.ML	Wed Mar 27 14:47:49 2019 +0100
@@ -8,12 +8,15 @@
 
 signature SPEC_RULES =
 sig
-  datatype recursion = Primrec of string list | Recdef | Unknown_Recursion
+  datatype recursion =
+    Primrec of string list | Recdef | Primcorec of string list | Corec | Unknown_Recursion
   val recursion_ord: recursion * recursion -> order
   datatype rough_classification = Equational of recursion | Inductive | Co_Inductive | Unknown
   val rough_classification_ord: rough_classification * rough_classification -> order
   val equational_primrec: string list -> rough_classification
   val equational_recdef: rough_classification
+  val equational_primcorec: string list -> rough_classification
+  val equational_corec: rough_classification
   val equational: rough_classification
   val is_equational: rough_classification -> bool
   val is_inductive: rough_classification -> bool
@@ -33,11 +36,15 @@
 
 (* recursion *)
 
-datatype recursion = Primrec of string list | Recdef | Unknown_Recursion;
+datatype recursion =
+  Primrec of string list | Recdef | Primcorec of string list | Corec | Unknown_Recursion;
+
+val recursion_index =
+  fn Primrec _ => 0 | Recdef => 1 | Primcorec _ => 2 | Corec => 3 | Unknown_Recursion => 4;
 
 fun recursion_ord (Primrec Ts1, Primrec Ts2) = list_ord fast_string_ord (Ts1, Ts2)
-  | recursion_ord rs =
-      int_ord (apply2 (fn Primrec _ => 0 | Recdef => 1 | Unknown_Recursion => 2) rs);
+  | recursion_ord (Primcorec Ts1, Primcorec Ts2) = list_ord fast_string_ord (Ts1, Ts2)
+  | recursion_ord rs = int_ord (apply2 recursion_index rs);
 
 
 (* rough classification *)
@@ -50,6 +57,8 @@
 
 val equational_primrec = Equational o Primrec;
 val equational_recdef = Equational Recdef;
+val equational_primcorec = Equational o Primcorec;
+val equational_corec = Equational Corec;
 val equational = Equational Unknown_Recursion;
 
 val is_equational = fn Equational _ => true | _ => false;
diff -r 2d5c313e8582 -r 8f2d3a27aff0 src/Pure/Thy/export_theory.ML
--- a/src/Pure/Thy/export_theory.ML	Wed Mar 27 12:08:08 2019 +0100
+++ b/src/Pure/Thy/export_theory.ML	Wed Mar 27 14:47:49 2019 +0100
@@ -105,8 +105,11 @@
 
 fun primrec_types ctxt const =
   Spec_Rules.retrieve ctxt (Const const)
-  |> get_first (fn (Spec_Rules.Equational (Spec_Rules.Primrec types), _) => SOME types | _ => NONE)
-  |> the_default [];
+  |> get_first
+    (fn (Spec_Rules.Equational (Spec_Rules.Primrec types), _) => SOME (types, false)
+      | (Spec_Rules.Equational (Spec_Rules.Primcorec types), _) => SOME (types, true)
+      | _ => NONE)
+  |> the_default ([], false);
 
 
 (* locales content *)
@@ -240,7 +243,8 @@
     val encode_const =
       let open XML.Encode Term_XML.Encode in
         pair encode_syntax
-          (pair (list string) (pair typ (pair (option term) (pair bool (list string)))))
+          (pair (list string)
+            (pair typ (pair (option term) (pair bool (pair (list string) bool)))))
       end;
 
     fun export_const c (T, abbrev) =
@@ -248,11 +252,11 @@
         val syntax = get_syntax_const thy_ctxt c;
         val U = Logic.unvarifyT_global T;
         val U0 = Type.strip_sorts U;
-        val primrec_types = primrec_types thy_ctxt (c, U);
+        val recursion = primrec_types thy_ctxt (c, U);
         val abbrev' = abbrev |> Option.map (standard_vars_global #> map_types Type.strip_sorts);
         val args = map (#1 o dest_TFree) (Consts.typargs (Sign.consts_of thy) (c, U0));
         val propositional = Object_Logic.is_propositional thy_ctxt (Term.body_type U0);
-      in encode_const (syntax, (args, (U0, (abbrev', (propositional, primrec_types))))) end;
+      in encode_const (syntax, (args, (U0, (abbrev', (propositional, recursion))))) end;
 
     val _ =
       export_entities "consts" (SOME oo export_const) Sign.const_space
diff -r 2d5c313e8582 -r 8f2d3a27aff0 src/Pure/Thy/export_theory.scala
--- a/src/Pure/Thy/export_theory.scala	Wed Mar 27 12:08:08 2019 +0100
+++ b/src/Pure/Thy/export_theory.scala	Wed Mar 27 14:47:49 2019 +0100
@@ -253,7 +253,8 @@
     typ: Term.Typ,
     abbrev: Option[Term.Term],
     propositional: Boolean,
-    primrec_types: List[String])
+    primrec_types: List[String],
+    corecursive: Boolean)
   {
     def cache(cache: Term.Cache): Const =
       Const(entity.cache(cache),
@@ -262,22 +263,24 @@
         cache.typ(typ),
         abbrev.map(cache.term(_)),
         propositional,
-        primrec_types.map(cache.string(_)))
+        primrec_types.map(cache.string(_)),
+        corecursive)
   }
 
   def read_consts(provider: Export.Provider): List[Const] =
     provider.uncompressed_yxml(export_prefix + "consts").map((tree: XML.Tree) =>
       {
         val (entity, body) = decode_entity(Kind.CONST, tree)
-        val (syntax, (args, (typ, (abbrev, (propositional, primrec_types))))) =
+        val (syntax, (args, (typ, (abbrev, (propositional, (primrec_types, corecursive)))))) =
         {
           import XML.Decode._
           pair(decode_syntax,
             pair(list(string),
               pair(Term_XML.Decode.typ,
-                pair(option(Term_XML.Decode.term), pair(bool, list(string))))))(body)
+                pair(option(Term_XML.Decode.term), pair(bool,
+                  pair(list(string), bool))))))(body)
         }
-        Const(entity, syntax, args, typ, abbrev, propositional, primrec_types)
+        Const(entity, syntax, args, typ, abbrev, propositional, primrec_types, corecursive)
       })