src/HOL/Code_Setup.thy
author berghofe
Fri May 23 16:41:39 2008 +0200 (2008-05-23)
changeset 26975 103dca19ef2e
parent 25962 13b6c0b31005
child 27103 d8549f4d900b
permissions -rw-r--r--
Replaced Pretty.str and Pretty.string_of by specific functions (from Codegen) that
set print_mode and margin appropriately.
     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 =
    24   let val b = one_of [false, true]
    25   in (b, fn () => term_of_bool b) end;
    26 *}
    27   "prop"  ("bool")
    28 attach (term_of) {*
    29 fun term_of_prop b =
    30   HOLogic.mk_Trueprop (if b then HOLogic.true_const else HOLogic.false_const);
    31 *}
    32 
    33 consts_code
    34   "Trueprop" ("(_)")
    35   "True"    ("true")
    36   "False"   ("false")
    37   "Not"     ("Bool.not")
    38   "op |"    ("(_ orelse/ _)")
    39   "op &"    ("(_ andalso/ _)")
    40   "If"      ("(if _/ then _/ else _)")
    41 
    42 setup {*
    43 let
    44 
    45 fun eq_codegen thy defs gr dep thyname b t =
    46     (case strip_comb t of
    47        (Const ("op =", Type (_, [Type ("fun", _), _])), _) => NONE
    48      | (Const ("op =", _), [t, u]) =>
    49           let
    50             val (gr', pt) = Codegen.invoke_codegen thy defs dep thyname false (gr, t);
    51             val (gr'', pu) = Codegen.invoke_codegen thy defs dep thyname false (gr', u);
    52             val (gr''', _) = Codegen.invoke_tycodegen thy defs dep thyname false (gr'', HOLogic.boolT)
    53           in
    54             SOME (gr''', Codegen.parens
    55               (Pretty.block [pt, Codegen.str " =", Pretty.brk 1, pu]))
    56           end
    57      | (t as Const ("op =", _), ts) => SOME (Codegen.invoke_codegen
    58          thy defs dep thyname b (gr, Codegen.eta_expand t ts 2))
    59      | _ => NONE);
    60 
    61 in
    62   Codegen.add_codegen "eq_codegen" eq_codegen
    63 end
    64 *}
    65 
    66 quickcheck_params [size = 5, iterations = 50]
    67 
    68 text {* Evaluation *}
    69 
    70 method_setup evaluation = {*
    71   Method.no_args (Method.SIMPLE_METHOD' (CONVERSION Codegen.evaluation_conv THEN' rtac TrueI))
    72 *} "solve goal by evaluation"
    73 
    74 
    75 subsection {* Generic code generator setup *}
    76 
    77 
    78 text {* using built-in Haskell equality *}
    79 
    80 code_class eq
    81   (Haskell "Eq" where "op =" \<equiv> "(==)")
    82 
    83 code_const "op ="
    84   (Haskell infixl 4 "==")
    85 
    86 
    87 text {* type bool *}
    88 
    89 lemmas [code func, code unfold, code post] = imp_conv_disj
    90 
    91 code_type bool
    92   (SML "bool")
    93   (OCaml "bool")
    94   (Haskell "Bool")
    95 
    96 code_const True and False and Not and "op &" and "op |" and If
    97   (SML "true" and "false" and "not"
    98     and infixl 1 "andalso" and infixl 0 "orelse"
    99     and "!(if (_)/ then (_)/ else (_))")
   100   (OCaml "true" and "false" and "not"
   101     and infixl 4 "&&" and infixl 2 "||"
   102     and "!(if (_)/ then (_)/ else (_))")
   103   (Haskell "True" and "False" and "not"
   104     and infixl 3 "&&" and infixl 2 "||"
   105     and "!(if (_)/ then (_)/ else (_))")
   106 
   107 code_reserved SML
   108   bool true false not
   109 
   110 code_reserved OCaml
   111   bool not
   112 
   113 
   114 text {* code generation for undefined as exception *}
   115 
   116 code_const undefined
   117   (SML "raise/ Fail/ \"undefined\"")
   118   (OCaml "failwith/ \"undefined\"")
   119   (Haskell "error/ \"undefined\"")
   120 
   121 
   122 text {* Let and If *}
   123 
   124 lemmas [code func] = Let_def if_True if_False
   125 
   126 
   127 subsection {* Evaluation oracle *}
   128 
   129 oracle eval_oracle ("term") = {* fn thy => fn t => 
   130   if CodePackage.satisfies thy (HOLogic.dest_Trueprop t) [] 
   131   then t
   132   else HOLogic.Trueprop $ HOLogic.true_const (*dummy*)
   133 *}
   134 
   135 method_setup eval = {*
   136 let
   137   fun eval_tac thy = 
   138     SUBGOAL (fn (t, i) => rtac (eval_oracle thy t) i)
   139 in 
   140   Method.ctxt_args (fn ctxt => 
   141     Method.SIMPLE_METHOD' (eval_tac (ProofContext.theory_of ctxt)))
   142 end
   143 *} "solve goal by evaluation"
   144 
   145 
   146 subsection {* Normalization by evaluation *}
   147 
   148 method_setup normalization = {*
   149   Method.no_args (Method.SIMPLE_METHOD'
   150     (CONVERSION (ObjectLogic.judgment_conv Nbe.norm_conv)
   151     THEN' (fn k => TRY (rtac TrueI k))
   152   ))
   153 *} "solve goal by normalization"
   154 
   155 end