src/HOL/BNF/Tools/bnf_lfp_compat.ML
author blanchet
Tue Oct 01 14:05:25 2013 +0200 (2013-10-01)
changeset 54006 9fe1bd54d437
parent 54003 c4343c31f86d
child 54009 f138452e8265
permissions -rw-r--r--
renamed theory file
blanchet@53303
     1
(*  Title:      HOL/BNF/Tools/bnf_lfp_compat.ML
blanchet@53303
     2
    Author:     Jasmin Blanchette, TU Muenchen
blanchet@53303
     3
    Copyright   2013
blanchet@53303
     4
blanchet@53303
     5
Compatibility layer with the old datatype package.
blanchet@53303
     6
*)
blanchet@53303
     7
blanchet@53303
     8
signature BNF_LFP_COMPAT =
blanchet@53303
     9
sig
blanchet@53309
    10
  val datatype_new_compat_cmd : string list -> local_theory -> local_theory
blanchet@53303
    11
end;
blanchet@53303
    12
blanchet@53303
    13
structure BNF_LFP_Compat : BNF_LFP_COMPAT =
blanchet@53303
    14
struct
blanchet@53303
    15
blanchet@54006
    16
open Ctr_Sugar
blanchet@53303
    17
open BNF_Util
blanchet@53303
    18
open BNF_FP_Util
blanchet@53303
    19
open BNF_FP_Def_Sugar
blanchet@53303
    20
open BNF_FP_N2M_Sugar
blanchet@53303
    21
blanchet@53303
    22
fun dtyp_of_typ _ (TFree a) = Datatype_Aux.DtTFree a
blanchet@53303
    23
  | dtyp_of_typ recTs (T as Type (s, Ts)) =
blanchet@53303
    24
    (case find_index (curry (op =) T) recTs of
blanchet@53303
    25
      ~1 => Datatype_Aux.DtType (s, map (dtyp_of_typ recTs) Ts)
blanchet@53303
    26
    | kk => Datatype_Aux.DtRec kk);
blanchet@53303
    27
blanchet@53303
    28
val compatN = "compat_";
blanchet@53303
    29
blanchet@53303
    30
(* TODO: graceful failure for local datatypes -- perhaps by making the command global *)
blanchet@53309
    31
fun datatype_new_compat_cmd raw_fpT_names lthy =
blanchet@53303
    32
  let
blanchet@53303
    33
    val thy = Proof_Context.theory_of lthy;
blanchet@53303
    34
blanchet@53303
    35
    fun not_datatype s = error (quote s ^ " is not a new-style datatype");
blanchet@53303
    36
    fun not_mutually_recursive ss =
blanchet@53303
    37
      error ("{" ^ commas ss ^ "} is not a complete set of mutually recursive new-style datatypes");
blanchet@53303
    38
blanchet@53303
    39
    val (fpT_names as fpT_name1 :: _) =
blanchet@53303
    40
      map (fst o dest_Type o Proof_Context.read_type_name_proper lthy false) raw_fpT_names;
blanchet@53303
    41
blanchet@53303
    42
    val Ss = Sign.arity_sorts thy fpT_name1 HOLogic.typeS;
blanchet@53303
    43
blanchet@53303
    44
    val (unsorted_As, _) = lthy |> mk_TFrees (length Ss);
blanchet@53303
    45
    val As = map2 resort_tfree Ss unsorted_As;
blanchet@53303
    46
blanchet@53303
    47
    fun lfp_sugar_of s =
blanchet@53303
    48
      (case fp_sugar_of lthy s of
blanchet@53303
    49
        SOME (fp_sugar as {fp = Least_FP, ...}) => fp_sugar
blanchet@53303
    50
      | _ => not_datatype s);
blanchet@53303
    51
blanchet@53303
    52
    val fp_sugar0 as {fp_res = {Ts = fpTs0, ...}, ...} = lfp_sugar_of fpT_name1;
blanchet@53303
    53
    val fpT_names' = map (fst o dest_Type) fpTs0;
blanchet@53303
    54
