src/HOL/Code_Setup.thy
author haftmann
Tue Jun 10 15:30:06 2008 +0200 (2008-06-10)
changeset 27103 d8549f4d900b
parent 26975 103dca19ef2e
child 27454 fb6a272fe5d0
permissions -rw-r--r--
major refactorings in code generator modules
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) {*
berghofe@25885
    23
fun gen_bool i =
berghofe@25885
    24
  let val b = one_of [false, true]
berghofe@25885
    25
  in (b, fn () => term_of_bool b) end;
haftmann@24285
    26
*}
haftmann@24285
    27
  "prop"  ("bool")
haftmann@24285
    28
attach (term_of) {*
haftmann@24285
    29
fun term_of_prop b =
haftmann@24285
    30
  HOLogic.mk_Trueprop (if b then HOLogic.true_const else HOLogic.false_const);
haftmann@24285
    31
*}
haftmann@24285
    32
haftmann@24285
    33
consts_code
haftmann@24285
    34
  "Trueprop" ("(_)")
haftmann@24285
    35
  "True"    ("true")
haftmann@24285
    36
  "False"   ("false")
haftmann@24285
    37
  "Not"     ("Bool.not")
haftmann@24285
    38
  "op |"    ("(_ orelse/ _)")
haftmann@24285
    39
  "op &"    ("(_ andalso/ _)")
haftmann@24285
    40
  "If"      ("(if _/ then _/ else _)")
haftmann@24285
    41
haftmann@24285
    42
