src/HOL/Code_Setup.thy
author haftmann
Thu Oct 04 19:54:44 2007 +0200 (2007-10-04)
changeset 24844 98c006a30218
parent 24835 8c26128f8997
child 25534 d0b74fdd6067
permissions -rw-r--r--
certificates for code generator case expressions
     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 quickcheck_params [size = 5, iterations = 50]
    65 
    66 text {* Evaluation *}
    67 
    68 method_setup evaluation = {*
    69   Method.no_args (Method.SIMPLE_METHOD' (CONVERSION Codegen.evaluation_conv THEN' rtac TrueI))
    70 *} "solve goal by evaluation"
    71 
    72 
    73 subsection {* Generic code generator setup *}
    74 
    75 
    76 text {* using built-in Haskell equality *}
    77 
    78 code_class eq
    79   (Haskell "Eq" where "op =" \<equiv> "(==)")
    80 
    81 code_const "op ="
    82   (Haskell infixl 4 "==")
    83 
    84 
    85 text {* type bool *}
    86 
    87 lemmas [code] = imp_conv_disj
    88 
    89 code_type bool
    90   (SML "bool")
    91   (OCaml "bool")
    92   (Haskell "Bool")
    93 
    94 code_instance bool :: eq
    95   (Haskell -)
    96 
    97 code_const "op = \<Colon> bool \<Rightarrow> bool \<Rightarrow> bool"
    98   (Haskell infixl 4 "==")
    99 
   100 code_const True and False and Not and "op &" and "op |" and If
   101   (SML "true" and "false" and "not"
   102     and infixl 1 "andalso" and infixl 0 "orelse"
   103     and "!(if (_)/ then (_)/ else (_))")
   104   (OCaml "true" and "false" and "not"
   105     and infixl 4 "&&" and infixl 2 "||"
   106     and "!(if (_)/ then (_)/ else (_))")
   107   (Haskell "True" and "False" and "not"
   108     and infixl 3 "&&" and infixl 2 "||"
   109     and "!(if (_)/ then (_)/ else (_))")
   110 
   111 code_reserved SML
   112   bool true false not
   113 
   114 code_reserved OCaml
   115   bool not
   116 
   117 
   118 text {* code generation for undefined as exception *}
   119 
   120 code_const undefined
   121   (SML "raise/ Fail/ \"undefined\"")
   122   (OCaml "failwith/ \"undefined\"")
   123   (Haskell "error/ \"undefined\"")
   124 
   125 
   126 text {* Let and If *}
   127 
   128 lemmas [code func] = Let_def if_True if_False
   129 
   130 
   131 subsection {* Evaluation oracle *}
   132 
   133 oracle eval_oracle ("term") = {* fn thy => fn t => 
   134   if CodePackage.satisfies thy (HOLogic.dest_Trueprop t) [] 
   135   then t
   136   else HOLogic.Trueprop $ HOLogic.true_const (*dummy*)
   137 *}
   138 
   139 method_setup eval = {*
   140 let
   141   fun eval_tac thy = 
   142     SUBGOAL (fn (t, i) => rtac (eval_oracle thy t) i)
   143 in 
   144   Method.ctxt_args (fn ctxt => 
   145     Method.SIMPLE_METHOD' (eval_tac (ProofContext.theory_of ctxt)))
   146 end
   147 *} "solve goal by evaluation"
   148 
   149 
   150 subsection {* Normalization by evaluation *}
   151 
   152 method_setup normalization = {*
   153   Method.no_args (Method.SIMPLE_METHOD'
   154     (CONVERSION (ObjectLogic.judgment_conv Nbe.norm_conv)
   155       THEN' resolve_tac [TrueI, refl]))
   156 *} "solve goal by normalization"
   157 
   158 end