polished code generator setup
authorhaftmann
Mon Sep 29 12:31:57 2008 +0200 (2008-09-29)
changeset 2840089904cfd41c3
parent 28399 b11b1ca701e5
child 28401 d5f39173444c
polished code generator setup
src/HOL/Code_Setup.thy
src/HOL/HOL.thy
     1.1 --- a/src/HOL/Code_Setup.thy	Mon Sep 29 12:31:56 2008 +0200
     1.2 +++ b/src/HOL/Code_Setup.thy	Mon Sep 29 12:31:57 2008 +0200
     1.3 @@ -3,16 +3,141 @@
     1.4      Author:     Florian Haftmann
     1.5  *)
     1.6  
     1.7 -header {* Setup of code generators and derived tools *}
     1.8 +header {* Setup of code generators and related tools *}
     1.9  
    1.10  theory Code_Setup
    1.11  imports HOL
    1.12 -uses "~~/src/HOL/Tools/recfun_codegen.ML"
    1.13 +begin
    1.14 +
    1.15 +subsection {* Generic code generator foundation *}
    1.16 +
    1.17 +text {* Datatypes *}
    1.18 +
    1.19 +code_datatype True False
    1.20 +
    1.21 +code_datatype "TYPE('a\<Colon>{})"
    1.22 +
    1.23 +code_datatype Trueprop "prop"
    1.24 +
    1.25 +text {* Code equations *}
    1.26 +
    1.27 +lemma [code func]:
    1.28 +  shows "False \<and> x \<longleftrightarrow> False"
    1.29 +    and "True \<and> x \<longleftrightarrow> x"
    1.30 +    and "x \<and> False \<longleftrightarrow> False"
    1.31 +    and "x \<and> True \<longleftrightarrow> x" by simp_all
    1.32 +
    1.33 +lemma [code func]:
    1.34 +  shows "False \<or> x \<longleftrightarrow> x"
    1.35 +    and "True \<or> x \<longleftrightarrow> True"
    1.36 +    and "x \<or> False \<longleftrightarrow> x"
    1.37 +    and "x \<or> True \<longleftrightarrow> True" by simp_all
    1.38 +
    1.39 +lemma [code func]:
    1.40 +  shows "\<not> True \<longleftrightarrow> False"
    1.41 +    and "\<not> False \<longleftrightarrow> True" by (rule HOL.simp_thms)+
    1.42 +
    1.43 +lemmas [code func] = Let_def if_True if_False
    1.44 +
    1.45 +lemmas [code func, code unfold, symmetric, code post] = imp_conv_disj
    1.46 +
    1.47 +text {* Equality *}
    1.48 +
    1.49 +context eq
    1.50  begin
    1.51  
    1.52 -subsection {* SML code generator setup *}
    1.53 +lemma equals_eq [code inline, code func]: "op = \<equiv> eq"
    1.54 +  by (rule eq_reflection) (rule ext, rule ext, rule sym, rule eq_equals)
    1.55 +
    1.56 +declare equals_eq [symmetric, code post]
    1.57 +
    1.58 +end
    1.59 +
    1.60 +declare simp_thms(6) [code nbe]
    1.61 +
    1.62 +hide (open) const eq
    1.63 +hide const eq
    1.64 +
    1.65 +setup {*
    1.66 +  Code_Unit.add_const_alias @{thm equals_eq}
    1.67 +*}
    1.68 +
    1.69 +text {* Cases *}
    1.70 +
    1.71 +lemma Let_case_cert:
    1.72 +  assumes "CASE \<equiv> (\<lambda>x. Let x f)"
    1.73 +  shows "CASE x \<equiv> f x"
    1.74 +  using assms by simp_all
    1.75 +
    1.76 +lemma If_case_cert:
    1.77 +  includes meta_conjunction_syntax
    1.78 +  assumes "CASE \<equiv> (\<lambda>b. If b f g)"
    1.79 +  shows "(CASE True \<equiv> f) && (CASE False \<equiv> g)"
    1.80 +  using assms by simp_all
    1.81 +
    1.82 +setup {*
    1.83 +  Code.add_case @{thm Let_case_cert}
    1.84 +  #> Code.add_case @{thm If_case_cert}
    1.85 +  #> Code.add_undefined @{const_name undefined}
    1.86 +*}
    1.87 +
    1.88 +code_abort undefined
    1.89 +
    1.90 +
    1.91 +subsection {* Generic code generator preprocessor *}
    1.92 +
    1.93 +setup {*
    1.94 +  Code.map_pre (K HOL_basic_ss)
    1.95 +  #> Code.map_post (K HOL_basic_ss)
    1.96 +*}
    1.97 +
    1.98  
    1.99 -setup RecfunCodegen.setup
   1.100 +subsection {* Generic code generator target languages *}
   1.101 +
   1.102 +text {* type bool *}
   1.103 +
   1.104 +code_type bool
   1.105 +  (SML "bool")
   1.106 +  (OCaml "bool")
   1.107 +  (Haskell "Bool")
   1.108 +
   1.109 +code_const True and False and Not and "op &" and "op |" and If
   1.110 +  (SML "true" and "false" and "not"
   1.111 +    and infixl 1 "andalso" and infixl 0 "orelse"
   1.112 +    and "!(if (_)/ then (_)/ else (_))")
   1.113 +  (OCaml "true" and "false" and "not"
   1.114 +    and infixl 4 "&&" and infixl 2 "||"
   1.115 +    and "!(if (_)/ then (_)/ else (_))")
   1.116 +  (Haskell "True" and "False" and "not"
   1.117 +    and infixl 3 "&&" and infixl 2 "||"
   1.118 +    and "!(if (_)/ then (_)/ else (_))")
   1.119 +
   1.120 +code_reserved SML
   1.121 +  bool true false not
   1.122 +
   1.123 +code_reserved OCaml
   1.124 +  bool not
   1.125 +
   1.126 +text {* using built-in Haskell equality *}
   1.127 +
   1.128 +code_class eq
   1.129 +  (Haskell "Eq" where "eq_class.eq" \<equiv> "(==)")
   1.130 +
   1.131 +code_const "eq_class.eq"
   1.132 +  (Haskell infixl 4 "==")
   1.133 +
   1.134 +code_const "op ="
   1.135 +  (Haskell infixl 4 "==")
   1.136 +
   1.137 +text {* undefined *}
   1.138 +
   1.139 +code_const undefined
   1.140 +  (SML "raise/ Fail/ \"undefined\"")
   1.141 +  (OCaml "failwith/ \"undefined\"")
   1.142 +  (Haskell "error/ \"undefined\"")
   1.143 +
   1.144 +
   1.145 +subsection {* SML code generator setup *}
   1.146  
   1.147  types_code
   1.148    "bool"  ("bool")
   1.149 @@ -63,65 +188,8 @@
   1.150  end
   1.151  *}
   1.152  
   1.153 -quickcheck_params [size = 5, iterations = 50]
   1.154  
   1.155 -text {* Evaluation *}
   1.156 -
   1.157 -method_setup evaluation = {*
   1.158 -  Method.no_args (Method.SIMPLE_METHOD' (CONVERSION Codegen.evaluation_conv THEN' rtac TrueI))
   1.159 -*} "solve goal by evaluation"
   1.160 -
   1.161 -
   1.162 -subsection {* Generic code generator setup *}
   1.163 -
   1.164 -text {* using built-in Haskell equality *}
   1.165 -
   1.166 -code_class eq
   1.167 -  (Haskell "Eq" where "eq_class.eq" \<equiv> "(==)")
   1.168 -
   1.169 -code_const "eq_class.eq"
   1.170 -  (Haskell infixl 4 "==")
   1.171 -
   1.172 -code_const "op ="
   1.173 -  (Haskell infixl 4 "==")
   1.174 -
   1.175 -
   1.176 -text {* type bool *}
   1.177 -
   1.178 -code_type bool
   1.179 -  (SML "bool")
   1.180 -  (OCaml "bool")
   1.181 -  (Haskell "Bool")
   1.182 -
   1.183 -code_const True and False and Not and "op &" and "op |" and If
   1.184 -  (SML "true" and "false" and "not"
   1.185 -    and infixl 1 "andalso" and infixl 0 "orelse"
   1.186 -    and "!(if (_)/ then (_)/ else (_))")
   1.187 -  (OCaml "true" and "false" and "not"
   1.188 -    and infixl 4 "&&" and infixl 2 "||"
   1.189 -    and "!(if (_)/ then (_)/ else (_))")
   1.190 -  (Haskell "True" and "False" and "not"
   1.191 -    and infixl 3 "&&" and infixl 2 "||"
   1.192 -    and "!(if (_)/ then (_)/ else (_))")
   1.193 -
   1.194 -code_reserved SML
   1.195 -  bool true false not
   1.196 -
   1.197 -code_reserved OCaml
   1.198 -  bool not
   1.199 -
   1.200 -
   1.201 -text {* code generation for undefined as exception *}
   1.202 -
   1.203 -code_abort undefined
   1.204 -
   1.205 -code_const undefined
   1.206 -  (SML "raise/ Fail/ \"undefined\"")
   1.207 -  (OCaml "failwith/ \"undefined\"")
   1.208 -  (Haskell "error/ \"undefined\"")
   1.209 -
   1.210 -
   1.211 -subsection {* Evaluation oracle *}
   1.212 +subsection {* Evaluation and normalization by evaluation *}
   1.213  
   1.214  ML {*
   1.215  structure Eval_Method =
   1.216 @@ -155,7 +223,10 @@
   1.217  *} "solve goal by evaluation"
   1.218  
   1.219  
   1.220 -subsection {* Normalization by evaluation *}
   1.221 +method_setup evaluation = {*
   1.222 +  Method.no_args (Method.SIMPLE_METHOD' (CONVERSION Codegen.evaluation_conv THEN' rtac TrueI))
   1.223 +*} "solve goal by evaluation"
   1.224 +
   1.225  
   1.226  method_setup normalization = {*
   1.227    Method.no_args (Method.SIMPLE_METHOD'
   1.228 @@ -164,4 +235,9 @@
   1.229    ))
   1.230  *} "solve goal by normalization"
   1.231  
   1.232 +
   1.233 +subsection {* Quickcheck *}
   1.234 +
   1.235 +quickcheck_params [size = 5, iterations = 50]
   1.236 +
   1.237  end
     2.1 --- a/src/HOL/HOL.thy	Mon Sep 29 12:31:56 2008 +0200
     2.2 +++ b/src/HOL/HOL.thy	Mon Sep 29 12:31:57 2008 +0200
     2.3 @@ -35,6 +35,7 @@
     2.4    "~~/src/Tools/code/code_ml.ML"
     2.5    "~~/src/Tools/code/code_haskell.ML"
     2.6    "~~/src/Tools/nbe.ML"
     2.7 +  ("~~/src/HOL/Tools/recfun_codegen.ML")
     2.8  begin
     2.9  
    2.10  subsection {* Primitive logic *}
    2.11 @@ -1678,88 +1679,37 @@
    2.12  *}
    2.13  
    2.14  
    2.15 -subsection {* Code generator basic setup -- see further @{text Code_Setup.thy} *}
    2.16 +subsection {* Code generator basics -- see further theory @{text "Code_Setup"} *}
    2.17 +
    2.18 +text {* Module setup *}
    2.19 +
    2.20 +use "~~/src/HOL/Tools/recfun_codegen.ML"
    2.21  
    2.22  setup {*
    2.23 -  Code.map_pre (K HOL_basic_ss)
    2.24 -  #> Code.map_post (K HOL_basic_ss)
    2.25 +  Code_Name.setup
    2.26 +  #> Code_ML.setup
    2.27 +  #> Code_Haskell.setup
    2.28 +  #> Nbe.setup
    2.29 +  #> Codegen.setup
    2.30 +  #> RecfunCodegen.setup
    2.31  *}
    2.32  
    2.33 -code_datatype True False
    2.34  
    2.35 -code_datatype "TYPE('a\<Colon>{})"
    2.36 -
    2.37 -code_datatype Trueprop "prop"
    2.38 -
    2.39 -lemma Let_case_cert:
    2.40 -  assumes "CASE \<equiv> (\<lambda>x. Let x f)"
    2.41 -  shows "CASE x \<equiv> f x"
    2.42 -  using assms by simp_all
    2.43 -
    2.44 -lemma If_case_cert:
    2.45 -  includes meta_conjunction_syntax
    2.46 -  assumes "CASE \<equiv> (\<lambda>b. If b f g)"
    2.47 -  shows "(CASE True \<equiv> f) && (CASE False \<equiv> g)"
    2.48 -  using assms by simp_all
    2.49 -
    2.50 -setup {*
    2.51 -  Code.add_case @{thm Let_case_cert}
    2.52 -  #> Code.add_case @{thm If_case_cert}
    2.53 -  #> Code.add_undefined @{const_name undefined}
    2.54 -*}
    2.55 +text {* Equality *}
    2.56  
    2.57  class eq = type +
    2.58    fixes eq :: "'a \<Rightarrow> 'a \<Rightarrow> bool"
    2.59 -  assumes eq_equals: "eq x y \<longleftrightarrow> x = y "
    2.60 +  assumes eq_equals: "eq x y \<longleftrightarrow> x = y"
    2.61  begin
    2.62  
    2.63  lemma eq: "eq = (op =)"
    2.64    by (rule ext eq_equals)+
    2.65  
    2.66 -lemma equals_eq [code inline, code func]: "op = \<equiv> eq"
    2.67 -  by (rule eq_reflection) (rule ext, rule ext, rule sym, rule eq_equals)
    2.68 -
    2.69 -declare equals_eq [symmetric, code post]
    2.70 -
    2.71  lemma eq_refl: "eq x x \<longleftrightarrow> True"
    2.72    unfolding eq by rule+
    2.73  
    2.74  end
    2.75  
    2.76 -declare simp_thms(6) [code nbe]
    2.77 -
    2.78 -hide (open) const eq
    2.79 -hide const eq
    2.80 -
    2.81 -setup {*
    2.82 -  Code_Unit.add_const_alias @{thm equals_eq}
    2.83 -  #> Code_Name.setup
    2.84 -  #> Code_ML.setup
    2.85 -  #> Code_Haskell.setup
    2.86 -  #> Nbe.setup
    2.87 -  #> Codegen.setup
    2.88 -*}
    2.89 -
    2.90 -lemma [code func]:
    2.91 -  shows "False \<and> x \<longleftrightarrow> False"
    2.92 -    and "True \<and> x \<longleftrightarrow> x"
    2.93 -    and "x \<and> False \<longleftrightarrow> False"
    2.94 -    and "x \<and> True \<longleftrightarrow> x" by simp_all
    2.95 -
    2.96 -lemma [code func]:
    2.97 -  shows "False \<or> x \<longleftrightarrow> x"
    2.98 -    and "True \<or> x \<longleftrightarrow> True"
    2.99 -    and "x \<or> False \<longleftrightarrow> x"
   2.100 -    and "x \<or> True \<longleftrightarrow> True" by simp_all
   2.101 -
   2.102 -lemma [code func]:
   2.103 -  shows "\<not> True \<longleftrightarrow> False"
   2.104 -    and "\<not> False \<longleftrightarrow> True" by (rule HOL.simp_thms)+
   2.105 -
   2.106 -lemmas [code func] = Let_def if_True if_False
   2.107 -
   2.108 -lemmas [code func, code unfold, symmetric, code post] = imp_conv_disj
   2.109 -
   2.110  
   2.111  subsection {* Legacy tactics and ML bindings *}
   2.112