setup {*
haftmann@24285
    43
let
haftmann@24285
    44
haftmann@24285
    45
fun eq_codegen thy defs gr dep thyname b t =
haftmann@24285
    46
    (case strip_comb t of
haftmann@24285
    47
       (Const ("op =", Type (_, [Type ("fun", _), _])), _) => NONE
haftmann@24285
    48
     | (Const ("op =", _), [t, u]) =>
haftmann@24285
    49
          let
haftmann@24285
    50
            val (gr', pt) = Codegen.invoke_codegen thy defs dep thyname false (gr, t);
haftmann@24285
    51
            val (gr'', pu) = Codegen.invoke_codegen thy defs dep thyname false (gr', u);
haftmann@24285
    52
            val (gr''', _) = Codegen.invoke_tycodegen thy defs dep thyname false (gr'', HOLogic.boolT)
haftmann@24285
    53
          in
haftmann@24285
    54
            SOME (gr''', Codegen.parens
berghofe@26975
    55
              (Pretty.block [pt, Codegen.str " =", Pretty.brk 1, pu]))
haftmann@24285
    56
          end
haftmann@24285
    57
     | (t as Const ("op =", _), ts) => SOME (Codegen.invoke_codegen
haftmann@24285
    58
         thy defs dep thyname b (gr, Codegen.eta_expand t ts 2))
haftmann@24285
    59
     | _ => NONE);
haftmann@24285
    60
haftmann@24285
    61
in
haftmann@24285
    62
  Codegen.add_codegen "eq_codegen" eq_codegen
haftmann@24285
    63
end
haftmann@24285
    64
*}
haftmann@24285
    65
berghofe@24463
    66
quickcheck_params [size = 5, iterations = 50]
berghofe@24463
    67
haftmann@24285
    68
text {* Evaluation *}
haftmann@24285
    69
haftmann@24285
    70
method_setup evaluation = {*
haftmann@24285
    71
  Method.no_args (Method.SIMPLE_METHOD' (CONVERSION Codegen.evaluation_conv THEN' rtac TrueI))
haftmann@24285
    72
*} "solve goal by evaluation"
haftmann@24285
    73
haftmann@24285
    74
haftmann@24285
    75
subsection {* Generic code generator setup *}
haftmann@24285
    76
haftmann@24285
    77
haftmann@24285
    78
text {* using built-in Haskell equality *}
haftmann@24285
    79
haftmann@24285
    80
code_class eq
haftmann@24285
    81
  (Haskell "Eq" where "op =" \<equiv> "(==)")
haftmann@24285
    82
haftmann@24285
    83
code_const "op ="
haftmann@24285
    84
  (Haskell infixl 4 "==")
haftmann@24285
    85
haftmann@24285
    86
haftmann@24285
    87
text {* type bool *}
haftmann@24285
    88
haftmann@25962
    89
lemmas [code func, code unfold, code post] = imp_conv_disj
haftmann@24285
    90
haftmann@24285
    91
code_type bool
haftmann@24285
    92
  (SML "bool")
haftmann@24285
    93
  (OCaml "bool")
haftmann@24285
    94
  (Haskell "Bool")
haftmann@24285
    95
haftmann@24285
    96
code_const True and False and Not and "op &" and "op |" and If
haftmann@24285
    97
  (SML "true" and "false" and "not"
haftmann@24285
    98
    and infixl 1 "andalso" and infixl 0 "orelse"
haftmann@24285
    99
    and "!(if (_)/ then (_)/ else (_))")
haftmann@24285
   100
  (OCaml "true" and "false" and "not"
haftmann@24285
   101
    and infixl 4 "&&" and infixl 2 "||"
haftmann@24285
   102
    and "!(if (_)/ then (_)/ else (_))")
haftmann@24285
   103
  (Haskell "True" and "False" and "not"
haftmann@24285
   104
    and infixl 3 "&&" and infixl 2 "||"
haftmann@24285
   105
    and "!(if (_)/ then (_)/ else (_))")
haftmann@24285
   106
haftmann@24285
   107
code_reserved SML
haftmann@24285
   108
  bool true false not
haftmann@24285
   109
haftmann@24285
   110
code_reserved OCaml
haftmann@24285
   111
  bool not
haftmann@24285
   112
haftmann@24285
   113
haftmann@24285
   114
text {* code generation for undefined as exception *}
haftmann@24285
   115
haftmann@24285
   116
code_const undefined
haftmann@24285
   117
  (SML "raise/ Fail/ \"undefined\"")
haftmann@24285
   118
  (OCaml "failwith/ \"undefined\"")
haftmann@24285
   119
  (Haskell "error/ \"undefined\"")
haftmann@24285
   120
haftmann@24285
   121
haftmann@24285
   122
text {* Let and If *}
haftmann@24285
   123
haftmann@24285
   124
lemmas [code func] = Let_def if_True if_False
haftmann@24285
   125
haftmann@24285
   126
haftmann@24285
   127
subsection {* Evaluation oracle *}
haftmann@24285
   128
haftmann@27103
   129
ML {*
haftmann@27103
   130
structure Eval_Method =
haftmann@27103
   131
struct
haftmann@27103
   132
haftmann@27103
   133
val eval_ref : (unit -> bool) option ref = ref NONE;
haftmann@27103
   134
haftmann@27103
   135
end;
haftmann@27103
   136
*}
haftmann@27103
   137
haftmann@24285
   138
oracle eval_oracle ("term") = {* fn thy => fn t => 
haftmann@27103
   139
  if CodeTarget.eval_term ("Eval_Method.eval_ref", Eval_Method.eval_ref) thy
haftmann@27103
   140
    (HOLogic.dest_Trueprop t) [] 
haftmann@24285
   141
  then t
haftmann@24285
   142
  else HOLogic.Trueprop $ HOLogic.true_const (*dummy*)
haftmann@24285
   143
*}
haftmann@24285
   144
haftmann@24285
   145
method_setup eval = {*
haftmann@24285
   146
let
haftmann@24285
   147
  fun eval_tac thy = 
haftmann@24285
   148
    SUBGOAL (fn (t, i) => rtac (eval_oracle thy t) i)
haftmann@24285
   149
in 
haftmann@24285
   150
  Method.ctxt_args (fn ctxt => 
haftmann@24285
   151
    Method.SIMPLE_METHOD' (eval_tac (ProofContext.theory_of ctxt)))
haftmann@24285
   152
end
haftmann@24285
   153
*} "solve goal by evaluation"
haftmann@24285
   154
haftmann@24285
   155
haftmann@24285
   156
subsection {* Normalization by evaluation *}
haftmann@24285
   157
haftmann@24285
   158
method_setup normalization = {*
haftmann@24285
   159
  Method.no_args (Method.SIMPLE_METHOD'
haftmann@25962
   160
    (CONVERSION (ObjectLogic.judgment_conv Nbe.norm_conv)
haftmann@25962
   161
    THEN' (fn k => TRY (rtac TrueI k))
haftmann@25866
   162
  ))
haftmann@24285
   163
*} "solve goal by normalization"
haftmann@24285
   164
haftmann@24285
   165
end