src/HOL/Code_Setup.thy
author wenzelm
Wed Sep 17 21:27:14 2008 +0200 (2008-09-17)
changeset 28263 69eaa97e7e96
parent 28054 2b84d34c5d02
child 28290 4cc2b6046258
permissions -rw-r--r--
moved global ML bindings to global place;
     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 text {* using built-in Haskell equality *}
    78 
    79 code_class eq
    80   (Haskell "Eq" where "op =" \<equiv> "(==)")
    81 
    82 code_const "op ="
    83   (Haskell infixl 4 "==")
    84 
    85 
    86 text {* type bool *}
    87 
    88 code_type bool
    89   (SML "bool")
    90   (OCaml "bool")
    91   (Haskell "Bool")
    92 
    93 code_const True and False and Not and "op &" and "op |" and If
    94   (SML "true" and "false" and "not"
    95     and infixl 1 "andalso" and infixl 0 "orelse"
    96     and "!(if (_)/ then (_)/ else (_))")
    97   (OCaml "true" and "false" and "not"
    98     and infixl 4 "&&" and infixl 2 "||"
    99     and "!(if (_)/ then (_)/ else (_))")
   100   (Haskell "True" and "False" and "not"
   101     and infixl 3 "&&" and infixl 2 "||"
   102     and "!(if (_)/ then (_)/ else (_))")
   103 
   104 code_reserved SML
   105   bool true false not
   106 
   107 code_reserved OCaml
   108   bool not
   109 
   110 
   111 text {* code generation for undefined as exception *}
   112 
   113 code_abort undefined
   114 
   115 code_const undefined
   116   (SML "raise/ Fail/ \"undefined\"")
   117   (OCaml "failwith/ \"undefined\"")
   118   (Haskell "error/ \"undefined\"")
   119 
   120 
   121 subsection {* Evaluation oracle *}
   122 
   123 ML {*
   124 structure Eval_Method =
   125 struct
   126 
   127 val eval_ref : (unit -> bool) option ref = ref NONE;
   128 
   129 end;
   130 *}
   131 
   132 oracle eval_oracle ("term") = {* fn thy => fn t => 
   133   if Code_ML.eval_term ("Eval_Method.eval_ref", Eval_Method.eval_ref) thy
   134     (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' (fn k => TRY (rtac TrueI k))
   156   ))
   157 *} "solve goal by normalization"
   158 
   159 end