# HG changeset patch # User haftmann # Date 1222684317 -7200 # Node ID 89904cfd41c32adb0583fa1e07315bf862cde771 # Parent b11b1ca701e555e7d2e04951f5d78ee1d4cc029f polished code generator setup diff -r b11b1ca701e5 -r 89904cfd41c3 src/HOL/Code_Setup.thy --- a/src/HOL/Code_Setup.thy Mon Sep 29 12:31:56 2008 +0200 +++ b/src/HOL/Code_Setup.thy Mon Sep 29 12:31:57 2008 +0200 @@ -3,16 +3,141 @@ Author: Florian Haftmann *) -header {* Setup of code generators and derived tools *} +header {* Setup of code generators and related tools *} theory Code_Setup imports HOL -uses "~~/src/HOL/Tools/recfun_codegen.ML" +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 func]: + shows "False \ x \ False" + and "True \ x \ x" + and "x \ False \ False" + and "x \ True \ x" by simp_all + +lemma [code func]: + shows "False \ x \ x" + and "True \ x \ True" + and "x \ False \ x" + and "x \ True \ True" by simp_all + +lemma [code func]: + shows "\ True \ False" + and "\ False \ True" by (rule HOL.simp_thms)+ + +lemmas [code func] = Let_def if_True if_False + +lemmas [code func, code unfold, symmetric, code post] = imp_conv_disj + +text {* Equality *} + +context eq begin -subsection {* SML code generator setup *} +lemma equals_eq [code inline, code func]: "op = \ eq" + by (rule eq_reflection) (rule ext, rule ext, rule sym, rule eq_equals) + +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: + includes meta_conjunction_syntax + 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) +*} + -setup RecfunCodegen.setup +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" where "eq_class.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") @@ -63,65 +188,8 @@ end *} -quickcheck_params [size = 5, iterations = 50] -text {* Evaluation *} - -method_setup evaluation = {* - Method.no_args (Method.SIMPLE_METHOD' (CONVERSION Codegen.evaluation_conv THEN' rtac TrueI)) -*} "solve goal by evaluation" - - -subsection {* Generic code generator setup *} - -text {* using built-in Haskell equality *} - -code_class eq - (Haskell "Eq" where "eq_class.eq" \ "(==)") - -code_const "eq_class.eq" - (Haskell infixl 4 "==") - -code_const "op =" - (Haskell infixl 4 "==") - - -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 {* code generation for undefined as exception *} - -code_abort undefined - -code_const undefined - (SML "raise/ Fail/ \"undefined\"") - (OCaml "failwith/ \"undefined\"") - (Haskell "error/ \"undefined\"") - - -subsection {* Evaluation oracle *} +subsection {* Evaluation and normalization by evaluation *} ML {* structure Eval_Method = @@ -155,7 +223,10 @@ *} "solve goal by evaluation" -subsection {* Normalization 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' @@ -164,4 +235,9 @@ )) *} "solve goal by normalization" + +subsection {* Quickcheck *} + +quickcheck_params [size = 5, iterations = 50] + end diff -r b11b1ca701e5 -r 89904cfd41c3 src/HOL/HOL.thy --- a/src/HOL/HOL.thy Mon Sep 29 12:31:56 2008 +0200 +++ b/src/HOL/HOL.thy Mon Sep 29 12:31:57 2008 +0200 @@ -35,6 +35,7 @@ "~~/src/Tools/code/code_ml.ML" "~~/src/Tools/code/code_haskell.ML" "~~/src/Tools/nbe.ML" + ("~~/src/HOL/Tools/recfun_codegen.ML") begin subsection {* Primitive logic *} @@ -1678,88 +1679,37 @@ *} -subsection {* Code generator basic setup -- see further @{text Code_Setup.thy} *} +subsection {* Code generator basics -- see further theory @{text "Code_Setup"} *} + +text {* Module setup *} + +use "~~/src/HOL/Tools/recfun_codegen.ML" setup {* - Code.map_pre (K HOL_basic_ss) - #> Code.map_post (K HOL_basic_ss) + Code_Name.setup + #> Code_ML.setup + #> Code_Haskell.setup + #> Nbe.setup + #> Codegen.setup + #> RecfunCodegen.setup *} -code_datatype True False -code_datatype "TYPE('a\{})" - -code_datatype Trueprop "prop" - -lemma Let_case_cert: - assumes "CASE \ (\x. Let x f)" - shows "CASE x \ f x" - using assms by simp_all - -lemma If_case_cert: - includes meta_conjunction_syntax - 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} -*} +text {* Equality *} class eq = type + fixes eq :: "'a \ 'a \ bool" - assumes eq_equals: "eq x y \ x = y " + assumes eq_equals: "eq x y \ x = y" begin lemma eq: "eq = (op =)" by (rule ext eq_equals)+ -lemma equals_eq [code inline, code func]: "op = \ eq" - by (rule eq_reflection) (rule ext, rule ext, rule sym, rule eq_equals) - -declare equals_eq [symmetric, code post] - lemma eq_refl: "eq x x \ True" unfolding eq by rule+ end -declare simp_thms(6) [code nbe] - -hide (open) const eq -hide const eq - -setup {* - Code_Unit.add_const_alias @{thm equals_eq} - #> Code_Name.setup - #> Code_ML.setup - #> Code_Haskell.setup - #> Nbe.setup - #> Codegen.setup -*} - -lemma [code func]: - shows "False \ x \ False" - and "True \ x \ x" - and "x \ False \ False" - and "x \ True \ x" by simp_all - -lemma [code func]: - shows "False \ x \ x" - and "True \ x \ True" - and "x \ False \ x" - and "x \ True \ True" by simp_all - -lemma [code func]: - shows "\ True \ False" - and "\ False \ True" by (rule HOL.simp_thms)+ - -lemmas [code func] = Let_def if_True if_False - -lemmas [code func, code unfold, symmetric, code post] = imp_conv_disj - subsection {* Legacy tactics and ML bindings *}