src/HOL/Code_Setup.thy
author haftmann
Thu Nov 13 15:58:37 2008 +0100 (2008-11-13)
changeset 28740 22a8125d66fa
parent 28699 32b6a8f12c1c
child 28856 5e009a80fe6d
permissions -rw-r--r--
improved handling of !!/==> for eval and normalization
haftmann@24285
     1
(*  Title:      HOL/Code_Setup.thy
haftmann@24285
     2
    ID:         $Id$
haftmann@24285
     3
    Author:     Florian Haftmann
haftmann@24285
     4
*)
haftmann@24285
     5
haftmann@28400
     6
header {* Setup of code generators and related tools *}
haftmann@24285
     7
haftmann@24285
     8
theory Code_Setup
haftmann@24285
     9
imports HOL
haftmann@28400
    10
begin
haftmann@28400
    11
haftmann@28400
    12
subsection {* Generic code generator foundation *}
haftmann@28400
    13
haftmann@28400
    14
text {* Datatypes *}
haftmann@28400
    15
haftmann@28400
    16
code_datatype True False
haftmann@28400
    17
haftmann@28400
    18
code_datatype "TYPE('a\<Colon>{})"
haftmann@28400
    19
haftmann@28400
    20
code_datatype Trueprop "prop"
haftmann@28400
    21
haftmann@28400
    22
text {* Code equations *}
haftmann@28400
    23
haftmann@28562
    24
lemma [code]:
haftmann@28740
    25
  shows "(True \<Longrightarrow> PROP P) \<equiv> PROP P" 
haftmann@28740
    26
    and "(False \<Longrightarrow> Q) \<equiv> Trueprop True" 
haftmann@28740
    27
    and "(PROP P \<Longrightarrow> True) \<equiv> Trueprop True" 
haftmann@28740
    28
    and "(Q \<Longrightarrow> False) \<equiv> Trueprop (\<not> Q)" by (auto intro!: equal_intr_rule)
haftmann@28740
    29
haftmann@28740
    30
lemma [code]:
haftmann@28400
    31
  shows "False \<and> x \<longleftrightarrow> False"
haftmann@28400
    32
    and "True \<and> x \<longleftrightarrow> x"
haftmann@28400
    33
    and "x \<and> False \<longleftrightarrow> False"
haftmann@28400
    34
    and "x \<and> True \<longleftrightarrow> x" by simp_all
haftmann@28400
    35
haftmann@28562
    36
lemma [code]:
haftmann@28400
    37
  shows "False \<or> x \<longleftrightarrow> x"
haftmann@28400
    38
    and "True \<or> x \<longleftrightarrow> True"
haftmann@28400
    39
    and "x \<or> False \<longleftrightarrow> x"
haftmann@28400
    40
    and "x \<or> True \<longleftrightarrow> True" by simp_all
haftmann@28400
    41
haftmann@28562
    42
lemma [code]:
haftmann@28400
    43
  shows "\<not> True \<longleftrightarrow> False"
haftmann@28400
    44
    and "\<not> False \<longleftrightarrow> True" by (rule HOL.simp_thms)+
haftmann@28400
    45
haftmann@28562
    46
lemmas [code] = Let_def if_True if_False
haftmann@28400
    47
haftmann@28562
    48
lemmas [code, code unfold, symmetric, code post] = imp_conv_disj
haftmann@28400
    49
haftmann@28400
    50
text {* Equality *}
haftmann@28400
    51
haftmann@28400
    52
context eq
haftmann@24285
    53
begin
haftmann@24285
    54
haftmann@28562
    55
lemma equals_eq [code inline, code]: "op = \<equiv> eq"
haftmann@28400
    56
  by (rule eq_reflection) (rule ext, rule ext, rule sym, rule eq_equals)
haftmann@28400
    57
haftmann@28512
    58
declare eq [code unfold, code inline del]
haftmann@28512
    59
haftmann@28400
    60
declare equals_eq [symmetric, code post]
haftmann@28400
    61
haftmann@28400
    62
end
haftmann@28400
    63
haftmann@28400
    64
declare simp_thms(6) [code nbe]
haftmann@28400
    65
haftmann@28400
    66
hide (open) const eq
haftmann@28400
    67
hide const eq
haftmann@28400
    68
haftmann@28400
    69
setup {*
haftmann@28400
    70
  Code_Unit.add_const_alias @{thm equals_eq}
haftmann@28400
    71
*}
haftmann@28400
    72
haftmann@28400
    73
text {* Cases *}
haftmann@28400
    74
haftmann@28400
    75
lemma Let_case_cert:
haftmann@28400
    76
  assumes "CASE \<equiv> (\<lambda>x. Let x f)"
haftmann@28400
    77
  shows "CASE x \<equiv> f x"
haftmann@28400
    78
  using assms by simp_all
haftmann@28400
    79
haftmann@28400
    80
