# HG changeset patch # User haftmann # Date 1239803557 -7200 # Node ID d9343c0aac11b3577060d80d4dd24afd8d2ff7ad # Parent 983dfcce45ad945a3c0714e58fad583a78d9b8c5 code generator bootstrap theory src/Tools/Code_Generator.thy diff -r 983dfcce45ad -r d9343c0aac11 src/HOL/Code_Setup.thy --- a/src/HOL/Code_Setup.thy Wed Apr 15 15:38:30 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 diff -r 983dfcce45ad -r d9343c0aac11 src/HOL/HOL.thy --- a/src/HOL/HOL.thy Wed Apr 15 15:38:30 2009 +0200 +++ b/src/HOL/HOL.thy Wed Apr 15 15:52:37 2009 +0200 @@ -5,7 +5,7 @@ header {* The basis of Higher-Order Logic *} theory HOL -imports Pure +imports Pure "~~/src/Tools/Code_Generator" uses ("Tools/hologic.ML") "~~/src/Tools/IsaPlanner/zipper.ML" @@ -27,15 +27,6 @@ "~~/src/Tools/atomize_elim.ML" "~~/src/Tools/induct.ML" ("~~/src/Tools/induct_tacs.ML") - "~~/src/Tools/value.ML" - "~~/src/Tools/code/code_name.ML" - "~~/src/Tools/code/code_wellsorted.ML" - "~~/src/Tools/code/code_thingol.ML" - "~~/src/Tools/code/code_printer.ML" - "~~/src/Tools/code/code_target.ML" - "~~/src/Tools/code/code_ml.ML" - "~~/src/Tools/code/code_haskell.ML" - "~~/src/Tools/nbe.ML" ("Tools/recfun_codegen.ML") begin @@ -1673,35 +1664,259 @@ *} -subsection {* Code generator basics -- see further theory @{text "Code_Setup"} *} +subsection {* Code generator setup *} + +subsubsection {* SML code generator setup *} + +use "Tools/recfun_codegen.ML" + +setup {* + Codegen.setup + #> RecfunCodegen.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); +*} -text {* Equality *} +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 +*} + +subsubsection {* Equality *} class eq = fixes eq :: "'a \ 'a \ bool" assumes eq_equals: "eq x y \ x = y" begin -lemma eq: "eq = (op =)" +lemma eq [code unfold, code inline del]: "eq = (op =)" by (rule ext eq_equals)+ lemma eq_refl: "eq x x \ True" unfolding eq by rule+ +lemma equals_eq [code inline, code]: "(op =) \ eq" + by (rule eq_reflection) (rule ext, rule ext, rule sym, rule eq_equals) + +declare equals_eq [symmetric, code post] + end -text {* Module setup *} +subsubsection {* 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)+ -use "Tools/recfun_codegen.ML" +lemmas [code] = Let_def if_True if_False + +lemmas [code, code unfold, symmetric, code post] = imp_conv_disj + +text {* Equality *} + +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 + +subsubsection {* Generic code generator preprocessor *} setup {* - Code_ML.setup - #> Code_Haskell.setup - #> Nbe.setup - #> Codegen.setup - #> RecfunCodegen.setup + Code.map_pre (K HOL_basic_ss) + #> Code.map_post (K HOL_basic_ss) *} +subsubsection {* 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\"") + +subsubsection {* 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" + +subsubsection {* Quickcheck *} + +setup {* + Quickcheck.add_generator ("SML", Codegen.test_term) +*} + +quickcheck_params [size = 5, iterations = 50] + subsection {* Nitpick hooks *} diff -r 983dfcce45ad -r d9343c0aac11 src/HOL/IsaMakefile --- a/src/HOL/IsaMakefile Wed Apr 15 15:38:30 2009 +0200 +++ b/src/HOL/IsaMakefile Wed Apr 15 15:52:37 2009 +0200 @@ -105,7 +105,7 @@ $(SRC)/Tools/project_rule.ML \ $(SRC)/Tools/random_word.ML \ $(SRC)/Tools/value.ML \ - Code_Setup.thy \ + $(SRC)/Tools/Code_Generator.thy \ HOL.thy \ Tools/hologic.ML \ Tools/recfun_codegen.ML \ diff -r 983dfcce45ad -r d9343c0aac11 src/HOL/Orderings.thy --- a/src/HOL/Orderings.thy Wed Apr 15 15:38:30 2009 +0200 +++ b/src/HOL/Orderings.thy Wed Apr 15 15:52:37 2009 +0200 @@ -5,7 +5,7 @@ header {* Abstract orderings *} theory Orderings -imports Code_Setup +imports HOL uses "~~/src/Provers/order.ML" begin diff -r 983dfcce45ad -r d9343c0aac11 src/HOL/base.ML --- a/src/HOL/base.ML Wed Apr 15 15:38:30 2009 +0200 +++ b/src/HOL/base.ML Wed Apr 15 15:52:37 2009 +0200 @@ -1,2 +1,2 @@ (*side-entry for HOL-Base*) -use_thy "Code_Setup"; +use_thy "HOL"; diff -r 983dfcce45ad -r d9343c0aac11 src/Tools/Code_Generator.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Tools/Code_Generator.thy Wed Apr 15 15:52:37 2009 +0200 @@ -0,0 +1,27 @@ +(* Title: Tools/Code_Generator.thy + Author: Florian Haftmann, TU Muenchen +*) + +header {* Loading the code generator modules *} + +theory Code_Generator +imports Pure +uses + "~~/src/Tools/value.ML" + "~~/src/Tools/code/code_name.ML" + "~~/src/Tools/code/code_wellsorted.ML" + "~~/src/Tools/code/code_thingol.ML" + "~~/src/Tools/code/code_printer.ML" + "~~/src/Tools/code/code_target.ML" + "~~/src/Tools/code/code_ml.ML" + "~~/src/Tools/code/code_haskell.ML" + "~~/src/Tools/nbe.ML" +begin + +setup {* + Code_ML.setup + #> Code_Haskell.setup + #> Nbe.setup +*} + +end \ No newline at end of file