src/HOL/Tools/BNF/bnf_lfp_size.ML
author blanchet
Wed Apr 23 10:23:26 2014 +0200 (2014-04-23)
changeset 56638 092a306bcc3d
child 56639 c9d6b581bd3b
permissions -rw-r--r--
generate size instances for new-style datatypes
blanchet@56638
     1
(*  Title:      HOL/Tools/BNF/bnf_lfp_size.ML
blanchet@56638
     2
    Author:     Jasmin Blanchette, TU Muenchen
blanchet@56638
     3
    Copyright   2014
blanchet@56638
     4
blanchet@56638
     5
Generation of size functions for new-style datatypes.
blanchet@56638
     6
*)
blanchet@56638
     7
blanchet@56638
     8
structure BNF_LFP_Size : sig end =
blanchet@56638
     9
struct
blanchet@56638
    10
blanchet@56638
    11
open BNF_Util
blanchet@56638
    12
open BNF_Def
blanchet@56638
    13
open BNF_FP_Def_Sugar
blanchet@56638
    14
blanchet@56638
    15
val size_N = "size_"
blanchet@56638
    16
blanchet@56638
    17
val sizeN = "size"
blanchet@56638
    18
val size_mapN = "size_map"
blanchet@56638
    19
blanchet@56638
    20
structure Data = Theory_Data
blanchet@56638
    21
(
blanchet@56638
    22
  type T = (string * (thm list * thm list)) Symtab.table;
blanchet@56638
    23
  val empty = Symtab.empty;
blanchet@56638
    24
  val extend = I
blanchet@56638
    25
  fun merge data = Symtab.merge (K true) data;
blanchet@56638
    26
);
blanchet@56638
    27
blanchet@56638
    28
val zero_nat = @{const zero_class.zero (nat)};
blanchet@56638
    29
blanchet@56638
    30
fun mk_plus_nat (t1, t2) = Const (@{const_name Groups.plus},
blanchet@56638
    31
  HOLogic.natT --> HOLogic.natT --> HOLogic.natT) $ t1 $ t2;
blanchet@56638
    32
blanchet@56638
    33
fun mk_to_natT T = T --> HOLogic.natT;
blanchet@56638
    34
blanchet@56638
    35
fun mk_abs_zero_nat T = Term.absdummy T zero_nat;
blanchet@56638
    36
blanchet@56638
    37
fun generate_size (fp_sugars as ({T = Type (_, As), BT = Type (_, Bs),
blanchet@56638
    38
    fp_res = {bnfs = fp_bnfs, ...}, common_co_inducts = common_inducts, ...} : fp_sugar) :: _) thy =
blanchet@56638
    39
  let
blanchet@56638
    40
    val data = Data.get thy;
blanchet@56638
    41
blanchet@56638
    42
    val Ts = map #T fp_sugars
blanchet@56638
    43
    val T_names = map (fst o dest_Type) Ts;
blanchet@56638
    44
    val nn = length Ts;
blanchet@56638
    45
blanchet@56638
    46
    val B_ify = Term.typ_subst_atomic (As ~~ Bs);
blanchet@56638
    47
blanchet@56638
    48
    val recs = map #co_rec fp_sugars;
blanchet@56638
    49
    val rec_thmss = map #co_rec_thms fp_sugars;
blanchet@56638
    50
    val rec_Ts = map fastype_of recs;
blanchet@56638
    51
    val Cs = map body_type rec_Ts;
blanchet@56638
    52
    val Cs_rho = map (rpair HOLogic.natT) Cs;
blanchet@56638
    53
    val substCT = Term.subst_atomic_types Cs_rho;
blanchet@56638
    54
blanchet@56638
    55
    val f_Ts = map mk_to_natT As;
blanchet@56638
    56
    val f_TsB = map mk_to_natT Bs;
blanchet@56638
    57
    val num_As = length As;
blanchet@56638
    58
blanchet@56638
    59
    val f_names = map (prefix "f" o string_of_int) (1 upto num_As);
blanchet@56638
    60
    val fs = map2 (curry Free) f_names f_Ts;
blanchet@56638
    61
    val fsB = map2 (curry Free) f_names f_TsB;
blanchet@56638
    62
    val As_fs = As ~~ fs;
blanchet@56638
    63
blanchet@56638
    64
    val gen_size_names = map (Long_Name.map_base_name (prefix size_N)) T_names;
blanchet@56638
    65
