src/HOL/Code_Setup.thy
author wenzelm
Wed Sep 17 21:27:14 2008 +0200 (2008-09-17)
changeset 28263 69eaa97e7e96
parent 28054 2b84d34c5d02
child 28290 4cc2b6046258
permissions -rw-r--r--
moved global ML bindings to global place;
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
text {* using built-in Haskell equality *}
haftmann@24285
    78
haftmann@24285
    79
code_class eq
haftmann@24285
    80
  (Haskell "Eq" where "op =" \<equiv> "(==)")
haftmann@24285
    81
haftmann@24285
    82
code_const "op ="
haftmann@24285
    83
  (Haskell infixl 4 "==")
haftmann@24285
    84
haftmann@24285
    85
haftmann@24285
    86
text {* type bool *}
haftmann@24285
    87
haftmann@24285
    88
code_type bool
haftmann@24285
    89
  (SML "bool")
haftmann@24285
    90
  (OCaml "bool")
haftmann@24285
    91
  (Haskell "Bool")
haftmann@24285
    92
haftmann@24285
    93
code_const True and False and Not and "op &" and "op |" and If
haftmann@24285
    94
  (SML "true" and "false" and "not"
haftmann@24285
    95
    and infixl 1 "andalso" and infixl 0 "orelse"
haftmann@24285
    96
    and "!(if (_)/ then (_)/ else (_))")
haftmann@24285
    97
  (OCaml "true" and "false" and "not"
haftmann@24285
    98
    and infixl 4 "&&" and infixl 2 "||"
haftmann@24285
    99
    and "!(if (_)/ then (_)/ else (_))")
haftmann@24285
   100
  (Haskell "True" and "False" and "not"
haftmann@24285
   101
    and infixl 3 "&&" and infixl 2 "||"
haftmann@24285
   102
    and "!(if (_)/ then (_)/ else (_))")
haftmann@24285
   103
haftmann@24285
   104
code_reserved SML
haftmann@24285
   105
  bool true false not
haftmann@24285
   106
haftmann@24285
   107
code_reserved OCaml
haftmann@24285
   108
  bool not
haftmann@24285
   109
haftmann@24285
   110
haftmann@24285
   111
text {* code generation for undefined as exception *}
haftmann@24285
   112
haftmann@28012
   113
code_abort undefined
haftmann@28012
   114
haftmann@24285
   115
code_const undefined
haftmann@24285
   116
  (SML "raise/ Fail/ \"undefined\"")
haftmann@24285
   117
  (OCaml "failwith/ \"undefined\"")
haftmann@24285
   118
  (Haskell "error/ \"undefined\"")
haftmann@24285
   119
haftmann@24285
   120
haftmann@24285
   121
subsection {* Evaluation oracle *}
haftmann@24285
   122
haftmann@27103
   123
ML {*
haftmann@27103
   124
structure Eval_Method =
haftmann@27103
   125
struct
haftmann@27103
   126
haftmann@27103
   127
val eval_ref : (unit -> bool) option ref = ref NONE;
haftmann@27103
   128
haftmann@27103
   129
end;
haftmann@27103
   130
*}
haftmann@27103
   131
haftmann@24285
   132
oracle eval_oracle ("term") = {* fn thy => fn t => 
haftmann@28054
   133
  if Code_ML.eval_term ("Eval_Method.eval_ref", Eval_Method.eval_ref) thy
haftmann@27103
   134
    (HOLogic.dest_Trueprop t) [] 
haftmann@24285
   135
  then t
haftmann@24285
   136
  else HOLogic.Trueprop $ HOLogic.true_const (*dummy*)
haftmann@24285
   137
*}
haftmann@24285
   138
haftmann@24285
   139
method_setup eval = {*
haftmann@24285
   140
let
haftmann@24285
   141
  fun eval_tac thy = 
haftmann@24285
   142
    SUBGOAL (fn (t, i) => rtac (eval_oracle thy t) i)
haftmann@24285
   143
in 
haftmann@24285
   144
  Method.ctxt_args (fn ctxt => 
haftmann@24285
   145
    Method.SIMPLE_METHOD' (eval_tac (ProofContext.theory_of ctxt)))
haftmann@24285
   146
end
haftmann@24285
   147
*} "solve goal by evaluation"
haftmann@24285
   148
haftmann@24285
   149
haftmann@24285
   150
subsection {* Normalization by evaluation *}
haftmann@24285
   151
haftmann@24285
   152
method_setup normalization = {*
haftmann@24285
   153
  Method.no_args (Method.SIMPLE_METHOD'
haftmann@25962
   154
    (CONVERSION (ObjectLogic.judgment_conv Nbe.norm_conv)
haftmann@25962
   155
    THEN' (fn k => TRY (rtac TrueI k))
haftmann@25866
   156
  ))
haftmann@24285
   157
*} "solve goal by normalization"
haftmann@24285
   158
haftmann@24285
   159
end