src/HOL/Code_Generator.thy
author haftmann
Fri Apr 20 11:21:42 2007 +0200 (2007-04-20)
changeset 22744 5cbe966d67a2
parent 22499 68c8a8390e16
child 22758 a7790c8e3c14
permissions -rw-r--r--
Isar definitions are now added explicitly to code theorem table
haftmann@21046
     1
(*  ID:         $Id$
haftmann@21046
     2
    Author:     Florian Haftmann, TU Muenchen
haftmann@21046
     3
*)
haftmann@21046
     4
haftmann@21046
     5
header {* Setup of code generator tools *}
haftmann@21046
     6
haftmann@21046
     7
theory Code_Generator
haftmann@21046
     8
imports HOL
haftmann@21046
     9
begin
haftmann@21046
    10
haftmann@22385
    11
subsection {* SML code generator setup *}
haftmann@21046
    12
haftmann@21046
    13
types_code
haftmann@21046
    14
  "bool"  ("bool")
haftmann@21046
    15
attach (term_of) {*
haftmann@21046
    16
fun term_of_bool b = if b then HOLogic.true_const else HOLogic.false_const;
haftmann@21046
    17
*}
haftmann@21046
    18
attach (test) {*
haftmann@21046
    19
fun gen_bool i = one_of [false, true];
haftmann@21046
    20
*}
haftmann@21046
    21
  "prop"  ("bool")
haftmann@21046
    22
attach (term_of) {*
haftmann@21046
    23
fun term_of_prop b =
haftmann@21046
    24
  HOLogic.mk_Trueprop (if b then HOLogic.true_const else HOLogic.false_const);
haftmann@21046
    25
*}
haftmann@21046
    26
haftmann@21046
    27
consts_code
haftmann@21046
    28
  "Trueprop" ("(_)")
haftmann@21046
    29
  "True"    ("true")
haftmann@21046
    30
  "False"   ("false")
haftmann@21046
    31
  "Not"     ("not")
haftmann@21046
    32
  "op |"    ("(_ orelse/ _)")
haftmann@21046
    33
  "op &"    ("(_ andalso/ _)")
haftmann@21046
    34
  "HOL.If"      ("(if _/ then _/ else _)")
haftmann@21046
    35
haftmann@21046
    36
