src/HOL/BNF/Tools/bnf_fp_n2m_sugar.ML
author blanchet
Tue, 05 Nov 2013 16:47:10 +0100
changeset 54270 7405328f4c3c
parent 54268 807532d15d16
child 54273 7cb8442298f0
permissions -rw-r--r--
get mutually recursive maps as well
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
53303
ae49b835ca01 moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff changeset
     1
(*  Title:      HOL/BNF/Tools/bnf_fp_n2m_sugar.ML
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
54243
a596292be9a8 more robust n2m w.r.t. 'let's
blanchet
parents: 54240
diff changeset
    10
  val unfold_let: term -> term
a596292be9a8 more robust n2m w.r.t. 'let's
blanchet
parents: 54240
diff changeset
    11
  val dest_map: Proof.context -> string -> term -> term * term list
a596292be9a8 more robust n2m w.r.t. 'let's
blanchet
parents: 54240
diff changeset
    12
54009
f138452e8265 got rid of dead feature
blanchet
parents: 54006
diff changeset
    13
  val mutualize_fp_sugars: bool -> BNF_FP_Util.fp_kind -> binding list -> typ list ->
53303
ae49b835ca01 moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff changeset
    14
    (term -> int list) -> term list list list 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
    15
    local_theory ->
bd038e48526d have "datatype_new_compat" register induction and recursion theorems in nested case
blanchet
parents: 53678
diff changeset
    16
    (BNF_FP_Def_Sugar.fp_sugar list
bd038e48526d have "datatype_new_compat" register induction and recursion theorems in nested case
blanchet
parents: 53678
diff changeset
    17
     * (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
    18
    * local_theory
54267
78e8a178b690 use right permutation in 'map2'
blanchet
parents: 54266
diff changeset
    19
  val indexify_callsss: BNF_FP_Def_Sugar.fp_sugar -> (term * term list list) list ->
78e8a178b690 use right permutation in 'map2'
blanchet
parents: 54266
diff changeset
    20
    term list list list
54009
f138452e8265 got rid of dead feature
blanchet
parents: 54006
diff changeset
    21
  val nested_to_mutual_fps: BNF_FP_Util.fp_kind -> binding list -> typ list -> (term -> int list) ->
f138452e8265 got rid of dead feature
blanchet
parents: 54006
diff changeset
    22
    (term * term list list) list list -> local_theory ->
53746
bd038e48526d have "datatype_new_compat" register induction and recursion theorems in nested case
blanchet
parents: 53678
diff changeset
    23
    (typ list * int list * BNF_FP_Def_Sugar.fp_sugar list
bd038e48526d have "datatype_new_compat" register induction and recursion theorems in nested case
blanchet
parents: 53678
diff changeset
    24
     * (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
    25
    * local_theory
53303
ae49b835ca01 moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff changeset
    26
end;
ae49b835ca01 moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff changeset
    27
ae49b835ca01 moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff changeset
    28
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
    29
struct
ae49b835ca01 moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff changeset
    30
54006
9fe1bd54d437 renamed theory file
blanchet
parents: 53974
diff changeset
    31
open Ctr_Sugar
53303
ae49b835ca01 moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff changeset
    32
open BNF_Util
ae49b835ca01 moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff changeset
    33
open BNF_Def
ae49b835ca01 moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff changeset
    34
open BNF_FP_Util
ae49b835ca01 moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff changeset
    35
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
    36
open BNF_FP_N2M
ae49b835ca01 moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff changeset
    37
ae49b835ca01 moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff changeset
    38
val n2mN = "n2m_"
ae49b835ca01 moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff changeset
    39
54256
4843082be7ef added some N2M caching
blanchet
parents: 54255
diff changeset
    40
type n2m_sugar = fp_sugar list * (lfp_sugar_thms option * gfp_sugar_thms option);
4843082be7ef added some N2M caching
blanchet
parents: 54255
diff changeset
    41
4843082be7ef added some N2M caching
blanchet
parents: 54255
diff changeset
    42
structure Data = Generic_Data
4843082be7ef added some N2M caching
blanchet
parents: 54255
diff changeset
    43
(
4843082be7ef added some N2M caching
blanchet
parents: 54255
diff changeset
    44
  type T = n2m_sugar Typtab.table;
4843082be7ef added some N2M caching
blanchet
parents: 54255
diff changeset
    45
  val empty = Typtab.empty;
4843082be7ef added some N2M caching
blanchet
parents: 54255
diff changeset
    46
  val extend = I;
4843082be7ef added some N2M caching
blanchet
parents: 54255
diff changeset
    47
  val merge = Typtab.merge (eq_fst (eq_list eq_fp_sugar));
4843082be7ef added some N2M caching
blanchet
parents: 54255
diff changeset
    48
);
4843082be7ef added some N2M caching
blanchet
parents: 54255
diff changeset
    49
4843082be7ef added some N2M caching
blanchet
parents: 54255
diff changeset
    50
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
    51
  (map (morph_fp_sugar phi) fp_sugars,
4843082be7ef added some N2M caching
blanchet
parents: 54255
diff changeset
    52
   (Option.map (morph_lfp_sugar_thms phi) lfp_sugar_thms_opt,
4843082be7ef added some N2M caching
blanchet
parents: 54255
diff changeset
    53
    Option.map (morph_gfp_sugar_thms phi) gfp_sugar_thms_opt));
4843082be7ef added some N2M caching
blanchet
parents: 54255
diff changeset
    54
4843082be7ef added some N2M caching
blanchet
parents: 54255
diff changeset
    55
val transfer_n2m_sugar =
4843082be7ef added some N2M caching
blanchet
parents: 54255
diff changeset
    56
  morph_n2m_sugar o Morphism.thm_morphism o Thm.transfer o Proof_Context.theory_of;
4843082be7ef added some N2M caching
blanchet
parents: 54255
diff changeset
    57
4843082be7ef added some N2M caching
blanchet
parents: 54255
diff changeset
    58
fun n2m_sugar_of ctxt =
4843082be7ef added some N2M caching
blanchet
parents: 54255
diff changeset
    59
  Typtab.lookup (Data.get (Context.Proof ctxt))
4843082be7ef added some N2M caching
blanchet
parents: 54255
diff changeset
    60
  #> Option.map (transfer_n2m_sugar ctxt);
4843082be7ef added some N2M caching
blanchet
parents: 54255
diff changeset
    61
4843082be7ef added some N2M caching
blanchet
parents: 54255
diff changeset
    62
fun register_n2m_sugar key n2m_sugar =
4843082be7ef added some N2M caching
blanchet
parents: 54255
diff changeset
    63
  Local_Theory.declaration {syntax = false, pervasive = false}
4843082be7ef added some N2M caching
blanchet
parents: 54255
diff changeset
    64
    (fn phi => Data.map (Typtab.default (key, morph_n2m_sugar phi n2m_sugar)));
4843082be7ef added some N2M caching
blanchet
parents: 54255
diff changeset
    65
54243
a596292be9a8 more robust n2m w.r.t. 'let's
blanchet
parents: 54240
diff changeset
    66
fun unfold_let (Const (@{const_name Let}, _) $ arg1 $ arg2) = unfold_let (betapply (arg2, arg1))
a596292be9a8 more robust n2m w.r.t. 'let's
blanchet
parents: 54240
diff changeset
    67
  | unfold_let (Const (@{const_name prod_case}, _) $ t) =
a596292be9a8 more robust n2m w.r.t. 'let's
blanchet
parents: 54240
diff changeset
    68
    (case unfold_let t of
a596292be9a8 more robust n2m w.r.t. 'let's
blanchet
parents: 54240
diff changeset
    69
      t' as Abs (s1, T1, Abs (s2, T2, _)) =>
a596292be9a8 more robust n2m w.r.t. 'let's
blanchet
parents: 54240
diff changeset
    70
      let
a596292be9a8 more robust n2m w.r.t. 'let's
blanchet
parents: 54240
diff changeset
    71
        val x = (s1 ^ s2, Term.maxidx_of_term t + 1);
a596292be9a8 more robust n2m w.r.t. 'let's
blanchet
parents: 54240
diff changeset
    72
        val v = Var (x, HOLogic.mk_prodT (T1, T2));
a596292be9a8 more robust n2m w.r.t. 'let's
blanchet
parents: 54240
diff changeset
    73
      in
a596292be9a8 more robust n2m w.r.t. 'let's
blanchet
parents: 54240
diff changeset
    74
        lambda v (unfold_let (betapplys (t', [HOLogic.mk_fst v, HOLogic.mk_snd v])))
a596292be9a8 more robust n2m w.r.t. 'let's
blanchet
parents: 54240
diff changeset
    75
      end
a596292be9a8 more robust n2m w.r.t. 'let's
blanchet
parents: 54240
diff changeset
    76
    | _ => t)
a596292be9a8 more robust n2m w.r.t. 'let's
blanchet
parents: 54240
diff changeset
    77
  | unfold_let (t $ u) = betapply (unfold_let t, unfold_let u)
a596292be9a8 more robust n2m w.r.t. 'let's
blanchet
parents: 54240
diff changeset
    78
  | unfold_let (Abs (s, T, t)) = Abs (s, T, unfold_let t)
a596292be9a8 more robust n2m w.r.t. 'let's
blanchet
parents: 54240
diff changeset
    79
  | unfold_let t = t;
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
a596292be9a8 more robust n2m w.r.t. 'let's
blanchet
parents: 54240
diff changeset
   100
fun dest_abs_or_applied_map_or_ctr _ _ (Abs (_, _, t)) = (Term.dummy, [t])
a596292be9a8 more robust n2m w.r.t. 'let's
blanchet
parents: 54240
diff changeset
   101
  | dest_abs_or_applied_map_or_ctr ctxt s (t as t1 $ _) =
a596292be9a8 more robust n2m w.r.t. 'let's
blanchet
parents: 54240
diff changeset
   102
    (case try (dest_map ctxt s) t1 of
a596292be9a8 more robust n2m w.r.t. 'let's
blanchet
parents: 54240
diff changeset
   103
      SOME res => res
a596292be9a8 more robust n2m w.r.t. 'let's
blanchet
parents: 54240
diff changeset
   104
    | NONE =>
a596292be9a8 more robust n2m w.r.t. 'let's
blanchet
parents: 54240
diff changeset
   105
      let
a596292be9a8 more robust n2m w.r.t. 'let's
blanchet
parents: 54240
diff changeset
   106
        val thy = Proof_Context.theory_of ctxt;
54270
7405328f4c3c get mutually recursive maps as well
blanchet
parents: 54268
diff changeset
   107
        val map_thms = flat (#mapss (the (fp_sugar_of ctxt s)));
54243
a596292be9a8 more robust n2m w.r.t. 'let's
blanchet
parents: 54240
diff changeset
   108
        val map_thms' = map (fn thm => thm RS sym RS eq_reflection) map_thms;
a596292be9a8 more robust n2m w.r.t. 'let's
blanchet
parents: 54240
diff changeset
   109
        val t' = Raw_Simplifier.rewrite_term thy map_thms' [] t;
a596292be9a8 more robust n2m w.r.t. 'let's
blanchet
parents: 54240
diff changeset
   110
      in
54270
7405328f4c3c get mutually recursive maps as well
blanchet
parents: 54268
diff changeset
   111
        if t aconv t' then raise Fail "dest_abs_or_applied_map_or_ctr"
54243
a596292be9a8 more robust n2m w.r.t. 'let's
blanchet
parents: 54240
diff changeset
   112
        else dest_map ctxt s (fst (dest_comb t'))
a596292be9a8 more robust n2m w.r.t. 'let's
blanchet
parents: 54240
diff changeset
   113
      end);
54239
9bd91d5d8a7b handle constructor syntax in n2m primcorec
blanchet
parents: 54235
diff changeset
   114
54245
f91022745c85 better error handling
blanchet
parents: 54243
diff changeset
   115
fun map_partition f xs =
f91022745c85 better error handling
blanchet
parents: 54243
diff changeset
   116
  fold_rev (fn x => fn (ys, (good, bad)) =>
f91022745c85 better error handling
blanchet
parents: 54243
diff changeset
   117
      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
   118
    xs ([], ([], []));
f91022745c85 better error handling
blanchet
parents: 54243
diff changeset
   119
54256
4843082be7ef added some N2M caching
blanchet
parents: 54255
diff changeset
   120
fun key_of_fp_eqs fp fpTs fp_eqs =
54267
78e8a178b690 use right permutation in 'map2'
blanchet
parents: 54266
diff changeset
   121
  Type (fp_case fp "l" "g", fpTs @ maps (fn (x, T) => [TFree x, T]) fp_eqs);
54256
4843082be7ef added some N2M caching
blanchet
parents: 54255
diff changeset
   122
53303
ae49b835ca01 moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff changeset
   123
(* TODO: test with sort constraints on As *)
ae49b835ca01 moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff changeset
   124
(* TODO: use right sorting order for "fp_sort" w.r.t. original BNFs (?) -- treat new variables
ae49b835ca01 moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff changeset
   125
   as deads? *)
54245
f91022745c85 better error handling
blanchet
parents: 54243
diff changeset
   126
fun mutualize_fp_sugars has_nested fp bs fpTs get_indices callssss fp_sugars0 no_defs_lthy0 =
54253
04cd231e2b9e nicer error message in case of duplicates
blanchet
parents: 54245
diff changeset
   127
  if has_nested then
53303
ae49b835ca01 moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff changeset
   128
    let
ae49b835ca01 moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff changeset
   129
      val thy = Proof_Context.theory_of no_defs_lthy0;
ae49b835ca01 moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff changeset
   130
ae49b835ca01 moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff changeset
   131
      val qsotm = quote o Syntax.string_of_term no_defs_lthy0;
ae49b835ca01 moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff changeset
   132
54245
f91022745c85 better error handling
blanchet
parents: 54243
diff changeset
   133
      fun incompatible_calls t1 t2 =
f91022745c85 better error handling
blanchet
parents: 54243
diff changeset
   134
        error ("Incompatible " ^ co_prefix fp ^ "recursive calls: " ^ qsotm t1 ^ " vs. " ^
f91022745c85 better error handling
blanchet
parents: 54243
diff changeset
   135
          qsotm t2);
f91022745c85 better error handling
blanchet
parents: 54243
diff changeset
   136
53303
ae49b835ca01 moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff changeset
   137
      val b_names = map Binding.name_of bs;
ae49b835ca01 moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff changeset
   138
      val fp_b_names = map base_name_of_typ fpTs;
ae49b835ca01 moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff changeset
   139
ae49b835ca01 moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff changeset
   140
      val nn = length fpTs;
ae49b835ca01 moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff changeset
   141
53974
612505263257 make SML/NJ more happy;
wenzelm
parents: 53808
diff changeset
   142
      fun target_ctr_sugar_of_fp_sugar fpT ({T, index, ctr_sugars, ...} : fp_sugar) =
53303
ae49b835ca01 moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff changeset
   143
        let
ae49b835ca01 moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff changeset
   144
          val rho = Vartab.fold (cons o apsnd snd) (Sign.typ_match thy (T, fpT) Vartab.empty) [];
ae49b835ca01 moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff changeset
   145
          val phi = Morphism.term_morphism (Term.subst_TVars rho);
ae49b835ca01 moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff changeset
   146
        in
ae49b835ca01 moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff changeset
   147
          morph_ctr_sugar phi (nth ctr_sugars index)
ae49b835ca01 moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff changeset
   148
        end;
ae49b835ca01 moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff changeset
   149
ae49b835ca01 moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff changeset
   150
      val ctr_defss = map (of_fp_sugar #ctr_defss) fp_sugars0;
53476
eb3865c3ee58 include map theorems in datastructure for "primcorec"
blanchet
parents: 53475
diff changeset
   151
      val mapss = map (of_fp_sugar #mapss) fp_sugars0;
53303
ae49b835ca01 moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff changeset
   152
      val ctr_sugars0 = map2 target_ctr_sugar_of_fp_sugar fpTs fp_sugars0;
ae49b835ca01 moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff changeset
   153
ae49b835ca01 moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff changeset
   154
      val ctrss = map #ctrs ctr_sugars0;
ae49b835ca01 moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff changeset
   155
      val ctr_Tss = map (map fastype_of) ctrss;
ae49b835ca01 moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff changeset
   156
ae49b835ca01 moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff changeset
   157
      val As' = fold (fold Term.add_tfreesT) ctr_Tss [];
ae49b835ca01 moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff changeset
   158
      val As = map TFree As';
ae49b835ca01 moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff changeset
   159
ae49b835ca01 moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff changeset
   160
      val ((Cs, Xs), no_defs_lthy) =
ae49b835ca01 moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff changeset
   161
        no_defs_lthy0
ae49b835ca01 moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff changeset
   162
        |> fold Variable.declare_typ As
ae49b835ca01 moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff changeset
   163
        |> mk_TFrees nn
ae49b835ca01 moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff changeset
   164
        ||>> variant_tfrees fp_b_names;
ae49b835ca01 moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff changeset
   165
54245
f91022745c85 better error handling
blanchet
parents: 54243
diff changeset
   166
      fun check_call_dead live_call call =
f91022745c85 better error handling
blanchet
parents: 54243
diff changeset
   167
        if null (get_indices call) then () else incompatible_calls live_call call;
f91022745c85 better error handling
blanchet
parents: 54243
diff changeset
   168
54255
4f7c016d5bc6 also generalize fixed types
blanchet
parents: 54254
diff changeset
   169
      fun freeze_fpTs_simple (T as Type (s, Ts)) =
54253
04cd231e2b9e nicer error message in case of duplicates
blanchet
parents: 54245
diff changeset
   170
          (case find_index (curry (op =) T) fpTs of
54255
4f7c016d5bc6 also generalize fixed types
blanchet
parents: 54254
diff changeset
   171
            ~1 => Type (s, map freeze_fpTs_simple Ts)
54253
04cd231e2b9e nicer error message in case of duplicates
blanchet
parents: 54245
diff changeset
   172
          | kk => nth Xs kk)
54255
4f7c016d5bc6 also generalize fixed types
blanchet
parents: 54254
diff changeset
   173
        | freeze_fpTs_simple T = T;
54253
04cd231e2b9e nicer error message in case of duplicates
blanchet
parents: 54245
diff changeset
   174
54255
4f7c016d5bc6 also generalize fixed types
blanchet
parents: 54254
diff changeset
   175
      fun freeze_fpTs_map (callss, (live_call :: _, dead_calls)) s Ts =
54245
f91022745c85 better error handling
blanchet
parents: 54243
diff changeset
   176
        (List.app (check_call_dead live_call) dead_calls;
54255
4f7c016d5bc6 also generalize fixed types
blanchet
parents: 54254
diff changeset
   177
         Type (s, map2 freeze_fpTs (flatten_type_args_of_bnf (the (bnf_of no_defs_lthy s)) []
54245
f91022745c85 better error handling
blanchet
parents: 54243
diff changeset
   178
           (transpose callss)) Ts))
54255
4f7c016d5bc6 also generalize fixed types
blanchet
parents: 54254
diff changeset
   179
      and freeze_fpTs calls (T as Type (s, Ts)) =
54245
f91022745c85 better error handling
blanchet
parents: 54243
diff changeset
   180
          (case map_partition (try (snd o dest_map no_defs_lthy s)) calls of
f91022745c85 better error handling
blanchet
parents: 54243
diff changeset
   181
            ([], _) =>
f91022745c85 better error handling
blanchet
parents: 54243
diff changeset
   182
            (case map_partition (try (snd o dest_abs_or_applied_map_or_ctr no_defs_lthy s)) calls of
54255
4f7c016d5bc6 also generalize fixed types
blanchet
parents: 54254
diff changeset
   183
              ([], _) => freeze_fpTs_simple T
4f7c016d5bc6 also generalize fixed types
blanchet
parents: 54254
diff changeset
   184
            | callsp => freeze_fpTs_map callsp s Ts)
4f7c016d5bc6 also generalize fixed types
blanchet
parents: 54254
diff changeset
   185
          | callsp => freeze_fpTs_map callsp s Ts)
4f7c016d5bc6 also generalize fixed types
blanchet
parents: 54254
diff changeset
   186
        | freeze_fpTs _ T = T;
53303
ae49b835ca01 moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff changeset
   187
ae49b835ca01 moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff changeset
   188
      val ctr_Tsss = map (map binder_types) ctr_Tss;
54255
4f7c016d5bc6 also generalize fixed types
blanchet
parents: 54254
diff changeset
   189
      val ctrXs_Tsss = map2 (map2 (map2 freeze_fpTs)) callssss ctr_Tsss;
53303
ae49b835ca01 moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff changeset
   190
      val ctrXs_sum_prod_Ts = map (mk_sumTN_balanced o map HOLogic.mk_tupleT) ctrXs_Tsss;
ae49b835ca01 moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff changeset
   191
      val Ts = map (body_type o hd) ctr_Tss;
ae49b835ca01 moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff changeset
   192
ae49b835ca01 moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff changeset
   193
      val ns = map length ctr_Tsss;
ae49b835ca01 moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff changeset
   194
      val kss = map (fn n => 1 upto n) ns;
ae49b835ca01 moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff changeset
   195
      val mss = map (map length) ctr_Tsss;
ae49b835ca01 moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff changeset
   196
ae49b835ca01 moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff changeset
   197
      val fp_eqs = map dest_TFree Xs ~~ ctrXs_sum_prod_Ts;
54256
4843082be7ef added some N2M caching
blanchet
parents: 54255
diff changeset
   198
      val key = key_of_fp_eqs fp fpTs fp_eqs;
4843082be7ef added some N2M caching
blanchet
parents: 54255
diff changeset
   199
    in
4843082be7ef added some N2M caching
blanchet
parents: 54255
diff changeset
   200
      (case n2m_sugar_of no_defs_lthy key of
4843082be7ef added some N2M caching
blanchet
parents: 54255
diff changeset
   201
        SOME n2m_sugar => (n2m_sugar, no_defs_lthy)
4843082be7ef added some N2M caching
blanchet
parents: 54255
diff changeset
   202
      | NONE =>
4843082be7ef added some N2M caching
blanchet
parents: 54255
diff changeset
   203
        let
4843082be7ef added some N2M caching
blanchet
parents: 54255
diff changeset
   204
          val base_fp_names = Name.variant_list [] fp_b_names;
4843082be7ef added some N2M caching
blanchet
parents: 54255
diff changeset
   205
          val fp_bs = map2 (fn b_name => fn base_fp_name =>
4843082be7ef added some N2M caching
blanchet
parents: 54255
diff changeset
   206
              Binding.qualify true b_name (Binding.name (n2mN ^ base_fp_name)))
4843082be7ef added some N2M caching
blanchet
parents: 54255
diff changeset
   207
            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
   208
54256
4843082be7ef added some N2M caching
blanchet
parents: 54255
diff changeset
   209
          val (pre_bnfs, (fp_res as {xtor_co_iterss = xtor_co_iterss0, xtor_co_induct,
4843082be7ef added some N2M caching
blanchet
parents: 54255
diff changeset
   210
                 dtor_injects, dtor_ctors, xtor_co_iter_thmss, ...}, lthy)) =
4843082be7ef added some N2M caching
blanchet
parents: 54255
diff changeset
   211
            fp_bnf (construct_mutualized_fp fp fpTs fp_sugars0) fp_bs As' fp_eqs no_defs_lthy;
53303
ae49b835ca01 moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff changeset
   212
54256
4843082be7ef added some N2M caching
blanchet
parents: 54255
diff changeset
   213
          val nesting_bnfs = nesty_bnfs lthy ctrXs_Tsss As;
4843082be7ef added some N2M caching
blanchet
parents: 54255
diff changeset
   214
          val nested_bnfs = nesty_bnfs lthy ctrXs_Tsss Xs;
53303
ae49b835ca01 moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff changeset
   215
54256
4843082be7ef added some N2M caching
blanchet
parents: 54255
diff changeset
   216
          val ((xtor_co_iterss, iters_args_types, coiters_args_types), _) =
4843082be7ef added some N2M caching
blanchet
parents: 54255
diff changeset
   217
            mk_co_iters_prelims fp ctr_Tsss fpTs Cs ns mss xtor_co_iterss0 lthy;
4843082be7ef added some N2M caching
blanchet
parents: 54255
diff changeset
   218
4843082be7ef added some N2M caching
blanchet
parents: 54255
diff changeset
   219
          fun mk_binding b suf = Binding.suffix_name ("_" ^ suf) b;
53303
ae49b835ca01 moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff changeset
   220
54256
4843082be7ef added some N2M caching
blanchet
parents: 54255
diff changeset
   221
          val ((co_iterss, co_iter_defss), lthy) =
4843082be7ef added some N2M caching
blanchet
parents: 54255
diff changeset
   222
            fold_map2 (fn b =>
4843082be7ef added some N2M caching
blanchet
parents: 54255
diff changeset
   223
              (if fp = Least_FP then define_iters [foldN, recN] (the iters_args_types)
4843082be7ef added some N2M caching
blanchet
parents: 54255
diff changeset
   224
               else define_coiters [unfoldN, corecN] (the coiters_args_types))
4843082be7ef added some N2M caching
blanchet
parents: 54255
diff changeset
   225
                (mk_binding b) fpTs Cs) fp_bs xtor_co_iterss lthy
4843082be7ef added some N2M caching
blanchet
parents: 54255
diff changeset
   226
            |>> split_list;
53303
ae49b835ca01 moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff changeset
   227
54256
4843082be7ef added some N2M caching
blanchet
parents: 54255
diff changeset
   228
          val rho = tvar_subst thy Ts fpTs;
4843082be7ef added some N2M caching
blanchet
parents: 54255
diff changeset
   229
          val ctr_sugar_phi =
4843082be7ef added some N2M caching
blanchet
parents: 54255
diff changeset
   230
            Morphism.compose (Morphism.typ_morphism (Term.typ_subst_TVars rho))
4843082be7ef added some N2M caching
blanchet
parents: 54255
diff changeset
   231
              (Morphism.term_morphism (Term.subst_TVars rho));
4843082be7ef added some N2M caching
blanchet
parents: 54255
diff changeset
   232
          val inst_ctr_sugar = morph_ctr_sugar ctr_sugar_phi;
53303
ae49b835ca01 moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff changeset
   233
54256
4843082be7ef added some N2M caching
blanchet
parents: 54255
diff changeset
   234
          val ctr_sugars = map inst_ctr_sugar ctr_sugars0;
53303
ae49b835ca01 moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff changeset
   235
54256
4843082be7ef added some N2M caching
blanchet
parents: 54255
diff changeset
   236
          val ((co_inducts, un_fold_thmss, co_rec_thmss, disc_unfold_thmss, disc_corec_thmss,
4843082be7ef added some N2M caching
blanchet
parents: 54255
diff changeset
   237
                sel_unfold_thmsss, sel_corec_thmsss), fp_sugar_thms) =
4843082be7ef added some N2M caching
blanchet
parents: 54255
diff changeset
   238
            if fp = Least_FP then
4843082be7ef added some N2M caching
blanchet
parents: 54255
diff changeset
   239
              derive_induct_iters_thms_for_types pre_bnfs (the iters_args_types) xtor_co_induct
4843082be7ef added some N2M caching
blanchet
parents: 54255
diff changeset
   240
                xtor_co_iter_thmss nesting_bnfs nested_bnfs fpTs Cs Xs ctrXs_Tsss ctrss ctr_defss
4843082be7ef added some N2M caching
blanchet
parents: 54255
diff changeset
   241
                co_iterss co_iter_defss lthy
4843082be7ef added some N2M caching
blanchet
parents: 54255
diff changeset
   242
              |> `(fn ((_, induct, _), (fold_thmss, rec_thmss, _)) =>
4843082be7ef added some N2M caching
blanchet
parents: 54255
diff changeset
   243
                ([induct], fold_thmss, rec_thmss, [], [], [], []))
4843082be7ef added some N2M caching
blanchet
parents: 54255
diff changeset
   244
              ||> (fn info => (SOME info, NONE))
4843082be7ef added some N2M caching
blanchet
parents: 54255
diff changeset
   245
            else
4843082be7ef added some N2M caching
blanchet
parents: 54255
diff changeset
   246
              derive_coinduct_coiters_thms_for_types pre_bnfs (the coiters_args_types)
4843082be7ef added some N2M caching
blanchet
parents: 54255
diff changeset
   247
                xtor_co_induct dtor_injects dtor_ctors xtor_co_iter_thmss nesting_bnfs fpTs Cs Xs
4843082be7ef added some N2M caching
blanchet
parents: 54255
diff changeset
   248
                ctrXs_Tsss kss mss ns ctr_defss ctr_sugars co_iterss co_iter_defss
4843082be7ef added some N2M caching
blanchet
parents: 54255
diff changeset
   249
                (Proof_Context.export lthy no_defs_lthy) lthy
4843082be7ef added some N2M caching
blanchet
parents: 54255
diff changeset
   250
              |> `(fn ((coinduct_thms_pairs, _), (unfold_thmss, corec_thmss, _),
4843082be7ef added some N2M caching
blanchet
parents: 54255
diff changeset
   251
                      (disc_unfold_thmss, disc_corec_thmss, _), _,
4843082be7ef added some N2M caching
blanchet
parents: 54255
diff changeset
   252
                      (sel_unfold_thmsss, sel_corec_thmsss, _)) =>
4843082be7ef added some N2M caching
blanchet
parents: 54255
diff changeset
   253
                (map snd coinduct_thms_pairs, unfold_thmss, corec_thmss, disc_unfold_thmss,
4843082be7ef added some N2M caching
blanchet
parents: 54255
diff changeset
   254
                 disc_corec_thmss, sel_unfold_thmsss, sel_corec_thmsss))
4843082be7ef added some N2M caching
blanchet
parents: 54255
diff changeset
   255
              ||> (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
   256
54256
4843082be7ef added some N2M caching
blanchet
parents: 54255
diff changeset
   257
          val phi = Proof_Context.export_morphism no_defs_lthy no_defs_lthy0;
4843082be7ef added some N2M caching
blanchet
parents: 54255
diff changeset
   258
4843082be7ef added some N2M caching
blanchet
parents: 54255
diff changeset
   259
          fun mk_target_fp_sugar (kk, T) =
4843082be7ef added some N2M caching
blanchet
parents: 54255
diff changeset
   260
            {T = T, fp = fp, index = kk, pre_bnfs = pre_bnfs, nested_bnfs = nested_bnfs,
4843082be7ef added some N2M caching
blanchet
parents: 54255
diff changeset
   261
             nesting_bnfs = nesting_bnfs, fp_res = fp_res, ctr_defss = ctr_defss,
4843082be7ef added some N2M caching
blanchet
parents: 54255
diff changeset
   262
             ctr_sugars = ctr_sugars, co_iterss = co_iterss, mapss = mapss, co_inducts = co_inducts,
4843082be7ef added some N2M caching
blanchet
parents: 54255
diff changeset
   263
             co_iter_thmsss = transpose [un_fold_thmss, co_rec_thmss],
4843082be7ef added some N2M caching
blanchet
parents: 54255
diff changeset
   264
             disc_co_itersss = transpose [disc_unfold_thmss, disc_corec_thmss],
4843082be7ef added some N2M caching
blanchet
parents: 54255
diff changeset
   265
             sel_co_iterssss = transpose [sel_unfold_thmsss, sel_corec_thmsss]}
4843082be7ef added some N2M caching
blanchet
parents: 54255
diff changeset
   266
            |> morph_fp_sugar phi;
4843082be7ef added some N2M caching
blanchet
parents: 54255
diff changeset
   267
4843082be7ef added some N2M caching
blanchet
parents: 54255
diff changeset
   268
          val n2m_sugar = (map_index mk_target_fp_sugar fpTs, fp_sugar_thms);
4843082be7ef added some N2M caching
blanchet
parents: 54255
diff changeset
   269
        in
4843082be7ef added some N2M caching
blanchet
parents: 54255
diff changeset
   270
          (n2m_sugar, lthy |> register_n2m_sugar key n2m_sugar)
4843082be7ef added some N2M caching
blanchet
parents: 54255
diff changeset
   271
        end)
53303
ae49b835ca01 moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff changeset
   272
    end
ae49b835ca01 moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff changeset
   273
  else
53746
bd038e48526d have "datatype_new_compat" register induction and recursion theorems in nested case
blanchet
parents: 53678
diff changeset
   274
    ((fp_sugars0, (NONE, NONE)), no_defs_lthy0);
53303
ae49b835ca01 moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff changeset
   275
ae49b835ca01 moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff changeset
   276
fun indexify_callsss fp_sugar callsss =
ae49b835ca01 moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff changeset
   277
  let
ae49b835ca01 moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff changeset
   278
    val {ctrs, ...} = of_fp_sugar #ctr_sugars fp_sugar;
ae49b835ca01 moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff changeset
   279
    fun do_ctr ctr =
ae49b835ca01 moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff changeset
   280
      (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
   281
        NONE => replicate (num_binder_types (fastype_of ctr)) []
54243
a596292be9a8 more robust n2m w.r.t. 'let's
blanchet
parents: 54240
diff changeset
   282
      | SOME callss => map (map (Envir.beta_eta_contract o unfold_let)) callss);
53303
ae49b835ca01 moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff changeset
   283
  in
ae49b835ca01 moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff changeset
   284
    map do_ctr ctrs
ae49b835ca01 moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff changeset
   285
  end;
ae49b835ca01 moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff changeset
   286
54009
f138452e8265 got rid of dead feature
blanchet
parents: 54006
diff changeset
   287
fun nested_to_mutual_fps fp actual_bs actual_Ts get_indices actual_callssss0 lthy =
53303
ae49b835ca01 moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff changeset
   288
  let
ae49b835ca01 moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff changeset
   289
    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
   290
    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
   291
54253
04cd231e2b9e nicer error message in case of duplicates
blanchet
parents: 54245
diff changeset
   292
    fun duplicate_datatype T = error (qsoty T ^ " is not mutually recursive with itself");
53303
ae49b835ca01 moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff changeset
   293
    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
   294
    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
   295
        if fp = Least_FP andalso
ae49b835ca01 moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff changeset
   296
           is_some (Datatype_Data.get_info (Proof_Context.theory_of lthy) s) then
ae49b835ca01 moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff changeset
   297
          error (qsoty T ^ " is not a new-style datatype (cf. \"datatype_new\")")
ae49b835ca01 moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff changeset
   298
        else
ae49b835ca01 moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff changeset
   299
          not_co_datatype0 T
ae49b835ca01 moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff changeset
   300
      | not_co_datatype T = not_co_datatype0 T;
ae49b835ca01 moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff changeset
   301
    fun not_mutually_nested_rec Ts1 Ts2 =
ae49b835ca01 moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff changeset
   302
      error (qsotys Ts1 ^ " is neither mutually recursive with nor nested recursive via " ^
ae49b835ca01 moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff changeset
   303
        qsotys Ts2);
ae49b835ca01 moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff changeset
   304
54253
04cd231e2b9e nicer error message in case of duplicates
blanchet
parents: 54245
diff changeset
   305
    val _ = (case Library.duplicates (op =) actual_Ts of [] => () | T :: _ => duplicate_datatype T);
04cd231e2b9e nicer error message in case of duplicates
blanchet
parents: 54245
diff changeset
   306
53303
ae49b835ca01 moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff changeset
   307
    val perm_actual_Ts as Type (_, ty_args0) :: _ =
54266
4e0738356ac9 stronger normalization, to increase n2m cache effectiveness
blanchet
parents: 54265
diff changeset
   308
      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
   309
ae49b835ca01 moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff changeset
   310
    fun check_enrich_with_mutuals _ [] = []
ae49b835ca01 moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff changeset
   311
      | check_enrich_with_mutuals seen ((T as Type (T_name, ty_args)) :: Ts) =
ae49b835ca01 moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff changeset
   312
        (case fp_sugar_of lthy T_name of
ae49b835ca01 moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff changeset
   313
          SOME ({fp = fp', fp_res = {Ts = Ts', ...}, ...}) =>
ae49b835ca01 moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff changeset
   314
          if fp = fp' then
ae49b835ca01 moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff changeset
   315
            let
ae49b835ca01 moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff changeset
   316
              val mutual_Ts = map (fn Type (s, _) => Type (s, ty_args)) Ts';
ae49b835ca01 moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff changeset
   317
              val _ =
ae49b835ca01 moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff changeset
   318
                seen = [] orelse exists (exists_subtype_in seen) mutual_Ts orelse
ae49b835ca01 moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff changeset
   319
                not_mutually_nested_rec mutual_Ts seen;
ae49b835ca01 moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff changeset
   320
              val (seen', Ts') = List.partition (member (op =) mutual_Ts) Ts;
ae49b835ca01 moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff changeset
   321
            in
ae49b835ca01 moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff changeset
   322
              mutual_Ts @ check_enrich_with_mutuals (seen @ T :: seen') Ts'
ae49b835ca01 moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff changeset
   323
            end
ae49b835ca01 moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff changeset
   324
          else
ae49b835ca01 moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff changeset
   325
            not_co_datatype T
ae49b835ca01 moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff changeset
   326
        | NONE => not_co_datatype T)
ae49b835ca01 moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff changeset
   327
      | check_enrich_with_mutuals _ (T :: _) = not_co_datatype T;
ae49b835ca01 moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff changeset
   328
ae49b835ca01 moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff changeset
   329
    val perm_Ts = check_enrich_with_mutuals [] perm_actual_Ts;
ae49b835ca01 moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff changeset
   330
    val missing_Ts = perm_Ts |> subtract (op =) actual_Ts;
ae49b835ca01 moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff changeset
   331
    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
   332
54266
4e0738356ac9 stronger normalization, to increase n2m cache effectiveness
blanchet
parents: 54265
diff changeset
   333
    (* The name "'z" is likely not to clash with the context, resulting in more cache hits. *)
54255
4f7c016d5bc6 also generalize fixed types
blanchet
parents: 54254
diff changeset
   334
    fun generalize_simple_type T (seen, lthy) =
54266
4e0738356ac9 stronger normalization, to increase n2m cache effectiveness
blanchet
parents: 54265
diff changeset
   335
      variant_tfrees ["z"] lthy |> (fn ([U], lthy) => (U, ((T, U) :: seen, lthy)));
54255
4f7c016d5bc6 also generalize fixed types
blanchet
parents: 54254
diff changeset
   336
4f7c016d5bc6 also generalize fixed types
blanchet
parents: 54254
diff changeset
   337
    fun generalize_type T (seen_lthy as (seen, _)) =
4f7c016d5bc6 also generalize fixed types
blanchet
parents: 54254
diff changeset
   338
      (case AList.lookup (op =) seen T of
4f7c016d5bc6 also generalize fixed types
blanchet
parents: 54254
diff changeset
   339
        SOME U => (U, seen_lthy)
4f7c016d5bc6 also generalize fixed types
blanchet
parents: 54254
diff changeset
   340
      | NONE =>
4f7c016d5bc6 also generalize fixed types
blanchet
parents: 54254
diff changeset
   341
        (case T of
54268
807532d15d16 fixed subtle name shadowing bug
blanchet
parents: 54267
diff changeset
   342
          Type (s, Ts') =>
807532d15d16 fixed subtle name shadowing bug
blanchet
parents: 54267
diff changeset
   343
          if exists_subtype_in Ts T then fold_map generalize_type Ts' seen_lthy |>> curry Type s
54255
4f7c016d5bc6 also generalize fixed types
blanchet
parents: 54254
diff changeset
   344
          else generalize_simple_type T seen_lthy
4f7c016d5bc6 also generalize fixed types
blanchet
parents: 54254
diff changeset
   345
        | _ => generalize_simple_type T seen_lthy));
54254
d1478807f287 generalize types when synthetizing n2m (co)recursors, to facilitate reuse
blanchet
parents: 54253
diff changeset
   346
d1478807f287 generalize types when synthetizing n2m (co)recursors, to facilitate reuse
blanchet
parents: 54253
diff changeset
   347
    val (perm_Us, _) = fold_map generalize_type perm_Ts ([], lthy);
d1478807f287 generalize types when synthetizing n2m (co)recursors, to facilitate reuse
blanchet
parents: 54253
diff changeset
   348
53303
ae49b835ca01 moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff changeset
   349
    val nn = length Ts;
ae49b835ca01 moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff changeset
   350
    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
   351
54267
78e8a178b690 use right permutation in 'map2'
blanchet
parents: 54266
diff changeset
   352
    val callssss0 = pad_list [] nn actual_callssss0;
78e8a178b690 use right permutation in 'map2'
blanchet
parents: 54266
diff changeset
   353
53303
ae49b835ca01 moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff changeset
   354
    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
   355
    val bs = pad_list (Binding.name common_name) nn actual_bs;
ae49b835ca01 moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff changeset
   356
ae49b835ca01 moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff changeset
   357
    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
   358
    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
   359
ae49b835ca01 moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff changeset
   360
    val perm_bs = permute bs;
ae49b835ca01 moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff changeset
   361
    val perm_kks = permute kks;
54267
78e8a178b690 use right permutation in 'map2'
blanchet
parents: 54266
diff changeset
   362
    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
   363
    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
   364
54180
blanchet
parents: 54030
diff changeset
   365
    val has_nested = exists (fn Type (_, ty_args) => ty_args <> ty_args0) Ts;
54267
78e8a178b690 use right permutation in 'map2'
blanchet
parents: 54266
diff changeset
   366
    val perm_callssss = map2 indexify_callsss 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
   367
ae49b835ca01 moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff changeset
   368
    val get_perm_indices = map (fn kk => find_index (curry (op =) kk) perm_kks) o get_indices;
ae49b835ca01 moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff changeset
   369
53746
bd038e48526d have "datatype_new_compat" register induction and recursion theorems in nested case
blanchet
parents: 53678
diff changeset
   370
    val ((perm_fp_sugars, fp_sugar_thms), lthy) =
54254
d1478807f287 generalize types when synthetizing n2m (co)recursors, to facilitate reuse
blanchet
parents: 54253
diff changeset
   371
      mutualize_fp_sugars has_nested fp perm_bs perm_Us get_perm_indices perm_callssss
53303
ae49b835ca01 moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff changeset
   372
        perm_fp_sugars0 lthy;
ae49b835ca01 moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff changeset
   373
ae49b835ca01 moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff changeset
   374
    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
   375
  in
53746
bd038e48526d have "datatype_new_compat" register induction and recursion theorems in nested case
blanchet
parents: 53678
diff changeset
   376
    ((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
   377
  end;
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
end;