src/HOL/Tools/BNF/bnf_lfp_compat.ML
author blanchet
Mon Sep 01 17:34:03 2014 +0200 (2014-09-01)
changeset 58129 3ec65a7f2b50
parent 58126 3831312eb476
child 58130 5e9170812356
permissions -rw-r--r--
ported Refute to use new datatypes when possible
blanchet@55061
     1
(*  Title:      HOL/Tools/BNF/bnf_lfp_compat.ML
blanchet@53303
     2
    Author:     Jasmin Blanchette, TU Muenchen
blanchet@58117
     3
    Copyright   2013, 2014
blanchet@53303
     4
blanchet@58119
     5
Compatibility layer with the old datatype package. Parly based on:
blanchet@58119
     6
blanchet@58119
     7
    Title:      HOL/Tools/Old_Datatype/old_datatype_data.ML
blanchet@58119
     8
    Author:     Stefan Berghofer, TU Muenchen
blanchet@53303
     9
*)
blanchet@53303
    10
blanchet@53303
    11
signature BNF_LFP_COMPAT =
blanchet@53303
    12
sig
blanchet@58125
    13
  datatype nesting_preference = Keep_Nesting | Unfold_Nesting
blanchet@58123
    14
blanchet@58125
    15
  val get_all: theory -> nesting_preference -> Old_Datatype_Aux.info Symtab.table
blanchet@58125
    16
  val get_info: theory -> nesting_preference -> string -> Old_Datatype_Aux.info option
blanchet@58125
    17
  val the_info: theory -> nesting_preference -> string -> Old_Datatype_Aux.info
blanchet@58129
    18
  val the_spec: theory -> string -> (string * sort) list * (string * typ list) list
blanchet@58125
    19
  val the_descr: theory -> nesting_preference -> string list ->
blanchet@58117
    20
    Old_Datatype_Aux.descr * (string * sort) list * string list * string
blanchet@58117
    21
    * (string list * string list) * (typ list * typ list)
blanchet@58129
    22
  val get_constrs: theory -> string -> (string * typ) list option
blanchet@58125
    23
  val interpretation: nesting_preference ->
blanchet@58123
    24
    (Old_Datatype_Aux.config -> string list -> theory -> theory) -> theory -> theory
blanchet@58125
    25
  val datatype_compat: string list -> local_theory -> local_theory
blanchet@58125
    26
  val datatype_compat_global: string list -> theory -> theory
blanchet@58117
    27
  val datatype_compat_cmd: string list -> local_theory -> local_theory
blanchet@58125
    28
  val add_datatype: nesting_preference -> Old_Datatype_Aux.spec list -> theory ->
blanchet@58125
    29
    string list * theory
blanchet@58126
    30
  val add_primrec: (binding * typ option * mixfix) list -> (Attrib.binding * term) list ->
blanchet@58126
    31
   local_theory -> (term list * thm list) * local_theory
blanchet@53303
    32
end;
blanchet@53303
    33
blanchet@53303
    34
structure BNF_LFP_Compat : BNF_LFP_COMPAT =
blanchet@53303
    35
struct
blanchet@53303
    36
blanchet@54006
    37
open Ctr_Sugar
blanchet@53303
    38
open BNF_Util
blanchet@53303
    39
open BNF_FP_Util
blanchet@53303
    40
open BNF_FP_Def_Sugar
blanchet@53303
    41
open BNF_FP_N2M_Sugar
blanchet@58123
    42
open BNF_LFP
blanchet@53303
    43
blanchet@53303
    44
val compatN = "compat_";
blanchet@53303
    45
blanchet@58125
    46
datatype nesting_preference = Keep_Nesting | Unfold_Nesting;
blanchet@58123
    47
blanchet@56453
    48
fun reindex_desc desc =
blanchet@56453
    49
  let
blanchet@56453
    50
    val kks = map fst desc;
blanchet@56453
    51
    val perm_kks = sort int_ord kks;
blanchet@56453
    52
