src/HOL/Tools/BNF/bnf_fp_n2m_sugar.ML
author wenzelm
Sat, 08 Nov 2014 16:55:41 +0100
changeset 58948 f6ecc0fb2066
parent 58734 20235f0512e2
child 59040 ac836bcddb3b
permissions -rw-r--r--
proper Envir.norm_type for result of Type.raw_unifys;
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_fp_n2m_sugar.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
ae49b835ca01 moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff changeset
     5
Suggared flattening of nested to mutual (co)recursion.
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_FP_N2M_SUGAR =
ae49b835ca01 moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff changeset
     9
sig
55343
5ebf832b58a1 expand 'split' in direct corecursion as well
blanchet
parents: 55336
diff changeset
    10
  val unfold_lets_splits: term -> term
57895
a85e0ab840c1 less aggressive unfolding; removed debugging;
blanchet
parents: 57489
diff changeset
    11
  val unfold_splits_lets: term -> term
54243
a596292be9a8 more robust n2m w.r.t. 'let's
blanchet
parents: 54240
diff changeset
    12
  val dest_map: Proof.context -> string -> term -> term * term list
a596292be9a8 more robust n2m w.r.t. 'let's
blanchet
parents: 54240
diff changeset
    13
58335
a5a3b576fcfb generate 'code' attribute only if 'code' plugin is enabled
blanchet
parents: 58315
diff changeset
    14
  val mutualize_fp_sugars: (string -> bool) -> BNF_Util.fp_kind -> int list -> binding list ->
a5a3b576fcfb generate 'code' attribute only if 'code' plugin is enabled
blanchet
parents: 58315
diff changeset
    15
    typ list -> term list -> term list list list list -> BNF_FP_Def_Sugar.fp_sugar list ->
a5a3b576fcfb generate 'code' attribute only if 'code' plugin is enabled
blanchet
parents: 58315
diff changeset
    16
    local_theory ->
58180
95397823f39e moved code around
blanchet
parents: 58179
diff changeset
    17
    (BNF_FP_Def_Sugar.fp_sugar list
53746
bd038e48526d have "datatype_new_compat" register induction and recursion theorems in nested case
blanchet
parents: 53678
diff changeset
    18
     * (BNF_FP_Def_Sugar.lfp_sugar_thms option * BNF_FP_Def_Sugar.gfp_sugar_thms option))
bd038e48526d have "datatype_new_compat" register induction and recursion theorems in nested case
blanchet
parents: 53678
diff changeset
    19
    * local_theory
58335
a5a3b576fcfb generate 'code' attribute only if 'code' plugin is enabled
blanchet
parents: 58315
diff changeset
    20
  val nested_to_mutual_fps: (string -> bool) -> BNF_Util.fp_kind -> binding list -> typ list ->
a5a3b576fcfb generate 'code' attribute only if 'code' plugin is enabled
blanchet
parents: 58315
diff changeset
    21
    term list -> (term * term list list) list list -> local_theory ->
58180
95397823f39e moved code around
blanchet
parents: 58179
diff changeset
    22
    (typ list * int list * BNF_FP_Def_Sugar.fp_sugar list
53746
bd038e48526d have "datatype_new_compat" register induction and recursion theorems in nested case
blanchet
parents: 53678
diff changeset
    23
     * (BNF_FP_Def_Sugar.lfp_sugar_thms option * BNF_FP_Def_Sugar.gfp_sugar_thms option))
bd038e48526d have "datatype_new_compat" register induction and recursion theorems in nested case
blanchet
parents: 53678
diff changeset
    24
    * local_theory
53303
ae49b835ca01 moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff changeset
    25
end;
ae49b835ca01 moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff changeset
    26
ae49b835ca01 moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff changeset
    27
structure BNF_FP_N2M_Sugar : BNF_FP_N2M_SUGAR =
ae49b835ca01 moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff changeset
    28
struct
ae49b835ca01 moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff changeset
    29
54006
9fe1bd54d437 renamed theory file
blanchet
parents: 53974
diff changeset
    30
open Ctr_Sugar
53303
ae49b835ca01 moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff changeset
    31
open BNF_Util
ae49b835ca01 moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff changeset
    32
open BNF_Def
ae49b835ca01 moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff changeset
    33
open BNF_FP_Util
ae49b835ca01 moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff changeset
    34
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
    35
open BNF_FP_N2M
ae49b835ca01 moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff changeset
    36
ae49b835ca01 moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff changeset
    37
val n2mN = "n2m_"
ae49b835ca01 moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff changeset
    38
54256
4843082be7ef added some N2M caching
blanchet
parents: 54255
diff changeset
    39
type n2m_sugar = fp_sugar list * (lfp_sugar_thms option * gfp_sugar_thms option);
4843082be7ef added some N2M caching
blanchet
parents: 54255
diff changeset
    40
4843082be7ef added some N2M caching
blanchet
parents: 54255
diff changeset
    41
structure Data = Generic_Data
4843082be7ef added some N2M caching
blanchet
parents: 54255
diff changeset
    42
(
4843082be7ef added some N2M caching
blanchet
parents: 54255
diff changeset
    43
  type T = n2m_sugar Typtab.table;
4843082be7ef added some N2M caching
blanchet
parents: 54255
diff changeset
    44
  val empty = Typtab.empty;
4843082be7ef added some N2M caching
blanchet
parents: 54255
diff changeset
    45
  val extend = I;
55394
d5ebe055b599 more liberal merging of BNFs and constructor sugar
blanchet
parents: 55343
diff changeset
    46
  fun merge data : T = Typtab.merge (K true) data;
54256
4843082be7ef added some N2M caching
blanchet
parents: 54255
diff changeset
    47
);
4843082be7ef added some N2M caching
blanchet
parents: 54255
diff changeset
    48
4843082be7ef added some N2M caching
blanchet
parents: 54255
diff changeset
    49
fun morph_n2m_sugar phi (fp_sugars, (lfp_sugar_thms_opt, gfp_sugar_thms_opt)) =
4843082be7ef added some N2M caching
blanchet
parents: 54255
diff changeset
    50
  (map (morph_fp_sugar phi) fp_sugars,
4843082be7ef added some N2M caching
blanchet
parents: 54255
diff changeset
    51
   (Option.map (morph_lfp_sugar_thms phi) lfp_sugar_thms_opt,
4843082be7ef added some N2M caching
blanchet
parents: 54255
diff changeset
    52
    Option.map (morph_gfp_sugar_thms phi) gfp_sugar_thms_opt));
4843082be7ef added some N2M caching
blanchet
parents: 54255
diff changeset
    53
58115
bfde04fc5190 made transfer functions slightly more general
blanchet
parents: 58112
diff changeset
    54
val transfer_n2m_sugar = morph_n2m_sugar o Morphism.transfer_morphism;
54256
4843082be7ef added some N2M caching
blanchet
parents: 54255
diff changeset
    55
4843082be7ef added some N2M caching
blanchet
parents: 54255
diff changeset
    56
fun n2m_sugar_of ctxt =
4843082be7ef added some N2M caching
blanchet
parents: 54255
diff changeset
    57
  Typtab.lookup (Data.get (Context.Proof ctxt))
58115
bfde04fc5190 made transfer functions slightly more general
blanchet
parents: 58112
diff changeset
    58
  #> Option.map (transfer_n2m_sugar (Proof_Context.theory_of ctxt));
54256
4843082be7ef added some N2M caching
blanchet
parents: 54255
diff changeset
    59
4843082be7ef added some N2M caching
blanchet
parents: 54255
diff changeset
    60
fun register_n2m_sugar key n2m_sugar =
4843082be7ef added some N2M caching
blanchet
parents: 54255
diff changeset
    61
  Local_Theory.declaration {syntax = false, pervasive = false}
55444
ec73f81e49e7 iteration n in the 'default' vs. 'update_new' vs. 'update' saga -- 'update' makes sense now that we honor the canonical order on 'merge' (as opposed to raising 'DUP')
blanchet
parents: 55414
diff changeset
    62
    (fn phi => Data.map (Typtab.update (key, morph_n2m_sugar phi n2m_sugar)));
54256
4843082be7ef added some N2M caching
blanchet
parents: 54255
diff changeset
    63
57895
a85e0ab840c1 less aggressive unfolding; removed debugging;
blanchet
parents: 57489
diff changeset
    64
fun unfold_lets_splits (Const (@{const_name Let}, _) $ t $ u) =
57897
36778ca6847c improved unfolding of 'let's
blanchet
parents: 57895
diff changeset
    65
    unfold_lets_splits (betapply (unfold_splits_lets u, t))
57895
a85e0ab840c1 less aggressive unfolding; removed debugging;
blanchet
parents: 57489
diff changeset
    66
  | unfold_lets_splits (t $ u) = betapply (unfold_lets_splits t, unfold_lets_splits u)
a85e0ab840c1 less aggressive unfolding; removed debugging;
blanchet
parents: 57489
diff changeset
    67
  | unfold_lets_splits (Abs (s, T, t)) = Abs (s, T, unfold_lets_splits t)
a85e0ab840c1 less aggressive unfolding; removed debugging;
blanchet
parents: 57489
diff changeset
    68
  | unfold_lets_splits t = t
57897
36778ca6847c improved unfolding of 'let's
blanchet
parents: 57895
diff changeset
    69
