src/Pure/Tools/codegen_func.ML
author haftmann
Tue Mar 20 08:27:20 2007 +0100 (2007-03-20)
changeset 22475 bd3378255cc8
parent 22462 2a93fb199302
child 22484 25dfebd7b4c8
permissions -rw-r--r--
adjusted definition of defining equation
haftmann@22023
     1
(*  Title:      Pure/Tools/codegen_func.ML
haftmann@22023
     2
    ID:         $Id$
haftmann@22023
     3
    Author:     Florian Haftmann, TU Muenchen
haftmann@22023
     4
haftmann@22185
     5
Basic handling of defining equations ("func"s) for code generator framework.
haftmann@22023
     6
*)
haftmann@22023
     7
haftmann@22023
     8
signature CODEGEN_FUNC =
haftmann@22023
     9
sig
haftmann@22185
    10
  val assert_rew: thm -> thm
haftmann@22033
    11
  val mk_rew: thm -> thm list
haftmann@22185
    12
  val assert_func: thm -> thm
haftmann@22033
    13
  val mk_func: thm -> (CodegenConsts.const * thm) list
haftmann@22185
    14
  val mk_head: thm -> CodegenConsts.const * thm
haftmann@22033
    15
  val dest_func: thm -> (string * typ) * term list
haftmann@22033
    16
  val typ_func: thm -> typ
haftmann@22185
    17
haftmann@22197
    18
  val inst_thm: sort Vartab.table -> thm -> thm
haftmann@22033
    19
  val expand_eta: int -> thm -> thm
haftmann@22033
    20
  val rewrite_func: thm list -> thm -> thm
haftmann@22211
    21
  val norm_args: thm list -> thm list 
haftmann@22211
    22
  val norm_varnames: (string -> string) -> (string -> string) -> thm list -> thm list 
haftmann@22023
    23
end;
haftmann@22023
    24
haftmann@22023
    25
structure CodegenFunc : CODEGEN_FUNC =
haftmann@22023
    26
struct
haftmann@22023
    27
haftmann@22033
    28
fun lift_thm_thy f thm = f (Thm.theory_of_thm thm) thm;
haftmann@22033
    29
haftmann@22033
    30
fun bad_thm msg thm =
haftmann@22033
    31
  error (msg ^ ": " ^ string_of_thm thm);
haftmann@22033
    32
haftmann@22033
    33
haftmann@22033
    34
(* making rewrite theorems *)
haftmann@22033
    35
haftmann@22185
    36
fun assert_rew thm =
haftmann@22033
    37
  let
haftmann@22033
    38
    val thy = Thm.theory_of_thm thm;
haftmann@22033
    39
    val (lhs, rhs) = (Logic.dest_equals o Thm.prop_of) thm;
haftmann@22033
    40
    fun vars_of t = fold_aterms
haftmann@22033
    41
     (fn Var (v, _) => insert (op =) v
haftmann@22033
    42
       | Free _ => bad_thm "Illegal free variable in rewrite theorem" thm
haftmann@22033
    43
       | _ => I) t [];
haftmann@22033
    44
    fun tvars_of t = fold_term_types
haftmann@22033
    45
     (fn _ => fold_atyps (fn TVar (v, _) => insert (op =) v
haftmann@22033
    46
                          | TFree _ => bad_thm "Illegal free type variable in rewrite theorem" thm)) t [];
haftmann@22033
    47
    val lhs_vs = vars_of lhs;
haftmann@22033
    48
    val rhs_vs = vars_of rhs;
haftmann@22033
    49
    val lhs_tvs = tvars_of lhs;
haftmann@22033
    50
    val rhs_tvs = tvars_of lhs;
haftmann@22033
    51
    val _ = if null (subtract (op =) lhs_vs rhs_vs)
haftmann@22033
    52
      then ()
haftmann@22033
    53
      else bad_thm "Free variables on right hand side of rewrite theorems" thm
haftmann@22033
    54
    val _ = if null (subtract (op =) lhs_tvs rhs_tvs)
haftmann@22033
    55
      then ()
haftmann@22033
    56
      else bad_thm "Free type variables on right hand side of rewrite theorems" thm
