# HG changeset patch # User haftmann # Date 1243950787 -7200 # Node ID d1cbf6393964940d76ae22131a82646877eb2a48 # Parent a48f9ef9de1559d6dd6d2dc5fe8ef0e16479c551 tuned code generator test theories diff -r a48f9ef9de15 -r d1cbf6393964 src/HOL/IsaMakefile --- a/src/HOL/IsaMakefile Tue Jun 02 15:53:05 2009 +0200 +++ b/src/HOL/IsaMakefile Tue Jun 02 15:53:07 2009 +0200 @@ -838,11 +838,12 @@ ex/Arith_Examples.thy \ ex/Arithmetic_Series_Complex.thy ex/BT.thy ex/BinEx.thy \ ex/Binary.thy ex/CTL.thy ex/Chinese.thy ex/Classical.thy \ - ex/CodegenSML_Test.thy ex/Codegenerator.thy \ - ex/Codegenerator_Pretty.thy ex/Coherent.thy \ + ex/CodegenSML_Test.thy ex/Codegenerator_Candidates.thy \ + ex/Codegenerator_Pretty.thy ex/Codegenerator_Test.thy \ + ex/Codegenerator_Pretty_Test.thy ex/Coherent.thy \ ex/Commutative_RingEx.thy ex/Commutative_Ring_Complete.thy \ ex/Efficient_Nat_examples.thy \ - ex/Eval_Examples.thy ex/ExecutableContent.thy \ + ex/Eval_Examples.thy \ ex/Formal_Power_Series_Examples.thy ex/Fundefs.thy \ ex/Groebner_Examples.thy ex/Guess.thy ex/HarmonicSeries.thy \ ex/Hebrew.thy ex/Hex_Bin_Examples.thy ex/Higher_Order_Logic.thy \ diff -r a48f9ef9de15 -r d1cbf6393964 src/HOL/ex/Codegenerator.thy --- a/src/HOL/ex/Codegenerator.thy Tue Jun 02 15:53:05 2009 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,27 +0,0 @@ -(* ID: $Id$ - Author: Florian Haftmann, TU Muenchen -*) - -header {* Tests and examples for code generator *} - -theory Codegenerator -imports ExecutableContent -begin - -ML {* (*FIXME get rid of this*) -nonfix union; -nonfix inter; -nonfix upto; -*} - -export_code * in SML module_name CodegenTest - in OCaml module_name CodegenTest file - - in Haskell file - - -ML {* -infix union; -infix inter; -infix 4 upto; -*} - -end diff -r a48f9ef9de15 -r d1cbf6393964 src/HOL/ex/Codegenerator_Candidates.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/ex/Codegenerator_Candidates.thy Tue Jun 02 15:53:07 2009 +0200 @@ -0,0 +1,44 @@ + +(* Author: Florian Haftmann, TU Muenchen *) + +header {* A huge collection of equations to generate code from *} + +theory Codegenerator_Candidates +imports + Complex_Main + AssocList + Binomial + Commutative_Ring + Enum + List_Prefix + Nat_Infinity + Nested_Environment + Option_ord + Permutation + Primes + Product_ord + SetsAndFunctions + While_Combinator + Word + "~~/src/HOL/ex/Commutative_Ring_Complete" + "~~/src/HOL/ex/Records" +begin + +(*temporary Haskell workaround*) +declare typerep_fun_def [code inline] +declare typerep_prod_def [code inline] +declare typerep_sum_def [code inline] +declare typerep_cpoint_ext_type_def [code inline] +declare typerep_itself_def [code inline] +declare typerep_list_def [code inline] +declare typerep_option_def [code inline] +declare typerep_point_ext_type_def [code inline] +declare typerep_point'_ext_type_def [code inline] +declare typerep_point''_ext_type_def [code inline] +declare typerep_pol_def [code inline] +declare typerep_polex_def [code inline] + +(*avoid popular infixes*) +code_reserved SML union inter upto + +end diff -r a48f9ef9de15 -r d1cbf6393964 src/HOL/ex/Codegenerator_Pretty.thy --- a/src/HOL/ex/Codegenerator_Pretty.thy Tue Jun 02 15:53:05 2009 +0200 +++ b/src/HOL/ex/Codegenerator_Pretty.thy Tue Jun 02 15:53:07 2009 +0200 @@ -1,29 +1,12 @@ -(* Title: HOL/ex/Codegenerator_Pretty.thy - Author: Florian Haftmann, TU Muenchen -*) -header {* Simple examples for pretty numerals and such *} +(* Author: Florian Haftmann, TU Muenchen *) + +header {* Generating code using pretty literals and natural number literals *} theory Codegenerator_Pretty -imports ExecutableContent Code_Char Efficient_Nat +imports "~~/src/HOL/ex/Codegenerator_Candidates" Code_Char Efficient_Nat begin declare isnorm.simps [code del] -ML {* (*FIXME get rid of this*) -nonfix union; -nonfix inter; -nonfix upto; -*} - -export_code * in SML module_name CodegenTest - in OCaml module_name CodegenTest file - - in Haskell file - - -ML {* -infix union; -infix inter; -infix 4 upto; -*} - end diff -r a48f9ef9de15 -r d1cbf6393964 src/HOL/ex/Codegenerator_Pretty_Test.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/ex/Codegenerator_Pretty_Test.thy Tue Jun 02 15:53:07 2009 +0200 @@ -0,0 +1,14 @@ + +(* Author: Florian Haftmann, TU Muenchen *) + +header {* Pervasive test of code generator using pretty literals *} + +theory Codegenerator_Pretty_Test +imports Codegenerator_Pretty +begin + +export_code * in SML module_name CodegenTest + in OCaml module_name CodegenTest file - + in Haskell file - + +end diff -r a48f9ef9de15 -r d1cbf6393964 src/HOL/ex/Codegenerator_Test.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/ex/Codegenerator_Test.thy Tue Jun 02 15:53:07 2009 +0200 @@ -0,0 +1,14 @@ + +(* Author: Florian Haftmann, TU Muenchen *) + +header {* Pervasive test of code generator *} + +theory Codegenerator_Test +imports Codegenerator_Candidates +begin + +export_code * in SML module_name CodegenTest + in OCaml module_name CodegenTest file - + in Haskell file - + +end diff -r a48f9ef9de15 -r d1cbf6393964 src/HOL/ex/ExecutableContent.thy --- a/src/HOL/ex/ExecutableContent.thy Tue Jun 02 15:53:05 2009 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,27 +0,0 @@ -(* Author: Florian Haftmann, TU Muenchen -*) - -header {* A huge set of executable constants *} - -theory ExecutableContent -imports - Complex_Main - AssocList - Binomial - Commutative_Ring - Enum - List_Prefix - Nat_Infinity - Nested_Environment - Option_ord - Permutation - Primes - Product_ord - SetsAndFunctions - While_Combinator - Word - "~~/src/HOL/ex/Commutative_Ring_Complete" - "~~/src/HOL/ex/Records" -begin - -end diff -r a48f9ef9de15 -r d1cbf6393964 src/HOL/ex/ROOT.ML --- a/src/HOL/ex/ROOT.ML Tue Jun 02 15:53:05 2009 +0200 +++ b/src/HOL/ex/ROOT.ML Tue Jun 02 15:53:07 2009 +0200 @@ -11,8 +11,8 @@ "Word", "Eval_Examples", "Quickcheck_Generators", - "Codegenerator", - "Codegenerator_Pretty", + "Codegenerator_Test", + "Codegenerator_Pretty_Test", "NormalForm", "../NumberTheory/Factorization", "Predicate_Compile",