src/HOL/Code_Setup.thy
author haftmann
Thu Aug 16 11:45:06 2007 +0200 (2007-08-16)
changeset 24293 7e67b9706211
parent 24285 066bb557570f
child 24463 841c2e24761f
permissions -rw-r--r--
fixed codegen 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@24285
     6
header {* Setup of code generators and derived tools *}
haftmann@24285
     7
haftmann@24285
     8
theory Code_Setup
haftmann@24285
     9
imports HOL
haftmann@24285
    10
uses "~~/src/HOL/Tools/recfun_codegen.ML"
haftmann@24285
    11
begin
haftmann@24285
    12
haftmann@24285
    13
subsection {* SML code generator setup *}
haftmann@24285
    14
haftmann@24285
    15
setup RecfunCodegen.setup
haftmann@24285
    16
haftmann@24285
    17
types_code
haftmann@24285
    18
  "bool"  ("bool")
haftmann@24285
    19
attach (term_of) {*
haftmann@24285
    20
fun term_of_bool b = if b then HOLogic.true_const else HOLogic.false_const;
haftmann@24285
    21
*}
haftmann@24285
    22
attach (test) {*
haftmann@24285
    23
fun gen_bool i = one_of [false, true];
haftmann@24285
    24
*}
haftmann@24285
    25
  "prop"  ("bool")
haftmann@24285
    26
attach (term_of) {*
haftmann@24285
    27
fun term_of_prop b =
haftmann@24285
    28
  HOLogic.mk_Trueprop (if b then HOLogic.true_const else HOLogic.false_const);
haftmann@24285
    29
*}
haftmann@24285
    30
haftmann@24285
    31
consts_code
haftmann@24285
    32
  "Trueprop" ("(_)")
haftmann@24285
    33
  "True"    ("true")
haftmann@24285
    34
  "False"   ("false")
haftmann@24285
    35
  "Not"     ("Bool.not")
haftmann@24285
    36
  "op |"    ("(_ orelse/ _)")
haftmann@24285
    37
  "op &"    ("(_ andalso/ _)")
haftmann@24285
    38
  "If"      ("(if _/ then _/ else _)")
haftmann@24285
    39
haftmann@24285
    40
