src/HOL/Tools/BNF/bnf_lfp_compat.ML
author blanchet
Tue, 08 Apr 2014 17:49:03 +0200
changeset 56453 00548d372f02
parent 56452 0c98c9118407
child 56455 1ff66e72628b
permissions -rw-r--r--
support deeply nested datatypes in 'datatype_compat'
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
55061
a0adf838e2d1 adjusted comments
blanchet
parents: 55060
diff changeset
     1
(*  Title:      HOL/Tools/BNF/bnf_lfp_compat.ML
53303
ae49b835ca01 moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff changeset
     2
    Author:     Jasmin Blanchette, TU Muenchen
ae49b835ca01 moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff changeset
     3
    Copyright   2013
ae49b835ca01 moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff changeset
     4
55539
0819931d652d simplified data structure by reducing the incidence of clumsy indices
blanchet
parents: 55531
diff changeset
     5
Compatibility layer with the old datatype package ("datatype_compat").
53303
ae49b835ca01 moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff changeset
     6
*)
ae49b835ca01 moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff changeset
     7
ae49b835ca01 moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff changeset
     8
signature BNF_LFP_COMPAT =
ae49b835ca01 moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff changeset
     9
sig
55531
601ca8efa000 renamed 'datatype_new_compat' to 'datatype_compat'
blanchet
parents: 55486
diff changeset
    10
  val datatype_compat_cmd : string list -> local_theory -> local_theory
53303
ae49b835ca01 moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff changeset
    11
end;
ae49b835ca01 moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff changeset
    12
ae49b835ca01 moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff changeset
    13
structure BNF_LFP_Compat : BNF_LFP_COMPAT =
ae49b835ca01 moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff changeset
    14
struct
ae49b835ca01 moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff changeset
    15
54006
9fe1bd54d437 renamed theory file
blanchet
parents: 54003
diff changeset
    16
open Ctr_Sugar
53303
ae49b835ca01 moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff changeset
    17
open BNF_Util
ae49b835ca01 moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff changeset
    18
open BNF_FP_Util
ae49b835ca01 moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff changeset
    19
open BNF_FP_Def_Sugar
ae49b835ca01 moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff changeset
    20
open BNF_FP_N2M_Sugar
ae49b835ca01 moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff changeset
    21
ae49b835ca01 moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff changeset
    22
val compatN = "compat_";
ae49b835ca01 moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff changeset
    23
55479
ece4910c3ea0 improved 'datatype_new_compat': generate more fixpoint equations for types like 'datatype_new x = C (x list) (x list)' (here, one equation for each x list instead of a single for both), for higher compatibility + code generation attributes on the recursor
blanchet
parents: 55409
diff changeset
    24
val code_nitpicksimp_simp_attrs = Code.add_default_eqn_attrib :: @{attributes [nitpick_simp, simp]};
ece4910c3ea0 improved 'datatype_new_compat': generate more fixpoint equations for types like 'datatype_new x = C (x list) (x list)' (here, one equation for each x list instead of a single for both), for higher compatibility + code generation attributes on the recursor
blanchet
parents: 55409
diff changeset
    25
56453
00548d372f02 support deeply nested datatypes in 'datatype_compat'
blanchet
parents: 56452
diff changeset
    26
fun reindex_desc desc =
00548d372f02 support deeply nested datatypes in 'datatype_compat'
blanchet
parents: 56452
diff changeset
    27
  let
00548d372f02 support deeply nested datatypes in 'datatype_compat'
blanchet
parents: 56452
diff changeset
    28
    val kks = map fst desc;
00548d372f02 support deeply nested datatypes in 'datatype_compat'
blanchet
parents: 56452
diff changeset
    29
    val perm_kks = sort int_ord kks;
00548d372f02 support deeply nested datatypes in 'datatype_compat'
blanchet
parents: 56452
diff changeset
    30
00548d372f02 support deeply nested datatypes in 'datatype_compat'
blanchet
parents: 56452
diff changeset
    31
    fun perm_dtyp (Datatype_Aux.DtType (s, Ds)) = Datatype_Aux.DtType (s, map perm_dtyp Ds)
00548d372f02 support deeply nested datatypes in 'datatype_compat'
blanchet
parents: 56452
diff changeset
    32
      | perm_dtyp (Datatype_Aux.DtRec kk) = Datatype_Aux.DtRec (find_index (curry (op =) kk) kks)
