src/HOL/Tools/BNF/bnf_fp_n2m_sugar.ML
author haftmann
Tue Oct 13 09:21:15 2015 +0200 (2015-10-13)
changeset 61424 c3658c18b7bc
parent 61334 8d40ddaa427f
child 61551 078c9fd2e052
permissions -rw-r--r--
prod_case as canonical name for product type eliminator
blanchet@55061
     1
(*  Title:      HOL/Tools/BNF/bnf_fp_n2m_sugar.ML
blanchet@53303
     2
    Author:     Jasmin Blanchette, TU Muenchen
blanchet@53303
     3
    Copyright   2013
blanchet@53303
     4
blanchet@53303
     5
Suggared flattening of nested to mutual (co)recursion.
blanchet@53303
     6
*)
blanchet@53303
     7
blanchet@53303
     8
signature BNF_FP_N2M_SUGAR =
blanchet@53303
     9
sig
blanchet@55343
    10
  val unfold_lets_splits: term -> term
blanchet@57895
    11
  val unfold_splits_lets: term -> term
blanchet@54243
    12
  val dest_map: Proof.context -> string -> term -> term * term list
blanchet@54243
    13
blanchet@58335
    14
  val mutualize_fp_sugars: (string -> bool) -> BNF_Util.fp_kind -> int list -> binding list ->
blanchet@58335
    15
    typ list -> term list -> term list list list list -> BNF_FP_Def_Sugar.fp_sugar list ->
blanchet@58335
    16
    local_theory ->
blanchet@58180
    17
    (BNF_FP_Def_Sugar.fp_sugar list
blanchet@53746
    18
     * (BNF_FP_Def_Sugar.lfp_sugar_thms option * BNF_FP_Def_Sugar.gfp_sugar_thms option))
blanchet@53746
    19
    * local_theory
blanchet@58335
    20
  val nested_to_mutual_fps: (string -> bool) -> BNF_Util.fp_kind -> binding list -> typ list ->
blanchet@58335
    21
    term list -> (term * term list list) list list -> local_theory ->
blanchet@58180
    22
    (typ list * int list * BNF_FP_Def_Sugar.fp_sugar list
blanchet@53746
    23
     * (BNF_FP_Def_Sugar.lfp_sugar_thms option * BNF_FP_Def_Sugar.gfp_sugar_thms option))
blanchet@53746
    24
    * local_theory
blanchet@53303
    25
end;
blanchet@53303
    26
blanchet@53303
    27
structure BNF_FP_N2M_Sugar : BNF_FP_N2M_SUGAR =
blanchet@53303
    28
struct
blanchet@53303
    29
blanchet@54006
    30
open Ctr_Sugar
blanchet@53303
    31
open BNF_Util
blanchet@53303
    32
open BNF_Def
blanchet@53303
    33
open BNF_FP_Util
blanchet@53303
    34
open BNF_FP_Def_Sugar
blanchet@53303
    35
open BNF_FP_N2M
blanchet@53303
    36
blanchet@59662
    37
val n2mN = "n2m_";
blanchet@53303
    38
blanchet@54256
    39
type n2m_sugar = fp_sugar list * (lfp_sugar_thms option * gfp_sugar_thms option);
blanchet@54256
    40
blanchet@54256
    41
structure Data = Generic_Data
blanchet@54256
    42
(
blanchet@54256
    43
  type T = n2m_sugar Typtab.table;
blanchet@54256
    44
  val empty = Typtab.empty;
blanchet@54256
    45
  val extend = I;
blanchet@55394
    46
  fun merge data : T = Typtab.merge (K true) data;
blanchet@54256
    47
);
blanchet@54256
    48
blanchet@54256
    49
fun morph_n2m_sugar phi (fp_sugars, (lfp_sugar_thms_opt, gfp_sugar_thms_opt)) =
blanchet@54256
    50
  (map (morph_fp_sugar phi) fp_sugars,
blanchet@54256
    51
   (Option.map (morph_lfp_sugar_thms phi) lfp_sugar_thms_opt,
blanchet@54256
    52
    Option.map (morph_gfp_sugar_thms phi) gfp_sugar_thms_opt));
blanchet@54256
    53
blanchet@58115
    54
val transfer_n2m_sugar = morph_n2m_sugar o Morphism.transfer_morphism;
blanchet@54256
    55
blanchet@54256
    56
fun n2m_sugar_of ctxt =
blanchet@54256
    57
  Typtab.lookup (Data.get (Context.Proof ctxt))
blanchet@58115
    58
  #> Option.map (transfer_n2m_sugar (Proof_Context.theory_of ctxt));
blanchet@54256
    59
blanchet@54256
    60
fun register_n2m_sugar key n2m_sugar =
blanchet@54256
    61
  Local_Theory.declaration {syntax = false, pervasive = false}
blanchet@55444
    62
    (fn phi => Data.map (Typtab.update (key, morph_n2m_sugar phi n2m_sugar)));
blanchet@54256
    63
blanchet@57895
    64
fun unfold_lets_splits (Const (@{const_name Let}, _) $ t $ u) =
blanchet@57897
    65
    unfold_lets_splits (betapply (unfold_splits_lets u, t))
