src/HOL/Code_Setup.thy
author berghofe
Tue Jan 08 10:24:34 2008 +0100 (2008-01-08)
changeset 25860 844ab7ace3db
parent 25534 d0b74fdd6067
child 25866 263aaf988d44
permissions -rw-r--r--
imp_conv_disj is now declared as a "code unfold" lemma to avoid that
conclusion is evaluated eagerly.
     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 unfold] = imp_conv_disj
    88 
    89 code_type bool
    90   (SML "bool")
    91   (OCaml "bool")
    92   (Haskell "Bool")
    93 
    94 code_const True and False and Not and "op &" and "op |" and If
    95   (SML "true" and "false" and "not"
    96     and infixl 1 "andalso" and infixl 0 "orelse"
    97     and "!(if (_)/ then (_)/ else (_))")
    98   (OCaml "true" and "false" and "not"
    99     and infixl 4 "&&" and infixl 2 "||"
   100     and "!(if (_)/ then (_)/ else (_))")
   101   (Haskell "True" and "False" and "not"
   102     and infixl 3 "&&" and infixl 2 "||"
   103     and "!(if (_)/ then (_)/ else (_))")
   104 
   105 code_reserved SML
   106   bool true false not
   107 
   108 code_reserved OCaml
   109   bool not
   110 
   111 
   112 text {* code generation for undefined as exception *}
   113 
   114 code_const undefined
   115   (SML "raise/ Fail/ \"undefined\"")
   116   (OCaml "failwith/ \"undefined\"")
   117   (Haskell "error/ \"undefined\"")
   118 
   119 
   120 text {* Let and If *}
   121 
   122 lemmas [code func] = Let_def if_True if_False
   123 
   124 
   125 subsection {* Evaluation oracle *}
   126 
   127 oracle eval_oracle ("term") = {* fn thy => fn t => 
   128   if CodePackage.satisfies thy (HOLogic.dest_Trueprop t) [] 
   129   then t
   130   else HOLogic.Trueprop $ HOLogic.true_const (*dummy*)
   131 *}
   132 
   133 method_setup eval = {*
   134 let
   135   fun eval_tac thy = 
   136     SUBGOAL (fn (t, i) => rtac (eval_oracle thy t) i)
   137 in 
   138   Method.ctxt_args (fn ctxt => 
   139     Method.SIMPLE_METHOD' (eval_tac (ProofContext.theory_of ctxt)))
   140 end
   141 *} "solve goal by evaluation"
   142 
   143 
   144 subsection {* Normalization by evaluation *}
   145 
   146 method_setup normalization = {*
   147   Method.no_args (Method.SIMPLE_METHOD'
   148     (CONVERSION (ObjectLogic.judgment_conv Nbe.norm_conv)
   149       THEN' resolve_tac [TrueI, refl]))
   150 *} "solve goal by normalization"
   151 
   152 end