haftmann@22033
    57
  in thm end;
haftmann@22033
    58
haftmann@22033
    59
fun mk_rew thm =
haftmann@22023
    60
  let
haftmann@22033
    61
    val thy = Thm.theory_of_thm thm;
haftmann@22033
    62
    val thms = (#mk o #mk_rews o snd o MetaSimplifier.rep_ss o Simplifier.simpset_of) thy thm;
haftmann@22033
    63
  in
haftmann@22185
    64
    map assert_rew thms
haftmann@22033
    65
  end;
haftmann@22033
    66
haftmann@22033
    67
haftmann@22197
    68
(* making defining equations *)
haftmann@22033
    69
haftmann@22033
    70
val typ_func = lift_thm_thy (fn thy => snd o dest_Const o fst o strip_comb
haftmann@22033
    71
  o fst o Logic.dest_equals o ObjectLogic.drop_judgment thy o Drule.plain_prop_of);
haftmann@22033
    72
haftmann@22033
    73
val dest_func = lift_thm_thy (fn thy => apfst dest_Const o strip_comb
haftmann@22033
    74
  o fst o Logic.dest_equals o ObjectLogic.drop_judgment thy o Drule.plain_prop_of
haftmann@22033
    75
  o Drule.fconv_rule Drule.beta_eta_conversion);
haftmann@22033
    76
haftmann@22033
    77
val mk_head = lift_thm_thy (fn thy => fn thm =>
haftmann@22033
    78
  ((CodegenConsts.norm_of_typ thy o fst o dest_func) thm, thm));
haftmann@22023
    79
haftmann@22185
    80
fun assert_func thm = case try dest_func thm
haftmann@22033
    81
 of SOME (c_ty as (c, ty), args) =>
haftmann@22033
    82
      let
haftmann@22033
    83
        val thy = Thm.theory_of_thm thm;
haftmann@22033
    84
        val _ =
haftmann@22033
    85
          if has_duplicates (op =)
haftmann@22033
    86
            ((fold o fold_aterms) (fn Var (v, _) => cons v
haftmann@22033
    87
              | _ => I
haftmann@22033
    88
            ) args [])
haftmann@22197
    89
          then bad_thm "Repeated variables on left hand side of defining equation" thm
haftmann@22033
    90
          else ()
haftmann@22462
    91
        fun check _ (Abs _) = bad_thm
haftmann@22462
    92
              "Abstraction on left hand side of defining equation" thm
haftmann@22475
    93
          | check 0 (Var _) = ()
haftmann@22475
    94
          | check _ (Var _) = bad_thm
haftmann@22462
    95
              "Variable with application on left hand side of defining equation" thm
haftmann@22475
    96
          | check n (t1 $ t2) = (check (n+1) t1; check 0 t2)
haftmann@22475
    97
          | check n (Const (_, ty)) = if n <> (length o fst o strip_type) ty
haftmann@22475
    98
              then bad_thm
haftmann@22475
    99
                ("Partially applied constant on left hand side of defining equation") thm
haftmann@22475
   100
              else ();
haftmann@22475
   101
        val _ = map (check 0) args;
haftmann@22185
   102
      in thm end
haftmann@22197
   103
  | NONE => bad_thm "Not a defining equation" thm;
haftmann@22023
   104
haftmann@22185
   105
val mk_func = map (mk_head o assert_func) o mk_rew;
haftmann@22033
   106
haftmann@22033
   107
haftmann@22033
   108
(* utilities *)
haftmann@22033
   109
haftmann@22197
   110
fun inst_thm tvars' thm =
haftmann@22197
   111
  let
haftmann@22197
   112
    val thy = Thm.theory_of_thm thm;
haftmann@22197
   113
    val tvars = (Term.add_tvars o Thm.prop_of) thm [];
haftmann@22197
   114
    fun mk_inst (tvar as (v, _)) = case Vartab.lookup tvars' v
haftmann@22197
   115
     of SOME sort => SOME (pairself (Thm.ctyp_of thy o TVar) (tvar, (v, sort)))
haftmann@22197
   116
      | NONE => NONE;
haftmann@22197
   117
    val insts = map_filter mk_inst tvars;
haftmann@22197
   118
  in Thm.instantiate (insts, []) thm end;
haftmann@22197
   119
haftmann@22033
   120
fun expand_eta k thm =
haftmann@22033
   121
  let
haftmann@22033
   122
    val thy = Thm.theory_of_thm thm;
haftmann@22023
   123
    val (lhs, rhs) = (Logic.dest_equals o Drule.plain_prop_of) thm;
haftmann@22023
   124
    val (head, args) = strip_comb lhs;
haftmann@22023
   125
    val l = if k = ~1
haftmann@22023
   126
      then (length o fst o strip_abs) rhs
haftmann@22023
   127
      else Int.max (0, k - length args);
haftmann@22023
   128
    val used = Name.make_context (map (fst o fst) (Term.add_vars lhs []));
haftmann@22023
   129
    fun get_name _ 0 used = ([], used)
haftmann@22023
   130
      | get_name (Abs (v, ty, t)) k used =
haftmann@22023
   131
          used
haftmann@22033
   132
          |> Name.variants [v]
haftmann@22023
   133
          ||>> get_name t (k - 1)
haftmann@22023
   134
          |>> (fn ([v'], vs') => (v', ty) :: vs')
haftmann@22023
   135
      | get_name t k used = 
haftmann@22023
   136
          let
haftmann@22023
   137
            val (tys, _) = (strip_type o fastype_of) t
haftmann@22023
   138
          in case tys
haftmann@22023
   139
           of [] => raise TERM ("expand_eta", [t])
haftmann@22023
   140
            | ty :: _ =>
haftmann@22023
   141
                used
haftmann@22023
   142
                |> Name.variants [""]
haftmann@22023
   143
                |-> (fn [v] => get_name (t $ Var ((v, 0), ty)) (k - 1)
haftmann@22023
   144
                #>> (fn vs' => (v, ty) :: vs'))
haftmann@22023
   145
          end;
haftmann@22023
   146
    val (vs, _) = get_name rhs l used;
haftmann@22023
   147
    val vs_refl = map (fn (v, ty) => Thm.reflexive (Thm.cterm_of thy (Var ((v, 0), ty)))) vs;
haftmann@22023
   148
  in
haftmann@22023
   149
    fold (fn refl => fn thm => Thm.combination thm refl) vs_refl thm
haftmann@22023
   150
  end;
haftmann@22023
   151
haftmann@22033
   152
fun rewrite_func rewrites thm =
haftmann@22033
   153
  let
haftmann@22033
   154
    val rewrite = MetaSimplifier.rewrite false rewrites;
haftmann@22033
   155
    val (ct_eq, [ct_lhs, ct_rhs]) = (Drule.strip_comb o Thm.cprop_of) thm;
haftmann@22033
   156
    val Const ("==", _) = Thm.term_of ct_eq;
haftmann@22033
   157
    val (ct_f, ct_args) = Drule.strip_comb ct_lhs;
haftmann@22033
   158
    val rhs' = rewrite ct_rhs;
haftmann@22033
   159
    val args' = map rewrite ct_args;
haftmann@22033
   160
    val lhs' = Thm.symmetric (fold (fn th1 => fn th2 => Thm.combination th2 th1)
haftmann@22033
   161
      args' (Thm.reflexive ct_f));
haftmann@22197
   162
  in Thm.transitive (Thm.transitive lhs' thm) rhs' end;
haftmann@22033
   163
haftmann@22211
   164
fun norm_args thms =
haftmann@22211
   165
  let
haftmann@22211
   166
    val num_args_of = length o snd o strip_comb o fst o Logic.dest_equals;
haftmann@22211
   167
    val k = fold (curry Int.max o num_args_of o Drule.plain_prop_of) thms 0;
haftmann@22211
   168
  in
haftmann@22211
   169
    thms
haftmann@22211
   170
    |> map (expand_eta k)
haftmann@22211
   171
    |> map (Drule.fconv_rule Drule.beta_eta_conversion)
haftmann@22211
   172
  end;
haftmann@22211
   173
haftmann@22211
   174
fun canonical_tvars purify_tvar thm =
haftmann@22211
   175
  let
haftmann@22211
   176
    val ctyp = Thm.ctyp_of (Thm.theory_of_thm thm);
haftmann@22211
   177
    fun tvars_subst_for thm = (fold_types o fold_atyps)
haftmann@22211
   178
      (fn TVar (v_i as (v, _), sort) => let
haftmann@22211
   179
            val v' = purify_tvar v
haftmann@22211
   180
          in if v = v' then I
haftmann@22211
   181
          else insert (op =) (v_i, (v', sort)) end
haftmann@22211
   182
        | _ => I) (prop_of thm) [];
haftmann@22211
   183
    fun mk_inst (v_i, (v', sort)) (maxidx, acc) =
haftmann@22211
   184
      let
haftmann@22211
   185
        val ty = TVar (v_i, sort)
haftmann@22211
   186
      in
haftmann@22211
   187
        (maxidx + 1, (ctyp ty, ctyp (TVar ((v', maxidx), sort))) :: acc)
haftmann@22211
   188
      end;
haftmann@22211
   189
    val maxidx = Thm.maxidx_of thm + 1;
haftmann@22211
   190
    val (_, inst) = fold mk_inst (tvars_subst_for thm) (maxidx + 1, []);
haftmann@22211
   191
  in Thm.instantiate (inst, []) thm end;
haftmann@22211
   192
haftmann@22211
   193
fun canonical_vars purify_var thm =
haftmann@22211
   194
  let
haftmann@22211
   195
    val cterm = Thm.cterm_of (Thm.theory_of_thm thm);
haftmann@22211
   196
    fun vars_subst_for thm = fold_aterms
haftmann@22211
   197
      (fn Var (v_i as (v, _), ty) => let
haftmann@22211
   198
            val v' = purify_var v
haftmann@22211
   199
          in if v = v' then I
haftmann@22211
   200
          else insert (op =) (v_i, (v', ty)) end
haftmann@22211
   201
        | _ => I) (prop_of thm) [];
haftmann@22211
   202
    fun mk_inst (v_i as (v, i), (v', ty)) (maxidx, acc) =
haftmann@22211
   203
      let
haftmann@22211
   204
        val t = Var (v_i, ty)
haftmann@22211
   205
      in
haftmann@22211
   206
        (maxidx + 1, (cterm t, cterm (Var ((v', maxidx), ty))) :: acc)
haftmann@22211
   207
      end;
haftmann@22211
   208
    val maxidx = Thm.maxidx_of thm + 1;
haftmann@22211
   209
    val (_, inst) = fold mk_inst (vars_subst_for thm) (maxidx + 1, []);
haftmann@22211
   210
  in Thm.instantiate ([], inst) thm end;
haftmann@22211
   211
haftmann@22211
   212
fun canonical_absvars purify_var thm =
haftmann@22211
   213
  let
haftmann@22211
   214
    val t = Thm.prop_of thm;
haftmann@22211
   215
    val t' = Term.map_abs_vars purify_var t;
haftmann@22211
   216
  in Thm.rename_boundvars t t' thm end;
haftmann@22211
   217
haftmann@22211
   218
fun norm_varnames purify_tvar purify_var thms =
haftmann@22211
   219
  let
haftmann@22211
   220
    fun burrow_thms f [] = []
haftmann@22211
   221
      | burrow_thms f thms =
haftmann@22211
   222
          thms
haftmann@22211
   223
          |> Conjunction.intr_list
haftmann@22211
   224
          |> f
haftmann@22211
   225
          |> Conjunction.elim_list;
haftmann@22211
   226
  in
haftmann@22211
   227
    thms
haftmann@22211
   228
    |> burrow_thms (canonical_tvars purify_tvar)
haftmann@22211
   229
    |> map (canonical_vars purify_var)
haftmann@22211
   230
    |> map (canonical_absvars purify_var)
haftmann@22211
   231
    |> map Drule.zero_var_indexes
haftmann@22211
   232
  end;
haftmann@22211
   233
haftmann@22023
   234
end;