setup {*
haftmann@24285
    41
let
haftmann@24285
    42
haftmann@24285
    43
fun eq_codegen thy defs gr dep thyname b t =
haftmann@24285
    44
    (case strip_comb t of
haftmann@24285
    45
       (Const ("op =", Type (_, [Type ("fun", _), _])), _) => NONE
haftmann@24285
    46
     | (Const ("op =", _), [t, u]) =>
haftmann@24285
    47
          let
haftmann@24285
    48
            val (gr', pt) = Codegen.invoke_codegen thy defs dep thyname false (gr, t);
haftmann@24285
    49
            val (gr'', pu) = Codegen.invoke_codegen thy defs dep thyname false (gr', u);
haftmann@24285
    50
            val (gr''', _) = Codegen.invoke_tycodegen thy defs dep thyname false (gr'', HOLogic.boolT)
haftmann@24285
    51
          in
haftmann@24285
    52
            SOME (gr''', Codegen.parens
haftmann@24285
    53
              (Pretty.block [pt, Pretty.str " =", Pretty.brk 1, pu]))
haftmann@24285
    54
          end
haftmann@24285
    55
     | (t as Const ("op =", _), ts) => SOME (Codegen.invoke_codegen
haftmann@24285
    56
         thy defs dep thyname b (gr, Codegen.eta_expand t ts 2))
haftmann@24285
    57
     | _ => NONE);
haftmann@24285
    58
haftmann@24285
    59
in
haftmann@24285
    60
  Codegen.add_codegen "eq_codegen" eq_codegen
haftmann@24285
    61
end
haftmann@24285
    62
*}
haftmann@24285
    63
haftmann@24285
    64
text {* Evaluation *}
haftmann@24285
    65
haftmann@24285
    66
method_setup evaluation = {*
haftmann@24285
    67
  Method.no_args (Method.SIMPLE_METHOD' (CONVERSION Codegen.evaluation_conv THEN' rtac TrueI))
haftmann@24285
    68
*} "solve goal by evaluation"
haftmann@24285
    69
haftmann@24285
    70
haftmann@24285
    71
subsection {* Generic code generator setup *}
haftmann@24285
    72
haftmann@24285
    73
haftmann@24285
    74
text {* using built-in Haskell equality *}
haftmann@24285
    75
haftmann@24285
    76
code_class eq
haftmann@24285
    77
  (Haskell "Eq" where "op =" \<equiv> "(==)")
haftmann@24285
    78
haftmann@24285
    79
code_const "op ="
haftmann@24285
    80
  (Haskell infixl 4 "==")
haftmann@24285
    81
haftmann@24285
    82
haftmann@24285
    83
text {* type bool *}
haftmann@24285
    84
haftmann@24285
    85
lemmas [code] = imp_conv_disj
haftmann@24285
    86
haftmann@24285
    87
code_type bool
haftmann@24285
    88
  (SML "bool")
haftmann@24285
    89
  (OCaml "bool")
haftmann@24285
    90
  (Haskell "Bool")
haftmann@24285
    91
haftmann@24285
    92
code_instance bool :: eq
haftmann@24285
    93
  (Haskell -)
haftmann@24285
    94
haftmann@24285
    95
code_const "op = \<Colon> bool \<Rightarrow> bool \<Rightarrow> bool"
haftmann@24285
    96
  (Haskell infixl 4 "==")
haftmann@24285
    97
haftmann@24285
    98
code_const True and False and Not and "op &" and "op |" and If
haftmann@24285
    99
  (SML "true" and "false" and "not"
haftmann@24285
   100
    and infixl 1 "andalso" and infixl 0 "orelse"
haftmann@24285
   101
    and "!(if (_)/ then (_)/ else (_))")
haftmann@24285
   102
  (OCaml "true" and "false" and "not"
haftmann@24285
   103
    and infixl 4 "&&" and infixl 2 "||"
haftmann@24285
   104
    and "!(if (_)/ then (_)/ else (_))")
haftmann@24285
   105
  (Haskell "True" and "False" and "not"
haftmann@24285
   106
    and infixl 3 "&&" and infixl 2 "||"
haftmann@24285
   107
    and "!(if (_)/ then (_)/ else (_))")
haftmann@24285
   108
haftmann@24285
   109
code_reserved SML
haftmann@24285
   110
  bool true false not
haftmann@24285
   111
haftmann@24285
   112
code_reserved OCaml
haftmann@24285
   113
  bool not
haftmann@24285
   114
haftmann@24285
   115
haftmann@24285
   116
text {* code generation for undefined as exception *}
haftmann@24285
   117
haftmann@24285
   118
code_const undefined
haftmann@24285
   119
  (SML "raise/ Fail/ \"undefined\"")
haftmann@24285
   120
  (OCaml "failwith/ \"undefined\"")
haftmann@24285
   121
  (Haskell "error/ \"undefined\"")
haftmann@24285
   122
haftmann@24285
   123
haftmann@24285
   124
text {* Let and If *}
haftmann@24285
   125
haftmann@24285
   126
lemmas [code func] = Let_def if_True if_False
haftmann@24285
   127
haftmann@24285
   128
setup {*
haftmann@24285
   129
  CodePackage.add_appconst (@{const_name Let}, CodePackage.appgen_let)
haftmann@24285
   130
  #> CodePackage.add_appconst (@{const_name If}, CodePackage.appgen_if)
haftmann@24285
   131
*}
haftmann@24285
   132
haftmann@24285
   133
haftmann@24285
   134
subsection {* Evaluation oracle *}
haftmann@24285
   135
haftmann@24285
   136
oracle eval_oracle ("term") = {* fn thy => fn t => 
haftmann@24285
   137
  if CodePackage.satisfies thy (Thm.cterm_of thy (HOLogic.dest_Trueprop t)) [] 
haftmann@24285
   138
  then t
haftmann@24285
   139
  else HOLogic.Trueprop $ HOLogic.true_const (*dummy*)
haftmann@24285
   140
*}
haftmann@24285
   141
haftmann@24285
   142
method_setup eval = {*
haftmann@24285
   143
let
haftmann@24285
   144
  fun eval_tac thy = 
haftmann@24285
   145
    SUBGOAL (fn (t, i) => rtac (eval_oracle thy t) i)
haftmann@24285
   146
in 
haftmann@24285
   147
  Method.ctxt_args (fn ctxt => 
haftmann@24285
   148
    Method.SIMPLE_METHOD' (eval_tac (ProofContext.theory_of ctxt)))
haftmann@24285
   149
end
haftmann@24285
   150
*} "solve goal by evaluation"
haftmann@24285
   151
haftmann@24285
   152
haftmann@24285
   153
subsection {* Normalization by evaluation *}
haftmann@24285
   154
haftmann@24285
   155
method_setup normalization = {*
haftmann@24285
   156
  Method.no_args (Method.SIMPLE_METHOD'
haftmann@24285
   157
    (CONVERSION (ObjectLogic.judgment_conv Nbe.normalization_conv)
haftmann@24285
   158
      THEN' resolve_tac [TrueI, refl]))
haftmann@24285
   159
*} "solve goal by normalization"
haftmann@24285
   160
haftmann@24285
   161
haftmann@24285
   162
end