src/HOL/Tools/BNF/bnf_lfp_compat.ML
author blanchet
Mon, 01 Sep 2014 19:58:25 +0200
changeset 58133 c7cc358a6972
parent 58131 1abeda3c3bc2
child 58137 feb69891e0fd
permissions -rw-r--r--
avoid more 'bad background theory' issues
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
58117
9608028d8f43 more compatibility between old- and new-style datatypes
blanchet
parents: 58113
diff changeset
     3
    Copyright   2013, 2014
53303
ae49b835ca01 moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff changeset
     4
58119
blanchet
parents: 58117
diff changeset
     5
Compatibility layer with the old datatype package. Parly based on:
blanchet
parents: 58117
diff changeset
     6
blanchet
parents: 58117
diff changeset
     7
    Title:      HOL/Tools/Old_Datatype/old_datatype_data.ML
blanchet
parents: 58117
diff changeset
     8
    Author:     Stefan Berghofer, TU Muenchen
53303
ae49b835ca01 moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff changeset
     9
*)
ae49b835ca01 moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff changeset
    10
ae49b835ca01 moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff changeset
    11
signature BNF_LFP_COMPAT =
ae49b835ca01 moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff changeset
    12
sig
58125
a2ba381607fb more work on compatibility interfaces
blanchet
parents: 58123
diff changeset
    13
  datatype nesting_preference = Keep_Nesting | Unfold_Nesting
58123
62765d39539f implemented compatibility definition of datatype
blanchet
parents: 58122
diff changeset
    14
58125
a2ba381607fb more work on compatibility interfaces
blanchet
parents: 58123
diff changeset
    15
  val get_all: theory -> nesting_preference -> Old_Datatype_Aux.info Symtab.table
a2ba381607fb more work on compatibility interfaces
blanchet
parents: 58123
diff changeset
    16
  val get_info: theory -> nesting_preference -> string -> Old_Datatype_Aux.info option
a2ba381607fb more work on compatibility interfaces
blanchet
parents: 58123
diff changeset
    17
  val the_info: theory -> nesting_preference -> string -> Old_Datatype_Aux.info
58129
3ec65a7f2b50 ported Refute to use new datatypes when possible
blanchet
parents: 58126
diff changeset
    18
  val the_spec: theory -> string -> (string * sort) list * (string * typ list) list
58125
a2ba381607fb more work on compatibility interfaces
blanchet
parents: 58123
diff changeset
    19
  val the_descr: theory -> nesting_preference -> string list ->
58117
9608028d8f43 more compatibility between old- and new-style datatypes
blanchet
parents: 58113
diff changeset
    20
    Old_Datatype_Aux.descr * (string * sort) list * string list * string
9608028d8f43 more compatibility between old- and new-style datatypes
blanchet
parents: 58113
diff changeset
    21
    * (string list * string list) * (typ list * typ list)
58129
3ec65a7f2b50 ported Refute to use new datatypes when possible
blanchet
parents: 58126
diff changeset
    22
  val get_constrs: theory -> string -> (string * typ) list option
58125
a2ba381607fb more work on compatibility interfaces
blanchet
parents: 58123
diff changeset
    23
  val interpretation: nesting_preference ->
58123
62765d39539f implemented compatibility definition of datatype
blanchet
parents: 58122
diff changeset
    24
    (Old_Datatype_Aux.config -> string list -> theory -> theory) -> theory -> theory
58125
a2ba381607fb more work on compatibility interfaces
blanchet
parents: 58123
diff changeset
    25
  val datatype_compat: string list -> local_theory -> local_theory
a2ba381607fb more work on compatibility interfaces
blanchet
parents: 58123
diff changeset
    26
  val datatype_compat_global: string list -> theory -> theory
58117
9608028d8f43 more compatibility between old- and new-style datatypes
blanchet
parents: 58113
diff changeset
    27
  val datatype_compat_cmd: string list -> local_theory -> local_theory
58125
a2ba381607fb more work on compatibility interfaces
blanchet
parents: 58123
diff changeset
    28
  val add_datatype: nesting_preference -> Old_Datatype_Aux.spec list -> theory ->
a2ba381607fb more work on compatibility interfaces
blanchet
parents: 58123
diff changeset
    29
    string list * theory
58126
3831312eb476 added primrec compatibility function
blanchet
parents: 58125
diff changeset
    30
  val add_primrec: (binding * typ option * mixfix) list -> (Attrib.binding * term) list ->
3831312eb476 added primrec compatibility function
blanchet
parents: 58125
diff changeset
    31
   local_theory -> (term list * thm list) * local_theory
53303
ae49b835ca01 moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff changeset
    32
end;
ae49b835ca01 moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff changeset
    33
ae49b835ca01 moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff changeset
    34
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
    35
struct
ae49b835ca01 moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff changeset
    36
54006
9fe1bd54d437 renamed theory file
blanchet
parents: 54003
diff changeset
    37
open Ctr_Sugar
53303
ae49b835ca01 moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff changeset
    38
open BNF_Util
ae49b835ca01 moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff changeset
    39
open BNF_FP_Util
ae49b835ca01 moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff changeset
    40
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
    41
open BNF_FP_N2M_Sugar
58123
62765d39539f implemented compatibility definition of datatype
blanchet
parents: 58122
diff changeset
    42
open BNF_LFP
53303
ae49b835ca01 moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff changeset
    43
ae49b835ca01 moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff changeset
    44
val compatN = "compat_";
ae49b835ca01 moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff changeset
    45
58125
a2ba381607fb more work on compatibility interfaces
blanchet
parents: 58123
diff changeset
    46
datatype nesting_preference = Keep_Nesting | Unfold_Nesting;
58123
62765d39539f implemented compatibility definition of datatype
blanchet
parents: 58122
diff changeset
    47
56453
00548d372f02 support deeply nested datatypes in 'datatype_compat'
blanchet
parents: 56452
diff changeset
    48
fun reindex_desc desc =
00548d372f02 support deeply nested datatypes in 'datatype_compat'
blanchet
parents: 56452
diff changeset
    49
  let
00548d372f02 support deeply nested datatypes in 'datatype_compat'
blanchet
parents: 56452
diff changeset
    50
    val kks = map fst desc;
