src/HOL/Code_Setup.thy
author haftmann
Thu Sep 25 09:28:03 2008 +0200 (2008-09-25)
changeset 28346 b8390cd56b8f
parent 28290 4cc2b6046258
child 28400 89904cfd41c3
permissions -rw-r--r--
discontinued special treatment of op = vs. eq_class.eq
     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 "eq_class.eq" \<equiv> "(==)")
    81 
    82 code_const "eq_class.eq"
    83   (Haskell infixl 4 "==")
    84 
    85 code_const "op ="
    86   (Haskell infixl 4 "==")
    87 
    88 
    89 text {* type bool *}
    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_abort undefined
   117 
   118 code_const undefined
   119   (SML "raise/ Fail/ \"undefined\"")
   120   (OCaml "failwith/ \"undefined\"")
   121   (Haskell "error/ \"undefined\"")
   122 
   123 
   124 subsection {* Evaluation oracle *}
   125 
   126 ML {*
   127 structure Eval_Method =
   128 struct
   129 
   130 val eval_ref : (unit -> bool) option ref = ref NONE;
   131 
   132 end;
   133 *}
   134 
   135 oracle eval_oracle = {* fn ct =>
   136   let
   137     val thy = Thm.theory_of_cterm ct;
   138     val t = Thm.term_of ct;
   139   in
   140     if Code_ML.eval_term ("Eval_Method.eval_ref", Eval_Method.eval_ref) thy
   141       (HOLogic.dest_Trueprop t) [] 
   142     then ct
   143     else @{cprop True} (*dummy*)
   144   end
   145 *}
   146 
   147 method_setup eval = {*
   148 let
   149   fun eval_tac thy = 
   150     CSUBGOAL (fn (ct, i) => rtac (eval_oracle ct) i)
   151 in 
   152   Method.ctxt_args (fn ctxt => 
   153     Method.SIMPLE_METHOD' (eval_tac (ProofContext.theory_of ctxt)))
   154 end
   155 *} "solve goal by evaluation"
   156 
   157 
   158 subsection {* Normalization by evaluation *}
   159 
   160 method_setup normalization = {*
   161   Method.no_args (Method.SIMPLE_METHOD'
   162     (CONVERSION (ObjectLogic.judgment_conv Nbe.norm_conv)
   163     THEN' (fn k => TRY (rtac TrueI k))
   164   ))
   165 *} "solve goal by normalization"
   166 
   167 end