src/HOL/Code_Setup.thy
author huffman
Wed Apr 22 11:00:25 2009 -0700 (2009-04-22)
changeset 31006 644d18da3c77
parent 30549 d2d7874648bd
permissions -rw-r--r--
add module signature to domain_library.ML
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:
haftmann@28400
    81
  assumes "CASE \<equiv> (\<lambda>b. If b f g)"
wenzelm@28856
    82
  shows "(CASE True \<equiv> f) &&& (CASE False \<equiv> g)"
haftmann@28400
    83
  using assms by simp_all
haftmann@28400
    84
haftmann@28400
    85
setup {*
haftmann@28400
    86
  Code.add_case @{thm Let_case_cert}
haftmann@28400
    87
  #> Code.add_case @{thm If_case_cert}
haftmann@28400
    88
  #> Code.add_undefined @{const_name undefined}
haftmann@28400
    89
*}
haftmann@28400
    90
haftmann@28400
    91
code_abort undefined
haftmann@28400
    92
haftmann@28400
    93
haftmann@28400
    94
subsection {* Generic code generator preprocessor *}
haftmann@28400
    95
haftmann@28400
    96
setup {*
haftmann@28400
    97
  Code.map_pre (K HOL_basic_ss)
haftmann@28400
    98
  #> Code.map_post (K HOL_basic_ss)
haftmann@28400
    99
*}
haftmann@28400
   100
haftmann@24285
   101
haftmann@28400
   102
subsection {* Generic code generator target languages *}
haftmann@28400
   103
haftmann@28400
   104
text {* type bool *}
haftmann@28400
   105
haftmann@28400
   106
code_type bool
haftmann@28400
   107
  (SML "bool")
haftmann@28400
   108
  (OCaml "bool")
haftmann@28400
   109
  (Haskell "Bool")
haftmann@28400
   110
haftmann@28400
   111
code_const True and False and Not and "op &" and "op |" and If
haftmann@28400
   112
  (SML "true" and "false" and "not"
haftmann@28400
   113
    and infixl 1 "andalso" and infixl 0 "orelse"
haftmann@28400
   114
    and "!(if (_)/ then (_)/ else (_))")
haftmann@28400
   115
  (OCaml "true" and "false" and "not"
haftmann@28400
   116
    and infixl 4 "&&" and infixl 2 "||"
haftmann@28400
   117
    and "!(if (_)/ then (_)/ else (_))")
haftmann@28400
   118
  (Haskell "True" and "False" and "not"
haftmann@28400
   119
    and infixl 3 "&&" and infixl 2 "||"
haftmann@28400
   120
    and "!(if (_)/ then (_)/ else (_))")
haftmann@28400
   121
haftmann@28400
   122
code_reserved SML
haftmann@28400
   123
  bool true false not
haftmann@28400
   124
haftmann@28400
   125
code_reserved OCaml
haftmann@28400
   126
  bool not
haftmann@28400
   127
haftmann@28400
   128
text {* using built-in Haskell equality *}
haftmann@28400
   129
haftmann@28400
   130
code_class eq
haftmann@28687
   131
  (Haskell "Eq")
haftmann@28400
   132
haftmann@28400
   133
code_const "eq_class.eq"
haftmann@28400
   134
  (Haskell infixl 4 "==")
haftmann@28400
   135
haftmann@28400
   136
code_const "op ="
haftmann@28400
   137
  (Haskell infixl 4 "==")
haftmann@28400
   138
haftmann@28400
   139
text {* undefined *}
haftmann@28400
   140
haftmann@28400
   141
code_const undefined
haftmann@28512
   142
  (SML "!(raise/ Fail/ \"undefined\")")
haftmann@28400
   143
  (OCaml "failwith/ \"undefined\"")
haftmann@28400
   144
  (Haskell "error/ \"undefined\"")
haftmann@28400
   145
haftmann@28400
   146
haftmann@28400
   147
subsection {* SML code generator setup *}
haftmann@24285
   148
haftmann@24285
   149
types_code
haftmann@24285
   150
  "bool"  ("bool")
haftmann@24285
   151
attach (term_of) {*
haftmann@24285
   152
fun term_of_bool b = if b then HOLogic.true_const else HOLogic.false_const;
haftmann@24285
   153
*}
haftmann@24285
   154
attach (test) {*
berghofe@25885
   155
fun gen_bool i =
berghofe@25885
   156
  let val b = one_of [false, true]
berghofe@25885
   157
  in (b, fn () => term_of_bool b) end;
haftmann@24285
   158
*}
haftmann@24285
   159
  "prop"  ("bool")
haftmann@24285
   160
attach (term_of) {*
haftmann@24285
   161
fun term_of_prop b =
haftmann@24285
   162
  HOLogic.mk_Trueprop (if b then HOLogic.true_const else HOLogic.false_const);
haftmann@24285
   163
*}
haftmann@24285
   164
haftmann@24285
   165
consts_code
haftmann@24285
   166
  "Trueprop" ("(_)")
haftmann@24285
   167
  "True"    ("true")
haftmann@24285
   168
  "False"   ("false")
haftmann@24285
   169
  "Not"     ("Bool.not")
haftmann@24285
   170
  "op |"    ("(_ orelse/ _)")
