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