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