blanchet@53303
    55
    val _ = eq_set (op =) (fpT_names, fpT_names') orelse not_mutually_recursive fpT_names;
blanchet@53303
    56
blanchet@53303
    57
    val fpTs as fpT1 :: _ = map (fn s => Type (s, As)) fpT_names';
blanchet@53303
    58
blanchet@53303
    59
    fun add_nested_types_of (T as Type (s, _)) seen =
blanchet@53303
    60
      if member (op =) seen T orelse s = @{type_name fun} then
blanchet@53303
    61
        seen
blanchet@53303
    62
      else
blanchet@53303
    63
        (case try lfp_sugar_of s of
blanchet@53303
    64
          SOME ({T = T0, fp_res = {Ts = mutual_Ts0, ...}, ctr_sugars, ...}) =>
blanchet@53303
    65
          let
blanchet@53303
    66
            val rho = Vartab.fold (cons o apsnd snd) (Sign.typ_match thy (T0, T) Vartab.empty) [];
blanchet@53303
    67
            val substT = Term.typ_subst_TVars rho;
blanchet@53303
    68
blanchet@53303
    69
            val mutual_Ts = map substT mutual_Ts0;
blanchet@53303
    70
blanchet@53901
    71
            fun add_interesting_subtypes (U as Type (_, Us)) =
blanchet@53303
    72
                (case filter (exists_subtype_in mutual_Ts) Us of [] => I
blanchet@53303
    73
                | Us' => insert (op =) U #> fold add_interesting_subtypes Us')
blanchet@53303
    74
              | add_interesting_subtypes _ = I;
blanchet@53303
    75
blanchet@53303
    76
            val ctrs = maps #ctrs ctr_sugars;
blanchet@53303
    77
            val ctr_Ts = maps (binder_types o substT o fastype_of) ctrs |> distinct (op =);
blanchet@53303
    78
            val subTs = fold add_interesting_subtypes ctr_Ts [];
blanchet@53303
    79
          in
blanchet@53303
    80
            fold add_nested_types_of subTs (seen @ mutual_Ts)
blanchet@53303
    81
          end
blanchet@53303
    82
        | NONE => error ("Unsupported recursion via type constructor " ^ quote s ^
blanchet@53303
    83
            " not associated with new-style datatype (cf. \"datatype_new\")"));
blanchet@53303
    84
blanchet@53303
    85
    val Ts = add_nested_types_of fpT1 [];
blanchet@53746
    86
    val b_names = map base_name_of_typ Ts;
blanchet@53746
    87
    val compat_b_names = map (prefix compatN) b_names;
blanchet@53746
    88
    val compat_bs = map Binding.name compat_b_names;
blanchet@53746
    89
    val common_name = compatN ^ mk_common_name b_names;
blanchet@53303
    90
    val nn_fp = length fpTs;
blanchet@53303
    91
    val nn = length Ts;
blanchet@53303
    92
    val get_indices = K [];
blanchet@53746
    93
    val fp_sugars0 = if nn = 1 then [fp_sugar0] else map (lfp_sugar_of o fst o dest_Type) Ts;
blanchet@53303
    94
    val callssss = pad_and_indexify_calls fp_sugars0 nn [];
blanchet@53303
    95
    val has_nested = nn > nn_fp;
blanchet@53303
    96
blanchet@53746
    97
    val ((fp_sugars, (lfp_sugar_thms, _)), lthy) =
blanchet@53746
    98
      mutualize_fp_sugars false has_nested Least_FP compat_bs Ts get_indices callssss fp_sugars0
blanchet@53746
    99
        lthy;
blanchet@53303
   100
blanchet@53303
   101
    val {ctr_sugars, co_inducts = [induct], co_iterss, co_iter_thmsss = iter_thmsss, ...} :: _ =
blanchet@53303
   102
      fp_sugars;
blanchet@53303
   103
    val inducts = conj_dests nn induct;
blanchet@53303
   104
blanchet@53303
   105
    val frozen_Ts = map Type.legacy_freeze_type Ts;
blanchet@53303
   106
    val mk_dtyp = dtyp_of_typ frozen_Ts;
blanchet@53303
   107
blanchet@53303
   108
    fun mk_ctr_descr (Const (s, T)) =
blanchet@53303
   109
      (s, map mk_dtyp (binder_types (Type.legacy_freeze_type T)));
blanchet@54003
   110
    fun mk_typ_descr index (Type (T_name, Ts)) ({ctrs, ...} : ctr_sugar) =
blanchet@53303
   111
      (index, (T_name, map mk_dtyp Ts, map mk_ctr_descr ctrs));
blanchet@53303
   112
blanchet@53303
   113
    val descr = map3 mk_typ_descr (0 upto nn - 1) frozen_Ts ctr_sugars;
blanchet@53303
   114
    val recs = map (fst o dest_Const o co_rec_of) co_iterss;
blanchet@53303
   115
    val rec_thms = flat (map co_rec_of iter_thmsss);
blanchet@53303
   116
blanchet@54003
   117
    fun mk_info ({T = Type (T_name0, _), index, ...} : fp_sugar) =
blanchet@53303
   118
      let
blanchet@53303
   119
        val {casex, exhaust, nchotomy, injects, distincts, case_thms, case_cong, weak_case_cong,
blanchet@53303
   120
          split, split_asm, ...} = nth ctr_sugars index;
blanchet@53303
   121
      in
blanchet@53303
   122
        (T_name0,
blanchet@53303
   123
         {index = index, descr = descr, inject = injects, distinct = distincts, induct = induct,
blanchet@53303
   124
         inducts = inducts, exhaust = exhaust, nchotomy = nchotomy, rec_names = recs,
blanchet@53303
   125
         rec_rewrites = rec_thms, case_name = fst (dest_Const casex), case_rewrites = case_thms,
blanchet@53303
   126
         case_cong = case_cong, weak_case_cong = weak_case_cong, split = split,
blanchet@53303
   127
         split_asm = split_asm})
blanchet@53303
   128
      end;
blanchet@53303
   129
blanchet@53303
   130
    val infos = map mk_info (take nn_fp fp_sugars);
blanchet@53303
   131
blanchet@53746
   132
    val all_notes =
blanchet@53746
   133
      (case lfp_sugar_thms of
blanchet@53746
   134
        NONE => []
blanchet@53808
   135
      | SOME ((induct_thms, induct_thm, induct_attrs), (fold_thmss, rec_thmss, _)) =>
blanchet@53746
   136
        let
blanchet@53746
   137
          val common_notes =
blanchet@53746
   138
            (if nn > 1 then [(inductN, [induct_thm], induct_attrs)] else [])
blanchet@53746
   139
            |> filter_out (null o #2)
blanchet@53746
   140
            |> map (fn (thmN, thms, attrs) =>
blanchet@53746
   141
              ((Binding.qualify true common_name (Binding.name thmN), attrs), [(thms, [])]));
blanchet@53746
   142
blanchet@53746
   143
          val notes =
blanchet@53747
   144
            [(foldN, fold_thmss, []),
blanchet@53746
   145
             (inductN, map single induct_thms, induct_attrs),
blanchet@53747
   146
             (recN, rec_thmss, [])]
blanchet@53746
   147
            |> filter_out (null o #2)
blanchet@53746
   148
            |> maps (fn (thmN, thmss, attrs) =>
blanchet@53746
   149
              if forall null thmss then
blanchet@53746
   150
                []
blanchet@53746
   151
              else
blanchet@53746
   152
                map2 (fn b_name => fn thms =>
blanchet@53746
   153
                    ((Binding.qualify true b_name (Binding.name thmN), attrs), [(thms, [])]))
blanchet@53746
   154
                  compat_b_names thmss);
blanchet@53746
   155
        in
blanchet@53746
   156
          common_notes @ notes
blanchet@53746
   157
        end);
blanchet@53746
   158
blanchet@53746
   159
    val register_interpret =
blanchet@53303
   160
      Datatype_Data.register infos
blanchet@53303
   161
      #> Datatype_Data.interpretation_data (Datatype_Aux.default_config, map fst infos)
blanchet@53303
   162
  in
blanchet@53746
   163
    lthy
blanchet@53746
   164
    |> Local_Theory.raw_theory register_interpret
blanchet@53746
   165
    |> Local_Theory.notes all_notes |> snd
blanchet@53303
   166
  end;
blanchet@53303
   167
blanchet@53303
   168
val _ =
blanchet@53309
   169
  Outer_Syntax.local_theory @{command_spec "datatype_new_compat"}
blanchet@53303
   170
    "register a new-style datatype as an old-style datatype"
blanchet@53309
   171
    (Scan.repeat1 Parse.type_const >> datatype_new_compat_cmd);
blanchet@53303
   172
blanchet@53303
   173
end;