00548d372f02 support deeply nested datatypes in 'datatype_compat'
blanchet
parents: 56452
diff changeset
    51
    val perm_kks = sort int_ord kks;
00548d372f02 support deeply nested datatypes in 'datatype_compat'
blanchet
parents: 56452
diff changeset
    52
58112
8081087096ad renamed modules defining old datatypes, as a step towards having 'datatype_new' take 'datatype's place
blanchet
parents: 57983
diff changeset
    53
    fun perm_dtyp (Old_Datatype_Aux.DtType (s, Ds)) = Old_Datatype_Aux.DtType (s, map perm_dtyp Ds)
8081087096ad renamed modules defining old datatypes, as a step towards having 'datatype_new' take 'datatype's place
blanchet
parents: 57983
diff changeset
    54
      | perm_dtyp (Old_Datatype_Aux.DtRec kk) =
8081087096ad renamed modules defining old datatypes, as a step towards having 'datatype_new' take 'datatype's place
blanchet
parents: 57983
diff changeset
    55
        Old_Datatype_Aux.DtRec (find_index (curry (op =) kk) kks)
58113
blanchet
parents: 58112
diff changeset
    56
      | perm_dtyp D = D;
56453
00548d372f02 support deeply nested datatypes in 'datatype_compat'
blanchet
parents: 56452
diff changeset
    57
  in
00548d372f02 support deeply nested datatypes in 'datatype_compat'
blanchet
parents: 56452
diff changeset
    58
    if perm_kks = kks then
00548d372f02 support deeply nested datatypes in 'datatype_compat'
blanchet
parents: 56452
diff changeset
    59
      desc
00548d372f02 support deeply nested datatypes in 'datatype_compat'
blanchet
parents: 56452
diff changeset
    60
    else
00548d372f02 support deeply nested datatypes in 'datatype_compat'
blanchet
parents: 56452
diff changeset
    61
      perm_kks ~~
00548d372f02 support deeply nested datatypes in 'datatype_compat'
blanchet
parents: 56452
diff changeset
    62
      map (fn (_, (s, Ds, sDss)) => (s, map perm_dtyp Ds, map (apsnd (map perm_dtyp)) sDss)) desc
58113
blanchet
parents: 58112
diff changeset
    63
  end;
56453
00548d372f02 support deeply nested datatypes in 'datatype_compat'
blanchet
parents: 56452
diff changeset
    64
58131
1abeda3c3bc2 drop hopeless feature -- unfolding of BNF datatype info without a prior 'datatype_compat'
blanchet
parents: 58130
diff changeset
    65
fun mk_infos_of_mutually_recursive_new_datatypes nesting_pref check_names fpT_names0 lthy =
53303
ae49b835ca01 moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff changeset
    66
  let
ae49b835ca01 moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff changeset
    67
    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
    68
ae49b835ca01 moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff changeset
    69
    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
    70
    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
    71
      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
    72
ae49b835ca01 moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff changeset
    73
    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
    74
      (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
    75
        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
    76
      | _ => not_datatype s);
ae49b835ca01 moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff changeset
    77
56455
1ff66e72628b allow arguments to 'datatype_compat' in disorder
blanchet
parents: 56453
diff changeset
    78
    val fpTs0 as Type (_, var_As) :: _ = #Ts (#fp_res (lfp_sugar_of (hd fpT_names0)));
1ff66e72628b allow arguments to 'datatype_compat' in disorder
blanchet
parents: 56453
diff changeset
    79
    val fpT_names = map (fst o dest_Type) fpTs0;
53303
ae49b835ca01 moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff changeset
    80
58117
9608028d8f43 more compatibility between old- and new-style datatypes
blanchet
parents: 58113
diff changeset
    81
    val _ = check_names (op =) (fpT_names0, fpT_names) orelse not_mutually_recursive fpT_names0;
53303
ae49b835ca01 moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff changeset
    82
58117
9608028d8f43 more compatibility between old- and new-style datatypes
blanchet
parents: 58113
diff changeset
    83
    val (As_names, _) = Variable.variant_fixes (map (fn TVar ((s, _), _) => s) var_As) lthy;
56452
0c98c9118407 preserve user type variable names to avoid mismatches/confusion
blanchet
parents: 56002
diff changeset
    84
    val As = map2 (fn s => fn TVar (_, S) => TFree (s, S)) As_names var_As;
56455
1ff66e72628b allow arguments to 'datatype_compat' in disorder
blanchet
parents: 56453
diff changeset
    85
    val fpTs = map (fn s => Type (s, As)) fpT_names;
56453
00548d372f02 support deeply nested datatypes in 'datatype_compat'
blanchet
parents: 56452
diff changeset
    86
00548d372f02 support deeply nested datatypes in 'datatype_compat'
blanchet
parents: 56452
diff changeset
    87
    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
    88
58112
8081087096ad renamed modules defining old datatypes, as a step towards having 'datatype_new' take 'datatype's place
blanchet
parents: 57983
diff changeset
    89
    val mk_dtyp = Old_Datatype_Aux.dtyp_of_typ (map (apsnd (map Term.dest_TFree) o dest_Type) fpTs);
56453
00548d372f02 support deeply nested datatypes in 'datatype_compat'
blanchet
parents: 56452
diff changeset
    90