blanchet@58112
    53
    fun perm_dtyp (Old_Datatype_Aux.DtType (s, Ds)) = Old_Datatype_Aux.DtType (s, map perm_dtyp Ds)
blanchet@58112
    54
      | perm_dtyp (Old_Datatype_Aux.DtRec kk) =
blanchet@58112
    55
        Old_Datatype_Aux.DtRec (find_index (curry (op =) kk) kks)
blanchet@58113
    56
      | perm_dtyp D = D;
blanchet@56453
    57
  in
blanchet@56453
    58
    if perm_kks = kks then
blanchet@56453
    59
      desc
blanchet@56453
    60
    else
blanchet@56453
    61
      perm_kks ~~
blanchet@56453
    62
      map (fn (_, (s, Ds, sDss)) => (s, map perm_dtyp Ds, map (apsnd (map perm_dtyp)) sDss)) desc
blanchet@58113
    63
  end;
blanchet@56453
    64
blanchet@58125
    65
fun mk_infos_of_mutually_recursive_new_datatypes nesting_pref need_co_inducts_recs check_names
blanchet@58125
    66
    fpT_names0 lthy =
blanchet@53303
    67
  let
blanchet@53303
    68
    val thy = Proof_Context.theory_of lthy;
blanchet@53303
    69
blanchet@53303
    70
    fun not_datatype s = error (quote s ^ " is not a new-style datatype");
blanchet@53303
    71
    fun not_mutually_recursive ss =
blanchet@53303
    72
      error ("{" ^ commas ss ^ "} is not a complete set of mutually recursive new-style datatypes");
blanchet@53303
    73
blanchet@53303
    74
    fun lfp_sugar_of s =
blanchet@53303
    75
      (case fp_sugar_of lthy s of
blanchet@53303
    76
        SOME (fp_sugar as {fp = Least_FP, ...}) => fp_sugar
blanchet@53303
    77
      | _ => not_datatype s);
blanchet@53303
    78
blanchet@56455
    79
    val fpTs0 as Type (_, var_As) :: _ = #Ts (#fp_res (lfp_sugar_of (hd fpT_names0)));
blanchet@56455
    80
    val fpT_names = map (fst o dest_Type) fpTs0;
blanchet@53303
    81
blanchet@58117
    82
    val _ = check_names (op =) (fpT_names0, fpT_names) orelse not_mutually_recursive fpT_names0;
blanchet@53303
    83
blanchet@58117
    84
    val (As_names, _) = Variable.variant_fixes (map (fn TVar ((s, _), _) => s) var_As) lthy;
blanchet@56452
    85
    val As = map2 (fn s => fn TVar (_, S) => TFree (s, S)) As_names var_As;
blanchet@56455
    86
    val fpTs = map (fn s => Type (s, As)) fpT_names;
blanchet@56453
    87
blanchet@56453
    88
    val nn_fp = length fpTs;
blanchet@53303
    89
blanchet@58112
    90
    val mk_dtyp = Old_Datatype_Aux.dtyp_of_typ (map (apsnd (map Term.dest_TFree) o dest_Type) fpTs);
blanchet@56453
    91
blanchet@56453
    92
    fun mk_ctr_descr Ts = mk_ctr Ts #> dest_Const ##> (binder_types #> map mk_dtyp);
blanchet@56453
    93
    fun mk_typ_descr index (Type (T_name, Ts)) ({ctrs, ...} : ctr_sugar) =
blanchet@56453
    94
      (index, (T_name, map mk_dtyp Ts, map (mk_ctr_descr Ts) ctrs));
blanchet@53303
    95