and unfold_splits_lets ((t as Const (@{const_name case_prod}, _)) $ u) =
57895
a85e0ab840c1 less aggressive unfolding; removed debugging;
blanchet
parents: 57489
diff changeset
    70
    (case unfold_splits_lets u of
55336
1401434a7e83 fixed handling of 'split'
blanchet
parents: 55099
diff changeset
    71
      u' as Abs (s1, T1, Abs (s2, T2, _)) =>
1401434a7e83 fixed handling of 'split'
blanchet
parents: 55099
diff changeset
    72
      let val v = Var ((s1 ^ s2, Term.maxidx_of_term u' + 1), HOLogic.mk_prodT (T1, T2)) in
1401434a7e83 fixed handling of 'split'
blanchet
parents: 55099
diff changeset
    73
        lambda v (incr_boundvars 1 (betapplys (u', [HOLogic.mk_fst v, HOLogic.mk_snd v])))
54243
a596292be9a8 more robust n2m w.r.t. 'let's
blanchet
parents: 54240
diff changeset
    74
      end
57897
36778ca6847c improved unfolding of 'let's
blanchet
parents: 57895
diff changeset
    75
    | _ => t $ unfold_lets_splits u)
36778ca6847c improved unfolding of 'let's
blanchet
parents: 57895
diff changeset
    76
  | unfold_splits_lets (t as Const (@{const_name Let}, _) $ _ $ _) = unfold_lets_splits t
36778ca6847c improved unfolding of 'let's
blanchet
parents: 57895
diff changeset
    77
  | unfold_splits_lets (t $ u) = betapply (unfold_splits_lets t, unfold_lets_splits u)
57895
a85e0ab840c1 less aggressive unfolding; removed debugging;
blanchet
parents: 57489
diff changeset
    78
  | unfold_splits_lets (Abs (s, T, t)) = Abs (s, T, unfold_splits_lets t)
a85e0ab840c1 less aggressive unfolding; removed debugging;
blanchet
parents: 57489
diff changeset
    79
  | unfold_splits_lets t = unfold_lets_splits t;
54243
a596292be9a8 more robust n2m w.r.t. 'let's
blanchet
parents: 54240
diff changeset
    80
a596292be9a8 more robust n2m w.r.t. 'let's
blanchet
parents: 54240
diff changeset
    81
fun mk_map_pattern ctxt s =
a596292be9a8 more robust n2m w.r.t. 'let's
blanchet
parents: 54240
diff changeset
    82
  let
a596292be9a8 more robust n2m w.r.t. 'let's
blanchet
parents: 54240
diff changeset
    83
    val bnf = the (bnf_of ctxt s);
a596292be9a8 more robust n2m w.r.t. 'let's
blanchet
parents: 54240
diff changeset
    84
    val mapx = map_of_bnf bnf;
a596292be9a8 more robust n2m w.r.t. 'let's
blanchet
parents: 54240
diff changeset
    85
    val live = live_of_bnf bnf;
a596292be9a8 more robust n2m w.r.t. 'let's
blanchet
parents: 54240
diff changeset
    86
    val (f_Ts, _) = strip_typeN live (fastype_of mapx);
54265
3e1d230f1c00 make local theory operations non-pervasive (makes more intuitive sense)
blanchet
parents: 54256
diff changeset
    87
    val fs = map_index (fn (i, T) => Var (("?f", i), T)) f_Ts;
54243
a596292be9a8 more robust n2m w.r.t. 'let's
blanchet
parents: 54240
diff changeset
    88
  in
a596292be9a8 more robust n2m w.r.t. 'let's
blanchet
parents: 54240
diff changeset
    89
    (mapx, betapplys (mapx, fs))
a596292be9a8 more robust n2m w.r.t. 'let's
blanchet
parents: 54240
diff changeset
    90
  end;
a596292be9a8 more robust n2m w.r.t. 'let's
blanchet
parents: 54240
diff changeset
    91
a596292be9a8 more robust n2m w.r.t. 'let's
blanchet
parents: 54240
diff changeset
    92
fun dest_map ctxt s call =
a596292be9a8 more robust n2m w.r.t. 'let's
blanchet
parents: 54240
diff changeset
    93
  let
a596292be9a8 more robust n2m w.r.t. 'let's
blanchet
parents: 54240
diff changeset
    94
    val (map0, pat) = mk_map_pattern ctxt s;
a596292be9a8 more robust n2m w.r.t. 'let's
blanchet
parents: 54240
diff changeset
    95
    val (_, tenv) = fo_match ctxt call pat;
a596292be9a8 more robust n2m w.r.t. 'let's
blanchet
parents: 54240
diff changeset
    96
  in
a596292be9a8 more robust n2m w.r.t. 'let's
blanchet
parents: 54240
diff changeset
    97
    (map0, Vartab.fold_rev (fn (_, (_, f)) => cons f) tenv [])
a596292be9a8 more robust n2m w.r.t. 'let's
blanchet
parents: 54240
diff changeset
    98
  end;
a596292be9a8 more robust n2m w.r.t. 'let's
blanchet
parents: 54240
diff changeset
    99
54276
d26b6b935a6f took out loopy code
blanchet
parents: 54275
diff changeset
   100
fun dest_abs_or_applied_map _ _ (Abs (_, _, t)) = (Term.dummy, [t])
d26b6b935a6f took out loopy code
blanchet
parents: 54275
diff changeset
   101
  | dest_abs_or_applied_map ctxt s (t1 $ _) = dest_map ctxt s t1;
54239
9bd91d5d8a7b handle constructor syntax in n2m primcorec
blanchet
parents: 54235
diff changeset
   102
54245
f91022745c85 better error handling
blanchet
parents: 54243
diff changeset
   103
fun map_partition f xs =
f91022745c85 better error handling
blanchet
parents: 54243
diff changeset
   104
  fold_rev (fn x => fn (ys, (good, bad)) =>
f91022745c85 better error handling
blanchet
parents: 54243
diff changeset
   105
      case f x of SOME y => (y :: ys, (x :: good, bad)) | NONE => (ys, (good, x :: bad)))
f91022745c85 better error handling
blanchet
parents: 54243
diff changeset
   106
    xs ([], ([], []));
f91022745c85 better error handling
blanchet
parents: 54243
diff changeset
   107
58222
0ea19fc3b957 improved caching
blanchet
parents: 58211
diff changeset
   108
fun key_of_fp_eqs fp As fpTs fp_eqs =
0ea19fc3b957 improved caching
blanchet
parents: 58211
diff changeset
   109
  Type (case_fp fp "l" "g", fpTs @ maps (fn (x, T) => [TFree x, T]) fp_eqs)
0ea19fc3b957 improved caching
blanchet
parents: 58211
diff changeset
   110
  |> Term.map_atyps (fn T as TFree (_, S) =>
0ea19fc3b957 improved caching
blanchet
parents: 58211
diff changeset
   111
    (case find_index (curry (op =) T) As of
0ea19fc3b957 improved caching
blanchet
parents: 58211
diff changeset
   112
      ~1 => T
0ea19fc3b957 improved caching
blanchet
parents: 58211
diff changeset
   113
    | j => TFree ("'" ^ string_of_int j, S)));
54256
4843082be7ef added some N2M caching
blanchet
parents: 54255
diff changeset
   114
55772
367ec44763fd correct most general type for mutual recursion when several identical types are involved
blanchet
parents: 55702
diff changeset
   115
fun get_indices callers t =
367ec44763fd correct most general type for mutual recursion when several identical types are involved
blanchet
parents: 55702
diff changeset
   116
  callers
367ec44763fd correct most general type for mutual recursion when several identical types are involved
blanchet
parents: 55702
diff changeset
   117
  |> map_index (fn (i, v) => if exists_subterm (equal v) t then SOME i else NONE)
367ec44763fd correct most general type for mutual recursion when several identical types are involved
blanchet
parents: 55702
diff changeset
   118
  |> map_filter I;
367ec44763fd correct most general type for mutual recursion when several identical types are involved
blanchet
parents: 55702
diff changeset
   119
58340
blanchet
parents: 58335
diff changeset
   120
fun mutualize_fp_sugars plugins fp mutual_cliques bs fpTs callers callssss fp_sugars0 no_defs_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: 54284
diff changeset
   121
  let
58280
2ec3e2de34c3 more canonical (and correct) local theory threading
blanchet
parents: 58236
diff changeset
   122
    val thy = Proof_Context.theory_of no_defs_lthy;
53303
ae49b835ca01 moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff changeset
   123
58280
2ec3e2de34c3 more canonical (and correct) local theory threading
blanchet
parents: 58236
diff changeset
   124
    val qsotm = quote o Syntax.string_of_term no_defs_lthy;
53303
ae49b835ca01 moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff changeset
   125
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: 55444
diff changeset
   126
    fun incompatible_calls ts =
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: 55444
diff changeset
   127
      error ("Incompatible " ^ co_prefix fp ^ "recursive calls: " ^ commas (map qsotm ts));
55772
367ec44763fd correct most general type for mutual recursion when several identical types are involved
blanchet
parents: 55702
diff changeset
   128
    fun mutual_self_call caller t =
367ec44763fd correct most general type for mutual recursion when several identical types are involved
blanchet
parents: 55702
diff changeset
   129
      error ("Unsupported mutual self-call " ^ qsotm t ^ " from " ^ qsotm caller);
54301
e0943a2ee400 added check to avoid odd situations the N2M code cannot handle
blanchet
parents: 54300
diff changeset
   130
    fun nested_self_call t =
e0943a2ee400 added check to avoid odd situations the N2M code cannot handle
blanchet
parents: 54300
diff changeset
   131
      error ("Unsupported nested self-call " ^ qsotm t);
54245
f91022745c85 better error handling
blanchet
parents: 54243
diff changeset
   132
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: 54284
diff changeset
   133
    val b_names = map Binding.name_of bs;
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: 54284
diff changeset
   134
    val fp_b_names = map base_name_of_typ fpTs;
53303
ae49b835ca01 moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff changeset
   135
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: 54284
diff changeset
   136
    val nn = length fpTs;
55539
0819931d652d simplified data structure by reducing the incidence of clumsy indices
blanchet
parents: 55486
diff changeset
   137
    val kks = 0 upto nn - 1;
53303
ae49b835ca01 moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff changeset
   138
58460
a88eb33058f7 refactor fp_sugar move theorems
desharna
parents: 58459
diff changeset
   139
    fun target_ctr_sugar_of_fp_sugar fpT ({T, fp_ctr_sugar = {ctr_sugar, ...}, ...} : fp_sugar) =
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: 54284
diff changeset
   140
      let
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: 54284
diff changeset
   141
        val rho = Vartab.fold (cons o apsnd snd) (Sign.typ_match thy (T, fpT) Vartab.empty) [];
54740
91f54d386680 maintain morphism names for diagnostic purposes;
wenzelm
parents: 54303
diff changeset
   142
        val phi = Morphism.term_morphism "BNF" (Term.subst_TVars rho);
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: 54284
diff changeset
   143
      in
55539
0819931d652d simplified data structure by reducing the incidence of clumsy indices
blanchet
parents: 55486
diff changeset
   144
        morph_ctr_sugar phi ctr_sugar
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: 54284
diff changeset
   145
      end;
53303
ae49b835ca01 moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff changeset
   146
58460
a88eb33058f7 refactor fp_sugar move theorems
desharna
parents: 58459
diff changeset
   147
    val ctr_defss = map (#ctr_defs o #fp_ctr_sugar) fp_sugars0;
58462
b46874f2090f refactor fp_sugar move theorems
desharna
parents: 58461
diff changeset
   148
    val mapss = map (#map_thms o #fp_bnf_sugar) fp_sugars0;
54302
880e5417b800 removed dead code
blanchet
parents: 54301
diff changeset
   149
    val ctr_sugars = map2 target_ctr_sugar_of_fp_sugar fpTs fp_sugars0;
53303
ae49b835ca01 moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff changeset
   150
54302
880e5417b800 removed dead code
blanchet
parents: 54301
diff changeset
   151
    val ctrss = map #ctrs ctr_sugars;
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: 54284
diff changeset
   152
    val ctr_Tss = map (map fastype_of) ctrss;
53303
ae49b835ca01 moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff changeset
   153
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: 54284
diff changeset
   154
    val As' = fold (fold Term.add_tfreesT) ctr_Tss [];
58236
4967e67cc53d made N2M work with sort constraints (cf. TODO)
blanchet
parents: 58234
diff changeset
   155
    val unsorted_As' = map (apsnd (K @{sort type})) As';
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: 54284
diff changeset
   156
    val As = map TFree As';
58236
4967e67cc53d made N2M work with sort constraints (cf. TODO)
blanchet
parents: 58234
diff changeset
   157
    val unsorted_As = map TFree unsorted_As';
4967e67cc53d made N2M work with sort constraints (cf. TODO)
blanchet
parents: 58234
diff changeset
   158
4967e67cc53d made N2M work with sort constraints (cf. TODO)
blanchet
parents: 58234
diff changeset
   159
    val unsortAT = Term.typ_subst_atomic (As ~~ unsorted_As);
4967e67cc53d made N2M work with sort constraints (cf. TODO)
blanchet
parents: 58234
diff changeset
   160
    val unsorted_fpTs = map unsortAT fpTs;
53303
ae49b835ca01 moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff changeset
   161
58280
2ec3e2de34c3 more canonical (and correct) local theory threading
blanchet
parents: 58236
diff changeset
   162
    val ((Cs, Xs), names_lthy) =
2ec3e2de34c3 more canonical (and correct) local theory threading
blanchet
parents: 58236
diff changeset
   163
      no_defs_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: 54284
diff changeset
   164
      |> fold Variable.declare_typ As
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: 54284
diff changeset
   165
      |> mk_TFrees nn
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: 54284
diff changeset
   166
      ||>> variant_tfrees fp_b_names;
53303
ae49b835ca01 moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff changeset
   167
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: 54284
diff changeset
   168
    fun check_call_dead live_call call =
55772
367ec44763fd correct most general type for mutual recursion when several identical types are involved
blanchet
parents: 55702
diff changeset
   169
      if null (get_indices callers call) then () else incompatible_calls [live_call, call];
54245
f91022745c85 better error handling
blanchet
parents: 54243
diff changeset
   170
55480
59cc4a8bc28a allow different functions to recurse on the same type, like in the old package
blanchet
parents: 55479
diff changeset
   171
    fun freeze_fpTs_type_based_default (T as Type (s, Ts)) =
59cc4a8bc28a allow different functions to recurse on the same type, like in the old package
blanchet
parents: 55479
diff changeset
   172
        (case filter (curry (op =) T o snd) (map_index I fpTs) of
59cc4a8bc28a allow different functions to recurse on the same type, like in the old package
blanchet
parents: 55479
diff changeset
   173
          [(kk, _)] => nth Xs kk
59cc4a8bc28a allow different functions to recurse on the same type, like in the old package
blanchet
parents: 55479
diff changeset
   174
        | _ => Type (s, map freeze_fpTs_type_based_default Ts))
59cc4a8bc28a allow different functions to recurse on the same type, like in the old package
blanchet
parents: 55479
diff changeset
   175
      | freeze_fpTs_type_based_default T = T;
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: 55444
diff changeset
   176
55772
367ec44763fd correct most general type for mutual recursion when several identical types are involved
blanchet
parents: 55702
diff changeset
   177
    fun freeze_fpTs_mutual_call kk fpT calls T =
367ec44763fd correct most general type for mutual recursion when several identical types are involved
blanchet
parents: 55702
diff changeset
   178
      (case fold (union (op =)) (map (get_indices callers) calls) [] of
367ec44763fd correct most general type for mutual recursion when several identical types are involved
blanchet
parents: 55702
diff changeset
   179
        [] => if T = fpT then nth Xs kk else freeze_fpTs_type_based_default T
367ec44763fd correct most general type for mutual recursion when several identical types are involved
blanchet
parents: 55702
diff changeset
   180
      | [kk'] =>
367ec44763fd correct most general type for mutual recursion when several identical types are involved
blanchet
parents: 55702
diff changeset
   181
        if T = fpT andalso kk' <> kk then
367ec44763fd correct most general type for mutual recursion when several identical types are involved
blanchet
parents: 55702
diff changeset
   182
          mutual_self_call (nth callers kk)
367ec44763fd correct most general type for mutual recursion when several identical types are involved
blanchet
parents: 55702
diff changeset
   183
            (the (find_first (not o null o get_indices callers) calls))
58290
14e186d2dd3a proper checks -- the calls data structure may contain spurious entries
blanchet
parents: 58280
diff changeset
   184
        else if T = nth fpTs kk' then
14e186d2dd3a proper checks -- the calls data structure may contain spurious entries
blanchet
parents: 58280
diff changeset
   185
          nth Xs kk'
55772
367ec44763fd correct most general type for mutual recursion when several identical types are involved
blanchet
parents: 55702
diff changeset
   186
        else
58290
14e186d2dd3a proper checks -- the calls data structure may contain spurious entries
blanchet
parents: 58280
diff changeset
   187
          freeze_fpTs_type_based_default T
55480
59cc4a8bc28a allow different functions to recurse on the same type, like in the old package
blanchet
parents: 55479
diff changeset
   188
      | _ => incompatible_calls calls);
54253
04cd231e2b9e nicer error message in case of duplicates
blanchet
parents: 54245
diff changeset
   189
55772
367ec44763fd correct most general type for mutual recursion when several identical types are involved
blanchet
parents: 55702
diff changeset
   190
    fun freeze_fpTs_map kk (fpT as Type (_, Ts')) (callss, (live_call :: _, dead_calls))
55480
59cc4a8bc28a allow different functions to recurse on the same type, like in the old package
blanchet
parents: 55479
diff changeset
   191
        (Type (s, Ts)) =
54301
e0943a2ee400 added check to avoid odd situations the N2M code cannot handle
blanchet
parents: 54300
diff changeset
   192
      if Ts' = Ts then
e0943a2ee400 added check to avoid odd situations the N2M code cannot handle
blanchet
parents: 54300
diff changeset
   193
        nested_self_call live_call
e0943a2ee400 added check to avoid odd situations the N2M code cannot handle
blanchet
parents: 54300
diff changeset
   194
      else
e0943a2ee400 added check to avoid odd situations the N2M code cannot handle
blanchet
parents: 54300
diff changeset
   195
        (List.app (check_call_dead live_call) dead_calls;
55772
367ec44763fd correct most general type for mutual recursion when several identical types are involved
blanchet
parents: 55702
diff changeset
   196
         Type (s, map2 (freeze_fpTs_call kk fpT)
55480
59cc4a8bc28a allow different functions to recurse on the same type, like in the old package
blanchet
parents: 55479
diff changeset
   197
           (flatten_type_args_of_bnf (the (bnf_of no_defs_lthy s)) [] (transpose callss)) Ts))
55772
367ec44763fd correct most general type for mutual recursion when several identical types are involved
blanchet
parents: 55702
diff changeset
   198
    and freeze_fpTs_call kk fpT calls (T as Type (s, _)) =
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: 54284
diff changeset
   199
        (case map_partition (try (snd o dest_map no_defs_lthy s)) calls of
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: 54284
diff changeset
   200
          ([], _) =>
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: 54284
diff changeset
   201
          (case map_partition (try (snd o dest_abs_or_applied_map no_defs_lthy s)) calls of
55772
367ec44763fd correct most general type for mutual recursion when several identical types are involved
blanchet
parents: 55702
diff changeset
   202
            ([], _) => freeze_fpTs_mutual_call kk fpT calls T
367ec44763fd correct most general type for mutual recursion when several identical types are involved
blanchet
parents: 55702
diff changeset
   203
          | callsp => freeze_fpTs_map kk fpT callsp T)
367ec44763fd correct most general type for mutual recursion when several identical types are involved
blanchet
parents: 55702
diff changeset
   204
        | callsp => freeze_fpTs_map kk fpT callsp T)
367ec44763fd correct most general type for mutual recursion when several identical types are involved
blanchet
parents: 55702
diff changeset
   205
      | freeze_fpTs_call _ _ _ T = T;
53303
ae49b835ca01 moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff changeset
   206
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: 54284
diff changeset
   207
    val ctr_Tsss = map (map binder_types) ctr_Tss;
58634
9f10d82e8188 added parameterized ML antiquotations @{map N}, @{fold N}, @{fold_map N}, @{split_list N};
wenzelm
parents: 58577
diff changeset
   208
    val ctrXs_Tsss = @{map 4} (map2 o map2 oo freeze_fpTs_call) kks fpTs callssss ctr_Tsss;
55966
972f0aa7091b balance tuples that represent curried functions
blanchet
parents: 55868
diff changeset
   209
    val ctrXs_repTs = map mk_sumprodT_balanced ctrXs_Tsss;
53303
ae49b835ca01 moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff changeset
   210
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: 54284
diff changeset
   211
    val ns = map length ctr_Tsss;
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: 54284
diff changeset
   212
    val kss = map (fn n => 1 upto n) ns;
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: 54284
diff changeset
   213
    val mss = map (map length) ctr_Tsss;
53303
ae49b835ca01 moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff changeset
   214
58236
4967e67cc53d made N2M work with sort constraints (cf. TODO)
blanchet
parents: 58234
diff changeset
   215
    val fp_eqs = map dest_TFree Xs ~~ map unsortAT ctrXs_repTs;
4967e67cc53d made N2M work with sort constraints (cf. TODO)
blanchet
parents: 58234
diff changeset
   216
    val key = key_of_fp_eqs fp unsorted_As unsorted_fpTs fp_eqs;
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: 54284
diff changeset
   217
  in
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: 54284
diff changeset
   218
    (case n2m_sugar_of no_defs_lthy key of
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: 54284
diff changeset
   219
      SOME n2m_sugar => (n2m_sugar, no_defs_lthy)
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: 54284
diff changeset
   220
    | NONE =>
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: 54284
diff changeset
   221
      let
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: 54284
diff changeset
   222
        val base_fp_names = Name.variant_list [] fp_b_names;
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: 54284
diff changeset
   223
        val fp_bs = map2 (fn b_name => fn base_fp_name =>
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: 54284
diff changeset
   224
            Binding.qualify true b_name (Binding.name (n2mN ^ base_fp_name)))
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: 54284
diff changeset
   225
          b_names base_fp_names;
53303
ae49b835ca01 moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff changeset
   226
55702
63c80031d8dd improved accounting for dead variables when naming set functions (refines d71c2737ee21)
blanchet
parents: 55701
diff changeset
   227
        val Type (s, Us) :: _ = fpTs;
63c80031d8dd improved accounting for dead variables when naming set functions (refines d71c2737ee21)
blanchet
parents: 55701
diff changeset
   228
        val killed_As' =
63c80031d8dd improved accounting for dead variables when naming set functions (refines d71c2737ee21)
blanchet
parents: 55701
diff changeset
   229
          (case bnf_of no_defs_lthy s of
58236
4967e67cc53d made N2M work with sort constraints (cf. TODO)
blanchet
parents: 58234
diff changeset
   230
            NONE => unsorted_As'
55702
63c80031d8dd improved accounting for dead variables when naming set functions (refines d71c2737ee21)
blanchet
parents: 55701
diff changeset
   231
          | SOME bnf =>
63c80031d8dd improved accounting for dead variables when naming set functions (refines d71c2737ee21)
blanchet
parents: 55701
diff changeset
   232
            let
63c80031d8dd improved accounting for dead variables when naming set functions (refines d71c2737ee21)
blanchet
parents: 55701
diff changeset
   233
              val Type (_, Ts) = T_of_bnf bnf;
63c80031d8dd improved accounting for dead variables when naming set functions (refines d71c2737ee21)
blanchet
parents: 55701
diff changeset
   234
              val deads = deads_of_bnf bnf;
63c80031d8dd improved accounting for dead variables when naming set functions (refines d71c2737ee21)
blanchet
parents: 55701
diff changeset
   235
              val dead_Us =
63c80031d8dd improved accounting for dead variables when naming set functions (refines d71c2737ee21)
blanchet
parents: 55701
diff changeset
   236
                map_filter (fn (T, U) => if member (op =) deads T then SOME U else NONE) (Ts ~~ Us);
63c80031d8dd improved accounting for dead variables when naming set functions (refines d71c2737ee21)
blanchet
parents: 55701
diff changeset
   237
            in fold Term.add_tfreesT dead_Us [] end);
63c80031d8dd improved accounting for dead variables when naming set functions (refines d71c2737ee21)
blanchet
parents: 55701
diff changeset
   238
55803
74d3fe9031d8 joint work with blanchet: intermediate typedef for the input to fp-operations
traytel
parents: 55772
diff changeset
   239
        val fp_absT_infos = map #absT_info fp_sugars0;
74d3fe9031d8 joint work with blanchet: intermediate typedef for the input to fp-operations
traytel
parents: 55772
diff changeset
   240
58211
c1f3fa32d322 extended 'datatype_compat' to generate the expected, old-style recursor in the presence of recursion through functions
blanchet
parents: 58180
diff changeset
   241
        val ((pre_bnfs, absT_infos), (fp_res as {xtor_co_recs = xtor_co_recs0, xtor_co_induct,
c1f3fa32d322 extended 'datatype_compat' to generate the expected, old-style recursor in the presence of recursion through functions
blanchet
parents: 58180
diff changeset
   242
               dtor_injects, dtor_ctors, xtor_co_rec_thms, ...}, lthy)) =
58340
blanchet
parents: 58335
diff changeset
   243
          fp_bnf (construct_mutualized_fp fp mutual_cliques unsorted_fpTs fp_sugars0) fp_bs
blanchet
parents: 58335
diff changeset
   244
            unsorted_As' killed_As' fp_eqs no_defs_lthy;
55803
74d3fe9031d8 joint work with blanchet: intermediate typedef for the input to fp-operations
traytel
parents: 55772
diff changeset
   245
58211
c1f3fa32d322 extended 'datatype_compat' to generate the expected, old-style recursor in the presence of recursion through functions
blanchet
parents: 58180
diff changeset
   246
        val fp_abs_inverses = map #abs_inverse fp_absT_infos;
c1f3fa32d322 extended 'datatype_compat' to generate the expected, old-style recursor in the presence of recursion through functions
blanchet
parents: 58180
diff changeset
   247
        val fp_type_definitions = map #type_definition fp_absT_infos;
55803
74d3fe9031d8 joint work with blanchet: intermediate typedef for the input to fp-operations
traytel
parents: 55772
diff changeset
   248
58211
c1f3fa32d322 extended 'datatype_compat' to generate the expected, old-style recursor in the presence of recursion through functions
blanchet
parents: 58180
diff changeset
   249
        val abss = map #abs absT_infos;
c1f3fa32d322 extended 'datatype_compat' to generate the expected, old-style recursor in the presence of recursion through functions
blanchet
parents: 58180
diff changeset
   250
        val reps = map #rep absT_infos;
c1f3fa32d322 extended 'datatype_compat' to generate the expected, old-style recursor in the presence of recursion through functions
blanchet
parents: 58180
diff changeset
   251
        val absTs = map #absT absT_infos;
c1f3fa32d322 extended 'datatype_compat' to generate the expected, old-style recursor in the presence of recursion through functions
blanchet
parents: 58180
diff changeset
   252
        val repTs = map #repT absT_infos;
c1f3fa32d322 extended 'datatype_compat' to generate the expected, old-style recursor in the presence of recursion through functions
blanchet
parents: 58180
diff changeset
   253
        val abs_inverses = map #abs_inverse absT_infos;
53303
ae49b835ca01 moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff changeset
   254
58211
c1f3fa32d322 extended 'datatype_compat' to generate the expected, old-style recursor in the presence of recursion through functions
blanchet
parents: 58180
diff changeset
   255
        val fp_nesting_bnfs = nesting_bnfs lthy ctrXs_Tsss Xs;
c1f3fa32d322 extended 'datatype_compat' to generate the expected, old-style recursor in the presence of recursion through functions
blanchet
parents: 58180
diff changeset
   256
        val live_nesting_bnfs = nesting_bnfs lthy ctrXs_Tsss As;
53303
ae49b835ca01 moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff changeset
   257
58211
c1f3fa32d322 extended 'datatype_compat' to generate the expected, old-style recursor in the presence of recursion through functions
blanchet
parents: 58180
diff changeset
   258
        val ((xtor_co_recs, recs_args_types, corecs_args_types), _) =
c1f3fa32d322 extended 'datatype_compat' to generate the expected, old-style recursor in the presence of recursion through functions
blanchet
parents: 58180
diff changeset
   259
          mk_co_recs_prelims fp ctr_Tsss fpTs Cs absTs repTs ns mss xtor_co_recs0 lthy;
54256
4843082be7ef added some N2M caching
blanchet
parents: 54255
diff changeset
   260
58211
c1f3fa32d322 extended 'datatype_compat' to generate the expected, old-style recursor in the presence of recursion through functions
blanchet
parents: 58180
diff changeset
   261
        fun mk_binding b pre = Binding.prefix_name (pre ^ "_") b;
53303
ae49b835ca01 moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff changeset
   262
58211
c1f3fa32d322 extended 'datatype_compat' to generate the expected, old-style recursor in the presence of recursion through functions
blanchet
parents: 58180
diff changeset
   263
        val ((co_recs, co_rec_defs), lthy) =
58634
9f10d82e8188 added parameterized ML antiquotations @{map N}, @{fold N}, @{fold_map N}, @{split_list N};
wenzelm
parents: 58577
diff changeset
   264
          @{fold_map 2} (fn b =>
58211
c1f3fa32d322 extended 'datatype_compat' to generate the expected, old-style recursor in the presence of recursion through functions
blanchet
parents: 58180
diff changeset
   265
              if fp = Least_FP then define_rec (the recs_args_types) (mk_binding b) fpTs Cs reps
c1f3fa32d322 extended 'datatype_compat' to generate the expected, old-style recursor in the presence of recursion through functions
blanchet
parents: 58180
diff changeset
   266
              else define_corec (the corecs_args_types) (mk_binding b) fpTs Cs abss)
c1f3fa32d322 extended 'datatype_compat' to generate the expected, old-style recursor in the presence of recursion through functions
blanchet
parents: 58180
diff changeset
   267
            fp_bs xtor_co_recs lthy
c1f3fa32d322 extended 'datatype_compat' to generate the expected, old-style recursor in the presence of recursion through functions
blanchet
parents: 58180
diff changeset
   268
          |>> split_list;
58131
1abeda3c3bc2 drop hopeless feature -- unfolding of BNF datatype info without a prior 'datatype_compat'
blanchet
parents: 58117
diff changeset
   269
58211
c1f3fa32d322 extended 'datatype_compat' to generate the expected, old-style recursor in the presence of recursion through functions
blanchet
parents: 58180
diff changeset
   270
        val ((common_co_inducts, co_inductss', co_rec_thmss, co_rec_disc_thmss, co_rec_sel_thmsss),
c1f3fa32d322 extended 'datatype_compat' to generate the expected, old-style recursor in the presence of recursion through functions
blanchet
parents: 58180
diff changeset
   271
             fp_sugar_thms) =
c1f3fa32d322 extended 'datatype_compat' to generate the expected, old-style recursor in the presence of recursion through functions
blanchet
parents: 58180
diff changeset
   272
          if fp = Least_FP then
58335
a5a3b576fcfb generate 'code' attribute only if 'code' plugin is enabled
blanchet
parents: 58315
diff changeset
   273
            derive_induct_recs_thms_for_types plugins pre_bnfs recs_args_types xtor_co_induct
58211
c1f3fa32d322 extended 'datatype_compat' to generate the expected, old-style recursor in the presence of recursion through functions
blanchet
parents: 58180
diff changeset
   274
              xtor_co_rec_thms live_nesting_bnfs fp_nesting_bnfs fpTs Cs Xs ctrXs_Tsss
c1f3fa32d322 extended 'datatype_compat' to generate the expected, old-style recursor in the presence of recursion through functions
blanchet
parents: 58180
diff changeset
   275
              fp_abs_inverses fp_type_definitions abs_inverses ctrss ctr_defss co_recs co_rec_defs
c1f3fa32d322 extended 'datatype_compat' to generate the expected, old-style recursor in the presence of recursion through functions
blanchet
parents: 58180
diff changeset
   276
              lthy
c1f3fa32d322 extended 'datatype_compat' to generate the expected, old-style recursor in the presence of recursion through functions
blanchet
parents: 58180
diff changeset
   277
            |> `(fn ((inducts, induct, _), (rec_thmss, _)) =>
c1f3fa32d322 extended 'datatype_compat' to generate the expected, old-style recursor in the presence of recursion through functions
blanchet
parents: 58180
diff changeset
   278
              ([induct], [inducts], rec_thmss, replicate nn [], replicate nn []))
c1f3fa32d322 extended 'datatype_compat' to generate the expected, old-style recursor in the presence of recursion through functions
blanchet
parents: 58180
diff changeset
   279
            ||> (fn info => (SOME info, NONE))
c1f3fa32d322 extended 'datatype_compat' to generate the expected, old-style recursor in the presence of recursion through functions
blanchet
parents: 58180
diff changeset
   280
          else
c1f3fa32d322 extended 'datatype_compat' to generate the expected, old-style recursor in the presence of recursion through functions
blanchet
parents: 58180
diff changeset
   281
            derive_coinduct_corecs_thms_for_types pre_bnfs (the corecs_args_types)
c1f3fa32d322 extended 'datatype_compat' to generate the expected, old-style recursor in the presence of recursion through functions
blanchet
parents: 58180
diff changeset
   282
              xtor_co_induct dtor_injects dtor_ctors xtor_co_rec_thms live_nesting_bnfs fpTs Cs Xs
c1f3fa32d322 extended 'datatype_compat' to generate the expected, old-style recursor in the presence of recursion through functions
blanchet
parents: 58180
diff changeset
   283
              ctrXs_Tsss kss mss ns fp_abs_inverses abs_inverses
c1f3fa32d322 extended 'datatype_compat' to generate the expected, old-style recursor in the presence of recursion through functions
blanchet
parents: 58180
diff changeset
   284
              (fn thm => thm RS @{thm vimage2p_refl}) ctr_defss ctr_sugars co_recs co_rec_defs
c1f3fa32d322 extended 'datatype_compat' to generate the expected, old-style recursor in the presence of recursion through functions
blanchet
parents: 58180
diff changeset
   285
              (Proof_Context.export lthy no_defs_lthy) lthy
c1f3fa32d322 extended 'datatype_compat' to generate the expected, old-style recursor in the presence of recursion through functions
blanchet
parents: 58180
diff changeset
   286
            |> `(fn ((coinduct_thms_pairs, _), corec_thmss, corec_disc_thmss, _,
c1f3fa32d322 extended 'datatype_compat' to generate the expected, old-style recursor in the presence of recursion through functions
blanchet
parents: 58180
diff changeset
   287
                     (corec_sel_thmsss, _)) =>
c1f3fa32d322 extended 'datatype_compat' to generate the expected, old-style recursor in the presence of recursion through functions
blanchet
parents: 58180
diff changeset
   288
              (map snd coinduct_thms_pairs, map fst coinduct_thms_pairs, corec_thmss,
c1f3fa32d322 extended 'datatype_compat' to generate the expected, old-style recursor in the presence of recursion through functions
blanchet
parents: 58180
diff changeset
   289
               corec_disc_thmss, corec_sel_thmsss))
c1f3fa32d322 extended 'datatype_compat' to generate the expected, old-style recursor in the presence of recursion through functions
blanchet
parents: 58180
diff changeset
   290
            ||> (fn info => (NONE, SOME info));
53303
ae49b835ca01 moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff changeset
   291
58280
2ec3e2de34c3 more canonical (and correct) local theory threading
blanchet
parents: 58236
diff changeset
   292
        val phi = Proof_Context.export_morphism names_lthy no_defs_lthy;
54256
4843082be7ef added some N2M caching
blanchet
parents: 54255
diff changeset
   293
56648
2ffa440b3074 manual merge + added 'rel_distincts' field to record for symmetry
blanchet
parents: 56641
diff changeset
   294
        fun mk_target_fp_sugar T X kk pre_bnf absT_info ctrXs_Tss ctr_defs ctr_sugar co_rec
58462
b46874f2090f refactor fp_sugar move theorems
desharna
parents: 58461
diff changeset
   295
            co_rec_def map_thms co_inducts co_rec_thms co_rec_disc_thms co_rec_sel_thmss
58676
cdf84b6e1297 generate 'sel_transfer' for (co)datatypes
desharna
parents: 58674
diff changeset
   296
            ({fp_ctr_sugar = {ctr_transfers, case_transfers, disc_transfers, sel_transfers, ...},
58672
3f0d612ebd8e preserve the structure of 'map_sel' theorem in ML
desharna
parents: 58671
diff changeset
   297
              fp_bnf_sugar = {map_disc_iffs, map_selss, rel_injects, rel_distincts, rel_sels,
58673
add1a78da098 preserve the structure of 'set_intros' theorem in ML
desharna
parents: 58672
diff changeset
   298
                rel_intros, rel_cases, set_thms, set_selssss, set_introssss, set_cases, ...},
58574
e66ed9634a74 add 'common_rel_co_induct' to 'fp_sugar'
desharna
parents: 58573
diff changeset
   299
              fp_co_induct_sugar = {co_rec_disc_iffs, co_rec_codes, co_rec_transfers,
58734
20235f0512e2 generate 'map_o_corec' for (co)datatypes
desharna
parents: 58732
diff changeset
   300
                co_rec_o_maps, common_rel_co_inducts, rel_co_inducts, common_set_inducts,
58732
854eed6e5aed move theorem 'rec_o_map'
desharna
parents: 58676
diff changeset
   301
                set_inducts, ...},
58568
727e014c6dbd add 'set_cases' to 'fp_sugar'
desharna
parents: 58567
diff changeset
   302
              ...} : fp_sugar) =
58117
9608028d8f43 more compatibility between old- and new-style datatypes
blanchet
parents: 58115
diff changeset
   303
          {T = T, BT = T (*wrong but harmless*), X = X, fp = fp, fp_res = fp_res, fp_res_index = kk,
58674
eb98d1971d2a add 'fp_bnf' to 'bnf_sugar'
desharna
parents: 58673
diff changeset
   304
           pre_bnf = pre_bnf, fp_bnf = nth (#bnfs fp_res) kk, absT_info = absT_info,
eb98d1971d2a add 'fp_bnf' to 'bnf_sugar'
desharna
parents: 58673
diff changeset
   305
           fp_nesting_bnfs = fp_nesting_bnfs, live_nesting_bnfs = live_nesting_bnfs,
58460
a88eb33058f7 refactor fp_sugar move theorems
desharna
parents: 58459
diff changeset
   306
           fp_ctr_sugar =
a88eb33058f7 refactor fp_sugar move theorems
desharna
parents: 58459
diff changeset
   307
             {ctrXs_Tss = ctrXs_Tss,
a88eb33058f7 refactor fp_sugar move theorems
desharna
parents: 58459
diff changeset
   308
              ctr_defs = ctr_defs,
58569
3f61adcc1fc9 add 'ctr_transfers' to 'fp_sugar'
desharna
parents: 58568
diff changeset
   309
              ctr_sugar = ctr_sugar,
58570
a3434015faf0 add 'case_transfers' to 'fp_sugar'
desharna
parents: 58569
diff changeset
   310
              ctr_transfers = ctr_transfers,
58571
d78b00f98de8 add 'disc_transfers' to 'fp_sugar'
desharna
parents: 58570
diff changeset
   311
              case_transfers = case_transfers,
58676
cdf84b6e1297 generate 'sel_transfer' for (co)datatypes
desharna
parents: 58674
diff changeset
   312
              disc_transfers = disc_transfers,
cdf84b6e1297 generate 'sel_transfer' for (co)datatypes
desharna
parents: 58674
diff changeset
   313
              sel_transfers = sel_transfers},
58459
f70bffabd7cf refactor fp_sugar move theorems
desharna
parents: 58458
diff changeset
   314
           fp_bnf_sugar =
58462
b46874f2090f refactor fp_sugar move theorems
desharna
parents: 58461
diff changeset
   315
             {map_thms = map_thms,
58560
ee502a9b38aa add 'map_disc_iffs' to 'fp_sugar'
desharna
parents: 58462
diff changeset
   316
              map_disc_iffs = map_disc_iffs,
58672
3f0d612ebd8e preserve the structure of 'map_sel' theorem in ML
desharna
parents: 58671
diff changeset
   317
              map_selss = map_selss,
58462
b46874f2090f refactor fp_sugar move theorems
desharna
parents: 58461
diff changeset
   318
              rel_injects = rel_injects,
58562
e94cd4f71d0c add 'rel_sels' to 'fp_sugar'
desharna
parents: 58561
diff changeset
   319
              rel_distincts = rel_distincts,
58563
f5019700efa5 add 'rel_intros' to 'fp_sugar'
desharna
parents: 58562
diff changeset
   320
              rel_sels = rel_sels,
58564
778a80674112 add 'rel_cases' to 'fp_sugar'
desharna
parents: 58563
diff changeset
   321
              rel_intros = rel_intros,
58565
97cefa5ef0be add 'set_thms' to 'fp_sugar'
desharna
parents: 58564
diff changeset
   322
              rel_cases = rel_cases,
58566
62aa83edad7e add 'set_sels' to 'fp_sugar'
desharna
parents: 58565
diff changeset
   323
              set_thms = set_thms,
58671
4cc24f1e52d5 preserve the structure of 'set_sel' theorem in ML
desharna
parents: 58634
diff changeset
   324
              set_selssss = set_selssss,
58673
add1a78da098 preserve the structure of 'set_intros' theorem in ML
desharna
parents: 58672
diff changeset
   325
              set_introssss = set_introssss,
58568
727e014c6dbd add 'set_cases' to 'fp_sugar'
desharna
parents: 58567
diff changeset
   326
              set_cases = set_cases},
58459
f70bffabd7cf refactor fp_sugar move theorems
desharna
parents: 58458
diff changeset
   327
           fp_co_induct_sugar =
58461
75ee8d49c724 refactor fp_sugar move theorems
desharna
parents: 58460
diff changeset
   328
             {co_rec = co_rec,
75ee8d49c724 refactor fp_sugar move theorems
desharna
parents: 58460
diff changeset
   329
              common_co_inducts = common_co_inducts,
75ee8d49c724 refactor fp_sugar move theorems
desharna
parents: 58460
diff changeset
   330
              co_inducts = co_inducts,
58674
eb98d1971d2a add 'fp_bnf' to 'bnf_sugar'
desharna
parents: 58673
diff changeset
   331
              co_rec_def = co_rec_def,
58459
f70bffabd7cf refactor fp_sugar move theorems
desharna
parents: 58458
diff changeset
   332
              co_rec_thms = co_rec_thms,
f70bffabd7cf refactor fp_sugar move theorems
desharna
parents: 58458
diff changeset
   333
              co_rec_discs = co_rec_disc_thms,
58572
2e0cf67fa89f add 'co_rec_disc_iffs' to 'fp_sugar'
desharna
parents: 58571
diff changeset
   334
              co_rec_disc_iffs = co_rec_disc_iffs,
58573
04f5d23cd9e5 add 'co_rec_transfers' to 'fp_sugar'
desharna
parents: 58572
diff changeset
   335
              co_rec_selss = co_rec_sel_thmss,
04f5d23cd9e5 add 'co_rec_transfers' to 'fp_sugar'
desharna
parents: 58572
diff changeset
   336
              co_rec_codes = co_rec_codes,
58574
e66ed9634a74 add 'common_rel_co_induct' to 'fp_sugar'
desharna
parents: 58573
diff changeset
   337
              co_rec_transfers = co_rec_transfers,
58734
20235f0512e2 generate 'map_o_corec' for (co)datatypes
desharna
parents: 58732
diff changeset
   338
              co_rec_o_maps = co_rec_o_maps,
58575
629891fd8c51 add 'rel_co_inducts' to 'fp_sugar'
desharna
parents: 58574
diff changeset
   339
              common_rel_co_inducts = common_rel_co_inducts,
58576
1f4a2d8142fe add 'common_set_inducts' to 'fp_sugar'
desharna
parents: 58575
diff changeset
   340
              rel_co_inducts = rel_co_inducts,
58577
15337ad05370 add 'set_inducts' to 'fp_sugar'
desharna
parents: 58576
diff changeset
   341
              common_set_inducts = common_set_inducts,
15337ad05370 add 'set_inducts' to 'fp_sugar'
desharna
parents: 58576
diff changeset
   342
              set_inducts = set_inducts}}
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: 54284
diff changeset
   343
          |> morph_fp_sugar phi;
54256
4843082be7ef added some N2M caching
blanchet
parents: 54255
diff changeset
   344
55539
0819931d652d simplified data structure by reducing the incidence of clumsy indices
blanchet
parents: 55486
diff changeset
   345
        val target_fp_sugars =
58634
9f10d82e8188 added parameterized ML antiquotations @{map N}, @{fold N}, @{fold_map N}, @{split_list N};
wenzelm
parents: 58577
diff changeset
   346
          @{map 16} mk_target_fp_sugar fpTs Xs kks pre_bnfs absT_infos ctrXs_Tsss ctr_defss
9f10d82e8188 added parameterized ML antiquotations @{map N}, @{fold N}, @{fold_map N}, @{split_list N};
wenzelm
parents: 58577
diff changeset
   347
            ctr_sugars co_recs co_rec_defs mapss (transpose co_inductss') co_rec_thmss
9f10d82e8188 added parameterized ML antiquotations @{map N}, @{fold N}, @{fold_map N}, @{split_list N};
wenzelm
parents: 58577
diff changeset
   348
            co_rec_disc_thmss co_rec_sel_thmsss fp_sugars0;
55539
0819931d652d simplified data structure by reducing the incidence of clumsy indices
blanchet
parents: 55486
diff changeset
   349
0819931d652d simplified data structure by reducing the incidence of clumsy indices
blanchet
parents: 55486
diff changeset
   350
        val n2m_sugar = (target_fp_sugars, fp_sugar_thms);
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: 54284
diff changeset
   351
      in
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: 54284
diff changeset
   352
        (n2m_sugar, lthy |> register_n2m_sugar key n2m_sugar)
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: 54284
diff changeset
   353
      end)
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: 54284
diff changeset
   354
  end;
53303
ae49b835ca01 moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff changeset
   355
55543
blanchet
parents: 55539
diff changeset
   356
fun indexify_callsss ctrs callsss =
53303
ae49b835ca01 moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff changeset
   357
  let
54283
6f0a49ed1bb1 fourth attempt at generalizing N2M types (to leverage caching)
blanchet
parents: 54282
diff changeset
   358
    fun indexify_ctr ctr =
53303
ae49b835ca01 moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff changeset
   359
      (case AList.lookup Term.aconv_untyped callsss ctr of
ae49b835ca01 moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff changeset
   360
        NONE => replicate (num_binder_types (fastype_of ctr)) []
55343
5ebf832b58a1 expand 'split' in direct corecursion as well
blanchet
parents: 55336
diff changeset
   361
      | SOME callss => map (map (Envir.beta_eta_contract o unfold_lets_splits)) callss);
53303
ae49b835ca01 moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff changeset
   362
  in
54283
6f0a49ed1bb1 fourth attempt at generalizing N2M types (to leverage caching)
blanchet
parents: 54282
diff changeset
   363
    map indexify_ctr ctrs
53303
ae49b835ca01 moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff changeset
   364
  end;
ae49b835ca01 moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff changeset
   365
54283
6f0a49ed1bb1 fourth attempt at generalizing N2M types (to leverage caching)
blanchet
parents: 54282
diff changeset
   366
fun retypargs tyargs (Type (s, _)) = Type (s, tyargs);
6f0a49ed1bb1 fourth attempt at generalizing N2M types (to leverage caching)
blanchet
parents: 54282
diff changeset
   367
6f0a49ed1bb1 fourth attempt at generalizing N2M types (to leverage caching)
blanchet
parents: 54282
diff changeset
   368
fun fold_subtype_pairs f (T as Type (s, Ts), U as Type (s', Us)) =
6f0a49ed1bb1 fourth attempt at generalizing N2M types (to leverage caching)
blanchet
parents: 54282
diff changeset
   369
    f (T, U) #> (if s = s' then fold (fold_subtype_pairs f) (Ts ~~ Us) else I)
6f0a49ed1bb1 fourth attempt at generalizing N2M types (to leverage caching)
blanchet
parents: 54282
diff changeset
   370
  | fold_subtype_pairs f TU = f TU;
6f0a49ed1bb1 fourth attempt at generalizing N2M types (to leverage caching)
blanchet
parents: 54282
diff changeset
   371
55772
367ec44763fd correct most general type for mutual recursion when several identical types are involved
blanchet
parents: 55702
diff changeset
   372
val impossible_caller = Bound ~1;
367ec44763fd correct most general type for mutual recursion when several identical types are involved
blanchet
parents: 55702
diff changeset
   373
58335
a5a3b576fcfb generate 'code' attribute only if 'code' plugin is enabled
blanchet
parents: 58315
diff changeset
   374
fun nested_to_mutual_fps plugins fp actual_bs actual_Ts actual_callers actual_callssss0 lthy =
53303
ae49b835ca01 moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff changeset
   375
  let
ae49b835ca01 moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff changeset
   376
    val qsoty = quote o Syntax.string_of_typ lthy;
ae49b835ca01 moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff changeset
   377
    val qsotys = space_implode " or " o map qsoty;
ae49b835ca01 moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff changeset
   378
ae49b835ca01 moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff changeset
   379
    fun not_co_datatype0 T = error (qsoty T ^ " is not a " ^ co_prefix fp ^ "datatype");
ae49b835ca01 moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff changeset
   380
    fun not_co_datatype (T as Type (s, _)) =
ae49b835ca01 moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff changeset
   381
        if fp = Least_FP andalso
58112
8081087096ad renamed modules defining old datatypes, as a step towards having 'datatype_new' take 'datatype's place
blanchet
parents: 57983
diff changeset
   382
           is_some (Old_Datatype_Data.get_info (Proof_Context.theory_of lthy) s) then
58315
6d8458bc6e27 tuning terminology
blanchet
parents: 58310
diff changeset
   383
          error (qsoty T ^ " is an old-style datatype")
53303
ae49b835ca01 moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff changeset
   384
        else
ae49b835ca01 moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff changeset
   385
          not_co_datatype0 T
ae49b835ca01 moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff changeset
   386
      | not_co_datatype T = not_co_datatype0 T;
54303
4f55054d197c reintroduced check from bd36da55d825 after all, due to hard-to-solve issues outside the N2M code
blanchet
parents: 54302
diff changeset
   387
    fun not_mutually_nested_rec Ts1 Ts2 =
4f55054d197c reintroduced check from bd36da55d825 after all, due to hard-to-solve issues outside the N2M code
blanchet
parents: 54302
diff changeset
   388
      error (qsotys Ts1 ^ " is neither mutually recursive with " ^ qsotys Ts2 ^
55480
59cc4a8bc28a allow different functions to recurse on the same type, like in the old package
blanchet
parents: 55479
diff changeset
   389
        " nor nested recursive through " ^
58117
9608028d8f43 more compatibility between old- and new-style datatypes
blanchet
parents: 58115
diff changeset
   390
        (if Ts1 = Ts2 andalso length Ts1 = 1 then "itself" else qsotys Ts2));
53303
ae49b835ca01 moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff changeset
   391
55480
59cc4a8bc28a allow different functions to recurse on the same type, like in the old package
blanchet
parents: 55479
diff changeset
   392
    val sorted_actual_Ts =
54266
4e0738356ac9 stronger normalization, to increase n2m cache effectiveness
blanchet
parents: 54265
diff changeset
   393
      sort (prod_ord int_ord Term_Ord.typ_ord o pairself (`Term.size_of_typ)) actual_Ts;
53303
ae49b835ca01 moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff changeset
   394
54283
6f0a49ed1bb1 fourth attempt at generalizing N2M types (to leverage caching)
blanchet
parents: 54282
diff changeset
   395
    fun the_ctrs_of (Type (s, Ts)) = map (mk_ctr Ts) (#ctrs (the (ctr_sugar_of lthy s)));
6f0a49ed1bb1 fourth attempt at generalizing N2M types (to leverage caching)
blanchet
parents: 54282
diff changeset
   396
54282
blanchet
parents: 54280
diff changeset
   397
    fun the_fp_sugar_of (T as Type (T_name, _)) =
blanchet
parents: 54280
diff changeset
   398
      (case fp_sugar_of lthy T_name of
blanchet
parents: 54280
diff changeset
   399
        SOME (fp_sugar as {fp = fp', ...}) => if fp = fp' then fp_sugar else not_co_datatype T
blanchet
parents: 54280
diff changeset
   400
      | NONE => not_co_datatype T);
blanchet
parents: 54280
diff changeset
   401
54283
6f0a49ed1bb1 fourth attempt at generalizing N2M types (to leverage caching)
blanchet
parents: 54282
diff changeset
   402
    fun gen_rhss_in gen_Ts rho subTs =
6f0a49ed1bb1 fourth attempt at generalizing N2M types (to leverage caching)
blanchet
parents: 54282
diff changeset
   403
      let
6f0a49ed1bb1 fourth attempt at generalizing N2M types (to leverage caching)
blanchet
parents: 54282
diff changeset
   404
        fun maybe_insert (T, Type (_, gen_tyargs)) =
6f0a49ed1bb1 fourth attempt at generalizing N2M types (to leverage caching)
blanchet
parents: 54282
diff changeset
   405
            if member (op =) subTs T then insert (op =) gen_tyargs else I
6f0a49ed1bb1 fourth attempt at generalizing N2M types (to leverage caching)
blanchet
parents: 54282
diff changeset
   406
          | maybe_insert _ = I;
6f0a49ed1bb1 fourth attempt at generalizing N2M types (to leverage caching)
blanchet
parents: 54282
diff changeset
   407
6f0a49ed1bb1 fourth attempt at generalizing N2M types (to leverage caching)
blanchet
parents: 54282
diff changeset
   408
        val ctrs = maps the_ctrs_of gen_Ts;
6f0a49ed1bb1 fourth attempt at generalizing N2M types (to leverage caching)
blanchet
parents: 54282
diff changeset
   409
        val gen_ctr_Ts = maps (binder_types o fastype_of) ctrs;
6f0a49ed1bb1 fourth attempt at generalizing N2M types (to leverage caching)
blanchet
parents: 54282
diff changeset
   410
        val ctr_Ts = map (Term.typ_subst_atomic rho) gen_ctr_Ts;
6f0a49ed1bb1 fourth attempt at generalizing N2M types (to leverage caching)
blanchet
parents: 54282
diff changeset
   411
      in
6f0a49ed1bb1 fourth attempt at generalizing N2M types (to leverage caching)
blanchet
parents: 54282
diff changeset
   412
        fold (fold_subtype_pairs maybe_insert) (ctr_Ts ~~ gen_ctr_Ts) []
6f0a49ed1bb1 fourth attempt at generalizing N2M types (to leverage caching)
blanchet
parents: 54282
diff changeset
   413
      end;
6f0a49ed1bb1 fourth attempt at generalizing N2M types (to leverage caching)
blanchet
parents: 54282
diff changeset
   414
56485
008634379465 generate cliques for 'prim(co)rec' N2M
blanchet
parents: 56484
diff changeset
   415
    fun gather_types _ _ rev_seens gen_seen [] = (rev rev_seens, gen_seen)
008634379465 generate cliques for 'prim(co)rec' N2M
blanchet
parents: 56484
diff changeset
   416
      | gather_types lthy rho rev_seens gen_seen ((T as Type (_, tyargs)) :: Ts) =
54282
blanchet
parents: 54280
diff changeset
   417
        let
58234
265aea1e9985 honour sorts in N2M
blanchet
parents: 58222
diff changeset
   418
          val {T = Type (_, tyargs0), fp_res = {Ts = mutual_Ts0, ...}, ...} = the_fp_sugar_of T;
54283
6f0a49ed1bb1 fourth attempt at generalizing N2M types (to leverage caching)
blanchet
parents: 54282
diff changeset
   419
          val mutual_Ts = map (retypargs tyargs) mutual_Ts0;
6f0a49ed1bb1 fourth attempt at generalizing N2M types (to leverage caching)
blanchet
parents: 54282
diff changeset
   420
56485
008634379465 generate cliques for 'prim(co)rec' N2M
blanchet
parents: 56484
diff changeset
   421
          val rev_seen = flat rev_seens;
008634379465 generate cliques for 'prim(co)rec' N2M
blanchet
parents: 56484
diff changeset
   422
          val _ = null rev_seens orelse exists (exists_strict_subtype_in rev_seen) mutual_Ts orelse
008634379465 generate cliques for 'prim(co)rec' N2M
blanchet
parents: 56484
diff changeset
   423
            not_mutually_nested_rec mutual_Ts rev_seen;
54303
4f55054d197c reintroduced check from bd36da55d825 after all, due to hard-to-solve issues outside the N2M code
blanchet
parents: 54302
diff changeset
   424
54283
6f0a49ed1bb1 fourth attempt at generalizing N2M types (to leverage caching)
blanchet
parents: 54282
diff changeset
   425
          fun fresh_tyargs () =
6f0a49ed1bb1 fourth attempt at generalizing N2M types (to leverage caching)
blanchet
parents: 54282
diff changeset
   426
            let
58234
265aea1e9985 honour sorts in N2M
blanchet
parents: 58222
diff changeset
   427
              val (unsorted_gen_tyargs, lthy') =
58280
2ec3e2de34c3 more canonical (and correct) local theory threading
blanchet
parents: 58236
diff changeset
   428
                variant_tfrees (replicate (length tyargs) "z") lthy
54283
6f0a49ed1bb1 fourth attempt at generalizing N2M types (to leverage caching)
blanchet
parents: 54282
diff changeset
   429
                |>> map Logic.varifyT_global;
58234
265aea1e9985 honour sorts in N2M
blanchet
parents: 58222
diff changeset
   430
              val gen_tyargs =
265aea1e9985 honour sorts in N2M
blanchet
parents: 58222
diff changeset
   431
                map2 (resort_tfree_or_tvar o snd o dest_TFree_or_TVar) tyargs0 unsorted_gen_tyargs;
54283
6f0a49ed1bb1 fourth attempt at generalizing N2M types (to leverage caching)
blanchet
parents: 54282
diff changeset
   432
              val rho' = (gen_tyargs ~~ tyargs) @ rho;
6f0a49ed1bb1 fourth attempt at generalizing N2M types (to leverage caching)
blanchet
parents: 54282
diff changeset
   433
            in
6f0a49ed1bb1 fourth attempt at generalizing N2M types (to leverage caching)
blanchet
parents: 54282
diff changeset
   434
              (rho', gen_tyargs, gen_seen, lthy')
6f0a49ed1bb1 fourth attempt at generalizing N2M types (to leverage caching)
blanchet
parents: 54282
diff changeset
   435
            end;
6f0a49ed1bb1 fourth attempt at generalizing N2M types (to leverage caching)
blanchet
parents: 54282
diff changeset
   436
6f0a49ed1bb1 fourth attempt at generalizing N2M types (to leverage caching)
blanchet
parents: 54282
diff changeset
   437
          val (rho', gen_tyargs, gen_seen', lthy') =
56485
008634379465 generate cliques for 'prim(co)rec' N2M
blanchet
parents: 56484
diff changeset
   438
            if exists (exists_subtype_in rev_seen) mutual_Ts then
54283
6f0a49ed1bb1 fourth attempt at generalizing N2M types (to leverage caching)
blanchet
parents: 54282
diff changeset
   439
              (case gen_rhss_in gen_seen rho mutual_Ts of
6f0a49ed1bb1 fourth attempt at generalizing N2M types (to leverage caching)
blanchet
parents: 54282
diff changeset
   440
                [] => fresh_tyargs ()
54899
7a01387c47d5 added tactic to prove 'disc_iff' properties in 'primcorec'
blanchet
parents: 54740
diff changeset
   441
              | gen_tyargs :: gen_tyargss_tl =>
54283
6f0a49ed1bb1 fourth attempt at generalizing N2M types (to leverage caching)
blanchet
parents: 54282
diff changeset
   442
                let
6f0a49ed1bb1 fourth attempt at generalizing N2M types (to leverage caching)
blanchet
parents: 54282
diff changeset
   443
                  val unify_pairs = split_list (maps (curry (op ~~) gen_tyargs) gen_tyargss_tl);
6f0a49ed1bb1 fourth attempt at generalizing N2M types (to leverage caching)
blanchet
parents: 54282
diff changeset
   444
                  val mgu = Type.raw_unifys unify_pairs Vartab.empty;
58948
f6ecc0fb2066 proper Envir.norm_type for result of Type.raw_unifys;
wenzelm
parents: 58734
diff changeset
   445
                  val gen_tyargs' = map (Envir.norm_type mgu) gen_tyargs;
f6ecc0fb2066 proper Envir.norm_type for result of Type.raw_unifys;
wenzelm
parents: 58734
diff changeset
   446
                  val gen_seen' = map (Envir.norm_type mgu) gen_seen;
54283
6f0a49ed1bb1 fourth attempt at generalizing N2M types (to leverage caching)
blanchet
parents: 54282
diff changeset
   447
                in
6f0a49ed1bb1 fourth attempt at generalizing N2M types (to leverage caching)
blanchet
parents: 54282
diff changeset
   448
                  (rho, gen_tyargs', gen_seen', lthy)
6f0a49ed1bb1 fourth attempt at generalizing N2M types (to leverage caching)
blanchet
parents: 54282
diff changeset
   449
                end)
6f0a49ed1bb1 fourth attempt at generalizing N2M types (to leverage caching)
blanchet
parents: 54282
diff changeset
   450
            else
6f0a49ed1bb1 fourth attempt at generalizing N2M types (to leverage caching)
blanchet
parents: 54282
diff changeset
   451
              fresh_tyargs ();
6f0a49ed1bb1 fourth attempt at generalizing N2M types (to leverage caching)
blanchet
parents: 54282
diff changeset
   452
6f0a49ed1bb1 fourth attempt at generalizing N2M types (to leverage caching)
blanchet
parents: 54282
diff changeset
   453
          val gen_mutual_Ts = map (retypargs gen_tyargs) mutual_Ts0;
55480
59cc4a8bc28a allow different functions to recurse on the same type, like in the old package
blanchet
parents: 55479
diff changeset
   454
          val other_mutual_Ts = remove1 (op =) T mutual_Ts;
59cc4a8bc28a allow different functions to recurse on the same type, like in the old package
blanchet
parents: 55479
diff changeset
   455
          val Ts' = fold (remove1 (op =)) other_mutual_Ts Ts;
54282
blanchet
parents: 54280
diff changeset
   456
        in
56485
008634379465 generate cliques for 'prim(co)rec' N2M
blanchet
parents: 56484
diff changeset
   457
          gather_types lthy' rho' (mutual_Ts :: rev_seens) (gen_seen' @ gen_mutual_Ts) Ts'
54282
blanchet
parents: 54280
diff changeset
   458
        end
56485
008634379465 generate cliques for 'prim(co)rec' N2M
blanchet
parents: 56484
diff changeset
   459
      | gather_types _ _ _ _ (T :: _) = not_co_datatype T;
53303
ae49b835ca01 moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff changeset
   460
56485
008634379465 generate cliques for 'prim(co)rec' N2M
blanchet
parents: 56484
diff changeset
   461
    val (perm_Tss, perm_gen_Ts) = gather_types lthy [] [] [] sorted_actual_Ts;
58340
blanchet
parents: 58335
diff changeset
   462
    val (perm_mutual_cliques, perm_Ts) =
56485
008634379465 generate cliques for 'prim(co)rec' N2M
blanchet
parents: 56484
diff changeset
   463
      split_list (flat (map_index (fn (i, perm_Ts) => map (pair i) perm_Ts) perm_Tss));
008634379465 generate cliques for 'prim(co)rec' N2M
blanchet
parents: 56484
diff changeset
   464
54283
6f0a49ed1bb1 fourth attempt at generalizing N2M types (to leverage caching)
blanchet
parents: 54282
diff changeset
   465
    val perm_frozen_gen_Ts = map Logic.unvarifyT_global perm_gen_Ts;
6f0a49ed1bb1 fourth attempt at generalizing N2M types (to leverage caching)
blanchet
parents: 54282
diff changeset
   466
56484
c451cf8b29c8 thread mutual cliques through
blanchet
parents: 55966
diff changeset
   467
    val missing_Ts = fold (remove1 (op =)) actual_Ts perm_Ts;
53303
ae49b835ca01 moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff changeset
   468
    val Ts = actual_Ts @ missing_Ts;
ae49b835ca01 moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff changeset
   469
ae49b835ca01 moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff changeset
   470
    val nn = length Ts;
ae49b835ca01 moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff changeset
   471
    val kks = 0 upto nn - 1;
ae49b835ca01 moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff changeset
   472
54267
78e8a178b690 use right permutation in 'map2'
blanchet
parents: 54266
diff changeset
   473
    val callssss0 = pad_list [] nn actual_callssss0;
78e8a178b690 use right permutation in 'map2'
blanchet
parents: 54266
diff changeset
   474
53303
ae49b835ca01 moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff changeset
   475
    val common_name = mk_common_name (map Binding.name_of actual_bs);
ae49b835ca01 moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff changeset
   476
    val bs = pad_list (Binding.name common_name) nn actual_bs;
55772
367ec44763fd correct most general type for mutual recursion when several identical types are involved
blanchet
parents: 55702
diff changeset
   477
    val callers = pad_list impossible_caller nn actual_callers;
53303
ae49b835ca01 moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff changeset
   478
ae49b835ca01 moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff changeset
   479
    fun permute xs = permute_like (op =) Ts perm_Ts xs;
ae49b835ca01 moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff changeset
   480
    fun unpermute perm_xs = permute_like (op =) perm_Ts Ts perm_xs;
ae49b835ca01 moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff changeset
   481
58340
blanchet
parents: 58335
diff changeset
   482
    (* The assignment of callers to mutual cliques is incorrect in general. This code would need to
blanchet
parents: 58335
diff changeset
   483
       inspect the actual calls to discover the correct cliques in the presence of type duplicates.
blanchet
parents: 58335
diff changeset
   484
       However, the naive scheme implemented here supports "prim(co)rec" specifications following
blanchet
parents: 58335
diff changeset
   485
       reasonable ordering of the duplicates (e.g., keeping the cliques together). *)
53303
ae49b835ca01 moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff changeset
   486
    val perm_bs = permute bs;
55772
367ec44763fd correct most general type for mutual recursion when several identical types are involved
blanchet
parents: 55702
diff changeset
   487
    val perm_callers = permute callers;
53303
ae49b835ca01 moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff changeset
   488
    val perm_kks = permute kks;
54267
78e8a178b690 use right permutation in 'map2'
blanchet
parents: 54266
diff changeset
   489
    val perm_callssss0 = permute callssss0;
53303
ae49b835ca01 moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff changeset
   490
    val perm_fp_sugars0 = map (the o fp_sugar_of lthy o fst o dest_Type) perm_Ts;
ae49b835ca01 moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff changeset
   491
58460
a88eb33058f7 refactor fp_sugar move theorems
desharna
parents: 58459
diff changeset
   492
    val perm_callssss =
a88eb33058f7 refactor fp_sugar move theorems
desharna
parents: 58459
diff changeset
   493
      map2 (indexify_callsss o #ctrs o #ctr_sugar o #fp_ctr_sugar) perm_fp_sugars0 perm_callssss0;
53303
ae49b835ca01 moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff changeset
   494
53746
bd038e48526d have "datatype_new_compat" register induction and recursion theorems in nested case
blanchet
parents: 53678
diff changeset
   495
    val ((perm_fp_sugars, fp_sugar_thms), lthy) =
58117
9608028d8f43 more compatibility between old- and new-style datatypes
blanchet
parents: 58115
diff changeset
   496
      if length perm_Tss = 1 then
56485
008634379465 generate cliques for 'prim(co)rec' N2M
blanchet
parents: 56484
diff changeset
   497
        ((perm_fp_sugars0, (NONE, NONE)), lthy)
008634379465 generate cliques for 'prim(co)rec' N2M
blanchet
parents: 56484
diff changeset
   498
      else
58340
blanchet
parents: 58335
diff changeset
   499
        mutualize_fp_sugars plugins fp perm_mutual_cliques perm_bs perm_frozen_gen_Ts perm_callers
58335
a5a3b576fcfb generate 'code' attribute only if 'code' plugin is enabled
blanchet
parents: 58315
diff changeset
   500
          perm_callssss perm_fp_sugars0 lthy;
53303
ae49b835ca01 moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff changeset
   501
ae49b835ca01 moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff changeset
   502
    val fp_sugars = unpermute perm_fp_sugars;
ae49b835ca01 moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff changeset
   503
  in
53746
bd038e48526d have "datatype_new_compat" register induction and recursion theorems in nested case
blanchet
parents: 53678
diff changeset
   504
    ((missing_Ts, perm_kks, fp_sugars, fp_sugar_thms), lthy)
53303
ae49b835ca01 moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff changeset
   505
  end;
ae49b835ca01 moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff changeset
   506
ae49b835ca01 moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff changeset
   507
end;