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