blanchet@56455
    96
    val fp_ctr_sugars = map (#ctr_sugar o lfp_sugar_of) fpT_names;
blanchet@56453
    97
    val orig_descr = map3 mk_typ_descr (0 upto nn_fp - 1) fpTs fp_ctr_sugars;
blanchet@58112
    98
    val all_infos = Old_Datatype_Data.get_all thy;
blanchet@58117
    99
    val (orig_descr' :: nested_descrs) =
blanchet@58125
   100
      if nesting_pref = Keep_Nesting then [orig_descr]
blanchet@58125
   101
      else fst (Old_Datatype_Aux.unfold_datatypes lthy orig_descr all_infos orig_descr nn_fp);
blanchet@53303
   102
blanchet@57798
   103
    fun cliquify_descr [] = []
blanchet@57798
   104
      | cliquify_descr [entry] = [[entry]]
blanchet@57798
   105
      | cliquify_descr (full_descr as (_, (T_name1, _, _)) :: _) =
blanchet@57798
   106
        let
blanchet@57798
   107
          val nn =
blanchet@57798
   108
            if member (op =) fpT_names T_name1 then
blanchet@57798
   109
              nn_fp
blanchet@57798
   110
            else
blanchet@57798
   111
              (case Symtab.lookup all_infos T_name1 of
blanchet@57798
   112
                SOME {descr, ...} =>
blanchet@58112
   113
                length (filter_out (exists Old_Datatype_Aux.is_rec_type o #2 o snd) descr)
blanchet@57798
   114
              | NONE => raise Fail "unknown old-style datatype");
blanchet@57798
   115
        in
blanchet@57798
   116
          chop nn full_descr ||> cliquify_descr |> op ::
blanchet@57798
   117
        end;
blanchet@57798
   118
blanchet@56453
   119
    (* put nested types before the types that nest them, as needed for N2M *)
blanchet@56484
   120
    val descrs = burrow reindex_desc (orig_descr' :: rev nested_descrs);
blanchet@56484
   121
    val (cliques, descr) =
blanchet@57798
   122
      split_list (flat (map_index (fn (i, descr) => map (pair i) descr)
blanchet@57798
   123
        (maps cliquify_descr descrs)));
blanchet@53303
   124
blanchet@58112
   125
    val dest_dtyp = Old_Datatype_Aux.typ_of_dtyp descr;
blanchet@55479
   126
blanchet@58112
   127
    val Ts = Old_Datatype_Aux.get_rec_types descr;
blanchet@56453
   128
    val nn = length Ts;
blanchet@55485
   129
blanchet@55485
   130
    val fp_sugars0 = map (lfp_sugar_of o fst o dest_Type) Ts;
blanchet@56453
   131
    val ctr_Tsss = map (map (map dest_dtyp o snd) o #3 o snd) descr;
blanchet@56453
   132
    val kkssss =
blanchet@58112
   133
      map (map (map (fn Old_Datatype_Aux.DtRec kk => [kk] | _ => []) o snd) o #3 o snd) descr;
blanchet@53303
   134
blanchet@55772
   135
    val callers = map (fn kk => Var ((Name.uu, kk), @{typ "unit => unit"})) (0 upto nn - 1);
blanchet@55772
   136
blanchet@55772
   137
    fun apply_comps n kk =
blanchet@55966
   138
      mk_partial_compN n (replicate n HOLogic.unitT ---> HOLogic.unitT) (nth callers kk);
blanchet@55772
   139
blanchet@55772
   140
    val callssss =
blanchet@56453
   141
      map2 (map2 (map2 (fn ctr_T => map (apply_comps (num_binder_types ctr_T))))) ctr_Tsss kkssss;
blanchet@56453
   142
blanchet@56453
   143
    val b_names = Name.variant_list [] (map base_name_of_typ Ts);
blanchet@56453
   144
    val compat_b_names = map (prefix compatN) b_names;
blanchet@56453
   145
    val compat_bs = map Binding.name compat_b_names;
blanchet@55772
   146
blanchet@58117
   147
    val ((fp_sugars, (lfp_sugar_thms, _)), lthy') =
blanchet@54286
   148
      if nn > nn_fp then
blanchet@58117
   149
        mutualize_fp_sugars Least_FP need_co_inducts_recs cliques compat_bs Ts callers callssss
blanchet@58117
   150
          fp_sugars0 lthy
blanchet@54286
   151
      else
blanchet@54286
   152
        ((fp_sugars0, (NONE, NONE)), lthy);
blanchet@53303
   153
blanchet@56453
   154
    val recs = map (fst o dest_Const o #co_rec) fp_sugars;
blanchet@56453
   155
    val rec_thms = maps #co_rec_thms fp_sugars;
blanchet@56453
   156
blanchet@55540
   157
    val {common_co_inducts = [induct], ...} :: _ = fp_sugars;
blanchet@55539
   158
    val inducts = map (the_single o #co_inducts) fp_sugars;
blanchet@53303
   159
blanchet@55567
   160
    fun mk_info (kk, {T = Type (T_name0, _), ctr_sugar = {casex, exhaust, nchotomy, injects,
blanchet@57983
   161
        distincts, case_thms, case_cong, case_cong_weak, split, split_asm, ...}, ...} : fp_sugar) =
blanchet@55539
   162
      (T_name0,
blanchet@55539
   163
       {index = kk, descr = descr, inject = injects, distinct = distincts, induct = induct,
blanchet@57794
   164
        inducts = inducts, exhaust = exhaust, nchotomy = nchotomy, rec_names = recs,
blanchet@57794
   165
        rec_rewrites = rec_thms, case_name = fst (dest_Const casex), case_rewrites = case_thms,
blanchet@57983
   166
        case_cong = case_cong, case_cong_weak = case_cong_weak, split = split,
blanchet@57794
   167
        split_asm = split_asm});
blanchet@53303
   168
blanchet@55539
   169
    val infos = map_index mk_info (take nn_fp fp_sugars);
blanchet@58117
   170
  in
blanchet@58117
   171
    (nn, b_names, compat_b_names, lfp_sugar_thms, infos, lthy')
blanchet@58117
   172
  end;
blanchet@58117
   173
blanchet@58125
   174
fun infos_of_new_datatype_mutual_cluster lthy nesting_pref fpT_name =
blanchet@58125
   175
  let
blanchet@58125
   176
    fun infos_of nesting_pref =
blanchet@58125
   177
      #5 (mk_infos_of_mutually_recursive_new_datatypes nesting_pref false subset [fpT_name] lthy);
blanchet@58125
   178
  in
blanchet@58125
   179
    infos_of nesting_pref
blanchet@58129
   180
    handle ERROR _ =>
blanchet@58129
   181
      (if nesting_pref = Unfold_Nesting then infos_of Keep_Nesting else [])
blanchet@58129
   182
      handle ERROR _ => []
blanchet@58125
   183
  end;
blanchet@58117
   184
blanchet@58125
   185
fun get_all thy nesting_pref =
blanchet@58117
   186
  let
blanchet@58117
   187
    val lthy = Named_Target.theory_init thy;
blanchet@58117
   188
    val old_info_tab = Old_Datatype_Data.get_all thy;
blanchet@58117
   189
    val new_T_names = BNF_FP_Def_Sugar.fp_sugars_of_global thy
blanchet@58117
   190
      |> map_filter (try (fn {T = Type (s, _), fp_res_index = 0, ...} => s));
blanchet@58125
   191
    val new_infos = maps (infos_of_new_datatype_mutual_cluster lthy nesting_pref) new_T_names;
blanchet@58117
   192
  in
blanchet@58125
   193
    fold (if nesting_pref = Keep_Nesting then Symtab.update else Symtab.default) new_infos
blanchet@58123
   194
      old_info_tab
blanchet@58117
   195
  end;
blanchet@58117
   196
blanchet@58125
   197
fun get_one get_old get_new thy nesting_pref x =
blanchet@58123
   198
  let
blanchet@58123
   199
    val (get_fst, get_snd) =
blanchet@58125
   200
      (get_old thy, get_new thy nesting_pref) |> nesting_pref = Keep_Nesting ? swap
blanchet@58123
   201
  in
blanchet@58117
   202
    (case get_fst x of NONE => get_snd x | res => res)
blanchet@58117
   203
  end;
blanchet@58117
   204
blanchet@58125
   205
fun get_info_of_new_datatype thy nesting_pref T_name =
blanchet@58117
   206
  let val lthy = Named_Target.theory_init thy in
blanchet@58125
   207
    AList.lookup (op =) (infos_of_new_datatype_mutual_cluster lthy nesting_pref T_name) T_name
blanchet@58117
   208
  end;
blanchet@58117
   209
blanchet@58117
   210
val get_info = get_one Old_Datatype_Data.get_info get_info_of_new_datatype;
blanchet@58117
   211
blanchet@58125
   212
fun the_info thy nesting_pref T_name =
blanchet@58125
   213
  (case get_info thy nesting_pref T_name of
blanchet@58117
   214
    SOME info => info
blanchet@58117
   215
  | NONE => error ("Unknown datatype " ^ quote T_name));
blanchet@58117
   216
blanchet@58129
   217
fun the_spec thy T_name =
blanchet@58117
   218
  let
blanchet@58129
   219
    val {descr, index, ...} = the_info thy Keep_Nesting T_name;
blanchet@58117
   220
    val (_, Ds, ctrs0) = the (AList.lookup (op =) descr index);
blanchet@58129
   221
    val tfrees = map Old_Datatype_Aux.dest_DtTFree Ds;
blanchet@58117
   222
    val ctrs = map (apsnd (map (Old_Datatype_Aux.typ_of_dtyp descr))) ctrs0;
blanchet@58129
   223
  in (tfrees, ctrs) end;
blanchet@58117
   224
blanchet@58125
   225
fun the_descr thy nesting_pref (T_names0 as T_name01 :: _) =
blanchet@58117
   226
  let
blanchet@58117
   227
    fun not_mutually_recursive ss =
blanchet@58117
   228
      error ("{" ^ commas ss ^ "} is not a complete set of mutually recursive datatypes");
blanchet@58117
   229
blanchet@58125
   230
    val info = the_info thy nesting_pref T_name01;
blanchet@58117
   231
    val descr = #descr info;
blanchet@58117
   232
blanchet@58117
   233
    val (_, Ds, _) = the (AList.lookup (op =) descr (#index info));
blanchet@58117
   234
    val vs = map Old_Datatype_Aux.dest_DtTFree Ds;
blanchet@58117
   235
blanchet@58117
   236
    fun is_DtTFree (Old_Datatype_Aux.DtTFree _) = true
blanchet@58117
   237
      | is_DtTFree _ = false;
blanchet@58117
   238
blanchet@58117
   239
    val k = find_index (fn (_, (_, dTs, _)) => not (forall is_DtTFree dTs)) descr;
blanchet@58117
   240
    val protoTs as (dataTs, _) = chop k descr
blanchet@58117
   241
      |> (pairself o map)
blanchet@58117
   242
        (fn (_, (T_name, Ds, _)) => (T_name, map (Old_Datatype_Aux.typ_of_dtyp descr) Ds));
blanchet@58117
   243
blanchet@58117
   244
    val T_names = map fst dataTs;
blanchet@58117
   245
    val _ = eq_set (op =) (T_names, T_names0) orelse not_mutually_recursive T_names0
blanchet@58117
   246
blanchet@58117
   247
    val (Ts, Us) = (pairself o map) Type protoTs;
blanchet@58117
   248
blanchet@58117
   249
    val names = map Long_Name.base_name T_names;
blanchet@58117
   250
    val (auxnames, _) = Name.make_context names
blanchet@58117
   251
      |> fold_map (Name.variant o Old_Datatype_Aux.name_of_typ) Us;
blanchet@58117
   252
    val prefix = space_implode "_" names;
blanchet@58117
   253
  in
blanchet@58117
   254
    (descr, vs, T_names, prefix, (names, auxnames), (Ts, Us))
blanchet@58117
   255
  end;
blanchet@58117
   256
blanchet@58129
   257
fun get_constrs thy T_name =
blanchet@58129
   258
  try (the_spec thy) T_name
blanchet@58119
   259
  |> Option.map (fn (tfrees, ctrs) =>
blanchet@58119
   260
    let
blanchet@58119
   261
      fun varify_tfree (s, S) = TVar ((s, 0), S);
blanchet@58119
   262
      fun varify_typ (TFree x) = varify_tfree x
blanchet@58119
   263
        | varify_typ T = T;
blanchet@58119
   264
blanchet@58119
   265
      val dataT = Type (T_name, map varify_tfree tfrees);
blanchet@58119
   266
blanchet@58119
   267
      fun mk_ctr_typ Ts = map (Term.map_atyps varify_typ) Ts ---> dataT;
blanchet@58119
   268
    in
blanchet@58119
   269
      map (apsnd mk_ctr_typ) ctrs
blanchet@58119
   270
    end);
blanchet@58117
   271
blanchet@58125
   272
fun old_interpretation_of nesting_pref f config T_names thy =
blanchet@58125
   273
  if nesting_pref = Unfold_Nesting orelse exists (is_none o fp_sugar_of_global thy) T_names then
blanchet@58122
   274
    f config T_names thy
blanchet@58122
   275
  else
blanchet@58122
   276
    thy;
blanchet@58122
   277
blanchet@58125
   278
fun new_interpretation_of nesting_pref f fp_sugars thy =
blanchet@58122
   279
  let val T_names = map (fst o dest_Type o #T) fp_sugars in
blanchet@58125
   280
    if nesting_pref = Keep_Nesting orelse
blanchet@58123
   281
        exists (is_none o Old_Datatype_Data.get_info thy) T_names then
blanchet@58123
   282
      f Old_Datatype_Aux.default_config T_names thy
blanchet@58122
   283
    else
blanchet@58122
   284
      thy
blanchet@58122
   285
  end;
blanchet@58122
   286
blanchet@58125
   287
fun interpretation nesting_pref f =
blanchet@58125
   288
  Old_Datatype_Data.interpretation (old_interpretation_of nesting_pref f)
blanchet@58125
   289
  #> fp_sugar_interpretation (new_interpretation_of nesting_pref f);
blanchet@58117
   290
blanchet@58117
   291
val code_nitpicksimp_simp_attrs = Code.add_default_eqn_attrib :: @{attributes [nitpick_simp, simp]};
blanchet@58117
   292
blanchet@58125
   293
fun datatype_compat fpT_names lthy =
blanchet@58117
   294
  let
blanchet@58117
   295
    val (nn, b_names, compat_b_names, lfp_sugar_thms, infos, lthy') =
blanchet@58125
   296
      mk_infos_of_mutually_recursive_new_datatypes Unfold_Nesting true eq_set fpT_names lthy;
blanchet@53303
   297
blanchet@53746
   298
    val all_notes =
blanchet@53746
   299
      (case lfp_sugar_thms of
blanchet@53746
   300
        NONE => []
blanchet@55856
   301
      | SOME ((induct_thms, induct_thm, induct_attrs), (rec_thmss, _)) =>
blanchet@53746
   302
        let
blanchet@58117
   303
          val common_name = compatN ^ mk_common_name b_names;
blanchet@58117
   304
blanchet@53746
   305
          val common_notes =
blanchet@53746
   306
            (if nn > 1 then [(inductN, [induct_thm], induct_attrs)] else [])
blanchet@53746
   307
            |> filter_out (null o #2)
blanchet@53746
   308
            |> map (fn (thmN, thms, attrs) =>
blanchet@53746
   309
              ((Binding.qualify true common_name (Binding.name thmN), attrs), [(thms, [])]));
blanchet@53746
   310
blanchet@53746
   311
          val notes =
blanchet@55856
   312
            [(inductN, map single induct_thms, induct_attrs),
blanchet@55479
   313
             (recN, rec_thmss, code_nitpicksimp_simp_attrs)]
blanchet@53746
   314
            |> filter_out (null o #2)
blanchet@53746
   315
            |> maps (fn (thmN, thmss, attrs) =>
blanchet@53746
   316
              if forall null thmss then
blanchet@53746
   317
                []
blanchet@53746
   318
              else
blanchet@53746
   319
                map2 (fn b_name => fn thms =>
blanchet@53746
   320
                    ((Binding.qualify true b_name (Binding.name thmN), attrs), [(thms, [])]))
blanchet@53746
   321
                  compat_b_names thmss);
blanchet@53746
   322
        in
blanchet@53746
   323
          common_notes @ notes
blanchet@53746
   324
        end);
blanchet@53746
   325
blanchet@53746
   326
    val register_interpret =
blanchet@58112
   327
      Old_Datatype_Data.register infos
blanchet@58113
   328
      #> Old_Datatype_Data.interpretation_data (Old_Datatype_Aux.default_config, map fst infos);
blanchet@53303
   329
  in
blanchet@58117
   330
    lthy'
blanchet@53746
   331
    |> Local_Theory.raw_theory register_interpret
blanchet@57633
   332
    |> Local_Theory.notes all_notes
blanchet@57633
   333
    |> snd
blanchet@53303
   334
  end;
blanchet@53303
   335
blanchet@58125
   336
fun datatype_compat_global fpT_names =
blanchet@58125
   337
  Named_Target.theory_init
blanchet@58125
   338
  #> datatype_compat fpT_names
blanchet@58125
   339
  #> Named_Target.exit;
blanchet@58125
   340
blanchet@58125
   341
fun datatype_compat_cmd raw_fpT_names lthy =
blanchet@58125
   342
  let
blanchet@58125
   343
    val fpT_names =
blanchet@58125
   344
      map (fst o dest_Type o Proof_Context.read_type_name {proper = true, strict = false} lthy)
blanchet@58125
   345
        raw_fpT_names;
blanchet@58125
   346
  in
blanchet@58125
   347
    datatype_compat fpT_names lthy
blanchet@58125
   348
  end;
blanchet@58125
   349
blanchet@58125
   350
fun add_datatype nesting_pref old_specs thy =
blanchet@58123
   351
  let
blanchet@58123
   352
    val fpT_names = map (Sign.full_name thy o #1 o fst) old_specs;
blanchet@58123
   353
blanchet@58123
   354
    fun new_type_args_of (s, S) = (SOME Binding.empty, (TFree (s, @{sort type}), S));
blanchet@58123
   355
    fun new_ctr_spec_of (b, Ts, mx) = (((Binding.empty, b), map (pair Binding.empty) Ts), mx);
blanchet@58123
   356
blanchet@58123
   357
    fun new_spec_of ((b, old_tyargs, mx), old_ctr_specs) =
blanchet@58123
   358
      (((((map new_type_args_of old_tyargs, b), mx), map new_ctr_spec_of old_ctr_specs),
blanchet@58123
   359
        (Binding.empty, Binding.empty)), []);
blanchet@58123
   360
blanchet@58123
   361
    val new_specs = map new_spec_of old_specs;
blanchet@58123
   362
  in
blanchet@58123
   363
    (fpT_names,
blanchet@58123
   364
     thy
blanchet@58123
   365
     |> Named_Target.theory_init
blanchet@58123
   366
     |> co_datatypes Least_FP construct_lfp ((false, false), new_specs)
blanchet@58125
   367
     |> Named_Target.exit
blanchet@58125
   368
     |> nesting_pref = Unfold_Nesting ? perhaps (try (datatype_compat_global fpT_names)))
blanchet@58123
   369
  end;
blanchet@58123
   370
blanchet@58126
   371
val add_primrec = apfst (apsnd flat) ooo BNF_LFP_Rec_Sugar.add_primrec;
blanchet@58126
   372
blanchet@53303
   373
val _ =
blanchet@55531
   374
  Outer_Syntax.local_theory @{command_spec "datatype_compat"}
blanchet@54025
   375
    "register new-style datatypes as old-style datatypes"
blanchet@55531
   376
    (Scan.repeat1 Parse.type_const >> datatype_compat_cmd);
blanchet@53303
   377
blanchet@53303
   378
end;