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