src/HOL/Code_Setup.thy
author haftmann
Fri Oct 24 17:48:40 2008 +0200 (2008-10-24)
changeset 28687 150a8a1eae1a
parent 28562 4e74209f113e
child 28699 32b6a8f12c1c
permissions -rw-r--r--
simplified syntax for class parameters
     1 (*  Title:      HOL/Code_Setup.thy
     2     ID:         $Id$
     3     Author:     Florian Haftmann
     4 *)
     5 
     6 header {* Setup of code generators and related tools *}
     7 
     8 theory Code_Setup
     9 imports HOL
    10 begin
    11 
    12 subsection {* Generic code generator foundation *}
    13 
    14 text {* Datatypes *}
    15 
    16 code_datatype True False
    17 
    18 code_datatype "TYPE('a\<Colon>{})"
    19 
    20 code_datatype Trueprop "prop"
    21 
    22 text {* Code equations *}
    23 
    24 lemma [code]:
    25   shows "False \<and> x \<longleftrightarrow> False"
    26     and "True \<and> x \<longleftrightarrow> x"
    27     and "x \<and> False \<longleftrightarrow> False"
    28     and "x \<and> True \<longleftrightarrow> x" by simp_all
    29 
    30 lemma [code]:
    31   shows "False \<or> x \<longleftrightarrow> x"
    32     and "True \<or> x \<longleftrightarrow> True"
    33     and "x \<or> False \<longleftrightarrow> x"
    34     and "x \<or> True \<longleftrightarrow> True" by simp_all
    35 
    36 lemma [code]:
    37   shows "\<not> True \<longleftrightarrow> False"
    38     and "\<not> False \<longleftrightarrow> True" by (rule HOL.simp_thms)+
    39 
    40 lemmas [code] = Let_def if_True if_False
    41 
    42 lemmas [code, code unfold, symmetric, code post] = imp_conv_disj
    43 
    44 text {* Equality *}
    45 
    46 context eq
    47 begin
    48 
    49 lemma equals_eq [code inline, code]: "op = \<equiv> eq"
    50   by (rule eq_reflection) (rule ext, rule ext, rule sym, rule eq_equals)
    51 
    52 declare eq [code unfold, code inline del]
    53 
    54 declare equals_eq [symmetric, code post]
    55 
    56 end
    57 
    58 declare simp_thms(6) [code nbe]
    59 
    60 hide (open) const eq
    61 hide const eq
    62 
    63 setup {*
    64   Code_Unit.add_const_alias @{thm equals_eq}
    65 *}
    66 
    67 text {* Cases *}
    68 
    69 lemma Let_case_cert:
    70   assumes "CASE \<equiv> (\<lambda>x. Let x f)"
    71   shows "CASE x \<equiv> f x"
    72   using assms by simp_all
    73 
    74 lemma If_case_cert:
    75   includes meta_conjunction_syntax
    76   assumes "CASE \<equiv> (\<lambda>b. If b f g)"
    77   shows "(CASE True \<equiv> f) && (CASE False \<equiv> g)"
    78   using assms by simp_all
    79 
    80 setup {*
    81   Code.add_case @{thm Let_case_cert}
    82   #> Code.add_case @{thm If_case_cert}
    83   #> Code.add_undefined @{const_name undefined}
    84 *}
    85 
    86 code_abort undefined
    87 
    88 
    89 subsection {* Generic code generator preprocessor *}
    90 
    91 setup {*
    92   Code.map_pre (K HOL_basic_ss)
    93   #> Code.map_post (K HOL_basic_ss)
    94 *}
    95 
    96 
    97 subsection {* Generic code generator target languages *}
    98 
    99 text {* type bool *}
   100 
   101 code_type bool
   102   (SML "bool")
   103   (OCaml "bool")
   104   (Haskell "Bool")
   105 
   106 code_const True and False and Not and "op &" and "op |" and If
   107   (SML "true" and "false" and "not"
   108     and infixl 1 "andalso" and infixl 0 "orelse"
   109     and "!(if (_)/ then (_)/ else (_))")
   110   (OCaml "true" and "false" and "not"
   111     and infixl 4 "&&" and infixl 2 "||"
   112     and "!(if (_)/ then (_)/ else (_))")
   113   (Haskell "True" and "False" and "not"
   114     and infixl 3 "&&" and infixl 2 "||"
   115     and "!(if (_)/ then (_)/ else (_))")
   116 
   117 code_reserved SML
   118   bool true false not
   119 
   120 code_reserved OCaml
   121   bool not
   122 
   123 text {* using built-in Haskell equality *}
   124 
   125 code_class eq
   126   (Haskell "Eq")
   127 
   128 code_const "eq_class.eq"
   129   (Haskell infixl 4 "==")
   130 
   131 code_const "op ="
   132   (Haskell infixl 4 "==")
   133 
   134 text {* undefined *}
   135 
   136 code_const undefined
   137   (SML "!(raise/ Fail/ \"undefined\")")
   138   (OCaml "failwith/ \"undefined\"")
   139   (Haskell "error/ \"undefined\"")
   140 
   141 
   142 subsection {* SML code generator setup *}
   143 
   144 types_code
   145   "bool"  ("bool")
   146 attach (term_of) {*
   147 fun term_of_bool b = if b then HOLogic.true_const else HOLogic.false_const;
   148 *}
   149 attach (test) {*
   150 fun gen_bool i =
   151   let val b = one_of [false, true]
   152   in (b, fn () => term_of_bool b) end;
   153 *}
   154   "prop"  ("bool")
   155 attach (term_of) {*
   156 fun term_of_prop b =
   157   HOLogic.mk_Trueprop (if b then HOLogic.true_const else HOLogic.false_const);
   158 *}
   159 
   160 consts_code
   161   "Trueprop" ("(_)")
   162   "True"    ("true")
   163   "False"   ("false")
   164   "Not"     ("Bool.not")
   165   "op |"    ("(_ orelse/ _)")
   166   "op &"    ("(_ andalso/ _)")
   167   "If"      ("(if _/ then _/ else _)")
   168 
   169 setup {*
   170 let
   171 
   172 fun eq_codegen thy defs dep thyname b t gr =
   173     (case strip_comb t of
   174        (Const ("op =", Type (_, [Type ("fun", _), _])), _) => NONE
   175      | (Const ("op =", _), [t, u]) =>
   176           let
   177             val (pt, gr') = Codegen.invoke_codegen thy defs dep thyname false t gr;
   178             val (pu, gr'') = Codegen.invoke_codegen thy defs dep thyname false u gr';
   179             val (_, gr''') = Codegen.invoke_tycodegen thy defs dep thyname false HOLogic.boolT gr'';
   180           in
   181             SOME (Codegen.parens
   182               (Pretty.block [pt, Codegen.str " =", Pretty.brk 1, pu]), gr''')
   183           end
   184      | (t as Const ("op =", _), ts) => SOME (Codegen.invoke_codegen
   185          thy defs dep thyname b (Codegen.eta_expand t ts 2) gr)
   186      | _ => NONE);
   187 
   188 in
   189   Codegen.add_codegen "eq_codegen" eq_codegen
   190 end
   191 *}
   192 
   193 
   194 subsection {* Evaluation and normalization by evaluation *}
   195 
   196 ML {*
   197 structure Eval_Method =
   198 struct
   199 
   200 val eval_ref : (unit -> bool) option ref = ref NONE;
   201 
   202 end;
   203 *}
   204 
   205 oracle eval_oracle = {* fn ct =>
   206   let
   207     val thy = Thm.theory_of_cterm ct;
   208     val t = Thm.term_of ct;
   209   in
   210     if Code_ML.eval_term ("Eval_Method.eval_ref", Eval_Method.eval_ref) thy
   211       (HOLogic.dest_Trueprop t) [] 
   212     then ct
   213     else @{cprop True} (*dummy*)
   214   end
   215 *}
   216 
   217 method_setup eval = {*
   218 let
   219   fun eval_tac thy = 
   220     CSUBGOAL (fn (ct, i) => rtac (eval_oracle ct) i)
   221 in 
   222   Method.ctxt_args (fn ctxt => 
   223     Method.SIMPLE_METHOD' (eval_tac (ProofContext.theory_of ctxt)))
   224 end
   225 *} "solve goal by evaluation"
   226 
   227 
   228 method_setup evaluation = {*
   229   Method.no_args (Method.SIMPLE_METHOD' (CONVERSION Codegen.evaluation_conv THEN' rtac TrueI))
   230 *} "solve goal by evaluation"
   231 
   232 
   233 method_setup normalization = {*
   234   Method.no_args (Method.SIMPLE_METHOD'
   235     (CONVERSION (ObjectLogic.judgment_conv Nbe.norm_conv)
   236     THEN' (fn k => TRY (rtac TrueI k))
   237   ))
   238 *} "solve goal by normalization"
   239 
   240 
   241 subsection {* Quickcheck *}
   242 
   243 quickcheck_params [size = 5, iterations = 50]
   244 
   245 end