code generator bootstrap theory src/Tools/Code_Generator.thy
authorhaftmann
Wed Apr 15 15:52:37 2009 +0200 (2009-04-15)
changeset 30929d9343c0aac11
parent 30928 983dfcce45ad
child 30930 11010e5f18f0
code generator bootstrap theory src/Tools/Code_Generator.thy
src/HOL/Code_Setup.thy
src/HOL/HOL.thy
src/HOL/IsaMakefile
src/HOL/Orderings.thy
src/HOL/base.ML
src/Tools/Code_Generator.thy
     1.1 --- a/src/HOL/Code_Setup.thy	Wed Apr 15 15:38:30 2009 +0200
     1.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.3 @@ -1,253 +0,0 @@
     1.4 -(*  Title:      HOL/Code_Setup.thy
     1.5 -    ID:         $Id$
     1.6 -    Author:     Florian Haftmann
     1.7 -*)
     1.8 -
     1.9 -header {* Setup of code generators and related tools *}
    1.10 -
    1.11 -theory Code_Setup
    1.12 -imports HOL
    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]:
    1.28 -  shows "(True \<Longrightarrow> PROP P) \<equiv> PROP P" 
    1.29 -    and "(False \<Longrightarrow> Q) \<equiv> Trueprop True" 
    1.30 -    and "(PROP P \<Longrightarrow> True) \<equiv> Trueprop True" 
    1.31 -    and "(Q \<Longrightarrow> False) \<equiv> Trueprop (\<not> Q)" by (auto intro!: equal_intr_rule)
    1.32 -
    1.33 -lemma [code]:
    1.34 -  shows "False \<and> x \<longleftrightarrow> False"
    1.35 -    and "True \<and> x \<longleftrightarrow> x"
    1.36 -    and "x \<and> False \<longleftrightarrow> False"
    1.37 -    and "x \<and> True \<longleftrightarrow> x" by simp_all
    1.38 -
    1.39 -lemma [code]:
    1.40 -  shows "False \<or> x \<longleftrightarrow> x"
    1.41 -    and "True \<or> x \<longleftrightarrow> True"
    1.42 -    and "x \<or> False \<longleftrightarrow> x"
    1.43 -    and "x \<or> True \<longleftrightarrow> True" by simp_all
    1.44 -
    1.45 -lemma [code]:
    1.46 -  shows "\<not> True \<longleftrightarrow> False"
    1.47 -    and "\<not> False \<longleftrightarrow> True" by (rule HOL.simp_thms)+
    1.48 -
    1.49 -lemmas [code] = Let_def if_True if_False
    1.50 -
    1.51 -lemmas [code, code unfold, symmetric, code post] = imp_conv_disj
    1.52 -
    1.53 -text {* Equality *}
    1.54 -
    1.55 -context eq
    1.56 -begin
    1.57 -
    1.58 -lemma equals_eq [code inline, code]: "op = \<equiv> eq"
    1.59 -  by (rule eq_reflection) (rule ext, rule ext, rule sym, rule eq_equals)
    1.60 -
    1.61 -declare eq [code unfold, code inline del]
    1.62 -
    1.63 -declare equals_eq [symmetric, code post]
    1.64 -
    1.65 -end
    1.66 -
    1.67 -declare simp_thms(6) [code nbe]
    1.68 -
    1.69 -hide (open) const eq
    1.70 -hide const eq
    1.71 -
    1.72 -setup {*
    1.73 -  Code_Unit.add_const_alias @{thm equals_eq}
    1.74 -*}
    1.75 -
    1.76 -text {* Cases *}
    1.77 -
    1.78 -lemma Let_case_cert:
    1.79 -  assumes "CASE \<equiv> (\<lambda>x. Let x f)"
    1.80 -  shows "CASE x \<equiv> f x"
    1.81 -  using assms by simp_all
    1.82 -
    1.83 -lemma If_case_cert:
    1.84 -  assumes "CASE \<equiv> (\<lambda>b. If b f g)"
    1.85 -  shows "(CASE True \<equiv> f) &&& (CASE False \<equiv> g)"
    1.86 -  using assms by simp_all
    1.87 -
    1.88 -setup {*
    1.89 -  Code.add_case @{thm Let_case_cert}
    1.90 -  #> Code.add_case @{thm If_case_cert}
    1.91 -  #> Code.add_undefined @{const_name undefined}
    1.92 -*}
    1.93 -
    1.94 -code_abort undefined
    1.95 -
    1.96 -
    1.97 -subsection {* Generic code generator preprocessor *}
    1.98 -
    1.99 -setup {*
   1.100 -  Code.map_pre (K HOL_basic_ss)
   1.101 -  #> Code.map_post (K HOL_basic_ss)
   1.102 -*}
   1.103 -
   1.104 -
   1.105 -subsection {* Generic code generator target languages *}
   1.106 -
   1.107 -text {* type bool *}
   1.108 -
   1.109 -code_type bool
   1.110 -  (SML "bool")
   1.111 -  (OCaml "bool")
   1.112 -  (Haskell "Bool")
   1.113 -
   1.114 -code_const True and False and Not and "op &" and "op |" and If
   1.115 -  (SML "true" and "false" and "not"
   1.116 -    and infixl 1 "andalso" and infixl 0 "orelse"
   1.117 -    and "!(if (_)/ then (_)/ else (_))")
   1.118 -  (OCaml "true" and "false" and "not"
   1.119 -    and infixl 4 "&&" and infixl 2 "||"
   1.120 -    and "!(if (_)/ then (_)/ else (_))")
   1.121 -  (Haskell "True" and "False" and "not"
   1.122 -    and infixl 3 "&&" and infixl 2 "||"
   1.123 -    and "!(if (_)/ then (_)/ else (_))")
   1.124 -
   1.125 -code_reserved SML
   1.126 -  bool true false not
   1.127 -
   1.128 -code_reserved OCaml
   1.129 -  bool not
   1.130 -
   1.131 -text {* using built-in Haskell equality *}
   1.132 -
   1.133 -code_class eq
   1.134 -  (Haskell "Eq")
   1.135 -
   1.136 -code_const "eq_class.eq"
   1.137 -  (Haskell infixl 4 "==")
   1.138 -
   1.139 -code_const "op ="
   1.140 -  (Haskell infixl 4 "==")
   1.141 -
   1.142 -text {* undefined *}
   1.143 -
   1.144 -code_const undefined
   1.145 -  (SML "!(raise/ Fail/ \"undefined\")")
   1.146 -  (OCaml "failwith/ \"undefined\"")
   1.147 -  (Haskell "error/ \"undefined\"")
   1.148 -
   1.149 -
   1.150 -subsection {* SML code generator setup *}
   1.151 -
   1.152 -types_code
   1.153 -  "bool"  ("bool")
   1.154 -attach (term_of) {*
   1.155 -fun term_of_bool b = if b then HOLogic.true_const else HOLogic.false_const;
   1.156 -*}
   1.157 -attach (test) {*
   1.158 -fun gen_bool i =
   1.159 -  let val b = one_of [false, true]
   1.160 -  in (b, fn () => term_of_bool b) end;
   1.161 -*}
   1.162 -  "prop"  ("bool")
   1.163 -attach (term_of) {*
   1.164 -fun term_of_prop b =
   1.165 -  HOLogic.mk_Trueprop (if b then HOLogic.true_const else HOLogic.false_const);
   1.166 -*}
   1.167 -
   1.168 -consts_code
   1.169 -  "Trueprop" ("(_)")
   1.170 -  "True"    ("true")
   1.171 -  "False"   ("false")
   1.172 -  "Not"     ("Bool.not")
   1.173 -  "op |"    ("(_ orelse/ _)")
   1.174 -  "op &"    ("(_ andalso/ _)")
   1.175 -  "If"      ("(if _/ then _/ else _)")
   1.176 -
   1.177 -setup {*
   1.178 -let
   1.179 -
   1.180 -fun eq_codegen thy defs dep thyname b t gr =
   1.181 -    (case strip_comb t of
   1.182 -       (Const ("op =", Type (_, [Type ("fun", _), _])), _) => NONE
   1.183 -     | (Const ("op =", _), [t, u]) =>
   1.184 -          let
   1.185 -            val (pt, gr') = Codegen.invoke_codegen thy defs dep thyname false t gr;
   1.186 -            val (pu, gr'') = Codegen.invoke_codegen thy defs dep thyname false u gr';
   1.187 -            val (_, gr''') = Codegen.invoke_tycodegen thy defs dep thyname false HOLogic.boolT gr'';
   1.188 -          in
   1.189 -            SOME (Codegen.parens
   1.190 -              (Pretty.block [pt, Codegen.str " =", Pretty.brk 1, pu]), gr''')
   1.191 -          end
   1.192 -     | (t as Const ("op =", _), ts) => SOME (Codegen.invoke_codegen
   1.193 -         thy defs dep thyname b (Codegen.eta_expand t ts 2) gr)
   1.194 -     | _ => NONE);
   1.195 -
   1.196 -in
   1.197 -  Codegen.add_codegen "eq_codegen" eq_codegen
   1.198 -end
   1.199 -*}
   1.200 -
   1.201 -
   1.202 -subsection {* Evaluation and normalization by evaluation *}
   1.203 -
   1.204 -setup {*
   1.205 -  Value.add_evaluator ("SML", Codegen.eval_term o ProofContext.theory_of)
   1.206 -*}
   1.207 -
   1.208 -ML {*
   1.209 -structure Eval_Method =
   1.210 -struct
   1.211 -
   1.212 -val eval_ref : (unit -> bool) option ref = ref NONE;
   1.213 -
   1.214 -end;
   1.215 -*}
   1.216 -
   1.217 -oracle eval_oracle = {* fn ct =>
   1.218 -  let
   1.219 -    val thy = Thm.theory_of_cterm ct;
   1.220 -    val t = Thm.term_of ct;
   1.221 -    val dummy = @{cprop True};
   1.222 -  in case try HOLogic.dest_Trueprop t
   1.223 -   of SOME t' => if Code_ML.eval_term
   1.224 -         ("Eval_Method.eval_ref", Eval_Method.eval_ref) thy t' [] 
   1.225 -       then Thm.capply (Thm.capply @{cterm "op \<equiv> \<Colon> prop \<Rightarrow> prop \<Rightarrow> prop"} ct) dummy
   1.226 -       else dummy
   1.227 -    | NONE => dummy
   1.228 -  end
   1.229 -*}
   1.230 -
   1.231 -ML {*
   1.232 -fun gen_eval_method conv ctxt = SIMPLE_METHOD'
   1.233 -  (CONVERSION (Conv.params_conv (~1) (K (Conv.concl_conv (~1) conv)) ctxt)
   1.234 -    THEN' rtac TrueI)
   1.235 -*}
   1.236 -
   1.237 -method_setup eval = {* Scan.succeed (gen_eval_method eval_oracle) *}
   1.238 -  "solve goal by evaluation"
   1.239 -
   1.240 -method_setup evaluation = {* Scan.succeed (gen_eval_method Codegen.evaluation_conv) *}
   1.241 -  "solve goal by evaluation"
   1.242 -
   1.243 -method_setup normalization = {*
   1.244 -  Scan.succeed (K (SIMPLE_METHOD' (CONVERSION Nbe.norm_conv THEN' (fn k => TRY (rtac TrueI k)))))
   1.245 -*} "solve goal by normalization"
   1.246 -
   1.247 -
   1.248 -subsection {* Quickcheck *}
   1.249 -
   1.250 -setup {*
   1.251 -  Quickcheck.add_generator ("SML", Codegen.test_term)
   1.252 -*}
   1.253 -
   1.254 -quickcheck_params [size = 5, iterations = 50]
   1.255 -
   1.256 -end
     2.1 --- a/src/HOL/HOL.thy	Wed Apr 15 15:38:30 2009 +0200
     2.2 +++ b/src/HOL/HOL.thy	Wed Apr 15 15:52:37 2009 +0200
     2.3 @@ -5,7 +5,7 @@
     2.4  header {* The basis of Higher-Order Logic *}
     2.5  
     2.6  theory HOL
     2.7 -imports Pure
     2.8 +imports Pure "~~/src/Tools/Code_Generator"
     2.9  uses
    2.10    ("Tools/hologic.ML")
    2.11    "~~/src/Tools/IsaPlanner/zipper.ML"
    2.12 @@ -27,15 +27,6 @@
    2.13    "~~/src/Tools/atomize_elim.ML"
    2.14    "~~/src/Tools/induct.ML"
    2.15    ("~~/src/Tools/induct_tacs.ML")
    2.16 -  "~~/src/Tools/value.ML"
    2.17 -  "~~/src/Tools/code/code_name.ML"
    2.18 -  "~~/src/Tools/code/code_wellsorted.ML" 
    2.19 -  "~~/src/Tools/code/code_thingol.ML"
    2.20 -  "~~/src/Tools/code/code_printer.ML"
    2.21 -  "~~/src/Tools/code/code_target.ML"
    2.22 -  "~~/src/Tools/code/code_ml.ML"
    2.23 -  "~~/src/Tools/code/code_haskell.ML"
    2.24 -  "~~/src/Tools/nbe.ML"
    2.25    ("Tools/recfun_codegen.ML")
    2.26  begin
    2.27  
    2.28 @@ -1673,35 +1664,259 @@
    2.29  *}
    2.30  
    2.31  
    2.32 -subsection {* Code generator basics -- see further theory @{text "Code_Setup"} *}
    2.33 +subsection {* Code generator setup *}
    2.34 +
    2.35 +subsubsection {* SML code generator setup *}
    2.36 +
    2.37 +use "Tools/recfun_codegen.ML"
    2.38 +
    2.39 +setup {*
    2.40 +  Codegen.setup
    2.41 +  #> RecfunCodegen.setup
    2.42 +*}
    2.43 +
    2.44 +types_code
    2.45 +  "bool"  ("bool")
    2.46 +attach (term_of) {*
    2.47 +fun term_of_bool b = if b then HOLogic.true_const else HOLogic.false_const;
    2.48 +*}
    2.49 +attach (test) {*
    2.50 +fun gen_bool i =
    2.51 +  let val b = one_of [false, true]
    2.52 +  in (b, fn () => term_of_bool b) end;
    2.53 +*}
    2.54 +  "prop"  ("bool")
    2.55 +attach (term_of) {*
    2.56 +fun term_of_prop b =
    2.57 +  HOLogic.mk_Trueprop (if b then HOLogic.true_const else HOLogic.false_const);
    2.58 +*}
    2.59  
    2.60 -text {* Equality *}
    2.61 +consts_code
    2.62 +  "Trueprop" ("(_)")
    2.63 +  "True"    ("true")
    2.64 +  "False"   ("false")
    2.65 +  "Not"     ("Bool.not")
    2.66 +  "op |"    ("(_ orelse/ _)")
    2.67 +  "op &"    ("(_ andalso/ _)")
    2.68 +  "If"      ("(if _/ then _/ else _)")
    2.69 +
    2.70 +setup {*
    2.71 +let
    2.72 +
    2.73 +fun eq_codegen thy defs dep thyname b t gr =
    2.74 +    (case strip_comb t of
    2.75 +       (Const ("op =", Type (_, [Type ("fun", _), _])), _) => NONE
    2.76 +     | (Const ("op =", _), [t, u]) =>
    2.77 +          let
    2.78 +            val (pt, gr') = Codegen.invoke_codegen thy defs dep thyname false t gr;
    2.79 +            val (pu, gr'') = Codegen.invoke_codegen thy defs dep thyname false u gr';
    2.80 +            val (_, gr''') = Codegen.invoke_tycodegen thy defs dep thyname false HOLogic.boolT gr'';
    2.81 +          in
    2.82 +            SOME (Codegen.parens
    2.83 +              (Pretty.block [pt, Codegen.str " =", Pretty.brk 1, pu]), gr''')
    2.84 +          end
    2.85 +     | (t as Const ("op =", _), ts) => SOME (Codegen.invoke_codegen
    2.86 +         thy defs dep thyname b (Codegen.eta_expand t ts 2) gr)
    2.87 +     | _ => NONE);
    2.88 +
    2.89 +in
    2.90 +  Codegen.add_codegen "eq_codegen" eq_codegen
    2.91 +end
    2.92 +*}
    2.93 +
    2.94 +subsubsection {* Equality *}
    2.95  
    2.96  class eq =
    2.97    fixes eq :: "'a \<Rightarrow> 'a \<Rightarrow> bool"
    2.98    assumes eq_equals: "eq x y \<longleftrightarrow> x = y"
    2.99  begin
   2.100  
   2.101 -lemma eq: "eq = (op =)"
   2.102 +lemma eq [code unfold, code inline del]: "eq = (op =)"
   2.103    by (rule ext eq_equals)+
   2.104  
   2.105  lemma eq_refl: "eq x x \<longleftrightarrow> True"
   2.106    unfolding eq by rule+
   2.107  
   2.108 +lemma equals_eq [code inline, code]: "(op =) \<equiv> eq"
   2.109 +  by (rule eq_reflection) (rule ext, rule ext, rule sym, rule eq_equals)
   2.110 +
   2.111 +declare equals_eq [symmetric, code post]
   2.112 +
   2.113  end
   2.114  
   2.115 -text {* Module setup *}
   2.116 +subsubsection {* Generic code generator foundation *}
   2.117 +
   2.118 +text {* Datatypes *}
   2.119 +
   2.120 +code_datatype True False
   2.121 +
   2.122 +code_datatype "TYPE('a\<Colon>{})"
   2.123 +
   2.124 +code_datatype Trueprop "prop"
   2.125 +
   2.126 +text {* Code equations *}
   2.127 +
   2.128 +lemma [code]:
   2.129 +  shows "(True \<Longrightarrow> PROP P) \<equiv> PROP P" 
   2.130 +    and "(False \<Longrightarrow> Q) \<equiv> Trueprop True" 
   2.131 +    and "(PROP P \<Longrightarrow> True) \<equiv> Trueprop True" 
   2.132 +    and "(Q \<Longrightarrow> False) \<equiv> Trueprop (\<not> Q)" by (auto intro!: equal_intr_rule)
   2.133 +
   2.134 +lemma [code]:
   2.135 +  shows "False \<and> x \<longleftrightarrow> False"
   2.136 +    and "True \<and> x \<longleftrightarrow> x"
   2.137 +    and "x \<and> False \<longleftrightarrow> False"
   2.138 +    and "x \<and> True \<longleftrightarrow> x" by simp_all
   2.139 +
   2.140 +lemma [code]:
   2.141 +  shows "False \<or> x \<longleftrightarrow> x"
   2.142 +    and "True \<or> x \<longleftrightarrow> True"
   2.143 +    and "x \<or> False \<longleftrightarrow> x"
   2.144 +    and "x \<or> True \<longleftrightarrow> True" by simp_all
   2.145 +
   2.146 +lemma [code]:
   2.147 +  shows "\<not> True \<longleftrightarrow> False"
   2.148 +    and "\<not> False \<longleftrightarrow> True" by (rule HOL.simp_thms)+
   2.149  
   2.150 -use "Tools/recfun_codegen.ML"
   2.151 +lemmas [code] = Let_def if_True if_False
   2.152 +
   2.153 +lemmas [code, code unfold, symmetric, code post] = imp_conv_disj
   2.154 +
   2.155 +text {* Equality *}
   2.156 +
   2.157 +declare simp_thms(6) [code nbe]
   2.158 +
   2.159 +hide (open) const eq
   2.160 +hide const eq
   2.161 +
   2.162 +setup {*
   2.163 +  Code_Unit.add_const_alias @{thm equals_eq}
   2.164 +*}
   2.165 +
   2.166 +text {* Cases *}
   2.167 +
   2.168 +lemma Let_case_cert:
   2.169 +  assumes "CASE \<equiv> (\<lambda>x. Let x f)"
   2.170 +  shows "CASE x \<equiv> f x"
   2.171 +  using assms by simp_all
   2.172 +
   2.173 +lemma If_case_cert:
   2.174 +  assumes "CASE \<equiv> (\<lambda>b. If b f g)"
   2.175 +  shows "(CASE True \<equiv> f) &&& (CASE False \<equiv> g)"
   2.176 +  using assms by simp_all
   2.177 +
   2.178 +setup {*
   2.179 +  Code.add_case @{thm Let_case_cert}
   2.180 +  #> Code.add_case @{thm If_case_cert}
   2.181 +  #> Code.add_undefined @{const_name undefined}
   2.182 +*}
   2.183 +
   2.184 +code_abort undefined
   2.185 +
   2.186 +subsubsection {* Generic code generator preprocessor *}
   2.187  
   2.188  setup {*
   2.189 -  Code_ML.setup
   2.190 -  #> Code_Haskell.setup
   2.191 -  #> Nbe.setup
   2.192 -  #> Codegen.setup
   2.193 -  #> RecfunCodegen.setup
   2.194 +  Code.map_pre (K HOL_basic_ss)
   2.195 +  #> Code.map_post (K HOL_basic_ss)
   2.196  *}
   2.197  
   2.198 +subsubsection {* Generic code generator target languages *}
   2.199 +
   2.200 +text {* type bool *}
   2.201 +
   2.202 +code_type bool
   2.203 +  (SML "bool")
   2.204 +  (OCaml "bool")
   2.205 +  (Haskell "Bool")
   2.206 +
   2.207 +code_const True and False and Not and "op &" and "op |" and If
   2.208 +  (SML "true" and "false" and "not"
   2.209 +    and infixl 1 "andalso" and infixl 0 "orelse"
   2.210 +    and "!(if (_)/ then (_)/ else (_))")
   2.211 +  (OCaml "true" and "false" and "not"
   2.212 +    and infixl 4 "&&" and infixl 2 "||"
   2.213 +    and "!(if (_)/ then (_)/ else (_))")
   2.214 +  (Haskell "True" and "False" and "not"
   2.215 +    and infixl 3 "&&" and infixl 2 "||"
   2.216 +    and "!(if (_)/ then (_)/ else (_))")
   2.217 +
   2.218 +code_reserved SML
   2.219 +  bool true false not
   2.220 +
   2.221 +code_reserved OCaml
   2.222 +  bool not
   2.223 +
   2.224 +text {* using built-in Haskell equality *}
   2.225 +
   2.226 +code_class eq
   2.227 +  (Haskell "Eq")
   2.228 +
   2.229 +code_const "eq_class.eq"
   2.230 +  (Haskell infixl 4 "==")
   2.231 +
   2.232 +code_const "op ="
   2.233 +  (Haskell infixl 4 "==")
   2.234 +
   2.235 +text {* undefined *}
   2.236 +
   2.237 +code_const undefined
   2.238 +  (SML "!(raise/ Fail/ \"undefined\")")
   2.239 +  (OCaml "failwith/ \"undefined\"")
   2.240 +  (Haskell "error/ \"undefined\"")
   2.241 +
   2.242 +subsubsection {* Evaluation and normalization by evaluation *}
   2.243 +
   2.244 +setup {*
   2.245 +  Value.add_evaluator ("SML", Codegen.eval_term o ProofContext.theory_of)
   2.246 +*}
   2.247 +
   2.248 +ML {*
   2.249 +structure Eval_Method =
   2.250 +struct
   2.251 +
   2.252 +val eval_ref : (unit -> bool) option ref = ref NONE;
   2.253 +
   2.254 +end;
   2.255 +*}
   2.256 +
   2.257 +oracle eval_oracle = {* fn ct =>
   2.258 +  let
   2.259 +    val thy = Thm.theory_of_cterm ct;
   2.260 +    val t = Thm.term_of ct;
   2.261 +    val dummy = @{cprop True};
   2.262 +  in case try HOLogic.dest_Trueprop t
   2.263 +   of SOME t' => if Code_ML.eval_term
   2.264 +         ("Eval_Method.eval_ref", Eval_Method.eval_ref) thy t' [] 
   2.265 +       then Thm.capply (Thm.capply @{cterm "op \<equiv> \<Colon> prop \<Rightarrow> prop \<Rightarrow> prop"} ct) dummy
   2.266 +       else dummy
   2.267 +    | NONE => dummy
   2.268 +  end
   2.269 +*}
   2.270 +
   2.271 +ML {*
   2.272 +fun gen_eval_method conv ctxt = SIMPLE_METHOD'
   2.273 +  (CONVERSION (Conv.params_conv (~1) (K (Conv.concl_conv (~1) conv)) ctxt)
   2.274 +    THEN' rtac TrueI)
   2.275 +*}
   2.276 +
   2.277 +method_setup eval = {* Scan.succeed (gen_eval_method eval_oracle) *}
   2.278 +  "solve goal by evaluation"
   2.279 +
   2.280 +method_setup evaluation = {* Scan.succeed (gen_eval_method Codegen.evaluation_conv) *}
   2.281 +  "solve goal by evaluation"
   2.282 +
   2.283 +method_setup normalization = {*
   2.284 +  Scan.succeed (K (SIMPLE_METHOD' (CONVERSION Nbe.norm_conv THEN' (fn k => TRY (rtac TrueI k)))))
   2.285 +*} "solve goal by normalization"
   2.286 +
   2.287 +subsubsection {* Quickcheck *}
   2.288 +
   2.289 +setup {*
   2.290 +  Quickcheck.add_generator ("SML", Codegen.test_term)
   2.291 +*}
   2.292 +
   2.293 +quickcheck_params [size = 5, iterations = 50]
   2.294 +
   2.295  
   2.296  subsection {* Nitpick hooks *}
   2.297  
     3.1 --- a/src/HOL/IsaMakefile	Wed Apr 15 15:38:30 2009 +0200
     3.2 +++ b/src/HOL/IsaMakefile	Wed Apr 15 15:52:37 2009 +0200
     3.3 @@ -105,7 +105,7 @@
     3.4    $(SRC)/Tools/project_rule.ML \
     3.5    $(SRC)/Tools/random_word.ML \
     3.6    $(SRC)/Tools/value.ML \
     3.7 -  Code_Setup.thy \
     3.8 +  $(SRC)/Tools/Code_Generator.thy \
     3.9    HOL.thy \
    3.10    Tools/hologic.ML \
    3.11    Tools/recfun_codegen.ML \
     4.1 --- a/src/HOL/Orderings.thy	Wed Apr 15 15:38:30 2009 +0200
     4.2 +++ b/src/HOL/Orderings.thy	Wed Apr 15 15:52:37 2009 +0200
     4.3 @@ -5,7 +5,7 @@
     4.4  header {* Abstract orderings *}
     4.5  
     4.6  theory Orderings
     4.7 -imports Code_Setup
     4.8 +imports HOL
     4.9  uses "~~/src/Provers/order.ML"
    4.10  begin
    4.11  
     5.1 --- a/src/HOL/base.ML	Wed Apr 15 15:38:30 2009 +0200
     5.2 +++ b/src/HOL/base.ML	Wed Apr 15 15:52:37 2009 +0200
     5.3 @@ -1,2 +1,2 @@
     5.4  (*side-entry for HOL-Base*)
     5.5 -use_thy "Code_Setup";
     5.6 +use_thy "HOL";
     6.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     6.2 +++ b/src/Tools/Code_Generator.thy	Wed Apr 15 15:52:37 2009 +0200
     6.3 @@ -0,0 +1,27 @@
     6.4 +(*  Title:   Tools/Code_Generator.thy
     6.5 +    Author:  Florian Haftmann, TU Muenchen
     6.6 +*)
     6.7 +
     6.8 +header {* Loading the code generator modules *}
     6.9 +
    6.10 +theory Code_Generator
    6.11 +imports Pure
    6.12 +uses
    6.13 +  "~~/src/Tools/value.ML"
    6.14 +  "~~/src/Tools/code/code_name.ML"
    6.15 +  "~~/src/Tools/code/code_wellsorted.ML" 
    6.16 +  "~~/src/Tools/code/code_thingol.ML"
    6.17 +  "~~/src/Tools/code/code_printer.ML"
    6.18 +  "~~/src/Tools/code/code_target.ML"
    6.19 +  "~~/src/Tools/code/code_ml.ML"
    6.20 +  "~~/src/Tools/code/code_haskell.ML"
    6.21 +  "~~/src/Tools/nbe.ML"
    6.22 +begin
    6.23 +
    6.24 +setup {*
    6.25 +  Code_ML.setup
    6.26 +  #> Code_Haskell.setup
    6.27 +  #> Nbe.setup
    6.28 +*}
    6.29 +
    6.30 +end
    6.31 \ No newline at end of file