haftmann@24285
   171
  "op &"    ("(_ andalso/ _)")
haftmann@24285
   172
  "If"      ("(if _/ then _/ else _)")
haftmann@24285
   173
haftmann@24285
   174
setup {*
haftmann@24285
   175
let
haftmann@24285
   176
haftmann@28537
   177
fun eq_codegen thy defs dep thyname b t gr =
haftmann@24285
   178
    (case strip_comb t of
haftmann@24285
   179
       (Const ("op =", Type (_, [Type ("fun", _), _])), _) => NONE
haftmann@24285
   180
     | (Const ("op =", _), [t, u]) =>
haftmann@24285
   181
          let
haftmann@28537
   182
            val (pt, gr') = Codegen.invoke_codegen thy defs dep thyname false t gr;
haftmann@28537
   183
            val (pu, gr'') = Codegen.invoke_codegen thy defs dep thyname false u gr';
haftmann@28537
   184
            val (_, gr''') = Codegen.invoke_tycodegen thy defs dep thyname false HOLogic.boolT gr'';
haftmann@24285
   185
          in
haftmann@28537
   186
            SOME (Codegen.parens
haftmann@28537
   187
              (Pretty.block [pt, Codegen.str " =", Pretty.brk 1, pu]), gr''')
haftmann@24285
   188
          end
haftmann@24285
   189
     | (t as Const ("op =", _), ts) => SOME (Codegen.invoke_codegen
haftmann@28537
   190
         thy defs dep thyname b (Codegen.eta_expand t ts 2) gr)
haftmann@24285
   191
     | _ => NONE);
haftmann@24285
   192
haftmann@24285
   193
in
haftmann@24285
   194
  Codegen.add_codegen "eq_codegen" eq_codegen
haftmann@24285
   195
end
haftmann@24285
   196
*}
haftmann@24285
   197
berghofe@24463
   198
haftmann@28400
   199
subsection {* Evaluation and normalization by evaluation *}
haftmann@24285
   200
haftmann@29105
   201
setup {*
haftmann@29105
   202
  Value.add_evaluator ("SML", Codegen.eval_term o ProofContext.theory_of)
haftmann@29105
   203
*}
haftmann@29105
   204
haftmann@27103
   205
ML {*
haftmann@27103
   206
structure Eval_Method =
haftmann@27103
   207
struct
haftmann@27103
   208
haftmann@27103
   209
val eval_ref : (unit -> bool) option ref = ref NONE;
haftmann@27103
   210
haftmann@27103
   211
end;
haftmann@27103
   212
*}
haftmann@27103
   213
wenzelm@28290
   214
oracle eval_oracle = {* fn ct =>
wenzelm@28290
   215
  let
wenzelm@28290
   216
    val thy = Thm.theory_of_cterm ct;
wenzelm@28290
   217
    val t = Thm.term_of ct;
haftmann@28740
   218
    val dummy = @{cprop True};
haftmann@28740
   219
  in case try HOLogic.dest_Trueprop t
haftmann@28740
   220
   of SOME t' => if Code_ML.eval_term
haftmann@28740
   221
         ("Eval_Method.eval_ref", Eval_Method.eval_ref) thy t' [] 
haftmann@28740
   222
       then Thm.capply (Thm.capply @{cterm "op \<equiv> \<Colon> prop \<Rightarrow> prop \<Rightarrow> prop"} ct) dummy
haftmann@28740
   223
       else dummy
haftmann@28740
   224
    | NONE => dummy
wenzelm@28290
   225
  end
haftmann@24285
   226
*}
haftmann@24285
   227
haftmann@28740
   228
ML {*
wenzelm@30549
   229
fun gen_eval_method conv ctxt = SIMPLE_METHOD'
haftmann@28740
   230
  (CONVERSION (Conv.params_conv (~1) (K (Conv.concl_conv (~1) conv)) ctxt)
wenzelm@30549
   231
    THEN' rtac TrueI)
haftmann@28740
   232
*}
haftmann@24285
   233
wenzelm@30549
   234
method_setup eval = {* Scan.succeed (gen_eval_method eval_oracle) *}
haftmann@28740
   235
  "solve goal by evaluation"
haftmann@24285
   236
wenzelm@30549
   237
method_setup evaluation = {* Scan.succeed (gen_eval_method Codegen.evaluation_conv) *}
haftmann@28740
   238
  "solve goal by evaluation"
haftmann@28740
   239
wenzelm@30549
   240
method_setup normalization = {*
wenzelm@30549
   241
  Scan.succeed (K (SIMPLE_METHOD' (CONVERSION Nbe.norm_conv THEN' (fn k => TRY (rtac TrueI k)))))
haftmann@24285
   242
*} "solve goal by normalization"
haftmann@24285
   243
haftmann@28400
   244
haftmann@28400
   245
subsection {* Quickcheck *}
haftmann@28400
   246
haftmann@29105
   247
setup {*
haftmann@29105
   248
  Quickcheck.add_generator ("SML", Codegen.test_term)
haftmann@29105
   249
*}
haftmann@29105
   250
haftmann@28400
   251
quickcheck_params [size = 5, iterations = 50]
haftmann@28400
   252
haftmann@24285
   253
end