blanchet@57895
    66
  | unfold_lets_splits (t $ u) = betapply (unfold_lets_splits t, unfold_lets_splits u)
blanchet@57895
    67
  | unfold_lets_splits (Abs (s, T, t)) = Abs (s, T, unfold_lets_splits t)
blanchet@57895
    68
  | unfold_lets_splits t = t
haftmann@61424
    69
and unfold_splits_lets ((t as Const (@{const_name case_prod}, _)) $ u) =
blanchet@57895
    70
    (case unfold_splits_lets u of
blanchet@55336
    71
      u' as Abs (s1, T1, Abs (s2, T2, _)) =>
blanchet@55336
    72
      let val v = Var ((s1 ^ s2, Term.maxidx_of_term u' + 1), HOLogic.mk_prodT (T1, T2)) in
blanchet@55336
    73
        lambda v (incr_boundvars 1 (betapplys (u', [HOLogic.mk_fst v, HOLogic.mk_snd v])))
blanchet@54243
    74
      end
blanchet@57897
    75
    | _ => t $ unfold_lets_splits u)
blanchet@57897
    76
  | unfold_splits_lets (t as Const (@{const_name Let}, _) $ _ $ _) = unfold_lets_splits t
blanchet@57897
    77
  | unfold_splits_lets (t $ u) = betapply (unfold_splits_lets t, unfold_lets_splits u)
blanchet@57895
    78
  | unfold_splits_lets (Abs (s, T, t)) = Abs (s, T, unfold_splits_lets t)
blanchet@57895
    79
  | unfold_splits_lets t = unfold_lets_splits t;
blanchet@54243
    80
blanchet@54243
    81
fun mk_map_pattern ctxt s =
blanchet@54243
    82
  let
blanchet@54243
    83
    val bnf = the (bnf_of ctxt s);
blanchet@54243
    84
    val mapx = map_of_bnf bnf;
blanchet@54243
    85
    val live = live_of_bnf bnf;
blanchet@54243
    86
    val (f_Ts, _) = strip_typeN live (fastype_of mapx);
blanchet@54265
    87
    val fs = map_index (fn (i, T) => Var (("?f", i), T)) f_Ts;
blanchet@54243
    88
  in
blanchet@54243
    89
    (mapx, betapplys (mapx, fs))
blanchet@54243
    90
  end;
blanchet@54243
    91
blanchet@54243
    92
fun dest_map ctxt s call =
blanchet@54243
    93
  let
blanchet@54243
    94
    val (map0, pat) = mk_map_pattern ctxt s;
blanchet@54243
    95
    val (_, tenv) = fo_match ctxt call pat;
blanchet@54243
    96
  in
blanchet@54243
    97
    (map0, Vartab.fold_rev (fn (_, (_, f)) => cons f) tenv [])
blanchet@54243
    98
  end;
blanchet@54243
    99
blanchet@54276
   100
fun dest_abs_or_applied_map _ _ (Abs (_, _, t)) = (Term.dummy, [t])
blanchet@54276
   101
  | dest_abs_or_applied_map ctxt s (t1 $ _) = dest_map ctxt s t1;
blanchet@54239
   102
blanchet@54245
   103
fun map_partition f xs =
blanchet@54245
   104
  fold_rev (fn x => fn (ys, (good, bad)) =>
blanchet@54245
   105
      case f x of SOME y => (y :: ys, (x :: good, bad)) | NONE => (ys, (good, x :: bad)))
blanchet@54245
   106
    xs ([], ([], []));
blanchet@54245
   107
blanchet@58222
   108
fun key_of_fp_eqs fp As fpTs fp_eqs =
blanchet@58222
   109
  Type (case_fp fp "l" "g", fpTs @ maps (fn (x, T) => [TFree x, T]) fp_eqs)
blanchet@58222
   110
  |> Term.map_atyps (fn T as TFree (_, S) =>
blanchet@58222
   111
    (case find_index (curry (op =) T) As of
blanchet@58222
   112
      ~1 => T
blanchet@58222
   113
    | j => TFree ("'" ^ string_of_int j, S)));
blanchet@54256
   114
blanchet@55772
   115
fun get_indices callers t =
blanchet@55772
   116
  callers
blanchet@55772
   117
  |> map_index (fn (i, v) => if exists_subterm (equal v) t then SOME i else NONE)
blanchet@55772
   118
  |> map_filter I;
blanchet@55772
   119
blanchet@58340
   120
fun mutualize_fp_sugars plugins fp mutual_cliques bs fpTs callers callssss fp_sugars0 no_defs_lthy =
blanchet@54286
   121
  let
blanchet@58280
   122
    val thy = Proof_Context.theory_of no_defs_lthy;
blanchet@53303
   123
blanchet@58280
   124
    val qsotm = quote o Syntax.string_of_term no_defs_lthy;
blanchet@53303
   125
blanchet@55479
   126
    fun incompatible_calls ts =
blanchet@55479
   127
      error ("Incompatible " ^ co_prefix fp ^ "recursive calls: " ^ commas (map qsotm ts));
blanchet@55772
   128
    fun mutual_self_call caller t =
blanchet@55772
   129
      error ("Unsupported mutual self-call " ^ qsotm t ^ " from " ^ qsotm caller);
blanchet@54301
   130
    fun nested_self_call t =
blanchet@54301
   131
      error ("Unsupported nested self-call " ^ qsotm t);
blanchet@54245
   132
blanchet@54286
   133
    val b_names = map Binding.name_of bs;
blanchet@54286
   134
    val fp_b_names = map base_name_of_typ fpTs;
blanchet@53303
   135
blanchet@54286
   136
    val nn = length fpTs;
blanchet@55539
   137
    val kks = 0 upto nn - 1;
blanchet@53303
   138
desharna@58460
   139
    fun target_ctr_sugar_of_fp_sugar fpT ({T, fp_ctr_sugar = {ctr_sugar, ...}, ...} : fp_sugar) =
blanchet@54286
   140
      let
blanchet@54286
   141
        val rho = Vartab.fold (cons o apsnd snd) (Sign.typ_match thy (T, fpT) Vartab.empty) [];
wenzelm@54740
   142
        val phi = Morphism.term_morphism "BNF" (Term.subst_TVars rho);
blanchet@54286
   143
      in
blanchet@55539
   144
        morph_ctr_sugar phi ctr_sugar
blanchet@54286
   145
      end;
blanchet@53303
   146
desharna@58460
   147
    val ctr_defss = map (#ctr_defs o #fp_ctr_sugar) fp_sugars0;
desharna@58462
   148
    val mapss = map (#map_thms o #fp_bnf_sugar) fp_sugars0;
blanchet@54302
   149
    val ctr_sugars = map2 target_ctr_sugar_of_fp_sugar fpTs fp_sugars0;
blanchet@53303
   150
blanchet@54302
   151
    val ctrss = map #ctrs ctr_sugars;
blanchet@54286
   152
    val ctr_Tss = map (map fastype_of) ctrss;
blanchet@53303
   153
blanchet@54286
   154
    val As' = fold (fold Term.add_tfreesT) ctr_Tss [];
blanchet@58236
   155
    val unsorted_As' = map (apsnd (K @{sort type})) As';
blanchet@54286
   156
    val As = map TFree As';
blanchet@58236
   157
    val unsorted_As = map TFree unsorted_As';
blanchet@58236
   158
blanchet@58236
   159
    val unsortAT = Term.typ_subst_atomic (As ~~ unsorted_As);
blanchet@58236
   160
    val unsorted_fpTs = map unsortAT fpTs;
blanchet@53303
   161
traytel@61334
   162
    val ((Cs, Xs), _) =
blanchet@58280
   163
      no_defs_lthy
blanchet@54286
   164
      |> fold Variable.declare_typ As
blanchet@54286
   165
      |> mk_TFrees nn
blanchet@54286
   166
      ||>> variant_tfrees fp_b_names;
blanchet@53303
   167
blanchet@54286
   168
    fun check_call_dead live_call call =
blanchet@55772
   169
      if null (get_indices callers call) then () else incompatible_calls [live_call, call];
blanchet@54245
   170
blanchet@55480
   171
    fun freeze_fpTs_type_based_default (T as Type (s, Ts)) =
blanchet@55480
   172
        (case filter (curry (op =) T o snd) (map_index I fpTs) of
blanchet@55480
   173
          [(kk, _)] => nth Xs kk
blanchet@55480
   174
        | _ => Type (s, map freeze_fpTs_type_based_default Ts))
blanchet@55480
   175
      | freeze_fpTs_type_based_default T = T;
blanchet@55479
   176
blanchet@55772
   177
    fun freeze_fpTs_mutual_call kk fpT calls T =
blanchet@55772
   178
      (case fold (union (op =)) (map (get_indices callers) calls) [] of
blanchet@55772
   179
        [] => if T = fpT then nth Xs kk else freeze_fpTs_type_based_default T
blanchet@55772
   180
      | [kk'] =>
blanchet@55772
   181
        if T = fpT andalso kk' <> kk then
blanchet@55772
   182
          mutual_self_call (nth callers kk)
blanchet@55772
   183
            (the (find_first (not o null o get_indices callers) calls))
blanchet@58290
   184
        else if T = nth fpTs kk' then
blanchet@58290
   185
          nth Xs kk'
blanchet@55772
   186
        else
blanchet@58290
   187
          freeze_fpTs_type_based_default T
blanchet@55480
   188
      | _ => incompatible_calls calls);
blanchet@54253
   189
blanchet@55772
   190
    fun freeze_fpTs_map kk (fpT as Type (_, Ts')) (callss, (live_call :: _, dead_calls))
blanchet@55480
   191
        (Type (s, Ts)) =
blanchet@54301
   192
      if Ts' = Ts then
blanchet@54301
   193
        nested_self_call live_call
blanchet@54301
   194
      else
blanchet@54301
   195
        (List.app (check_call_dead live_call) dead_calls;
blanchet@55772
   196
         Type (s, map2 (freeze_fpTs_call kk fpT)
blanchet@55480
   197
           (flatten_type_args_of_bnf (the (bnf_of no_defs_lthy s)) [] (transpose callss)) Ts))
blanchet@55772
   198
    and freeze_fpTs_call kk fpT calls (T as Type (s, _)) =
blanchet@54286
   199
        (case map_partition (try (snd o dest_map no_defs_lthy s)) calls of
blanchet@54286
   200
          ([], _) =>
blanchet@54286
   201
          (case map_partition (try (snd o dest_abs_or_applied_map no_defs_lthy s)) calls of
blanchet@55772
   202
            ([], _) => freeze_fpTs_mutual_call kk fpT calls T
blanchet@55772
   203
          | callsp => freeze_fpTs_map kk fpT callsp T)
blanchet@55772
   204
        | callsp => freeze_fpTs_map kk fpT callsp T)
blanchet@55772
   205
      | freeze_fpTs_call _ _ _ T = T;
blanchet@53303
   206
blanchet@54286
   207
    val ctr_Tsss = map (map binder_types) ctr_Tss;
wenzelm@58634
   208
    val ctrXs_Tsss = @{map 4} (map2 o map2 oo freeze_fpTs_call) kks fpTs callssss ctr_Tsss;
blanchet@55966
   209
    val ctrXs_repTs = map mk_sumprodT_balanced ctrXs_Tsss;
blanchet@53303
   210
blanchet@54286
   211
    val ns = map length ctr_Tsss;
blanchet@54286
   212
    val kss = map (fn n => 1 upto n) ns;
blanchet@54286
   213
    val mss = map (map length) ctr_Tsss;
blanchet@53303
   214
blanchet@58236
   215
    val fp_eqs = map dest_TFree Xs ~~ map unsortAT ctrXs_repTs;
blanchet@58236
   216
    val key = key_of_fp_eqs fp unsorted_As unsorted_fpTs fp_eqs;
blanchet@54286
   217
  in
blanchet@54286
   218
    (case n2m_sugar_of no_defs_lthy key of
blanchet@54286
   219
      SOME n2m_sugar => (n2m_sugar, no_defs_lthy)
blanchet@54286
   220
    | NONE =>
blanchet@54286
   221
      let
blanchet@54286
   222
        val base_fp_names = Name.variant_list [] fp_b_names;
blanchet@54286
   223
        val fp_bs = map2 (fn b_name => fn base_fp_name =>
blanchet@54286
   224
            Binding.qualify true b_name (Binding.name (n2mN ^ base_fp_name)))
blanchet@54286
   225
          b_names base_fp_names;
blanchet@53303
   226
blanchet@55702
   227
        val Type (s, Us) :: _ = fpTs;
blanchet@55702
   228
        val killed_As' =
blanchet@55702
   229
          (case bnf_of no_defs_lthy s of
blanchet@58236
   230
            NONE => unsorted_As'
blanchet@55702
   231
          | SOME bnf =>
blanchet@55702
   232
            let
blanchet@55702
   233
              val Type (_, Ts) = T_of_bnf bnf;
blanchet@55702
   234
              val deads = deads_of_bnf bnf;
blanchet@55702
   235
              val dead_Us =
blanchet@55702
   236
                map_filter (fn (T, U) => if member (op =) deads T then SOME U else NONE) (Ts ~~ Us);
blanchet@55702
   237
            in fold Term.add_tfreesT dead_Us [] end);
blanchet@55702
   238
traytel@55803
   239
        val fp_absT_infos = map #absT_info fp_sugars0;
traytel@55803
   240
blanchet@58211
   241
        val ((pre_bnfs, absT_infos), (fp_res as {xtor_co_recs = xtor_co_recs0, xtor_co_induct,
blanchet@58211
   242
               dtor_injects, dtor_ctors, xtor_co_rec_thms, ...}, lthy)) =
blanchet@58340
   243
          fp_bnf (construct_mutualized_fp fp mutual_cliques unsorted_fpTs fp_sugars0) fp_bs
blanchet@58340
   244
            unsorted_As' killed_As' fp_eqs no_defs_lthy;
traytel@55803
   245
blanchet@58211
   246
        val fp_abs_inverses = map #abs_inverse fp_absT_infos;
blanchet@58211
   247
        val fp_type_definitions = map #type_definition fp_absT_infos;
traytel@55803
   248
blanchet@58211
   249
        val abss = map #abs absT_infos;
blanchet@58211
   250
        val reps = map #rep absT_infos;
blanchet@58211
   251
        val absTs = map #absT absT_infos;
blanchet@58211
   252
        val repTs = map #repT absT_infos;
blanchet@58211
   253
        val abs_inverses = map #abs_inverse absT_infos;
blanchet@53303
   254
blanchet@58211
   255
        val fp_nesting_bnfs = nesting_bnfs lthy ctrXs_Tsss Xs;
blanchet@58211
   256
        val live_nesting_bnfs = nesting_bnfs lthy ctrXs_Tsss As;
blanchet@53303
   257
blanchet@58211
   258
        val ((xtor_co_recs, recs_args_types, corecs_args_types), _) =
blanchet@58211
   259
          mk_co_recs_prelims fp ctr_Tsss fpTs Cs absTs repTs ns mss xtor_co_recs0 lthy;
blanchet@54256
   260
blanchet@58211
   261
        fun mk_binding b pre = Binding.prefix_name (pre ^ "_") b;
blanchet@53303
   262
blanchet@58211
   263
        val ((co_recs, co_rec_defs), lthy) =
wenzelm@58634
   264
          @{fold_map 2} (fn b =>
blanchet@58211
   265
              if fp = Least_FP then define_rec (the recs_args_types) (mk_binding b) fpTs Cs reps
blanchet@58211
   266
              else define_corec (the corecs_args_types) (mk_binding b) fpTs Cs abss)
blanchet@58211
   267
            fp_bs xtor_co_recs lthy
blanchet@58211
   268
          |>> split_list;
blanchet@58131
   269
blanchet@58211
   270
        val ((common_co_inducts, co_inductss', co_rec_thmss, co_rec_disc_thmss, co_rec_sel_thmsss),
blanchet@58211
   271
             fp_sugar_thms) =
blanchet@58211
   272
          if fp = Least_FP then
blanchet@58335
   273
            derive_induct_recs_thms_for_types plugins pre_bnfs recs_args_types xtor_co_induct
blanchet@58211
   274
              xtor_co_rec_thms live_nesting_bnfs fp_nesting_bnfs fpTs Cs Xs ctrXs_Tsss
blanchet@58211
   275
              fp_abs_inverses fp_type_definitions abs_inverses ctrss ctr_defss co_recs co_rec_defs
blanchet@58211
   276
              lthy
blanchet@58211
   277
            |> `(fn ((inducts, induct, _), (rec_thmss, _)) =>
blanchet@58211
   278
              ([induct], [inducts], rec_thmss, replicate nn [], replicate nn []))
blanchet@58211
   279
            ||> (fn info => (SOME info, NONE))
blanchet@58211
   280
          else
blanchet@58211
   281
            derive_coinduct_corecs_thms_for_types pre_bnfs (the corecs_args_types)
blanchet@58211
   282
              xtor_co_induct dtor_injects dtor_ctors xtor_co_rec_thms live_nesting_bnfs fpTs Cs Xs
blanchet@58211
   283
              ctrXs_Tsss kss mss ns fp_abs_inverses abs_inverses
traytel@61334
   284
              (fn thm => thm RS @{thm vimage2p_refl}) ctr_defss ctr_sugars co_recs co_rec_defs lthy
blanchet@58211
   285
            |> `(fn ((coinduct_thms_pairs, _), corec_thmss, corec_disc_thmss, _,
blanchet@58211
   286
                     (corec_sel_thmsss, _)) =>
blanchet@58211
   287
              (map snd coinduct_thms_pairs, map fst coinduct_thms_pairs, corec_thmss,
blanchet@58211
   288
               corec_disc_thmss, corec_sel_thmsss))
blanchet@58211
   289
            ||> (fn info => (NONE, SOME info));
blanchet@53303
   290
traytel@61334
   291
        val names_lthy = lthy |> fold Variable.declare_typ (As @ Cs @ Xs);
traytel@61334
   292
        val phi = Proof_Context.export_morphism names_lthy lthy;
blanchet@54256
   293
blanchet@56648
   294
        fun mk_target_fp_sugar T X kk pre_bnf absT_info ctrXs_Tss ctr_defs ctr_sugar co_rec
desharna@58462
   295
            co_rec_def map_thms co_inducts co_rec_thms co_rec_disc_thms co_rec_sel_thmss
desharna@58676
   296
            ({fp_ctr_sugar = {ctr_transfers, case_transfers, disc_transfers, sel_transfers, ...},
desharna@58672
   297
              fp_bnf_sugar = {map_disc_iffs, map_selss, rel_injects, rel_distincts, rel_sels,
desharna@58673
   298
                rel_intros, rel_cases, set_thms, set_selssss, set_introssss, set_cases, ...},
desharna@58574
   299
              fp_co_induct_sugar = {co_rec_disc_iffs, co_rec_codes, co_rec_transfers,
desharna@58734
   300
                co_rec_o_maps, common_rel_co_inducts, rel_co_inducts, common_set_inducts,
desharna@58732
   301
                set_inducts, ...},
desharna@58568
   302
              ...} : fp_sugar) =
blanchet@58117
   303
          {T = T, BT = T (*wrong but harmless*), X = X, fp = fp, fp_res = fp_res, fp_res_index = kk,
desharna@58674
   304
           pre_bnf = pre_bnf, fp_bnf = nth (#bnfs fp_res) kk, absT_info = absT_info,
desharna@58674
   305
           fp_nesting_bnfs = fp_nesting_bnfs, live_nesting_bnfs = live_nesting_bnfs,
desharna@58460
   306
           fp_ctr_sugar =
desharna@58460
   307
             {ctrXs_Tss = ctrXs_Tss,
desharna@58460
   308
              ctr_defs = ctr_defs,
desharna@58569
   309
              ctr_sugar = ctr_sugar,
desharna@58570
   310
              ctr_transfers = ctr_transfers,
desharna@58571
   311
              case_transfers = case_transfers,
desharna@58676
   312
              disc_transfers = disc_transfers,
desharna@58676
   313
              sel_transfers = sel_transfers},
desharna@58459
   314
           fp_bnf_sugar =
desharna@58462
   315
             {map_thms = map_thms,
desharna@58560
   316
              map_disc_iffs = map_disc_iffs,
desharna@58672
   317
              map_selss = map_selss,
desharna@58462
   318
              rel_injects = rel_injects,
desharna@58562
   319
              rel_distincts = rel_distincts,
desharna@58563
   320
              rel_sels = rel_sels,
desharna@58564
   321
              rel_intros = rel_intros,
desharna@58565
   322
              rel_cases = rel_cases,
desharna@58566
   323
              set_thms = set_thms,
desharna@58671
   324
              set_selssss = set_selssss,
desharna@58673
   325
              set_introssss = set_introssss,
desharna@58568
   326
              set_cases = set_cases},
desharna@58459
   327
           fp_co_induct_sugar =
desharna@58461
   328
             {co_rec = co_rec,
desharna@58461
   329
              common_co_inducts = common_co_inducts,
desharna@58461
   330
              co_inducts = co_inducts,
desharna@58674
   331
              co_rec_def = co_rec_def,
desharna@58459
   332
              co_rec_thms = co_rec_thms,
desharna@58459
   333
              co_rec_discs = co_rec_disc_thms,
desharna@58572
   334
              co_rec_disc_iffs = co_rec_disc_iffs,
desharna@58573
   335
              co_rec_selss = co_rec_sel_thmss,
desharna@58573
   336
              co_rec_codes = co_rec_codes,
desharna@58574
   337
              co_rec_transfers = co_rec_transfers,
desharna@58734
   338
              co_rec_o_maps = co_rec_o_maps,
desharna@58575
   339
              common_rel_co_inducts = common_rel_co_inducts,
desharna@58576
   340
              rel_co_inducts = rel_co_inducts,
desharna@58577
   341
              common_set_inducts = common_set_inducts,
desharna@58577
   342
              set_inducts = set_inducts}}
blanchet@54286
   343
          |> morph_fp_sugar phi;
blanchet@54256
   344
blanchet@55539
   345
        val target_fp_sugars =
wenzelm@58634
   346
          @{map 16} mk_target_fp_sugar fpTs Xs kks pre_bnfs absT_infos ctrXs_Tsss ctr_defss
wenzelm@58634
   347
            ctr_sugars co_recs co_rec_defs mapss (transpose co_inductss') co_rec_thmss
wenzelm@58634
   348
            co_rec_disc_thmss co_rec_sel_thmsss fp_sugars0;
blanchet@55539
   349
blanchet@55539
   350
        val n2m_sugar = (target_fp_sugars, fp_sugar_thms);
blanchet@54286
   351
      in
blanchet@54286
   352
        (n2m_sugar, lthy |> register_n2m_sugar key n2m_sugar)
blanchet@54286
   353
      end)
blanchet@54286
   354
  end;
blanchet@53303
   355
blanchet@55567
   356
fun indexify_callsss ctrs callsss =
blanchet@53303
   357
  let
blanchet@54283
   358
    fun indexify_ctr ctr =
blanchet@53303
   359
      (case AList.lookup Term.aconv_untyped callsss ctr of
blanchet@53303
   360
        NONE => replicate (num_binder_types (fastype_of ctr)) []
blanchet@55343
   361
      | SOME callss => map (map (Envir.beta_eta_contract o unfold_lets_splits)) callss);
blanchet@53303
   362
  in
blanchet@54283
   363
    map indexify_ctr ctrs
blanchet@53303
   364
  end;
blanchet@53303
   365
blanchet@54283
   366
fun retypargs tyargs (Type (s, _)) = Type (s, tyargs);
blanchet@54283
   367
blanchet@54283
   368
fun fold_subtype_pairs f (T as Type (s, Ts), U as Type (s', Us)) =
blanchet@54283
   369
    f (T, U) #> (if s = s' then fold (fold_subtype_pairs f) (Ts ~~ Us) else I)
blanchet@54283
   370
  | fold_subtype_pairs f TU = f TU;
blanchet@54283
   371
blanchet@55772
   372
val impossible_caller = Bound ~1;
blanchet@55772
   373
blanchet@58335
   374
fun nested_to_mutual_fps plugins fp actual_bs actual_Ts actual_callers actual_callssss0 lthy =
blanchet@53303
   375
  let
blanchet@53303
   376
    val qsoty = quote o Syntax.string_of_typ lthy;
blanchet@53303
   377
    val qsotys = space_implode " or " o map qsoty;
blanchet@53303
   378
blanchet@53303
   379
    fun not_co_datatype0 T = error (qsoty T ^ " is not a " ^ co_prefix fp ^ "datatype");
blanchet@53303
   380
    fun not_co_datatype (T as Type (s, _)) =
blanchet@53303
   381
        if fp = Least_FP andalso
blanchet@58112
   382
           is_some (Old_Datatype_Data.get_info (Proof_Context.theory_of lthy) s) then
blanchet@58315
   383
          error (qsoty T ^ " is an old-style datatype")
blanchet@53303
   384
        else
blanchet@53303
   385
          not_co_datatype0 T
blanchet@53303
   386
      | not_co_datatype T = not_co_datatype0 T;
blanchet@54303
   387
    fun not_mutually_nested_rec Ts1 Ts2 =
blanchet@59040
   388
      error (qsotys Ts1 ^ " is neither mutually " ^ co_prefix fp ^ "recursive with " ^ qsotys Ts2 ^
blanchet@59040
   389
        " nor nested " ^ co_prefix fp ^ "recursive through " ^
blanchet@58117
   390
        (if Ts1 = Ts2 andalso length Ts1 = 1 then "itself" else qsotys Ts2));
blanchet@53303
   391
blanchet@55480
   392
    val sorted_actual_Ts =
wenzelm@59058
   393
      sort (prod_ord int_ord Term_Ord.typ_ord o apply2 (`Term.size_of_typ)) actual_Ts;
blanchet@53303
   394
blanchet@54283
   395
    fun the_ctrs_of (Type (s, Ts)) = map (mk_ctr Ts) (#ctrs (the (ctr_sugar_of lthy s)));
blanchet@54283
   396
blanchet@54282
   397
    fun the_fp_sugar_of (T as Type (T_name, _)) =
blanchet@54282
   398
      (case fp_sugar_of lthy T_name of
blanchet@54282
   399
        SOME (fp_sugar as {fp = fp', ...}) => if fp = fp' then fp_sugar else not_co_datatype T
blanchet@54282
   400
      | NONE => not_co_datatype T);
blanchet@54282
   401
blanchet@54283
   402
    fun gen_rhss_in gen_Ts rho subTs =
blanchet@54283
   403
      let
blanchet@54283
   404
        fun maybe_insert (T, Type (_, gen_tyargs)) =
blanchet@54283
   405
            if member (op =) subTs T then insert (op =) gen_tyargs else I
blanchet@54283
   406
          | maybe_insert _ = I;
blanchet@54283
   407
blanchet@54283
   408
        val ctrs = maps the_ctrs_of gen_Ts;
blanchet@54283
   409
        val gen_ctr_Ts = maps (binder_types o fastype_of) ctrs;
blanchet@54283
   410
        val ctr_Ts = map (Term.typ_subst_atomic rho) gen_ctr_Ts;
blanchet@54283
   411
      in
blanchet@54283
   412
        fold (fold_subtype_pairs maybe_insert) (ctr_Ts ~~ gen_ctr_Ts) []
blanchet@54283
   413
      end;
blanchet@54283
   414
blanchet@56485
   415
    fun gather_types _ _ rev_seens gen_seen [] = (rev rev_seens, gen_seen)
blanchet@56485
   416
      | gather_types lthy rho rev_seens gen_seen ((T as Type (_, tyargs)) :: Ts) =
blanchet@54282
   417
        let
blanchet@58234
   418
          val {T = Type (_, tyargs0), fp_res = {Ts = mutual_Ts0, ...}, ...} = the_fp_sugar_of T;
blanchet@54283
   419
          val mutual_Ts = map (retypargs tyargs) mutual_Ts0;
blanchet@54283
   420
blanchet@56485
   421
          val rev_seen = flat rev_seens;
blanchet@56485
   422
          val _ = null rev_seens orelse exists (exists_strict_subtype_in rev_seen) mutual_Ts orelse
blanchet@56485
   423
            not_mutually_nested_rec mutual_Ts rev_seen;
blanchet@54303
   424
blanchet@54283
   425
          fun fresh_tyargs () =
blanchet@54283
   426
            let
blanchet@58234
   427
              val (unsorted_gen_tyargs, lthy') =
blanchet@58280
   428
                variant_tfrees (replicate (length tyargs) "z") lthy
blanchet@54283
   429
                |>> map Logic.varifyT_global;
blanchet@58234
   430
              val gen_tyargs =
blanchet@58234
   431
                map2 (resort_tfree_or_tvar o snd o dest_TFree_or_TVar) tyargs0 unsorted_gen_tyargs;
blanchet@54283
   432
              val rho' = (gen_tyargs ~~ tyargs) @ rho;
blanchet@54283
   433
            in
blanchet@54283
   434
              (rho', gen_tyargs, gen_seen, lthy')
blanchet@54283
   435
            end;
blanchet@54283
   436
blanchet@54283
   437
          val (rho', gen_tyargs, gen_seen', lthy') =
blanchet@56485
   438
            if exists (exists_subtype_in rev_seen) mutual_Ts then
blanchet@54283
   439
              (case gen_rhss_in gen_seen rho mutual_Ts of
blanchet@54283
   440
                [] => fresh_tyargs ()
blanchet@54899
   441
              | gen_tyargs :: gen_tyargss_tl =>
blanchet@54283
   442
                let
blanchet@54283
   443
                  val unify_pairs = split_list (maps (curry (op ~~) gen_tyargs) gen_tyargss_tl);
blanchet@54283
   444
                  val mgu = Type.raw_unifys unify_pairs Vartab.empty;
wenzelm@58948
   445
                  val gen_tyargs' = map (Envir.norm_type mgu) gen_tyargs;
wenzelm@58948
   446
                  val gen_seen' = map (Envir.norm_type mgu) gen_seen;
blanchet@54283
   447
                in
blanchet@54283
   448
                  (rho, gen_tyargs', gen_seen', lthy)
blanchet@54283
   449
                end)
blanchet@54283
   450
            else
blanchet@54283
   451
              fresh_tyargs ();
blanchet@54283
   452
blanchet@54283
   453
          val gen_mutual_Ts = map (retypargs gen_tyargs) mutual_Ts0;
blanchet@55480
   454
          val other_mutual_Ts = remove1 (op =) T mutual_Ts;
blanchet@55480
   455
          val Ts' = fold (remove1 (op =)) other_mutual_Ts Ts;
blanchet@54282
   456
        in
blanchet@56485
   457
          gather_types lthy' rho' (mutual_Ts :: rev_seens) (gen_seen' @ gen_mutual_Ts) Ts'
blanchet@54282
   458
        end
blanchet@56485
   459
      | gather_types _ _ _ _ (T :: _) = not_co_datatype T;
blanchet@53303
   460
blanchet@56485
   461
    val (perm_Tss, perm_gen_Ts) = gather_types lthy [] [] [] sorted_actual_Ts;
blanchet@58340
   462
    val (perm_mutual_cliques, perm_Ts) =
blanchet@56485
   463
      split_list (flat (map_index (fn (i, perm_Ts) => map (pair i) perm_Ts) perm_Tss));
blanchet@56485
   464
blanchet@54283
   465
    val perm_frozen_gen_Ts = map Logic.unvarifyT_global perm_gen_Ts;
blanchet@54283
   466
blanchet@56484
   467
    val missing_Ts = fold (remove1 (op =)) actual_Ts perm_Ts;
blanchet@53303
   468
    val Ts = actual_Ts @ missing_Ts;
blanchet@53303
   469
blanchet@53303
   470
    val nn = length Ts;
blanchet@53303
   471
    val kks = 0 upto nn - 1;
blanchet@53303
   472
blanchet@54267
   473
    val callssss0 = pad_list [] nn actual_callssss0;
blanchet@54267
   474
blanchet@53303
   475
    val common_name = mk_common_name (map Binding.name_of actual_bs);
blanchet@53303
   476
    val bs = pad_list (Binding.name common_name) nn actual_bs;
blanchet@55772
   477
    val callers = pad_list impossible_caller nn actual_callers;
blanchet@53303
   478
blanchet@53303
   479
    fun permute xs = permute_like (op =) Ts perm_Ts xs;
blanchet@53303
   480
    fun unpermute perm_xs = permute_like (op =) perm_Ts Ts perm_xs;
blanchet@53303
   481
blanchet@58340
   482
    (* The assignment of callers to mutual cliques is incorrect in general. This code would need to
blanchet@58340
   483
       inspect the actual calls to discover the correct cliques in the presence of type duplicates.
blanchet@58340
   484
       However, the naive scheme implemented here supports "prim(co)rec" specifications following
blanchet@58340
   485
       reasonable ordering of the duplicates (e.g., keeping the cliques together). *)
blanchet@53303
   486
    val perm_bs = permute bs;
blanchet@55772
   487
    val perm_callers = permute callers;
blanchet@53303
   488
    val perm_kks = permute kks;
blanchet@54267
   489
    val perm_callssss0 = permute callssss0;
blanchet@53303
   490
    val perm_fp_sugars0 = map (the o fp_sugar_of lthy o fst o dest_Type) perm_Ts;
blanchet@53303
   491
desharna@58460
   492
    val perm_callssss =
desharna@58460
   493
      map2 (indexify_callsss o #ctrs o #ctr_sugar o #fp_ctr_sugar) perm_fp_sugars0 perm_callssss0;
blanchet@53303
   494
blanchet@53746
   495
    val ((perm_fp_sugars, fp_sugar_thms), lthy) =
blanchet@58117
   496
      if length perm_Tss = 1 then
blanchet@56485
   497
        ((perm_fp_sugars0, (NONE, NONE)), lthy)
blanchet@56485
   498
      else
blanchet@58340
   499
        mutualize_fp_sugars plugins fp perm_mutual_cliques perm_bs perm_frozen_gen_Ts perm_callers
blanchet@58335
   500
          perm_callssss perm_fp_sugars0 lthy;
blanchet@53303
   501
blanchet@53303
   502
    val fp_sugars = unpermute perm_fp_sugars;
blanchet@53303
   503
  in
blanchet@53746
   504
    ((missing_Ts, perm_kks, fp_sugars, fp_sugar_thms), lthy)
blanchet@53303
   505
  end;
blanchet@53303
   506
blanchet@53303
   507
end;