00548d372f02 support deeply nested datatypes in 'datatype_compat'
blanchet
parents: 56452
diff changeset
    33
      | perm_dtyp D = D
00548d372f02 support deeply nested datatypes in 'datatype_compat'
blanchet
parents: 56452
diff changeset
    34
  in
00548d372f02 support deeply nested datatypes in 'datatype_compat'
blanchet
parents: 56452
diff changeset
    35
    if perm_kks = kks then
00548d372f02 support deeply nested datatypes in 'datatype_compat'
blanchet
parents: 56452
diff changeset
    36
      desc
00548d372f02 support deeply nested datatypes in 'datatype_compat'
blanchet
parents: 56452
diff changeset
    37
    else
00548d372f02 support deeply nested datatypes in 'datatype_compat'
blanchet
parents: 56452
diff changeset
    38
      perm_kks ~~
00548d372f02 support deeply nested datatypes in 'datatype_compat'
blanchet
parents: 56452
diff changeset
    39
      map (fn (_, (s, Ds, sDss)) => (s, map perm_dtyp Ds, map (apsnd (map perm_dtyp)) sDss)) desc
00548d372f02 support deeply nested datatypes in 'datatype_compat'
blanchet
parents: 56452
diff changeset
    40
  end
00548d372f02 support deeply nested datatypes in 'datatype_compat'
blanchet
parents: 56452
diff changeset
    41
53303
ae49b835ca01 moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff changeset
    42
(* TODO: graceful failure for local datatypes -- perhaps by making the command global *)
55531
601ca8efa000 renamed 'datatype_new_compat' to 'datatype_compat'
blanchet
parents: 55486
diff changeset
    43
fun datatype_compat_cmd raw_fpT_names lthy =
53303
ae49b835ca01 moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff changeset
    44
  let
ae49b835ca01 moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff changeset
    45
    val thy = Proof_Context.theory_of lthy;
ae49b835ca01 moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff changeset
    46
ae49b835ca01 moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff changeset
    47
    fun not_datatype s = error (quote s ^ " is not a new-style datatype");
ae49b835ca01 moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff changeset
    48
    fun not_mutually_recursive ss =
ae49b835ca01 moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff changeset
    49
      error ("{" ^ commas ss ^ "} is not a complete set of mutually recursive new-style datatypes");
ae49b835ca01 moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff changeset
    50
55539
0819931d652d simplified data structure by reducing the incidence of clumsy indices
blanchet
parents: 55531
diff changeset
    51
    val fpT_names =
56002
2028467b4df4 tuned signature;
wenzelm
parents: 55966
diff changeset
    52
      map (fst o dest_Type o Proof_Context.read_type_name {proper = true, strict = false} lthy)
55951
c07d184aebe9 tuned signature -- more uniform check_type_name/read_type_name;
wenzelm
parents: 55863
diff changeset
    53
        raw_fpT_names;
53303
ae49b835ca01 moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff changeset
    54
ae49b835ca01 moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff changeset
    55
    fun lfp_sugar_of s =
ae49b835ca01 moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff changeset
    56
      (case fp_sugar_of lthy s of
ae49b835ca01 moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff changeset
    57
        SOME (fp_sugar as {fp = Least_FP, ...}) => fp_sugar
ae49b835ca01 moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff changeset
    58
      | _ => not_datatype s);
ae49b835ca01 moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff changeset
    59