setup {*
haftmann@21046
    37
let
haftmann@21046
    38
haftmann@21046
    39
fun eq_codegen thy defs gr dep thyname b t =
haftmann@21046
    40
    (case strip_comb t of
haftmann@21046
    41
       (Const ("op =", Type (_, [Type ("fun", _), _])), _) => NONE
haftmann@21046
    42
     | (Const ("op =", _), [t, u]) =>
haftmann@21046
    43
          let
haftmann@21046
    44
            val (gr', pt) = Codegen.invoke_codegen thy defs dep thyname false (gr, t);
haftmann@21046
    45
            val (gr'', pu) = Codegen.invoke_codegen thy defs dep thyname false (gr', u);
haftmann@21046
    46
            val (gr''', _) = Codegen.invoke_tycodegen thy defs dep thyname false (gr'', HOLogic.boolT)
haftmann@21046
    47
          in
haftmann@21046
    48
            SOME (gr''', Codegen.parens
haftmann@21046
    49
              (Pretty.block [pt, Pretty.str " =", Pretty.brk 1, pu]))
haftmann@21046
    50
          end
haftmann@21046
    51
     | (t as Const ("op =", _), ts) => SOME (Codegen.invoke_codegen
haftmann@21046
    52
         thy defs dep thyname b (gr, Codegen.eta_expand t ts 2))
haftmann@21046
    53
     | _ => NONE);
haftmann@21046
    54
haftmann@21046
    55
in
haftmann@21046
    56
haftmann@21046
    57
Codegen.add_codegen "eq_codegen" eq_codegen
haftmann@21046
    58
haftmann@21046
    59
end
haftmann@21046
    60
*}
haftmann@21046
    61
haftmann@21046
    62
text {* Evaluation *}
haftmann@21046
    63
wenzelm@22099
    64
method_setup evaluation = {*
haftmann@21046
    65
let
haftmann@21046
    66
haftmann@21046
    67
fun evaluation_tac i = Tactical.PRIMITIVE (Drule.fconv_rule
haftmann@21046
    68
  (Drule.goals_conv (equal i) Codegen.evaluation_conv));
haftmann@21046
    69
wenzelm@22099
    70
in Method.no_args (Method.SIMPLE_METHOD' (evaluation_tac THEN' rtac TrueI)) end
wenzelm@22099
    71
*} "solve goal by evaluation"
haftmann@21046
    72
haftmann@21046
    73
haftmann@21046
    74
subsection {* Generic code generator setup *}
haftmann@21046
    75
haftmann@21904
    76
text {* operational equality for code generation *}
haftmann@21904
    77
haftmann@22473
    78
class eq (attach "op =") = type
haftmann@21904
    79
haftmann@21904
    80
haftmann@21904
    81
text {* equality for Haskell *}
haftmann@21904
    82
haftmann@21904
    83
code_class eq
haftmann@21904
    84
  (Haskell "Eq" where "op =" \<equiv> "(==)")
haftmann@21904
    85
haftmann@21904
    86
code_const "op ="
haftmann@21904
    87
  (Haskell infixl 4 "==")
haftmann@21904
    88
haftmann@21904
    89
haftmann@22423
    90
text {* type bool *}
haftmann@22423
    91
haftmann@22423
    92
code_datatype True False
haftmann@21904
    93
haftmann@21904
    94
lemma [code func]:
haftmann@21904
    95
  shows "(False \<and> x) = False"
haftmann@21904
    96
    and "(True \<and> x) = x"
haftmann@21904
    97
    and "(x \<and> False) = False"
haftmann@21904
    98
    and "(x \<and> True) = x" by simp_all
haftmann@21904
    99
haftmann@21904
   100
lemma [code func]:
haftmann@21904
   101
  shows "(False \<or> x) = x"
haftmann@21904
   102
    and "(True \<or> x) = True"
haftmann@21904
   103
    and "(x \<or> False) = x"
haftmann@21904
   104
    and "(x \<or> True) = True" by simp_all
haftmann@21904
   105
haftmann@21904
   106
lemma [code func]:
haftmann@21904
   107
  shows "(\<not> True) = False"
haftmann@21904
   108
    and "(\<not> False) = True" by (rule HOL.simp_thms)+
haftmann@21904
   109
haftmann@21904
   110
lemmas [code func] = imp_conv_disj
haftmann@21904
   111
haftmann@21904
   112
lemmas [code func] = if_True if_False
haftmann@21904
   113
haftmann@21904
   114
instance bool :: eq ..
haftmann@21904
   115
haftmann@21904
   116
lemma [code func]:
haftmann@21904
   117
  "True = P \<longleftrightarrow> P" by simp
haftmann@21904
   118
haftmann@21904
   119
lemma [code func]:
haftmann@21904
   120
  "False = P \<longleftrightarrow> \<not> P" by simp
haftmann@21904
   121
haftmann@21904
   122
lemma [code func]:
haftmann@21904
   123
  "P = True \<longleftrightarrow> P" by simp
haftmann@21904
   124
haftmann@21904
   125
lemma [code func]:
haftmann@21904
   126
  "P = False \<longleftrightarrow> \<not> P" by simp
haftmann@21904
   127
haftmann@21904
   128
code_type bool
haftmann@21904
   129
  (SML "bool")
haftmann@21904
   130
  (OCaml "bool")
haftmann@21904
   131
  (Haskell "Bool")
haftmann@21904
   132
haftmann@21904
   133
code_instance bool :: eq
haftmann@21904
   134
  (Haskell -)
haftmann@21904
   135
haftmann@21904
   136
code_const "op = \<Colon> bool \<Rightarrow> bool \<Rightarrow> bool"
haftmann@21904
   137
  (Haskell infixl 4 "==")
haftmann@21904
   138
haftmann@21904
   139
code_const True and False and Not and "op &" and "op |" and If
haftmann@21904
   140
  (SML "true" and "false" and "not"
haftmann@21904
   141
    and infixl 1 "andalso" and infixl 0 "orelse"
haftmann@21904
   142
    and "!(if (_)/ then (_)/ else (_))")
haftmann@21904
   143
  (OCaml "true" and "false" and "not"
haftmann@21904
   144
    and infixl 4 "&&" and infixl 2 "||"
haftmann@21904
   145
    and "!(if (_)/ then (_)/ else (_))")
haftmann@21904
   146
  (Haskell "True" and "False" and "not"
haftmann@21904
   147
    and infixl 3 "&&" and infixl 2 "||"
haftmann@21904
   148
    and "!(if (_)/ then (_)/ else (_))")
haftmann@21904
   149
haftmann@21904
   150
code_reserved SML
haftmann@21904
   151
  bool true false not
haftmann@21904
   152
haftmann@21904
   153
code_reserved OCaml
haftmann@21904
   154
  bool true false not
haftmann@21904
   155
haftmann@21904
   156
haftmann@22423
   157
text {* type prop *}
haftmann@22423
   158
haftmann@22423
   159
code_datatype Trueprop "prop"
haftmann@22423
   160
haftmann@22423
   161
haftmann@22423
   162
text {* type itself *}
haftmann@21046
   163
haftmann@22423
   164
code_datatype "TYPE('a)"
haftmann@22423
   165
haftmann@22423
   166
haftmann@22423
   167
text {* prevent unfolding of quantifier definitions *}
haftmann@22423
   168
haftmann@22423
   169
lemma [code func]:
haftmann@22423
   170
  "Ex = Ex"
haftmann@22423
   171
  "All = All"
haftmann@22423
   172
  by rule+
haftmann@21046
   173
haftmann@21046
   174
haftmann@22480
   175
text {* code generation for undefined as exception *}
haftmann@21046
   176
haftmann@22480
   177
code_const undefined
haftmann@22499
   178
  (SML "raise/ Fail/ \"undefined\"")
haftmann@22499
   179
  (OCaml "failwith/ \"undefined\"")
haftmann@22480
   180
  (Haskell "error/ \"undefined\"")
haftmann@21046
   181
haftmann@21079
   182
code_reserved SML Fail
haftmann@21904
   183
code_reserved OCaml failwith
haftmann@21046
   184
haftmann@21046
   185
haftmann@21378
   186
subsection {* Evaluation oracle *}
haftmann@21378
   187
krauss@22487
   188
oracle eval_oracle ("term") = {* fn thy => fn t => 
krauss@22487
   189
  if CodegenPackage.satisfies thy (HOLogic.dest_Trueprop t) [] 
krauss@22487
   190
  then t
krauss@22487
   191
  else HOLogic.Trueprop $ (HOLogic.true_const) (*dummy*)
haftmann@21869
   192
*}
haftmann@21378
   193
wenzelm@22099
   194
method_setup eval = {*
wenzelm@22099
   195
let
krauss@22487
   196
  fun eval_tac thy = 
krauss@22487
   197
    SUBGOAL (fn (t, i) => rtac (eval_oracle thy t) i)
krauss@22487
   198
in 
krauss@22487
   199
  Method.ctxt_args (fn ctxt => 
krauss@22487
   200
    Method.SIMPLE_METHOD' (eval_tac (ProofContext.theory_of ctxt)))
krauss@22487
   201
end
wenzelm@22099
   202
*} "solve goal by evaluation"
haftmann@21378
   203
haftmann@21378
   204
haftmann@21378
   205
subsection {* Normalization by evaluation *}
haftmann@21046
   206
wenzelm@22099
   207
method_setup normalization = {*
haftmann@21046
   208
let
haftmann@21046
   209
  fun normalization_tac i = Tactical.PRIMITIVE (Drule.fconv_rule
haftmann@21546
   210
    (Drule.goals_conv (equal i) (HOLogic.Trueprop_conv
haftmann@21149
   211
      NBE.normalization_conv)));
haftmann@21046
   212
in
wenzelm@22099
   213
  Method.no_args (Method.SIMPLE_METHOD' (normalization_tac THEN' resolve_tac [TrueI, refl]))
wenzelm@22099
   214
end
wenzelm@22099
   215
*} "solve goal by normalization"
wenzelm@22099
   216
haftmann@21046
   217
haftmann@21059
   218
text {* lazy @{const If} *}
haftmann@21059
   219
haftmann@21059
   220
definition
wenzelm@21404
   221
  if_delayed :: "bool \<Rightarrow> (bool \<Rightarrow> 'a) \<Rightarrow> (bool \<Rightarrow> 'a) \<Rightarrow> 'a" where
haftmann@22744
   222
  [code nofunc]: "if_delayed b f g = (if b then f True else g False)"
haftmann@21059
   223
haftmann@21059
   224
lemma [code func]:
haftmann@21059
   225
  shows "if_delayed True f g = f True"
haftmann@21059
   226
    and "if_delayed False f g = g False"
haftmann@21059
   227
  unfolding if_delayed_def by simp_all
haftmann@21059
   228
haftmann@21059
   229
lemma [normal pre, symmetric, normal post]:
haftmann@21059
   230
  "(if b then x else y) = if_delayed b (\<lambda>_. x) (\<lambda>_. y)"
haftmann@21059
   231
  unfolding if_delayed_def ..
haftmann@21059
   232
haftmann@21454
   233
hide (open) const if_delayed
haftmann@21046
   234
wenzelm@22099
   235
end