00548d372f02 support deeply nested datatypes in 'datatype_compat'
blanchet
parents: 56452
diff changeset
    91
    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
    92
    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
    93
      (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
    94
56455
1ff66e72628b allow arguments to 'datatype_compat' in disorder
blanchet
parents: 56453
diff changeset
    95
    val fp_ctr_sugars = map (#ctr_sugar o lfp_sugar_of) fpT_names;
56453
00548d372f02 support deeply nested datatypes in 'datatype_compat'
blanchet
parents: 56452
diff changeset
    96
    val orig_descr = map3 mk_typ_descr (0 upto nn_fp - 1) fpTs fp_ctr_sugars;
58112
8081087096ad renamed modules defining old datatypes, as a step towards having 'datatype_new' take 'datatype's place
blanchet
parents: 57983
diff changeset
    97
    val all_infos = Old_Datatype_Data.get_all thy;
58117
9608028d8f43 more compatibility between old- and new-style datatypes
blanchet
parents: 58113
diff changeset
    98
    val (orig_descr' :: nested_descrs) =
58125
a2ba381607fb more work on compatibility interfaces
blanchet
parents: 58123
diff changeset
    99
      if nesting_pref = Keep_Nesting then [orig_descr]
a2ba381607fb more work on compatibility interfaces
blanchet
parents: 58123
diff changeset
   100
      else fst (Old_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
   101
57798
018dc778cbcc more correct clique computation for N2M
blanchet
parents: 57794
diff changeset
   102
    fun cliquify_descr [] = []
018dc778cbcc more correct clique computation for N2M
blanchet
parents: 57794
diff changeset
   103
      | cliquify_descr [entry] = [[entry]]
018dc778cbcc more correct clique computation for N2M
blanchet
parents: 57794
diff changeset
   104
      | cliquify_descr (full_descr as (_, (T_name1, _, _)) :: _) =
018dc778cbcc more correct clique computation for N2M
blanchet
parents: 57794
diff changeset
   105
        let
018dc778cbcc more correct clique computation for N2M
blanchet
parents: 57794
diff changeset
   106
          val nn =
018dc778cbcc more correct clique computation for N2M
blanchet
parents: 57794
diff changeset
   107
            if member (op =) fpT_names T_name1 then
018dc778cbcc more correct clique computation for N2M
blanchet
parents: 57794
diff changeset
   108
              nn_fp
018dc778cbcc more correct clique computation for N2M
blanchet
parents: 57794
diff changeset
   109
            else
018dc778cbcc more correct clique computation for N2M
blanchet
parents: 57794
diff changeset
   110
              (case Symtab.lookup all_infos T_name1 of
018dc778cbcc more correct clique computation for N2M
blanchet
parents: 57794
diff changeset
   111
                SOME {descr, ...} =>
58112
8081087096ad renamed modules defining old datatypes, as a step towards having 'datatype_new' take 'datatype's place
blanchet
parents: 57983
diff changeset
   112
                length (filter_out (exists Old_Datatype_Aux.is_rec_type o #2 o snd) descr)
57798
018dc778cbcc more correct clique computation for N2M
blanchet
parents: 57794
diff changeset
   113
              | NONE => raise Fail "unknown old-style datatype");
018dc778cbcc more correct clique computation for N2M
blanchet
parents: 57794
diff changeset
   114
        in
018dc778cbcc more correct clique computation for N2M
blanchet
parents: 57794
diff changeset
   115
          chop nn full_descr ||> cliquify_descr |> op ::
018dc778cbcc more correct clique computation for N2M
blanchet
parents: 57794
diff changeset
   116
        end;
018dc778cbcc more correct clique computation for N2M
blanchet
parents: 57794
diff changeset
   117
56453
00548d372f02 support deeply nested datatypes in 'datatype_compat'
blanchet
parents: 56452
diff changeset
   118
    (* put nested types before the types that nest them, as needed for N2M *)
56484
c451cf8b29c8 thread mutual cliques through
blanchet
parents: 56455
diff changeset
   119
    val descrs = burrow reindex_desc (orig_descr' :: rev nested_descrs);
c451cf8b29c8 thread mutual cliques through
blanchet
parents: 56455
diff changeset
   120
    val (cliques, descr) =
57798
018dc778cbcc more correct clique computation for N2M
blanchet
parents: 57794
diff changeset
   121
      split_list (flat (map_index (fn (i, descr) => map (pair i) descr)
018dc778cbcc more correct clique computation for N2M
blanchet
parents: 57794
diff changeset
   122
        (maps cliquify_descr descrs)));
53303
ae49b835ca01 moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff changeset
   123
58112
8081087096ad renamed modules defining old datatypes, as a step towards having 'datatype_new' take 'datatype's place
blanchet
parents: 57983
diff changeset
   124
    val dest_dtyp = Old_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
   125
58112
8081087096ad renamed modules defining old datatypes, as a step towards having 'datatype_new' take 'datatype's place
blanchet
parents: 57983
diff changeset
   126
    val Ts = Old_Datatype_Aux.get_rec_types descr;
56453
00548d372f02 support deeply nested datatypes in 'datatype_compat'
blanchet
parents: 56452
diff changeset
   127
    val nn = length Ts;
55485
bdfb607543f4 better handling of recursion through functions
blanchet
parents: 55481
diff changeset
   128
bdfb607543f4 better handling of recursion through functions
blanchet
parents: 55481
diff changeset
   129
    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
   130
    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
   131
    val kkssss =
58112
8081087096ad renamed modules defining old datatypes, as a step towards having 'datatype_new' take 'datatype's place
blanchet
parents: 57983
diff changeset
   132
      map (map (map (fn Old_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
   133
55772
367ec44763fd correct most general type for mutual recursion when several identical types are involved
blanchet
parents: 55571
diff changeset
   134
    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
   135
367ec44763fd correct most general type for mutual recursion when several identical types are involved
blanchet
parents: 55571
diff changeset
   136
    fun apply_comps n kk =
55966
972f0aa7091b balance tuples that represent curried functions
blanchet
parents: 55951
diff changeset
   137
      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
   138
367ec44763fd correct most general type for mutual recursion when several identical types are involved
blanchet
parents: 55571
diff changeset
   139
    val callssss =
56453
00548d372f02 support deeply nested datatypes in 'datatype_compat'
blanchet
parents: 56452
diff changeset
   140
      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
   141
00548d372f02 support deeply nested datatypes in 'datatype_compat'
blanchet
parents: 56452
diff changeset
   142
    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
   143
    val compat_b_names = map (prefix compatN) b_names;
00548d372f02 support deeply nested datatypes in 'datatype_compat'
blanchet
parents: 56452
diff changeset
   144
    val compat_bs = map Binding.name compat_b_names;
55772
367ec44763fd correct most general type for mutual recursion when several identical types are involved
blanchet
parents: 55571
diff changeset
   145
58117
9608028d8f43 more compatibility between old- and new-style datatypes
blanchet
parents: 58113
diff changeset
   146
    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
   147
      if nn > nn_fp then
58131
1abeda3c3bc2 drop hopeless feature -- unfolding of BNF datatype info without a prior 'datatype_compat'
blanchet
parents: 58130
diff changeset
   148
        mutualize_fp_sugars Least_FP cliques 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
   149
      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
   150
        ((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
   151
56453
00548d372f02 support deeply nested datatypes in 'datatype_compat'
blanchet
parents: 56452
diff changeset
   152
    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
   153
    val rec_thms = maps #co_rec_thms fp_sugars;
00548d372f02 support deeply nested datatypes in 'datatype_compat'
blanchet
parents: 56452
diff changeset
   154
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
   155
    val {common_co_inducts = [induct], ...} :: _ = fp_sugars;
55539
0819931d652d simplified data structure by reducing the incidence of clumsy indices
blanchet
parents: 55531
diff changeset
   156
    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
   157
55567
blanchet
parents: 55540
diff changeset
   158
    fun mk_info (kk, {T = Type (T_name0, _), ctr_sugar = {casex, exhaust, nchotomy, injects,
57983
6edc3529bb4e reordered some (co)datatype property names for more consistency
blanchet
parents: 57807
diff changeset
   159
        distincts, case_thms, case_cong, case_cong_weak, split, split_asm, ...}, ...} : fp_sugar) =
55539
0819931d652d simplified data structure by reducing the incidence of clumsy indices
blanchet
parents: 55531
diff changeset
   160
      (T_name0,
0819931d652d simplified data structure by reducing the incidence of clumsy indices
blanchet
parents: 55531
diff changeset
   161
       {index = kk, descr = descr, inject = injects, distinct = distincts, induct = induct,
57794
73052169b213 tuning whitespace
blanchet
parents: 57633
diff changeset
   162
        inducts = inducts, exhaust = exhaust, nchotomy = nchotomy, rec_names = recs,
73052169b213 tuning whitespace
blanchet
parents: 57633
diff changeset
   163
        rec_rewrites = rec_thms, case_name = fst (dest_Const casex), case_rewrites = case_thms,
57983
6edc3529bb4e reordered some (co)datatype property names for more consistency
blanchet
parents: 57807
diff changeset
   164
        case_cong = case_cong, case_cong_weak = case_cong_weak, split = split,
57794
73052169b213 tuning whitespace
blanchet
parents: 57633
diff changeset
   165
        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
   166
55539
0819931d652d simplified data structure by reducing the incidence of clumsy indices
blanchet
parents: 55531
diff changeset
   167
    val infos = map_index mk_info (take nn_fp fp_sugars);
58117
9608028d8f43 more compatibility between old- and new-style datatypes
blanchet
parents: 58113
diff changeset
   168
  in
9608028d8f43 more compatibility between old- and new-style datatypes
blanchet
parents: 58113
diff changeset
   169
    (nn, b_names, compat_b_names, lfp_sugar_thms, infos, lthy')
9608028d8f43 more compatibility between old- and new-style datatypes
blanchet
parents: 58113
diff changeset
   170
  end;
9608028d8f43 more compatibility between old- and new-style datatypes
blanchet
parents: 58113
diff changeset
   171
58131
1abeda3c3bc2 drop hopeless feature -- unfolding of BNF datatype info without a prior 'datatype_compat'
blanchet
parents: 58130
diff changeset
   172
fun infos_of_new_datatype_mutual_cluster lthy fpT_name =
1abeda3c3bc2 drop hopeless feature -- unfolding of BNF datatype info without a prior 'datatype_compat'
blanchet
parents: 58130
diff changeset
   173
  #5 (mk_infos_of_mutually_recursive_new_datatypes Keep_Nesting subset [fpT_name] lthy)
1abeda3c3bc2 drop hopeless feature -- unfolding of BNF datatype info without a prior 'datatype_compat'
blanchet
parents: 58130
diff changeset
   174
  handle ERROR _ => [];
58117
9608028d8f43 more compatibility between old- and new-style datatypes
blanchet
parents: 58113
diff changeset
   175
58125
a2ba381607fb more work on compatibility interfaces
blanchet
parents: 58123
diff changeset
   176
fun get_all thy nesting_pref =
58117
9608028d8f43 more compatibility between old- and new-style datatypes
blanchet
parents: 58113
diff changeset
   177
  let
58133
c7cc358a6972 avoid more 'bad background theory' issues
blanchet
parents: 58131
diff changeset
   178
    val lthy = Proof_Context.init_global thy;
58117
9608028d8f43 more compatibility between old- and new-style datatypes
blanchet
parents: 58113
diff changeset
   179
    val old_info_tab = Old_Datatype_Data.get_all thy;
9608028d8f43 more compatibility between old- and new-style datatypes
blanchet
parents: 58113
diff changeset
   180
    val new_T_names = BNF_FP_Def_Sugar.fp_sugars_of_global thy
9608028d8f43 more compatibility between old- and new-style datatypes
blanchet
parents: 58113
diff changeset
   181
      |> map_filter (try (fn {T = Type (s, _), fp_res_index = 0, ...} => s));
58131
1abeda3c3bc2 drop hopeless feature -- unfolding of BNF datatype info without a prior 'datatype_compat'
blanchet
parents: 58130
diff changeset
   182
    val new_infos = maps (infos_of_new_datatype_mutual_cluster lthy) new_T_names;
58117
9608028d8f43 more compatibility between old- and new-style datatypes
blanchet
parents: 58113
diff changeset
   183
  in
58125
a2ba381607fb more work on compatibility interfaces
blanchet
parents: 58123
diff changeset
   184
    fold (if nesting_pref = Keep_Nesting then Symtab.update else Symtab.default) new_infos
58123
62765d39539f implemented compatibility definition of datatype
blanchet
parents: 58122
diff changeset
   185
      old_info_tab
58117
9608028d8f43 more compatibility between old- and new-style datatypes
blanchet
parents: 58113
diff changeset
   186
  end;
9608028d8f43 more compatibility between old- and new-style datatypes
blanchet
parents: 58113
diff changeset
   187
58125
a2ba381607fb more work on compatibility interfaces
blanchet
parents: 58123
diff changeset
   188
fun get_one get_old get_new thy nesting_pref x =
58131
1abeda3c3bc2 drop hopeless feature -- unfolding of BNF datatype info without a prior 'datatype_compat'
blanchet
parents: 58130
diff changeset
   189
  let val (get_fst, get_snd) = (get_old thy, get_new thy) |> nesting_pref = Keep_Nesting ? swap in
58117
9608028d8f43 more compatibility between old- and new-style datatypes
blanchet
parents: 58113
diff changeset
   190
    (case get_fst x of NONE => get_snd x | res => res)
9608028d8f43 more compatibility between old- and new-style datatypes
blanchet
parents: 58113
diff changeset
   191
  end;
9608028d8f43 more compatibility between old- and new-style datatypes
blanchet
parents: 58113
diff changeset
   192
58131
1abeda3c3bc2 drop hopeless feature -- unfolding of BNF datatype info without a prior 'datatype_compat'
blanchet
parents: 58130
diff changeset
   193
fun get_info_of_new_datatype thy T_name =
58130
5e9170812356 ported to use new-style datatypes
blanchet
parents: 58129
diff changeset
   194
  let val lthy = Proof_Context.init_global thy in
58131
1abeda3c3bc2 drop hopeless feature -- unfolding of BNF datatype info without a prior 'datatype_compat'
blanchet
parents: 58130
diff changeset
   195
    AList.lookup (op =) (infos_of_new_datatype_mutual_cluster lthy T_name) T_name
58117
9608028d8f43 more compatibility between old- and new-style datatypes
blanchet
parents: 58113
diff changeset
   196
  end;
9608028d8f43 more compatibility between old- and new-style datatypes
blanchet
parents: 58113
diff changeset
   197
9608028d8f43 more compatibility between old- and new-style datatypes
blanchet
parents: 58113
diff changeset
   198
val get_info = get_one Old_Datatype_Data.get_info get_info_of_new_datatype;
9608028d8f43 more compatibility between old- and new-style datatypes
blanchet
parents: 58113
diff changeset
   199
58125
a2ba381607fb more work on compatibility interfaces
blanchet
parents: 58123
diff changeset
   200
fun the_info thy nesting_pref T_name =
a2ba381607fb more work on compatibility interfaces
blanchet
parents: 58123
diff changeset
   201
  (case get_info thy nesting_pref T_name of
58117
9608028d8f43 more compatibility between old- and new-style datatypes
blanchet
parents: 58113
diff changeset
   202
    SOME info => info
9608028d8f43 more compatibility between old- and new-style datatypes
blanchet
parents: 58113
diff changeset
   203
  | NONE => error ("Unknown datatype " ^ quote T_name));
9608028d8f43 more compatibility between old- and new-style datatypes
blanchet
parents: 58113
diff changeset
   204
58129
3ec65a7f2b50 ported Refute to use new datatypes when possible
blanchet
parents: 58126
diff changeset
   205
fun the_spec thy T_name =
58117
9608028d8f43 more compatibility between old- and new-style datatypes
blanchet
parents: 58113
diff changeset
   206
  let
58129
3ec65a7f2b50 ported Refute to use new datatypes when possible
blanchet
parents: 58126
diff changeset
   207
    val {descr, index, ...} = the_info thy Keep_Nesting T_name;
58117
9608028d8f43 more compatibility between old- and new-style datatypes
blanchet
parents: 58113
diff changeset
   208
    val (_, Ds, ctrs0) = the (AList.lookup (op =) descr index);
58129
3ec65a7f2b50 ported Refute to use new datatypes when possible
blanchet
parents: 58126
diff changeset
   209
    val tfrees = map Old_Datatype_Aux.dest_DtTFree Ds;
58117
9608028d8f43 more compatibility between old- and new-style datatypes
blanchet
parents: 58113
diff changeset
   210
    val ctrs = map (apsnd (map (Old_Datatype_Aux.typ_of_dtyp descr))) ctrs0;
58129
3ec65a7f2b50 ported Refute to use new datatypes when possible
blanchet
parents: 58126
diff changeset
   211
  in (tfrees, ctrs) end;
58117
9608028d8f43 more compatibility between old- and new-style datatypes
blanchet
parents: 58113
diff changeset
   212
58125
a2ba381607fb more work on compatibility interfaces
blanchet
parents: 58123
diff changeset
   213
fun the_descr thy nesting_pref (T_names0 as T_name01 :: _) =
58117
9608028d8f43 more compatibility between old- and new-style datatypes
blanchet
parents: 58113
diff changeset
   214
  let
9608028d8f43 more compatibility between old- and new-style datatypes
blanchet
parents: 58113
diff changeset
   215
    fun not_mutually_recursive ss =
9608028d8f43 more compatibility between old- and new-style datatypes
blanchet
parents: 58113
diff changeset
   216
      error ("{" ^ commas ss ^ "} is not a complete set of mutually recursive datatypes");
9608028d8f43 more compatibility between old- and new-style datatypes
blanchet
parents: 58113
diff changeset
   217
58125
a2ba381607fb more work on compatibility interfaces
blanchet
parents: 58123
diff changeset
   218
    val info = the_info thy nesting_pref T_name01;
58117
9608028d8f43 more compatibility between old- and new-style datatypes
blanchet
parents: 58113
diff changeset
   219
    val descr = #descr info;
9608028d8f43 more compatibility between old- and new-style datatypes
blanchet
parents: 58113
diff changeset
   220
9608028d8f43 more compatibility between old- and new-style datatypes
blanchet
parents: 58113
diff changeset
   221
    val (_, Ds, _) = the (AList.lookup (op =) descr (#index info));
9608028d8f43 more compatibility between old- and new-style datatypes
blanchet
parents: 58113
diff changeset
   222
    val vs = map Old_Datatype_Aux.dest_DtTFree Ds;
9608028d8f43 more compatibility between old- and new-style datatypes
blanchet
parents: 58113
diff changeset
   223
9608028d8f43 more compatibility between old- and new-style datatypes
blanchet
parents: 58113
diff changeset
   224
    fun is_DtTFree (Old_Datatype_Aux.DtTFree _) = true
9608028d8f43 more compatibility between old- and new-style datatypes
blanchet
parents: 58113
diff changeset
   225
      | is_DtTFree _ = false;
9608028d8f43 more compatibility between old- and new-style datatypes
blanchet
parents: 58113
diff changeset
   226
9608028d8f43 more compatibility between old- and new-style datatypes
blanchet
parents: 58113
diff changeset
   227
    val k = find_index (fn (_, (_, dTs, _)) => not (forall is_DtTFree dTs)) descr;
9608028d8f43 more compatibility between old- and new-style datatypes
blanchet
parents: 58113
diff changeset
   228
    val protoTs as (dataTs, _) = chop k descr
9608028d8f43 more compatibility between old- and new-style datatypes
blanchet
parents: 58113
diff changeset
   229
      |> (pairself o map)
9608028d8f43 more compatibility between old- and new-style datatypes
blanchet
parents: 58113
diff changeset
   230
        (fn (_, (T_name, Ds, _)) => (T_name, map (Old_Datatype_Aux.typ_of_dtyp descr) Ds));
9608028d8f43 more compatibility between old- and new-style datatypes
blanchet
parents: 58113
diff changeset
   231
9608028d8f43 more compatibility between old- and new-style datatypes
blanchet
parents: 58113
diff changeset
   232
    val T_names = map fst dataTs;
9608028d8f43 more compatibility between old- and new-style datatypes
blanchet
parents: 58113
diff changeset
   233
    val _ = eq_set (op =) (T_names, T_names0) orelse not_mutually_recursive T_names0
9608028d8f43 more compatibility between old- and new-style datatypes
blanchet
parents: 58113
diff changeset
   234
9608028d8f43 more compatibility between old- and new-style datatypes
blanchet
parents: 58113
diff changeset
   235
    val (Ts, Us) = (pairself o map) Type protoTs;
9608028d8f43 more compatibility between old- and new-style datatypes
blanchet
parents: 58113
diff changeset
   236
9608028d8f43 more compatibility between old- and new-style datatypes
blanchet
parents: 58113
diff changeset
   237
    val names = map Long_Name.base_name T_names;
9608028d8f43 more compatibility between old- and new-style datatypes
blanchet
parents: 58113
diff changeset
   238
    val (auxnames, _) = Name.make_context names
9608028d8f43 more compatibility between old- and new-style datatypes
blanchet
parents: 58113
diff changeset
   239
      |> fold_map (Name.variant o Old_Datatype_Aux.name_of_typ) Us;
9608028d8f43 more compatibility between old- and new-style datatypes
blanchet
parents: 58113
diff changeset
   240
    val prefix = space_implode "_" names;
9608028d8f43 more compatibility between old- and new-style datatypes
blanchet
parents: 58113
diff changeset
   241
  in
9608028d8f43 more compatibility between old- and new-style datatypes
blanchet
parents: 58113
diff changeset
   242
    (descr, vs, T_names, prefix, (names, auxnames), (Ts, Us))
9608028d8f43 more compatibility between old- and new-style datatypes
blanchet
parents: 58113
diff changeset
   243
  end;
9608028d8f43 more compatibility between old- and new-style datatypes
blanchet
parents: 58113
diff changeset
   244
58129
3ec65a7f2b50 ported Refute to use new datatypes when possible
blanchet
parents: 58126
diff changeset
   245
fun get_constrs thy T_name =
3ec65a7f2b50 ported Refute to use new datatypes when possible
blanchet
parents: 58126
diff changeset
   246
  try (the_spec thy) T_name
58119
blanchet
parents: 58117
diff changeset
   247
  |> Option.map (fn (tfrees, ctrs) =>
blanchet
parents: 58117
diff changeset
   248
    let
blanchet
parents: 58117
diff changeset
   249
      fun varify_tfree (s, S) = TVar ((s, 0), S);
blanchet
parents: 58117
diff changeset
   250
      fun varify_typ (TFree x) = varify_tfree x
blanchet
parents: 58117
diff changeset
   251
        | varify_typ T = T;
blanchet
parents: 58117
diff changeset
   252
blanchet
parents: 58117
diff changeset
   253
      val dataT = Type (T_name, map varify_tfree tfrees);
blanchet
parents: 58117
diff changeset
   254
blanchet
parents: 58117
diff changeset
   255
      fun mk_ctr_typ Ts = map (Term.map_atyps varify_typ) Ts ---> dataT;
blanchet
parents: 58117
diff changeset
   256
    in
blanchet
parents: 58117
diff changeset
   257
      map (apsnd mk_ctr_typ) ctrs
blanchet
parents: 58117
diff changeset
   258
    end);
58117
9608028d8f43 more compatibility between old- and new-style datatypes
blanchet
parents: 58113
diff changeset
   259
58125
a2ba381607fb more work on compatibility interfaces
blanchet
parents: 58123
diff changeset
   260
fun old_interpretation_of nesting_pref f config T_names thy =
a2ba381607fb more work on compatibility interfaces
blanchet
parents: 58123
diff changeset
   261
  if nesting_pref = Unfold_Nesting orelse exists (is_none o fp_sugar_of_global thy) T_names then
58122
eaac3e01158a implemented compatibility interpretation
blanchet
parents: 58119
diff changeset
   262
    f config T_names thy
eaac3e01158a implemented compatibility interpretation
blanchet
parents: 58119
diff changeset
   263
  else
eaac3e01158a implemented compatibility interpretation
blanchet
parents: 58119
diff changeset
   264
    thy;
eaac3e01158a implemented compatibility interpretation
blanchet
parents: 58119
diff changeset
   265
58125
a2ba381607fb more work on compatibility interfaces
blanchet
parents: 58123
diff changeset
   266
fun new_interpretation_of nesting_pref f fp_sugars thy =
58122
eaac3e01158a implemented compatibility interpretation
blanchet
parents: 58119
diff changeset
   267
  let val T_names = map (fst o dest_Type o #T) fp_sugars in
58125
a2ba381607fb more work on compatibility interfaces
blanchet
parents: 58123
diff changeset
   268
    if nesting_pref = Keep_Nesting orelse
58123
62765d39539f implemented compatibility definition of datatype
blanchet
parents: 58122
diff changeset
   269
        exists (is_none o Old_Datatype_Data.get_info thy) T_names then
62765d39539f implemented compatibility definition of datatype
blanchet
parents: 58122
diff changeset
   270
      f Old_Datatype_Aux.default_config T_names thy
58122
eaac3e01158a implemented compatibility interpretation
blanchet
parents: 58119
diff changeset
   271
    else
eaac3e01158a implemented compatibility interpretation
blanchet
parents: 58119
diff changeset
   272
      thy
eaac3e01158a implemented compatibility interpretation
blanchet
parents: 58119
diff changeset
   273
  end;
eaac3e01158a implemented compatibility interpretation
blanchet
parents: 58119
diff changeset
   274
58125
a2ba381607fb more work on compatibility interfaces
blanchet
parents: 58123
diff changeset
   275
fun interpretation nesting_pref f =
a2ba381607fb more work on compatibility interfaces
blanchet
parents: 58123
diff changeset
   276
  Old_Datatype_Data.interpretation (old_interpretation_of nesting_pref f)
a2ba381607fb more work on compatibility interfaces
blanchet
parents: 58123
diff changeset
   277
  #> fp_sugar_interpretation (new_interpretation_of nesting_pref f);
58117
9608028d8f43 more compatibility between old- and new-style datatypes
blanchet
parents: 58113
diff changeset
   278
9608028d8f43 more compatibility between old- and new-style datatypes
blanchet
parents: 58113
diff changeset
   279
val code_nitpicksimp_simp_attrs = Code.add_default_eqn_attrib :: @{attributes [nitpick_simp, simp]};
9608028d8f43 more compatibility between old- and new-style datatypes
blanchet
parents: 58113
diff changeset
   280
58125
a2ba381607fb more work on compatibility interfaces
blanchet
parents: 58123
diff changeset
   281
fun datatype_compat fpT_names lthy =
58117
9608028d8f43 more compatibility between old- and new-style datatypes
blanchet
parents: 58113
diff changeset
   282
  let
9608028d8f43 more compatibility between old- and new-style datatypes
blanchet
parents: 58113
diff changeset
   283
    val (nn, b_names, compat_b_names, lfp_sugar_thms, infos, lthy') =
58131
1abeda3c3bc2 drop hopeless feature -- unfolding of BNF datatype info without a prior 'datatype_compat'
blanchet
parents: 58130
diff changeset
   284
      mk_infos_of_mutually_recursive_new_datatypes Unfold_Nesting eq_set fpT_names lthy;
53303
ae49b835ca01 moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff changeset
   285
53746
bd038e48526d have "datatype_new_compat" register induction and recursion theorems in nested case
blanchet
parents: 53309
diff changeset
   286
    val all_notes =
bd038e48526d have "datatype_new_compat" register induction and recursion theorems in nested case
blanchet
parents: 53309
diff changeset
   287
      (case lfp_sugar_thms of
bd038e48526d have "datatype_new_compat" register induction and recursion theorems in nested case
blanchet
parents: 53309
diff changeset
   288
        NONE => []
55856
bddaada24074 got rid of automatically generated fold constant and theorems (to reduce overhead)
blanchet
parents: 55772
diff changeset
   289
      | 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
   290
        let
58117
9608028d8f43 more compatibility between old- and new-style datatypes
blanchet
parents: 58113
diff changeset
   291
          val common_name = compatN ^ mk_common_name b_names;
9608028d8f43 more compatibility between old- and new-style datatypes
blanchet
parents: 58113
diff changeset
   292
53746
bd038e48526d have "datatype_new_compat" register induction and recursion theorems in nested case
blanchet
parents: 53309
diff changeset
   293
          val common_notes =
bd038e48526d have "datatype_new_compat" register induction and recursion theorems in nested case
blanchet
parents: 53309
diff changeset
   294
            (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
   295
            |> filter_out (null o #2)
bd038e48526d have "datatype_new_compat" register induction and recursion theorems in nested case
blanchet
parents: 53309
diff changeset
   296
            |> map (fn (thmN, thms, attrs) =>
bd038e48526d have "datatype_new_compat" register induction and recursion theorems in nested case
blanchet
parents: 53309
diff changeset
   297
              ((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
   298
bd038e48526d have "datatype_new_compat" register induction and recursion theorems in nested case
blanchet
parents: 53309
diff changeset
   299
          val notes =
55856
bddaada24074 got rid of automatically generated fold constant and theorems (to reduce overhead)
blanchet
parents: 55772
diff changeset
   300
            [(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
   301
             (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
   302
            |> filter_out (null o #2)
bd038e48526d have "datatype_new_compat" register induction and recursion theorems in nested case
blanchet
parents: 53309
diff changeset
   303
            |> maps (fn (thmN, thmss, attrs) =>
bd038e48526d have "datatype_new_compat" register induction and recursion theorems in nested case
blanchet
parents: 53309
diff changeset
   304
              if forall null thmss then
bd038e48526d have "datatype_new_compat" register induction and recursion theorems in nested case
blanchet
parents: 53309
diff changeset
   305
                []
bd038e48526d have "datatype_new_compat" register induction and recursion theorems in nested case
blanchet
parents: 53309
diff changeset
   306
              else
bd038e48526d have "datatype_new_compat" register induction and recursion theorems in nested case
blanchet
parents: 53309
diff changeset
   307
                map2 (fn b_name => fn thms =>
bd038e48526d have "datatype_new_compat" register induction and recursion theorems in nested case
blanchet
parents: 53309
diff changeset
   308
                    ((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
   309
                  compat_b_names thmss);
bd038e48526d have "datatype_new_compat" register induction and recursion theorems in nested case
blanchet
parents: 53309
diff changeset
   310
        in
bd038e48526d have "datatype_new_compat" register induction and recursion theorems in nested case
blanchet
parents: 53309
diff changeset
   311
          common_notes @ notes
bd038e48526d have "datatype_new_compat" register induction and recursion theorems in nested case
blanchet
parents: 53309
diff changeset
   312
        end);
bd038e48526d have "datatype_new_compat" register induction and recursion theorems in nested case
blanchet
parents: 53309
diff changeset
   313
bd038e48526d have "datatype_new_compat" register induction and recursion theorems in nested case
blanchet
parents: 53309
diff changeset
   314
    val register_interpret =
58112
8081087096ad renamed modules defining old datatypes, as a step towards having 'datatype_new' take 'datatype's place
blanchet
parents: 57983
diff changeset
   315
      Old_Datatype_Data.register infos
58113
blanchet
parents: 58112
diff changeset
   316
      #> Old_Datatype_Data.interpretation_data (Old_Datatype_Aux.default_config, map fst infos);
53303
ae49b835ca01 moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff changeset
   317
  in
58117
9608028d8f43 more compatibility between old- and new-style datatypes
blanchet
parents: 58113
diff changeset
   318
    lthy'
53746
bd038e48526d have "datatype_new_compat" register induction and recursion theorems in nested case
blanchet
parents: 53309
diff changeset
   319
    |> Local_Theory.raw_theory register_interpret
57633
4ff8c090d580 repaired named derivations
blanchet
parents: 56484
diff changeset
   320
    |> Local_Theory.notes all_notes
4ff8c090d580 repaired named derivations
blanchet
parents: 56484
diff changeset
   321
    |> snd
53303
ae49b835ca01 moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff changeset
   322
  end;
ae49b835ca01 moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff changeset
   323
58125
a2ba381607fb more work on compatibility interfaces
blanchet
parents: 58123
diff changeset
   324
fun datatype_compat_global fpT_names =
a2ba381607fb more work on compatibility interfaces
blanchet
parents: 58123
diff changeset
   325
  Named_Target.theory_init
a2ba381607fb more work on compatibility interfaces
blanchet
parents: 58123
diff changeset
   326
  #> datatype_compat fpT_names
a2ba381607fb more work on compatibility interfaces
blanchet
parents: 58123
diff changeset
   327
  #> Named_Target.exit;
a2ba381607fb more work on compatibility interfaces
blanchet
parents: 58123
diff changeset
   328
a2ba381607fb more work on compatibility interfaces
blanchet
parents: 58123
diff changeset
   329
fun datatype_compat_cmd raw_fpT_names lthy =
a2ba381607fb more work on compatibility interfaces
blanchet
parents: 58123
diff changeset
   330
  let
a2ba381607fb more work on compatibility interfaces
blanchet
parents: 58123
diff changeset
   331
    val fpT_names =
a2ba381607fb more work on compatibility interfaces
blanchet
parents: 58123
diff changeset
   332
      map (fst o dest_Type o Proof_Context.read_type_name {proper = true, strict = false} lthy)
a2ba381607fb more work on compatibility interfaces
blanchet
parents: 58123
diff changeset
   333
        raw_fpT_names;
a2ba381607fb more work on compatibility interfaces
blanchet
parents: 58123
diff changeset
   334
  in
a2ba381607fb more work on compatibility interfaces
blanchet
parents: 58123
diff changeset
   335
    datatype_compat fpT_names lthy
a2ba381607fb more work on compatibility interfaces
blanchet
parents: 58123
diff changeset
   336
  end;
a2ba381607fb more work on compatibility interfaces
blanchet
parents: 58123
diff changeset
   337
a2ba381607fb more work on compatibility interfaces
blanchet
parents: 58123
diff changeset
   338
fun add_datatype nesting_pref old_specs thy =
58123
62765d39539f implemented compatibility definition of datatype
blanchet
parents: 58122
diff changeset
   339
  let
62765d39539f implemented compatibility definition of datatype
blanchet
parents: 58122
diff changeset
   340
    val fpT_names = map (Sign.full_name thy o #1 o fst) old_specs;
62765d39539f implemented compatibility definition of datatype
blanchet
parents: 58122
diff changeset
   341
62765d39539f implemented compatibility definition of datatype
blanchet
parents: 58122
diff changeset
   342
    fun new_type_args_of (s, S) = (SOME Binding.empty, (TFree (s, @{sort type}), S));
62765d39539f implemented compatibility definition of datatype
blanchet
parents: 58122
diff changeset
   343
    fun new_ctr_spec_of (b, Ts, mx) = (((Binding.empty, b), map (pair Binding.empty) Ts), mx);
62765d39539f implemented compatibility definition of datatype
blanchet
parents: 58122
diff changeset
   344
62765d39539f implemented compatibility definition of datatype
blanchet
parents: 58122
diff changeset
   345
    fun new_spec_of ((b, old_tyargs, mx), old_ctr_specs) =
62765d39539f implemented compatibility definition of datatype
blanchet
parents: 58122
diff changeset
   346
      (((((map new_type_args_of old_tyargs, b), mx), map new_ctr_spec_of old_ctr_specs),
62765d39539f implemented compatibility definition of datatype
blanchet
parents: 58122
diff changeset
   347
        (Binding.empty, Binding.empty)), []);
62765d39539f implemented compatibility definition of datatype
blanchet
parents: 58122
diff changeset
   348
62765d39539f implemented compatibility definition of datatype
blanchet
parents: 58122
diff changeset
   349
    val new_specs = map new_spec_of old_specs;
62765d39539f implemented compatibility definition of datatype
blanchet
parents: 58122
diff changeset
   350
  in
62765d39539f implemented compatibility definition of datatype
blanchet
parents: 58122
diff changeset
   351
    (fpT_names,
62765d39539f implemented compatibility definition of datatype
blanchet
parents: 58122
diff changeset
   352
     thy
62765d39539f implemented compatibility definition of datatype
blanchet
parents: 58122
diff changeset
   353
     |> Named_Target.theory_init
62765d39539f implemented compatibility definition of datatype
blanchet
parents: 58122
diff changeset
   354
     |> co_datatypes Least_FP construct_lfp ((false, false), new_specs)
58125
a2ba381607fb more work on compatibility interfaces
blanchet
parents: 58123
diff changeset
   355
     |> Named_Target.exit
a2ba381607fb more work on compatibility interfaces
blanchet
parents: 58123
diff changeset
   356
     |> nesting_pref = Unfold_Nesting ? perhaps (try (datatype_compat_global fpT_names)))
58123
62765d39539f implemented compatibility definition of datatype
blanchet
parents: 58122
diff changeset
   357
  end;
62765d39539f implemented compatibility definition of datatype
blanchet
parents: 58122
diff changeset
   358
58126
3831312eb476 added primrec compatibility function
blanchet
parents: 58125
diff changeset
   359
val add_primrec = apfst (apsnd flat) ooo BNF_LFP_Rec_Sugar.add_primrec;
3831312eb476 added primrec compatibility function
blanchet
parents: 58125
diff changeset
   360
53303
ae49b835ca01 moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff changeset
   361
val _ =
55531
601ca8efa000 renamed 'datatype_new_compat' to 'datatype_compat'
blanchet
parents: 55486
diff changeset
   362
  Outer_Syntax.local_theory @{command_spec "datatype_compat"}
54025
70bc41e7a91e tuned command descriptions
blanchet
parents: 54009
diff changeset
   363
    "register new-style datatypes as old-style datatypes"
55531
601ca8efa000 renamed 'datatype_new_compat' to 'datatype_compat'
blanchet
parents: 55486
diff changeset
   364
    (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
   365
ae49b835ca01 moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff changeset
   366
end;