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