src/HOL/Code_Setup.thy
author wenzelm
Thu Oct 04 20:29:42 2007 +0200 (2007-10-04)
changeset 24850 0cfd722ab579
parent 24844 98c006a30218
child 25534 d0b74fdd6067
permissions -rw-r--r--
Name.uu, Name.aT;
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
berghofe@24463
    64
quickcheck_params [size = 5, iterations = 50]
berghofe@24463
    65
haftmann@24285
    66
text {* Evaluation *}
haftmann@24285
    67
haftmann@24285
    68
method_setup evaluation = {*
haftmann@24285
    69
  Method.no_args (Method.SIMPLE_METHOD' (CONVERSION Codegen.evaluation_conv THEN' rtac TrueI))
haftmann@24285
    70
*} "solve goal by evaluation"
haftmann@24285
    71
haftmann@24285
    72
haftmann@24285
    73
subsection {* Generic code generator setup *}
haftmann@24285
    74
haftmann@24285
    75
haftmann@24285
    76
text {* using built-in Haskell equality *}
haftmann@24285
    77
haftmann@24285
    78
code_class eq
haftmann@24285
    79
  (Haskell "Eq" where "op =" \<equiv> "(==)")
haftmann@24285
    80
haftmann@24285
    81
code_const "op ="
haftmann@24285
    82
  (Haskell infixl 4 "==")
haftmann@24285
    83
haftmann@24285
    84
haftmann@24285
    85
text {* type bool *}
haftmann@24285
    86
haftmann@24285
    87
lemmas [code] = imp_conv_disj
haftmann@24285
    88
haftmann@24285
    89
code_type bool
haftmann@24285
    90
  (SML "bool")
haftmann@24285
    91
  (OCaml "bool")
haftmann@24285
    92
  (Haskell "Bool")
haftmann@24285
    93
haftmann@24285
    94
code_instance bool :: eq
haftmann@24285
    95
  (Haskell -)
haftmann@24285
    96
haftmann@24285
    97
code_const "op = \<Colon> bool \<Rightarrow> bool \<Rightarrow> bool"
haftmann@24285
    98
  (Haskell infixl 4 "==")
haftmann@24285
    99
haftmann@24285
   100
code_const True and False and Not and "op &" and "op |" and If
haftmann@24285
   101
  (SML "true" and "false" and "not"
haftmann@24285
   102
    and infixl 1 "andalso" and infixl 0 "orelse"
haftmann@24285
   103
    and "!(if (_)/ then (_)/ else (_))")
haftmann@24285
   104
  (OCaml "true" and "false" and "not"
haftmann@24285
   105
    and infixl 4 "&&" and infixl 2 "||"
haftmann@24285
   106
    and "!(if (_)/ then (_)/ else (_))")
haftmann@24285
   107
  (Haskell "True" and "False" and "not"
haftmann@24285
   108
    and infixl 3 "&&" and infixl 2 "||"
haftmann@24285
   109
    and "!(if (_)/ then (_)/ else (_))")
haftmann@24285
   110
haftmann@24285
   111
code_reserved SML
haftmann@24285
   112
  bool true false not
haftmann@24285
   113
haftmann@24285
   114
code_reserved OCaml
haftmann@24285
   115
  bool not
haftmann@24285
   116
haftmann@24285
   117
haftmann@24285
   118
text {* code generation for undefined as exception *}
haftmann@24285
   119
haftmann@24285
   120
code_const undefined
haftmann@24285
   121
  (SML "raise/ Fail/ \"undefined\"")
haftmann@24285
   122
  (OCaml "failwith/ \"undefined\"")
haftmann@24285
   123
  (Haskell "error/ \"undefined\"")
haftmann@24285
   124
haftmann@24285
   125
haftmann@24285
   126
text {* Let and If *}
haftmann@24285
   127
haftmann@24285
   128
lemmas [code func] = Let_def if_True if_False
haftmann@24285
   129
haftmann@24285
   130
haftmann@24285
   131
subsection {* Evaluation oracle *}
haftmann@24285
   132
haftmann@24285
   133
oracle eval_oracle ("term") = {* fn thy => fn t => 
haftmann@24835
   134
  if CodePackage.satisfies thy (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@24835
   154
    (CONVERSION (ObjectLogic.judgment_conv Nbe.norm_conv)
haftmann@24285
   155
      THEN' resolve_tac [TrueI, refl]))
haftmann@24285
   156
*} "solve goal by normalization"
haftmann@24285
   157
haftmann@24285
   158
end