blanchet@56638
    66
    fun is_pair_C @{type_name prod} [_, T'] = member (op =) Cs T'
blanchet@56638
    67
      | is_pair_C _ _ = false;
blanchet@56638
    68
blanchet@56638
    69
    fun mk_size_of_typ (T as TFree _) =
blanchet@56638
    70
        pair (case AList.lookup (op =) As_fs T of
blanchet@56638
    71
            SOME f => f
blanchet@56638
    72
          | NONE => if member (op =) Cs T then Term.absdummy T (Bound 0) else mk_abs_zero_nat T)
blanchet@56638
    73
      | mk_size_of_typ (T as Type (s, Ts)) =
blanchet@56638
    74
        if is_pair_C s Ts then
blanchet@56638
    75
          pair (snd_const T)
blanchet@56638
    76
        else if exists (exists_subtype_in As) Ts then
blanchet@56638
    77
          (case Symtab.lookup data s of
blanchet@56638
    78
            SOME (gen_size_name, (_, gen_size_maps)) =>
blanchet@56638
    79
            let
blanchet@56638
    80
              val (args, gen_size_mapss') = split_list (map (fn T => mk_size_of_typ T []) Ts);
blanchet@56638
    81
              val gen_size_const = Const (gen_size_name, map fastype_of args ---> mk_to_natT T);
blanchet@56638
    82
            in
blanchet@56638
    83
              fold (union Thm.eq_thm) (gen_size_maps :: gen_size_mapss')
blanchet@56638
    84
              #> pair (Term.list_comb (gen_size_const, args))
blanchet@56638
    85
            end
blanchet@56638
    86
          | NONE => pair (mk_abs_zero_nat T))
blanchet@56638
    87
        else
blanchet@56638
    88
          pair (mk_abs_zero_nat T);
blanchet@56638
    89
blanchet@56638
    90
    fun mk_size_of_arg t =
blanchet@56638
    91
      mk_size_of_typ (fastype_of t) #>> (fn s => substCT (betapply (s, t)));
blanchet@56638
    92
blanchet@56638
    93
    fun mk_gen_size_arg arg_T gen_size_maps =
blanchet@56638
    94
      let
blanchet@56638
    95
        val x_Ts = binder_types arg_T;
blanchet@56638
    96
        val m = length x_Ts;
blanchet@56638
    97
        val x_names = map (prefix "x" o string_of_int) (1 upto m);
blanchet@56638
    98
        val xs = map2 (curry Free) x_names x_Ts;
blanchet@56638
    99
        val (summands, gen_size_maps') =
blanchet@56638
   100
          fold_map mk_size_of_arg xs gen_size_maps
blanchet@56638
   101
          |>> remove (op =) zero_nat;
blanchet@56638
   102
        val sum =
blanchet@56638
   103
          if null summands then HOLogic.zero
blanchet@56638
   104
          else foldl1 mk_plus_nat (summands @ [HOLogic.Suc_zero]);
blanchet@56638
   105
      in
blanchet@56638
   106
        (fold_rev Term.lambda (map substCT xs) sum, gen_size_maps')
blanchet@56638
   107
      end;
blanchet@56638
   108
blanchet@56638
   109
    fun mk_gen_size_rhs rec_T recx gen_size_maps =
blanchet@56638
   110
      let
blanchet@56638
   111
        val arg_Ts = binder_fun_types rec_T;
blanchet@56638
   112
        val (args, gen_size_maps') = fold_map mk_gen_size_arg arg_Ts gen_size_maps;
blanchet@56638
   113
      in
blanchet@56638
   114
        (fold_rev Term.lambda fs (Term.list_comb (substCT recx, args)), gen_size_maps')
blanchet@56638
   115
      end;
blanchet@56638
   116
blanchet@56638
   117
    fun mk_def_binding f = Binding.conceal o Binding.name o Thm.def_name o f o Long_Name.base_name;
blanchet@56638
   118
blanchet@56638
   119
    val (gen_size_rhss, nested_gen_size_maps) = fold_map2 mk_gen_size_rhs rec_Ts recs [];
blanchet@56638
   120
    val gen_size_Ts = map fastype_of gen_size_rhss;
blanchet@56638
   121
    val gen_size_consts = map2 (curry Const) gen_size_names gen_size_Ts;
blanchet@56638
   122
    val gen_size_constsB = map (Term.map_types B_ify) gen_size_consts;
blanchet@56638
   123
    val gen_size_def_bs = map (mk_def_binding I) gen_size_names;
blanchet@56638
   124
blanchet@56638
   125
    val (gen_size_defs, thy2) =
blanchet@56638
   126
      thy
blanchet@56638
   127
      |> Sign.add_consts (map (fn (s, T) => (Binding.name (Long_Name.base_name s), T, NoSyn))
blanchet@56638
   128
        (gen_size_names ~~ gen_size_Ts))
blanchet@56638
   129
      |> Global_Theory.add_defs false (map Thm.no_attributes (gen_size_def_bs ~~
blanchet@56638
   130
        map Logic.mk_equals (gen_size_consts ~~ gen_size_rhss)));
blanchet@56638
   131
blanchet@56638
   132
    val zeros = map mk_abs_zero_nat As;
blanchet@56638
   133
blanchet@56638
   134
    val spec_size_rhss = map (fn c => Term.list_comb (c, zeros)) gen_size_consts;
blanchet@56638
   135
    val spec_size_Ts = map fastype_of spec_size_rhss;
blanchet@56638
   136
    val spec_size_consts = map (curry Const @{const_name size}) spec_size_Ts;
blanchet@56638
   137
    val spec_size_def_bs = map (mk_def_binding (suffix "_overloaded")) gen_size_names;
blanchet@56638
   138
blanchet@56638
   139
    fun define_spec_size def_b lhs0 rhs lthy =
blanchet@56638
   140
      let
blanchet@56638
   141
        val Free (c, _) = Syntax.check_term lthy lhs0;
blanchet@56638
   142
        val (thm, lthy') = lthy
blanchet@56638
   143
          |> Local_Theory.define ((Binding.name c, NoSyn), ((def_b, []), rhs))
blanchet@56638
   144
          |-> (fn (t, (_, thm)) => Spec_Rules.add Spec_Rules.Equational ([t], [thm]) #> pair thm);
blanchet@56638
   145
        val ctxt_thy = Proof_Context.init_global (Proof_Context.theory_of lthy');
blanchet@56638
   146
        val thm' = singleton (Proof_Context.export lthy' ctxt_thy) thm;
blanchet@56638
   147
      in (thm', lthy') end;
blanchet@56638
   148
blanchet@56638
   149
    val (spec_size_defs, thy3) = thy2
blanchet@56638
   150
      |> Class.instantiation (T_names, map dest_TFree As, [HOLogic.class_size])
blanchet@56638
   151
      |> fold_map3 define_spec_size spec_size_def_bs spec_size_consts spec_size_rhss
blanchet@56638
   152
      ||> Class.prove_instantiation_instance (K (Class.intro_classes_tac []))
blanchet@56638
   153
      ||> Local_Theory.exit_global;
blanchet@56638
   154
blanchet@56638
   155
    val thy3_ctxt = Proof_Context.init_global thy3;
blanchet@56638
   156
blanchet@56638
   157
    val gen_size_defs' =
blanchet@56638
   158
      map (mk_unabs_def (num_As + 1) o (fn thm => thm RS meta_eq_to_obj_eq)) gen_size_defs;
blanchet@56638
   159
    val spec_size_defs' =
blanchet@56638
   160
      map (mk_unabs_def 1 o (fn thm => thm RS meta_eq_to_obj_eq)) spec_size_defs;
blanchet@56638
   161
blanchet@56638
   162
    fun derive_size_simp unfolds folds size_def' simp0 =
blanchet@56638
   163
      fold_thms thy3_ctxt folds (unfold_thms thy3_ctxt unfolds (trans OF [size_def', simp0]));
blanchet@56638
   164
    val derive_gen_size_simp =
blanchet@56638
   165
      derive_size_simp (@{thm snd_o_convol} :: nested_gen_size_maps) gen_size_defs';
blanchet@56638
   166
    val derive_spec_size_simp = derive_size_simp @{thms add_0_left add_0_right} spec_size_defs';
blanchet@56638
   167
blanchet@56638
   168
    val gen_size_simpss = map2 (map o derive_gen_size_simp) gen_size_defs' rec_thmss;
blanchet@56638
   169
    val gen_size_simps = flat gen_size_simpss;
blanchet@56638
   170
    val spec_size_simpss = map2 (map o derive_spec_size_simp) spec_size_defs' gen_size_simpss;
blanchet@56638
   171
blanchet@56638
   172
    val ABs = As ~~ Bs;
blanchet@56638
   173
    val g_names = map (prefix "g" o string_of_int) (1 upto num_As);
blanchet@56638
   174
    val gs = map2 (curry Free) g_names (map (op -->) ABs);
blanchet@56638
   175
blanchet@56638
   176
    val liveness = map (op <>) ABs;
blanchet@56638
   177
    val live_gs = AList.find (op =) (gs ~~ liveness) true;
blanchet@56638
   178
    val live = length live_gs;
blanchet@56638
   179
blanchet@56638
   180
    val u_names = map (prefix "u" o string_of_int) (1 upto nn);
blanchet@56638
   181
    val us = map2 (curry Free) u_names Ts;
blanchet@56638
   182
blanchet@56638
   183
    val maps0 = map map_of_bnf fp_bnfs;
blanchet@56638
   184
    val map_thms = maps #maps fp_sugars;
blanchet@56638
   185
blanchet@56638
   186
    fun mk_gen_size_map_tac ctxt =
blanchet@56638
   187
      HEADGOAL (rtac (co_induct_of common_inducts)) THEN
blanchet@56638
   188
      ALLGOALS (asm_simp_tac (ss_only (o_apply :: map_thms @ gen_size_simps) ctxt));
blanchet@56638
   189
blanchet@56638
   190
    val gen_size_map_thmss =
blanchet@56638
   191
      if live = 0 then
blanchet@56638
   192
        replicate nn []
blanchet@56638
   193
      else if null nested_gen_size_maps then
blanchet@56638
   194
        let
blanchet@56638
   195
          val xgmaps =
blanchet@56638
   196
            map2 (fn map0 => fn u => Term.list_comb (mk_map live As Bs map0, live_gs) $ u) maps0 us;
blanchet@56638
   197
          val fsizes =
blanchet@56638
   198
            map (fn gen_size_constB => Term.list_comb (gen_size_constB, fsB)) gen_size_constsB;
blanchet@56638
   199
          val lhss = map2 (curry (op $)) fsizes xgmaps;
blanchet@56638
   200
blanchet@56638
   201
          val fgs = map2 (fn fB => fn g as Free (_, Type (_, [A, B])) =>
blanchet@56638
   202
            if A = B then fB else HOLogic.mk_comp (fB, g)) fsB gs;
blanchet@56638
   203
          val rhss = map2 (fn gen_size_const => fn u => Term.list_comb (gen_size_const, fgs) $ u)
blanchet@56638
   204
            gen_size_consts us;
blanchet@56638
   205
blanchet@56638
   206
          val goal = Library.foldr1 HOLogic.mk_conj (map2 (curry HOLogic.mk_eq) lhss rhss)
blanchet@56638
   207
            |> HOLogic.mk_Trueprop;
blanchet@56638
   208
        in
blanchet@56638
   209
          Goal.prove_global thy3 [] [] goal (mk_gen_size_map_tac o #context)
blanchet@56638
   210
          |> Thm.close_derivation
blanchet@56638
   211
          |> conj_dests nn
blanchet@56638
   212
          |> map single
blanchet@56638
   213
        end
blanchet@56638
   214
      else
blanchet@56638
   215
        (* TODO: implement general case, with nesting of datatypes that themselves nest other
blanchet@56638
   216
           types *)
blanchet@56638
   217
        replicate nn [];
blanchet@56638
   218
blanchet@56638
   219
    val (_, thy4) = thy3
blanchet@56638
   220
      |> fold_map3 (fn T_name => fn size_simps => fn gen_size_map_thms =>
blanchet@56638
   221
          let val qualify = Binding.qualify true (Long_Name.base_name T_name) in
blanchet@56638
   222
            Global_Theory.note_thmss ""
blanchet@56638
   223
              ([((qualify (Binding.name sizeN),
blanchet@56638
   224
                   [Simplifier.simp_add, Nitpick_Simps.add, Thm.declaration_attribute
blanchet@56638
   225
                      (fn thm => Context.mapping (Code.add_default_eqn thm) I)]),
blanchet@56638
   226
                 [(size_simps, [])]),
blanchet@56638
   227
                ((qualify (Binding.name size_mapN), []), [(gen_size_map_thms, [])])]
blanchet@56638
   228
               |> filter_out (forall (null o fst) o snd))
blanchet@56638
   229
          end)
blanchet@56638
   230
        T_names (map2 append gen_size_simpss spec_size_simpss) gen_size_map_thmss
blanchet@56638
   231
      ||> Spec_Rules.add_global Spec_Rules.Equational (gen_size_consts, gen_size_simps);
blanchet@56638
   232
  in
blanchet@56638
   233
    thy4
blanchet@56638
   234
    |> Data.map (fold2 (fn T_name => fn gen_size_name =>
blanchet@56638
   235
        Symtab.update_new (T_name, (gen_size_name, (gen_size_simps, flat gen_size_map_thmss))))
blanchet@56638
   236
      T_names gen_size_names)
blanchet@56638
   237
  end;
blanchet@56638
   238
blanchet@56638
   239
val _ = Theory.setup (fp_sugar_interpretation generate_size);
blanchet@56638
   240
blanchet@56638
   241
end;