more informative Spec_Rules.Equational: support corecursion;
authorwenzelm
Wed Mar 27 14:47:49 2019 +0100 (6 months ago)
changeset 699968f2d3a27aff0
parent 69995 2d5c313e8582
child 69997 9c634887be9e
more informative Spec_Rules.Equational: support corecursion;
src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML
src/Pure/Isar/spec_rules.ML
src/Pure/Thy/export_theory.ML
src/Pure/Thy/export_theory.scala
     1.1 --- a/src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML	Wed Mar 27 12:08:08 2019 +0100
     1.2 +++ b/src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML	Wed Mar 27 14:47:49 2019 +0100
     1.3 @@ -1059,6 +1059,7 @@
     1.4    let
     1.5      val (bs, mxs) = map_split (apfst fst) fixes;
     1.6      val (arg_Ts, res_Ts) = map (strip_type o snd o fst #>> mk_tupleT_balanced) fixes |> split_list;
     1.7 +    val primcorec_types = map (#1 o dest_Type) res_Ts;
     1.8  
     1.9      val _ = check_duplicate_const_names bs;
    1.10      val _ = List.app (uncurry (check_top_sort lthy)) (bs ~~ arg_Ts);
    1.11 @@ -1532,7 +1533,7 @@
    1.12          val fun_ts0 = map fst def_infos;
    1.13        in
    1.14          lthy
    1.15 -        |> Spec_Rules.add Spec_Rules.equational (fun_ts0, flat sel_thmss)
    1.16 +        |> Spec_Rules.add (Spec_Rules.equational_primcorec primcorec_types) (fun_ts0, flat sel_thmss)
    1.17          |> Spec_Rules.add Spec_Rules.equational (fun_ts0, flat ctr_thmss)
    1.18          |> Spec_Rules.add Spec_Rules.equational (fun_ts0, flat code_thmss)
    1.19          |> plugins code_plugin ? Code.declare_default_eqns (map (rpair true) (flat code_thmss))
     2.1 --- a/src/Pure/Isar/spec_rules.ML	Wed Mar 27 12:08:08 2019 +0100
     2.2 +++ b/src/Pure/Isar/spec_rules.ML	Wed Mar 27 14:47:49 2019 +0100
     2.3 @@ -8,12 +8,15 @@
     2.4  
     2.5  signature SPEC_RULES =
     2.6  sig
     2.7 -  datatype recursion = Primrec of string list | Recdef | Unknown_Recursion
     2.8 +  datatype recursion =
     2.9 +    Primrec of string list | Recdef | Primcorec of string list | Corec | Unknown_Recursion
    2.10    val recursion_ord: recursion * recursion -> order
    2.11    datatype rough_classification = Equational of recursion | Inductive | Co_Inductive | Unknown
    2.12    val rough_classification_ord: rough_classification * rough_classification -> order
    2.13    val equational_primrec: string list -> rough_classification
    2.14    val equational_recdef: rough_classification
    2.15 +  val equational_primcorec: string list -> rough_classification
    2.16 +  val equational_corec: rough_classification
    2.17    val equational: rough_classification
    2.18    val is_equational: rough_classification -> bool
    2.19    val is_inductive: rough_classification -> bool
    2.20 @@ -33,11 +36,15 @@
    2.21  
    2.22  (* recursion *)
    2.23  
    2.24 -datatype recursion = Primrec of string list | Recdef | Unknown_Recursion;
    2.25 +datatype recursion =
    2.26 +  Primrec of string list | Recdef | Primcorec of string list | Corec | Unknown_Recursion;
    2.27 +
    2.28 +val recursion_index =
    2.29 +  fn Primrec _ => 0 | Recdef => 1 | Primcorec _ => 2 | Corec => 3 | Unknown_Recursion => 4;
    2.30  
    2.31  fun recursion_ord (Primrec Ts1, Primrec Ts2) = list_ord fast_string_ord (Ts1, Ts2)
    2.32 -  | recursion_ord rs =
    2.33 -      int_ord (apply2 (fn Primrec _ => 0 | Recdef => 1 | Unknown_Recursion => 2) rs);
    2.34 +  | recursion_ord (Primcorec Ts1, Primcorec Ts2) = list_ord fast_string_ord (Ts1, Ts2)
    2.35 +  | recursion_ord rs = int_ord (apply2 recursion_index rs);
    2.36  
    2.37  
    2.38  (* rough classification *)
    2.39 @@ -50,6 +57,8 @@
    2.40  
    2.41  val equational_primrec = Equational o Primrec;
    2.42  val equational_recdef = Equational Recdef;
    2.43 +val equational_primcorec = Equational o Primcorec;
    2.44 +val equational_corec = Equational Corec;
    2.45  val equational = Equational Unknown_Recursion;
    2.46  
    2.47  val is_equational = fn Equational _ => true | _ => false;
     3.1 --- a/src/Pure/Thy/export_theory.ML	Wed Mar 27 12:08:08 2019 +0100
     3.2 +++ b/src/Pure/Thy/export_theory.ML	Wed Mar 27 14:47:49 2019 +0100
     3.3 @@ -105,8 +105,11 @@
     3.4  
     3.5  fun primrec_types ctxt const =
     3.6    Spec_Rules.retrieve ctxt (Const const)
     3.7 -  |> get_first (fn (Spec_Rules.Equational (Spec_Rules.Primrec types), _) => SOME types | _ => NONE)
     3.8 -  |> the_default [];
     3.9 +  |> get_first
    3.10 +    (fn (Spec_Rules.Equational (Spec_Rules.Primrec types), _) => SOME (types, false)
    3.11 +      | (Spec_Rules.Equational (Spec_Rules.Primcorec types), _) => SOME (types, true)
    3.12 +      | _ => NONE)
    3.13 +  |> the_default ([], false);
    3.14  
    3.15  
    3.16  (* locales content *)
    3.17 @@ -240,7 +243,8 @@
    3.18      val encode_const =
    3.19        let open XML.Encode Term_XML.Encode in
    3.20          pair encode_syntax
    3.21 -          (pair (list string) (pair typ (pair (option term) (pair bool (list string)))))
    3.22 +          (pair (list string)
    3.23 +            (pair typ (pair (option term) (pair bool (pair (list string) bool)))))
    3.24        end;
    3.25  
    3.26      fun export_const c (T, abbrev) =
    3.27 @@ -248,11 +252,11 @@
    3.28          val syntax = get_syntax_const thy_ctxt c;
    3.29          val U = Logic.unvarifyT_global T;
    3.30          val U0 = Type.strip_sorts U;
    3.31 -        val primrec_types = primrec_types thy_ctxt (c, U);
    3.32 +        val recursion = primrec_types thy_ctxt (c, U);
    3.33          val abbrev' = abbrev |> Option.map (standard_vars_global #> map_types Type.strip_sorts);
    3.34          val args = map (#1 o dest_TFree) (Consts.typargs (Sign.consts_of thy) (c, U0));
    3.35          val propositional = Object_Logic.is_propositional thy_ctxt (Term.body_type U0);
    3.36 -      in encode_const (syntax, (args, (U0, (abbrev', (propositional, primrec_types))))) end;
    3.37 +      in encode_const (syntax, (args, (U0, (abbrev', (propositional, recursion))))) end;
    3.38  
    3.39      val _ =
    3.40        export_entities "consts" (SOME oo export_const) Sign.const_space
     4.1 --- a/src/Pure/Thy/export_theory.scala	Wed Mar 27 12:08:08 2019 +0100
     4.2 +++ b/src/Pure/Thy/export_theory.scala	Wed Mar 27 14:47:49 2019 +0100
     4.3 @@ -253,7 +253,8 @@
     4.4      typ: Term.Typ,
     4.5      abbrev: Option[Term.Term],
     4.6      propositional: Boolean,
     4.7 -    primrec_types: List[String])
     4.8 +    primrec_types: List[String],
     4.9 +    corecursive: Boolean)
    4.10    {
    4.11      def cache(cache: Term.Cache): Const =
    4.12        Const(entity.cache(cache),
    4.13 @@ -262,22 +263,24 @@
    4.14          cache.typ(typ),
    4.15          abbrev.map(cache.term(_)),
    4.16          propositional,
    4.17 -        primrec_types.map(cache.string(_)))
    4.18 +        primrec_types.map(cache.string(_)),
    4.19 +        corecursive)
    4.20    }
    4.21  
    4.22    def read_consts(provider: Export.Provider): List[Const] =
    4.23      provider.uncompressed_yxml(export_prefix + "consts").map((tree: XML.Tree) =>
    4.24        {
    4.25          val (entity, body) = decode_entity(Kind.CONST, tree)
    4.26 -        val (syntax, (args, (typ, (abbrev, (propositional, primrec_types))))) =
    4.27 +        val (syntax, (args, (typ, (abbrev, (propositional, (primrec_types, corecursive)))))) =
    4.28          {
    4.29            import XML.Decode._
    4.30            pair(decode_syntax,
    4.31              pair(list(string),
    4.32                pair(Term_XML.Decode.typ,
    4.33 -                pair(option(Term_XML.Decode.term), pair(bool, list(string))))))(body)
    4.34 +                pair(option(Term_XML.Decode.term), pair(bool,
    4.35 +                  pair(list(string), bool))))))(body)
    4.36          }
    4.37 -        Const(entity, syntax, args, typ, abbrev, propositional, primrec_types)
    4.38 +        Const(entity, syntax, args, typ, abbrev, propositional, primrec_types, corecursive)
    4.39        })
    4.40  
    4.41