diff -r 5c8618f95d24 -r 7ac037c75c26 src/HOL/Code_Setup.thy --- a/src/HOL/Code_Setup.thy Thu Apr 16 17:29:56 2009 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,253 +0,0 @@ -(* 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\{})" - -code_datatype Trueprop "prop" - -text {* Code equations *} - -lemma [code]: - shows "(True \ PROP P) \ PROP P" - and "(False \ Q) \ Trueprop True" - and "(PROP P \ True) \ Trueprop True" - and "(Q \ False) \ Trueprop (\ Q)" by (auto intro!: equal_intr_rule) - -lemma [code]: - shows "False \ x \ False" - and "True \ x \ x" - and "x \ False \ False" - and "x \ True \ x" by simp_all - -lemma [code]: - shows "False \ x \ x" - and "True \ x \ True" - and "x \ False \ x" - and "x \ True \ True" by simp_all - -lemma [code]: - shows "\ True \ False" - and "\ False \ 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 = \ 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 \ (\x. Let x f)" - shows "CASE x \ f x" - using assms by simp_all - -lemma If_case_cert: - assumes "CASE \ (\b. If b f g)" - shows "(CASE True \ f) &&& (CASE False \ 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 *} - -setup {* - Value.add_evaluator ("SML", Codegen.eval_term o ProofContext.theory_of) -*} - -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; - val dummy = @{cprop True}; - in case try HOLogic.dest_Trueprop t - of SOME t' => if Code_ML.eval_term - ("Eval_Method.eval_ref", Eval_Method.eval_ref) thy t' [] - then Thm.capply (Thm.capply @{cterm "op \ \ prop \ prop \ prop"} ct) dummy - else dummy - | NONE => dummy - end -*} - -ML {* -fun gen_eval_method conv ctxt = SIMPLE_METHOD' - (CONVERSION (Conv.params_conv (~1) (K (Conv.concl_conv (~1) conv)) ctxt) - THEN' rtac TrueI) -*} - -method_setup eval = {* Scan.succeed (gen_eval_method eval_oracle) *} - "solve goal by evaluation" - -method_setup evaluation = {* Scan.succeed (gen_eval_method Codegen.evaluation_conv) *} - "solve goal by evaluation" - -method_setup normalization = {* - Scan.succeed (K (SIMPLE_METHOD' (CONVERSION Nbe.norm_conv THEN' (fn k => TRY (rtac TrueI k))))) -*} "solve goal by normalization" - - -subsection {* Quickcheck *} - -setup {* - Quickcheck.add_generator ("SML", Codegen.test_term) -*} - -quickcheck_params [size = 5, iterations = 50] - -end