lemma If_case_cert:
ballarin@28699
    81
  fixes meta_conjunction :: "prop => prop => prop"  (infixr "&&" 2)
haftmann@28400
    82
  assumes "CASE \<equiv> (\<lambda>b. If b f g)"
haftmann@28400
    83
  shows "(CASE True \<equiv> f) && (CASE False \<equiv> g)"
haftmann@28400
    84
  using assms by simp_all
haftmann@28400
    85
haftmann@28400
    86
setup {*
haftmann@28400
    87
  Code.add_case @{thm Let_case_cert}
haftmann@28400
    88
  #> Code.add_case @{thm If_case_cert}
haftmann@28400
    89
  #> Code.add_undefined @{const_name undefined}
haftmann@28400
    90
*}
haftmann@28400
    91
haftmann@28400
    92
code_abort undefined
haftmann@28400
    93
haftmann@28400
    94
haftmann@28400
    95
subsection {* Generic code generator preprocessor *}
haftmann@28400
    96
haftmann@28400
    97
setup {*
haftmann@28400
    98
  Code.map_pre (K HOL_basic_ss)
haftmann@28400
    99
  #> Code.map_post (K HOL_basic_ss)
haftmann@28400
   100
*}
haftmann@28400
   101
haftmann@24285
   102
haftmann@28400
   103
subsection {* Generic code generator target languages *}
haftmann@28400
   104
haftmann@28400
   105
text {* type bool *}
haftmann@28400
   106
haftmann@28400
   107
code_type bool
haftmann@28400
   108
  (SML "bool")
haftmann@28400
   109
  (OCaml "bool")
haftmann@28400
   110
  (Haskell "Bool")
haftmann@28400
   111
haftmann@28400
   112
code_const True and False and Not and "op &" and "op |" and If
haftmann@28400
   113
  (SML "true" and "false" and "not"
haftmann@28400
   114
    and infixl 1 "andalso" and infixl 0 "orelse"
haftmann@28400
   115
    and "!(if (_)/ then (_)/ else (_))")
haftmann@28400
   116
  (OCaml "true" and "false" and "not"
haftmann@28400
   117
    and infixl 4 "&&" and infixl 2 "||"
haftmann@28400
   118
    and "!(if (_)/ then (_)/ else (_))")
haftmann@28400
   119
  (Haskell "True" and "False" and "not"
haftmann@28400
   120
    and infixl 3 "&&" and infixl 2 "||"
haftmann@28400
   121
    and "!(if (_)/ then (_)/ else (_))")
haftmann@28400
   122
haftmann@28400
   123
code_reserved SML
haftmann@28400
   124
  bool true false not
haftmann@28400
   125
haftmann@28400
   126
code_reserved OCaml
haftmann@28400
   127
  bool not
haftmann@28400
   128
haftmann@28400
   129
text {* using built-in Haskell equality *}
haftmann@28400
   130
haftmann@28400
   131
code_class eq
haftmann@28687
   132
  (Haskell "Eq")
haftmann@28400
   133
haftmann@28400
   134
code_const "eq_class.eq"
haftmann@28400
   135
  (Haskell infixl 4 "==")
haftmann@28400
   136
haftmann@28400
   137
code_const "op ="
haftmann@28400
   138
  (Haskell infixl 4 "==")
haftmann@28400
   139
haftmann@28400
   140
text {* undefined *}
haftmann@28400
   141
haftmann@28400
   142
code_const undefined
haftmann@28512
   143
  (SML "!(raise/ Fail/ \"undefined\")")
haftmann@28400
   144
  (OCaml "failwith/ \"undefined\"")
haftmann@28400
   145
  (Haskell "error/ \"undefined\"")
haftmann@28400
   146
haftmann@28400
   147
haftmann@28400
   148
subsection {* SML code generator setup *}
haftmann@24285
   149
haftmann@24285
   150
types_code
haftmann@24285
   151
  "bool"  ("bool")
haftmann@24285
   152
attach (term_of) {*
haftmann@24285
   153
fun term_of_bool b = if b then HOLogic.true_const else HOLogic.false_const;
haftmann@24285
   154
*}
haftmann@24285
   155
attach (test) {*
berghofe@25885
   156
fun gen_bool i =
berghofe@25885
   157
  let val b = one_of [false, true]
berghofe@25885
   158
  in (b, fn () => term_of_bool b) end;
haftmann@24285
   159
*}
haftmann@24285
   160
  "prop"  ("bool")
haftmann@24285
   161
attach (term_of) {*
haftmann@24285
   162
fun term_of_prop b =
haftmann@24285
   163
  HOLogic.mk_Trueprop (if b then HOLogic.true_const else HOLogic.false_const);
haftmann@24285
   164
*}
haftmann@24285
   165
haftmann@24285
   166
consts_code
haftmann@24285
   167
  "Trueprop" ("(_)")
haftmann@24285
   168
  "True"    ("true")
haftmann@24285
   169
  "False"   ("false")
