Removed 'includes meta_term_syntax' and 'includes meta_conjunction_syntax'.
(* Title: HOL/Code_Setup.thy
ID: $Id$
Author: Florian Haftmann
*)
header {* Setup of code generators and related tools *}
theory Code_Setup
imports HOL
begin
subsection {* Generic code generator foundation *}
text {* Datatypes *}
code_datatype True False
code_datatype "TYPE('a\<Colon>{})"
code_datatype Trueprop "prop"
text {* Code equations *}
lemma [code]:
shows "False \<and> x \<longleftrightarrow> False"
and "True \<and> x \<longleftrightarrow> x"
and "x \<and> False \<longleftrightarrow> False"
and "x \<and> True \<longleftrightarrow> x" by simp_all
lemma [code]:
shows "False \<or> x \<longleftrightarrow> x"
and "True \<or> x \<longleftrightarrow> True"
and "x \<or> False \<longleftrightarrow> x"
and "x \<or> True \<longleftrightarrow> True" by simp_all
lemma [code]:
shows "\<not> True \<longleftrightarrow> False"
and "\<not> False \<longleftrightarrow> True" by (rule HOL.simp_thms)+
lemmas [code] = Let_def if_True if_False
lemmas [code, code unfold, symmetric, code post] = imp_conv_disj
text {* Equality *}
context eq
begin
lemma equals_eq [code inline, code]: "op = \<equiv> eq"
by (rule eq_reflection) (rule ext, rule ext, rule sym, rule eq_equals)
declare eq [code unfold, code inline del]
declare equals_eq [symmetric, code post]
end
declare simp_thms(6) [code nbe]
hide (open) const eq
hide const eq
setup {*
Code_Unit.add_const_alias @{thm equals_eq}
*}
text {* Cases *}
lemma Let_case_cert:
assumes "CASE \<equiv> (\<lambda>x. Let x f)"
shows "CASE x \<equiv> f x"
using assms by simp_all
lemma If_case_cert:
fixes meta_conjunction :: "prop => prop => prop" (infixr "&&" 2)
assumes "CASE \<equiv> (\<lambda>b. If b f g)"
shows "(CASE True \<equiv> f) && (CASE False \<equiv> g)"
using assms by simp_all
setup {*
Code.add_case @{thm Let_case_cert}
#> Code.add_case @{thm If_case_cert}
#> Code.add_undefined @{const_name undefined}
*}
code_abort undefined
subsection {* Generic code generator preprocessor *}
setup {*
Code.map_pre (K HOL_basic_ss)
#> Code.map_post (K HOL_basic_ss)
*}
subsection {* Generic code generator target languages *}
text {* type bool *}
code_type bool
(SML "bool")
(OCaml "bool")
(Haskell "Bool")
code_const True and False and Not and "op &" and "op |" and If
(SML "true" and "false" and "not"
and infixl 1 "andalso" and infixl 0 "orelse"
and "!(if (_)/ then (_)/ else (_))")
(OCaml "true" and "false" and "not"
and infixl 4 "&&" and infixl 2 "||"
and "!(if (_)/ then (_)/ else (_))")
(Haskell "True" and "False" and "not"
and infixl 3 "&&" and infixl 2 "||"
and "!(if (_)/ then (_)/ else (_))")
code_reserved SML
bool true false not
code_reserved OCaml
bool not
text {* using built-in Haskell equality *}
code_class eq
(Haskell "Eq")
code_const "eq_class.eq"
(Haskell infixl 4 "==")
code_const "op ="
(Haskell infixl 4 "==")
text {* undefined *}
code_const undefined
(SML "!(raise/ Fail/ \"undefined\")")
(OCaml "failwith/ \"undefined\"")
(Haskell "error/ \"undefined\"")
subsection {* SML code generator setup *}
types_code
"bool" ("bool")
attach (term_of) {*
fun term_of_bool b = if b then HOLogic.true_const else HOLogic.false_const;
*}
attach (test) {*
fun gen_bool i =
let val b = one_of [false, true]
in (b, fn () => term_of_bool b) end;
*}
"prop" ("bool")
attach (term_of) {*
fun term_of_prop b =
HOLogic.mk_Trueprop (if b then HOLogic.true_const else HOLogic.false_const);
*}
consts_code
"Trueprop" ("(_)")
"True" ("true")
"False" ("false")
"Not" ("Bool.not")
"op |" ("(_ orelse/ _)")
"op &" ("(_ andalso/ _)")
"If" ("(if _/ then _/ else _)")
setup {*
let
fun eq_codegen thy defs dep thyname b t gr =
(case strip_comb t of
(Const ("op =", Type (_, [Type ("fun", _), _])), _) => NONE
| (Const ("op =", _), [t, u]) =>
let
val (pt, gr') = Codegen.invoke_codegen thy defs dep thyname false t gr;
val (pu, gr'') = Codegen.invoke_codegen thy defs dep thyname false u gr';
val (_, gr''') = Codegen.invoke_tycodegen thy defs dep thyname false HOLogic.boolT gr'';
in
SOME (Codegen.parens
(Pretty.block [pt, Codegen.str " =", Pretty.brk 1, pu]), gr''')
end
| (t as Const ("op =", _), ts) => SOME (Codegen.invoke_codegen
thy defs dep thyname b (Codegen.eta_expand t ts 2) gr)
| _ => NONE);
in
Codegen.add_codegen "eq_codegen" eq_codegen
end
*}
subsection {* Evaluation and normalization by evaluation *}
ML {*
structure Eval_Method =
struct
val eval_ref : (unit -> bool) option ref = ref NONE;
end;
*}
oracle eval_oracle = {* fn ct =>
let
val thy = Thm.theory_of_cterm ct;
val t = Thm.term_of ct;
in
if Code_ML.eval_term ("Eval_Method.eval_ref", Eval_Method.eval_ref) thy
(HOLogic.dest_Trueprop t) []
then ct
else @{cprop True} (*dummy*)
end
*}
method_setup eval = {*
let
fun eval_tac thy =
CSUBGOAL (fn (ct, i) => rtac (eval_oracle ct) i)
in
Method.ctxt_args (fn ctxt =>
Method.SIMPLE_METHOD' (eval_tac (ProofContext.theory_of ctxt)))
end
*} "solve goal by evaluation"
method_setup evaluation = {*
Method.no_args (Method.SIMPLE_METHOD' (CONVERSION Codegen.evaluation_conv THEN' rtac TrueI))
*} "solve goal by evaluation"
method_setup normalization = {*
Method.no_args (Method.SIMPLE_METHOD'
(CONVERSION (ObjectLogic.judgment_conv Nbe.norm_conv)
THEN' (fn k => TRY (rtac TrueI k))
))
*} "solve goal by normalization"
subsection {* Quickcheck *}
quickcheck_params [size = 5, iterations = 50]
end