55539
0819931d652d simplified data structure by reducing the incidence of clumsy indices
blanchet
parents: 55531
diff changeset
    60
    val fp_ctr_sugars = map (#ctr_sugar o lfp_sugar_of) fpT_names;
55485
bdfb607543f4 better handling of recursion through functions
blanchet
parents: 55481
diff changeset
    61
    val fpTs0 as Type (_, var_As) :: _ = map (body_type o fastype_of o hd o #ctrs) fp_ctr_sugars;
53303
ae49b835ca01 moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff changeset
    62
    val fpT_names' = map (fst o dest_Type) fpTs0;
ae49b835ca01 moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff changeset
    63
ae49b835ca01 moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff changeset
    64
    val _ = eq_set (op =) (fpT_names, fpT_names') orelse not_mutually_recursive fpT_names;
ae49b835ca01 moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff changeset
    65
56452
0c98c9118407 preserve user type variable names to avoid mismatches/confusion
blanchet
parents: 56002
diff changeset
    66
    val (As_names, _) = lthy |> Variable.variant_fixes (map (fn TVar ((s, _), _) => s) var_As);
0c98c9118407 preserve user type variable names to avoid mismatches/confusion
blanchet
parents: 56002
diff changeset
    67
    val As = map2 (fn s => fn TVar (_, S) => TFree (s, S)) As_names var_As;
56453
00548d372f02 support deeply nested datatypes in 'datatype_compat'
blanchet
parents: 56452
diff changeset
    68
    val fpTs = map (fn s => Type (s, As)) fpT_names';
00548d372f02 support deeply nested datatypes in 'datatype_compat'
blanchet
parents: 56452
diff changeset
    69
00548d372f02 support deeply nested datatypes in 'datatype_compat'
blanchet
parents: 56452
diff changeset
    70
    val nn_fp = length fpTs;
53303
ae49b835ca01 moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff changeset
    71
56453
00548d372f02 support deeply nested datatypes in 'datatype_compat'
blanchet
parents: 56452
diff changeset
    72
    val mk_dtyp = Datatype_Aux.dtyp_of_typ (map (apsnd (map Term.dest_TFree) o dest_Type) fpTs);
00548d372f02 support deeply nested datatypes in 'datatype_compat'
blanchet
parents: 56452
diff changeset
    73
00548d372f02 support deeply nested datatypes in 'datatype_compat'
blanchet
parents: 56452
diff changeset
    74
    fun mk_ctr_descr Ts = mk_ctr Ts #> dest_Const ##> (binder_types #> map mk_dtyp);
00548d372f02 support deeply nested datatypes in 'datatype_compat'
blanchet
parents: 56452
diff changeset
    75
    fun mk_typ_descr index (Type (T_name, Ts)) ({ctrs, ...} : ctr_sugar) =
00548d372f02 support deeply nested datatypes in 'datatype_compat'
blanchet
parents: 56452
diff changeset
    76
      (index, (T_name, map mk_dtyp Ts, map (mk_ctr_descr Ts) ctrs));
53303
ae49b835ca01 moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff changeset
    77
56453
00548d372f02 support deeply nested datatypes in 'datatype_compat'
blanchet
parents: 56452
diff changeset
    78
    val orig_descr = map3 mk_typ_descr (0 upto nn_fp - 1) fpTs fp_ctr_sugars;
00548d372f02 support deeply nested datatypes in 'datatype_compat'
blanchet
parents: 56452
diff changeset
    79
    val all_infos = Datatype_Data.get_all thy;
00548d372f02 support deeply nested datatypes in 'datatype_compat'
blanchet
parents: 56452
diff changeset
    80
    val (orig_descr' :: nested_descrs, _) =
00548d372f02 support deeply nested datatypes in 'datatype_compat'
blanchet
parents: 56452
diff changeset
    81
      Datatype_Aux.unfold_datatypes lthy orig_descr all_infos orig_descr nn_fp;
53303
ae49b835ca01 moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff changeset
    82
56453
00548d372f02 support deeply nested datatypes in 'datatype_compat'
blanchet
parents: 56452
diff changeset
    83
    (* put nested types before the types that nest them, as needed for N2M *)
00548d372f02 support deeply nested datatypes in 'datatype_compat'
blanchet
parents: 56452
diff changeset
    84
    val descr = reindex_desc (orig_descr' @ flat (rev nested_descrs));
53303
ae49b835ca01 moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff changeset
    85
56453
00548d372f02 support deeply nested datatypes in 'datatype_compat'
blanchet
parents: 56452
diff changeset
    86
    val dest_dtyp = Datatype_Aux.typ_of_dtyp descr;
55479
ece4910c3ea0 improved 'datatype_new_compat': generate more fixpoint equations for types like 'datatype_new x = C (x list) (x list)' (here, one equation for each x list instead of a single for both), for higher compatibility + code generation attributes on the recursor
blanchet
parents: 55409
diff changeset
    87
56453
00548d372f02 support deeply nested datatypes in 'datatype_compat'
blanchet
parents: 56452
diff changeset
    88
    val Ts = Datatype_Aux.get_rec_types descr;
00548d372f02 support deeply nested datatypes in 'datatype_compat'
blanchet
parents: 56452
diff changeset
    89
    val nn = length Ts;
55485
bdfb607543f4 better handling of recursion through functions
blanchet
parents: 55481
diff changeset
    90
bdfb607543f4 better handling of recursion through functions
blanchet
parents: 55481
diff changeset
    91
    val fp_sugars0 = map (lfp_sugar_of o fst o dest_Type) Ts;
56453
00548d372f02 support deeply nested datatypes in 'datatype_compat'
blanchet
parents: 56452
diff changeset
    92
    val ctr_Tsss = map (map (map dest_dtyp o snd) o #3 o snd) descr;
00548d372f02 support deeply nested datatypes in 'datatype_compat'
blanchet
parents: 56452
diff changeset
    93
    val kkssss =
00548d372f02 support deeply nested datatypes in 'datatype_compat'
blanchet
parents: 56452
diff changeset
    94
      map (map (map (fn Datatype_Aux.DtRec kk => [kk] | _ => []) o snd) o #3 o snd) descr;
53303
ae49b835ca01 moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff changeset
    95
55772
367ec44763fd correct most general type for mutual recursion when several identical types are involved
blanchet
parents: 55571
diff changeset
    96
    val callers = map (fn kk => Var ((Name.uu, kk), @{typ "unit => unit"})) (0 upto nn - 1);
367ec44763fd correct most general type for mutual recursion when several identical types are involved
blanchet
parents: 55571
diff changeset
    97
367ec44763fd correct most general type for mutual recursion when several identical types are involved
blanchet
parents: 55571
diff changeset
    98
    fun apply_comps n kk =
55966
972f0aa7091b balance tuples that represent curried functions
blanchet
parents: 55951
diff changeset
    99
      mk_partial_compN n (replicate n HOLogic.unitT ---> HOLogic.unitT) (nth callers kk);
55772
367ec44763fd correct most general type for mutual recursion when several identical types are involved
blanchet
parents: 55571
diff changeset
   100
367ec44763fd correct most general type for mutual recursion when several identical types are involved
blanchet
parents: 55571
diff changeset
   101
    val callssss =
56453
00548d372f02 support deeply nested datatypes in 'datatype_compat'
blanchet
parents: 56452
diff changeset
   102
      map2 (map2 (map2 (fn ctr_T => map (apply_comps (num_binder_types ctr_T))))) ctr_Tsss kkssss;
00548d372f02 support deeply nested datatypes in 'datatype_compat'
blanchet
parents: 56452
diff changeset
   103
00548d372f02 support deeply nested datatypes in 'datatype_compat'
blanchet
parents: 56452
diff changeset
   104
    val b_names = Name.variant_list [] (map base_name_of_typ Ts);
00548d372f02 support deeply nested datatypes in 'datatype_compat'
blanchet
parents: 56452
diff changeset
   105
    val compat_b_names = map (prefix compatN) b_names;
00548d372f02 support deeply nested datatypes in 'datatype_compat'
blanchet
parents: 56452
diff changeset
   106
    val compat_bs = map Binding.name compat_b_names;
00548d372f02 support deeply nested datatypes in 'datatype_compat'
blanchet
parents: 56452
diff changeset
   107
    val common_name = compatN ^ mk_common_name b_names;
55772
367ec44763fd correct most general type for mutual recursion when several identical types are involved
blanchet
parents: 55571
diff changeset
   108
53746
bd038e48526d have "datatype_new_compat" register induction and recursion theorems in nested case
blanchet
parents: 53309
diff changeset
   109
    val ((fp_sugars, (lfp_sugar_thms, _)), lthy) =
54286
22616f65d4ea properly detect when to perform n2m -- e.g. handle the case of two independent functions on irrelevant types being defined in parallel
blanchet
parents: 54267
diff changeset
   110
      if nn > nn_fp then
55772
367ec44763fd correct most general type for mutual recursion when several identical types are involved
blanchet
parents: 55571
diff changeset
   111
        mutualize_fp_sugars Least_FP compat_bs Ts callers callssss fp_sugars0 lthy
54286
22616f65d4ea properly detect when to perform n2m -- e.g. handle the case of two independent functions on irrelevant types being defined in parallel
blanchet
parents: 54267
diff changeset
   112
      else
22616f65d4ea properly detect when to perform n2m -- e.g. handle the case of two independent functions on irrelevant types being defined in parallel
blanchet
parents: 54267
diff changeset
   113
        ((fp_sugars0, (NONE, NONE)), lthy);
53303
ae49b835ca01 moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff changeset
   114
56453
00548d372f02 support deeply nested datatypes in 'datatype_compat'
blanchet
parents: 56452
diff changeset
   115
    val recs = map (fst o dest_Const o #co_rec) fp_sugars;
00548d372f02 support deeply nested datatypes in 'datatype_compat'
blanchet
parents: 56452
diff changeset
   116
    val rec_thms = maps #co_rec_thms fp_sugars;
00548d372f02 support deeply nested datatypes in 'datatype_compat'
blanchet
parents: 56452
diff changeset
   117
55540
892a425c5eaa follow up of 0819931d652d -- put right induction rule in the old data structure, repairs 'HOL-Proof'-based sessions
blanchet
parents: 55539
diff changeset
   118
    val {common_co_inducts = [induct], ...} :: _ = fp_sugars;
55539
0819931d652d simplified data structure by reducing the incidence of clumsy indices
blanchet
parents: 55531
diff changeset
   119
    val inducts = map (the_single o #co_inducts) fp_sugars;
53303
ae49b835ca01 moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff changeset
   120
55567
blanchet
parents: 55540
diff changeset
   121
    fun mk_info (kk, {T = Type (T_name0, _), ctr_sugar = {casex, exhaust, nchotomy, injects,
55539
0819931d652d simplified data structure by reducing the incidence of clumsy indices
blanchet
parents: 55531
diff changeset
   122
        distincts, case_thms, case_cong, weak_case_cong, split, split_asm, ...}, ...} : fp_sugar) =
0819931d652d simplified data structure by reducing the incidence of clumsy indices
blanchet
parents: 55531
diff changeset
   123
      (T_name0,
0819931d652d simplified data structure by reducing the incidence of clumsy indices
blanchet
parents: 55531
diff changeset
   124
       {index = kk, descr = descr, inject = injects, distinct = distincts, induct = induct,
0819931d652d simplified data structure by reducing the incidence of clumsy indices
blanchet
parents: 55531
diff changeset
   125
       inducts = inducts, exhaust = exhaust, nchotomy = nchotomy, rec_names = recs,
0819931d652d simplified data structure by reducing the incidence of clumsy indices
blanchet
parents: 55531
diff changeset
   126
       rec_rewrites = rec_thms, case_name = fst (dest_Const casex), case_rewrites = case_thms,
0819931d652d simplified data structure by reducing the incidence of clumsy indices
blanchet
parents: 55531
diff changeset
   127
       case_cong = case_cong, weak_case_cong = weak_case_cong, split = split,
0819931d652d simplified data structure by reducing the incidence of clumsy indices
blanchet
parents: 55531
diff changeset
   128
       split_asm = split_asm});
53303
ae49b835ca01 moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff changeset
   129
55539
0819931d652d simplified data structure by reducing the incidence of clumsy indices
blanchet
parents: 55531
diff changeset
   130
    val infos = map_index mk_info (take nn_fp fp_sugars);
53303
ae49b835ca01 moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff changeset
   131
53746
bd038e48526d have "datatype_new_compat" register induction and recursion theorems in nested case
blanchet
parents: 53309
diff changeset
   132
    val all_notes =
bd038e48526d have "datatype_new_compat" register induction and recursion theorems in nested case
blanchet
parents: 53309
diff changeset
   133
      (case lfp_sugar_thms of
bd038e48526d have "datatype_new_compat" register induction and recursion theorems in nested case
blanchet
parents: 53309
diff changeset
   134
        NONE => []
55856
bddaada24074 got rid of automatically generated fold constant and theorems (to reduce overhead)
blanchet
parents: 55772
diff changeset
   135
      | SOME ((induct_thms, induct_thm, induct_attrs), (rec_thmss, _)) =>
53746
bd038e48526d have "datatype_new_compat" register induction and recursion theorems in nested case
blanchet
parents: 53309
diff changeset
   136
        let
bd038e48526d have "datatype_new_compat" register induction and recursion theorems in nested case
blanchet
parents: 53309
diff changeset
   137
          val common_notes =
bd038e48526d have "datatype_new_compat" register induction and recursion theorems in nested case
blanchet
parents: 53309
diff changeset
   138
            (if nn > 1 then [(inductN, [induct_thm], induct_attrs)] else [])
bd038e48526d have "datatype_new_compat" register induction and recursion theorems in nested case
blanchet
parents: 53309
diff changeset
   139
            |> filter_out (null o #2)
bd038e48526d have "datatype_new_compat" register induction and recursion theorems in nested case
blanchet
parents: 53309
diff changeset
   140
            |> map (fn (thmN, thms, attrs) =>
bd038e48526d have "datatype_new_compat" register induction and recursion theorems in nested case
blanchet
parents: 53309
diff changeset
   141
              ((Binding.qualify true common_name (Binding.name thmN), attrs), [(thms, [])]));
bd038e48526d have "datatype_new_compat" register induction and recursion theorems in nested case
blanchet
parents: 53309
diff changeset
   142
bd038e48526d have "datatype_new_compat" register induction and recursion theorems in nested case
blanchet
parents: 53309
diff changeset
   143
          val notes =
55856
bddaada24074 got rid of automatically generated fold constant and theorems (to reduce overhead)
blanchet
parents: 55772
diff changeset
   144
            [(inductN, map single induct_thms, induct_attrs),
55479
ece4910c3ea0 improved 'datatype_new_compat': generate more fixpoint equations for types like 'datatype_new x = C (x list) (x list)' (here, one equation for each x list instead of a single for both), for higher compatibility + code generation attributes on the recursor
blanchet
parents: 55409
diff changeset
   145
             (recN, rec_thmss, code_nitpicksimp_simp_attrs)]
53746
bd038e48526d have "datatype_new_compat" register induction and recursion theorems in nested case
blanchet
parents: 53309
diff changeset
   146
            |> filter_out (null o #2)
bd038e48526d have "datatype_new_compat" register induction and recursion theorems in nested case
blanchet
parents: 53309
diff changeset
   147
            |> maps (fn (thmN, thmss, attrs) =>
bd038e48526d have "datatype_new_compat" register induction and recursion theorems in nested case
blanchet
parents: 53309
diff changeset
   148
              if forall null thmss then
bd038e48526d have "datatype_new_compat" register induction and recursion theorems in nested case
blanchet
parents: 53309
diff changeset
   149
                []
bd038e48526d have "datatype_new_compat" register induction and recursion theorems in nested case
blanchet
parents: 53309
diff changeset
   150
              else
bd038e48526d have "datatype_new_compat" register induction and recursion theorems in nested case
blanchet
parents: 53309
diff changeset
   151
                map2 (fn b_name => fn thms =>
bd038e48526d have "datatype_new_compat" register induction and recursion theorems in nested case
blanchet
parents: 53309
diff changeset
   152
                    ((Binding.qualify true b_name (Binding.name thmN), attrs), [(thms, [])]))
bd038e48526d have "datatype_new_compat" register induction and recursion theorems in nested case
blanchet
parents: 53309
diff changeset
   153
                  compat_b_names thmss);
bd038e48526d have "datatype_new_compat" register induction and recursion theorems in nested case
blanchet
parents: 53309
diff changeset
   154
        in
bd038e48526d have "datatype_new_compat" register induction and recursion theorems in nested case
blanchet
parents: 53309
diff changeset
   155
          common_notes @ notes
bd038e48526d have "datatype_new_compat" register induction and recursion theorems in nested case
blanchet
parents: 53309
diff changeset
   156
        end);
bd038e48526d have "datatype_new_compat" register induction and recursion theorems in nested case
blanchet
parents: 53309
diff changeset
   157
bd038e48526d have "datatype_new_compat" register induction and recursion theorems in nested case
blanchet
parents: 53309
diff changeset
   158
    val register_interpret =
53303
ae49b835ca01 moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff changeset
   159
      Datatype_Data.register infos
ae49b835ca01 moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff changeset
   160
      #> Datatype_Data.interpretation_data (Datatype_Aux.default_config, map fst infos)
ae49b835ca01 moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff changeset
   161
  in
53746
bd038e48526d have "datatype_new_compat" register induction and recursion theorems in nested case
blanchet
parents: 53309
diff changeset
   162
    lthy
bd038e48526d have "datatype_new_compat" register induction and recursion theorems in nested case
blanchet
parents: 53309
diff changeset
   163
    |> Local_Theory.raw_theory register_interpret
bd038e48526d have "datatype_new_compat" register induction and recursion theorems in nested case
blanchet
parents: 53309
diff changeset
   164
    |> Local_Theory.notes all_notes |> snd
53303
ae49b835ca01 moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff changeset
   165
  end;
ae49b835ca01 moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff changeset
   166
ae49b835ca01 moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff changeset
   167
val _ =
55531
601ca8efa000 renamed 'datatype_new_compat' to 'datatype_compat'
blanchet
parents: 55486
diff changeset
   168
  Outer_Syntax.local_theory @{command_spec "datatype_compat"}
54025
70bc41e7a91e tuned command descriptions
blanchet
parents: 54009
diff changeset
   169
    "register new-style datatypes as old-style datatypes"
55531
601ca8efa000 renamed 'datatype_new_compat' to 'datatype_compat'
blanchet
parents: 55486
diff changeset
   170
    (Scan.repeat1 Parse.type_const >> datatype_compat_cmd);
53303
ae49b835ca01 moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff changeset
   171
ae49b835ca01 moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff changeset
   172
end;