haftmann@24285
   170
  "Not"     ("Bool.not")
haftmann@24285
   171
  "op |"    ("(_ orelse/ _)")
haftmann@24285
   172
  "op &"    ("(_ andalso/ _)")
haftmann@24285
   173
  "If"      ("(if _/ then _/ else _)")
haftmann@24285
   174
haftmann@24285
   175
setup {*
haftmann@24285
   176
let
haftmann@24285
   177
haftmann@28537
   178
fun eq_codegen thy defs dep thyname b t gr =
haftmann@24285
   179
    (case strip_comb t of
haftmann@24285
   180
       (Const ("op =", Type (_, [Type ("fun", _), _])), _) => NONE
haftmann@24285
   181
     | (Const ("op =", _), [t, u]) =>
haftmann@24285
   182
          let
haftmann@28537
   183
            val (pt, gr') = Codegen.invoke_codegen thy defs dep thyname false t gr;
haftmann@28537
   184
            val (pu, gr'') = Codegen.invoke_codegen thy defs dep thyname false u gr';
haftmann@28537
   185
            val (_, gr''') = Codegen.invoke_tycodegen thy defs dep thyname false HOLogic.boolT gr'';
haftmann@24285
   186
          in
haftmann@28537
   187
            SOME (Codegen.parens
haftmann@28537
   188
              (Pretty.block [pt, Codegen.str " =", Pretty.brk 1, pu]), gr''')
haftmann@24285
   189
          end
haftmann@24285
   190
     | (t as Const ("op =", _), ts) => SOME (Codegen.invoke_codegen
haftmann@28537
   191
         thy defs dep thyname b (Codegen.eta_expand t ts 2) gr)
haftmann@24285
   192
     | _ => NONE);
haftmann@24285
   193
haftmann@24285
   194
in
haftmann@24285
   195
  Codegen.add_codegen "eq_codegen" eq_codegen
haftmann@24285
   196
end
haftmann@24285
   197
*}
haftmann@24285
   198
berghofe@24463
   199
haftmann@28400
   200
subsection {* Evaluation and normalization by evaluation *}
haftmann@24285
   201
haftmann@27103
   202
ML {*
haftmann@27103
   203
structure Eval_Method =
haftmann@27103
   204
struct
haftmann@27103
   205
haftmann@27103
   206
val eval_ref : (unit -> bool) option ref = ref NONE;
haftmann@27103
   207
haftmann@27103
   208
end;
haftmann@27103
   209
*}
haftmann@27103
   210
wenzelm@28290
   211
oracle eval_oracle = {* fn ct =>
wenzelm@28290
   212
  let
wenzelm@28290
   213
    val thy = Thm.theory_of_cterm ct;
wenzelm@28290
   214
    val t = Thm.term_of ct;
haftmann@28740
   215
    val dummy = @{cprop True};
haftmann@28740
   216
  in case try HOLogic.dest_Trueprop t
haftmann@28740
   217
   of SOME t' => if Code_ML.eval_term
haftmann@28740
   218
         ("Eval_Method.eval_ref", Eval_Method.eval_ref) thy t' [] 
haftmann@28740
   219
       then Thm.capply (Thm.capply @{cterm "op \<equiv> \<Colon> prop \<Rightarrow> prop \<Rightarrow> prop"} ct) dummy
haftmann@28740
   220
       else dummy
haftmann@28740
   221
    | NONE => dummy
wenzelm@28290
   222
  end
haftmann@24285
   223
*}
haftmann@24285
   224
haftmann@28740
   225
ML {*
haftmann@28740
   226
fun gen_eval_method conv = Method.ctxt_args (fn ctxt => Method.SIMPLE_METHOD'
haftmann@28740
   227
  (CONVERSION (Conv.params_conv (~1) (K (Conv.concl_conv (~1) conv)) ctxt)
haftmann@28740
   228
    THEN' rtac TrueI))
haftmann@28740
   229
*}
haftmann@24285
   230
haftmann@28740
   231
method_setup eval = {* gen_eval_method eval_oracle *}
haftmann@28740
   232
  "solve goal by evaluation"
haftmann@24285
   233
haftmann@28740
   234
method_setup evaluation = {* gen_eval_method Codegen.evaluation_conv *}
haftmann@28740
   235
  "solve goal by evaluation"
haftmann@28740
   236
haftmann@28740
   237
method_setup normalization = {* (Method.no_args o Method.SIMPLE_METHOD')
haftmann@28740
   238
  (CONVERSION Nbe.norm_conv THEN' (fn k => TRY (rtac TrueI k)))
haftmann@24285
   239
*} "solve goal by normalization"
haftmann@24285
   240
haftmann@28400
   241
haftmann@28400
   242
subsection {* Quickcheck *}
haftmann@28400
   243
haftmann@28400
   244
quickcheck_params [size = 5, iterations = 50]
haftmann@28400
   245
haftmann@24285
   246
end