tuned code generator test theories
authorhaftmann
Tue Jun 02 15:53:07 2009 +0200 (2009-06-02)
changeset 31378d1cbf6393964
parent 31377 a48f9ef9de15
child 31379 213299656575
tuned code generator test theories
src/HOL/IsaMakefile
src/HOL/ex/Codegenerator.thy
src/HOL/ex/Codegenerator_Candidates.thy
src/HOL/ex/Codegenerator_Pretty.thy
src/HOL/ex/Codegenerator_Pretty_Test.thy
src/HOL/ex/Codegenerator_Test.thy
src/HOL/ex/ExecutableContent.thy
src/HOL/ex/ROOT.ML
     1.1 --- a/src/HOL/IsaMakefile	Tue Jun 02 15:53:05 2009 +0200
     1.2 +++ b/src/HOL/IsaMakefile	Tue Jun 02 15:53:07 2009 +0200
     1.3 @@ -838,11 +838,12 @@
     1.4    ex/Arith_Examples.thy				\
     1.5    ex/Arithmetic_Series_Complex.thy ex/BT.thy ex/BinEx.thy		\
     1.6    ex/Binary.thy ex/CTL.thy ex/Chinese.thy ex/Classical.thy		\
     1.7 -  ex/CodegenSML_Test.thy ex/Codegenerator.thy				\
     1.8 -  ex/Codegenerator_Pretty.thy ex/Coherent.thy				\
     1.9 +  ex/CodegenSML_Test.thy ex/Codegenerator_Candidates.thy				\
    1.10 +  ex/Codegenerator_Pretty.thy ex/Codegenerator_Test.thy \
    1.11 +  ex/Codegenerator_Pretty_Test.thy ex/Coherent.thy				\
    1.12    ex/Commutative_RingEx.thy ex/Commutative_Ring_Complete.thy		\
    1.13    ex/Efficient_Nat_examples.thy		\
    1.14 -  ex/Eval_Examples.thy ex/ExecutableContent.thy				\
    1.15 +  ex/Eval_Examples.thy				\
    1.16    ex/Formal_Power_Series_Examples.thy ex/Fundefs.thy			\
    1.17    ex/Groebner_Examples.thy ex/Guess.thy ex/HarmonicSeries.thy		\
    1.18    ex/Hebrew.thy ex/Hex_Bin_Examples.thy ex/Higher_Order_Logic.thy	\
     2.1 --- a/src/HOL/ex/Codegenerator.thy	Tue Jun 02 15:53:05 2009 +0200
     2.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     2.3 @@ -1,27 +0,0 @@
     2.4 -(*  ID:         $Id$
     2.5 -    Author:     Florian Haftmann, TU Muenchen
     2.6 -*)
     2.7 -
     2.8 -header {* Tests and examples for code generator *}
     2.9 -
    2.10 -theory Codegenerator
    2.11 -imports ExecutableContent
    2.12 -begin
    2.13 -
    2.14 -ML {* (*FIXME get rid of this*)
    2.15 -nonfix union;
    2.16 -nonfix inter;
    2.17 -nonfix upto;
    2.18 -*}
    2.19 -
    2.20 -export_code * in SML module_name CodegenTest
    2.21 -  in OCaml module_name CodegenTest file -
    2.22 -  in Haskell file -
    2.23 -
    2.24 -ML {*
    2.25 -infix union;
    2.26 -infix inter;
    2.27 -infix 4 upto;
    2.28 -*}
    2.29 -
    2.30 -end
     3.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.2 +++ b/src/HOL/ex/Codegenerator_Candidates.thy	Tue Jun 02 15:53:07 2009 +0200
     3.3 @@ -0,0 +1,44 @@
     3.4 +
     3.5 +(* Author: Florian Haftmann, TU Muenchen *)
     3.6 +
     3.7 +header {* A huge collection of equations to generate code from *}
     3.8 +
     3.9 +theory Codegenerator_Candidates
    3.10 +imports
    3.11 +  Complex_Main
    3.12 +  AssocList
    3.13 +  Binomial
    3.14 +  Commutative_Ring
    3.15 +  Enum
    3.16 +  List_Prefix
    3.17 +  Nat_Infinity
    3.18 +  Nested_Environment
    3.19 +  Option_ord
    3.20 +  Permutation
    3.21 +  Primes
    3.22 +  Product_ord
    3.23 +  SetsAndFunctions
    3.24 +  While_Combinator
    3.25 +  Word
    3.26 +  "~~/src/HOL/ex/Commutative_Ring_Complete"
    3.27 +  "~~/src/HOL/ex/Records"
    3.28 +begin
    3.29 +
    3.30 +(*temporary Haskell workaround*)
    3.31 +declare typerep_fun_def [code inline]
    3.32 +declare typerep_prod_def [code inline]
    3.33 +declare typerep_sum_def [code inline]
    3.34 +declare typerep_cpoint_ext_type_def [code inline]
    3.35 +declare typerep_itself_def [code inline]
    3.36 +declare typerep_list_def [code inline]
    3.37 +declare typerep_option_def [code inline]
    3.38 +declare typerep_point_ext_type_def [code inline]
    3.39 +declare typerep_point'_ext_type_def [code inline]
    3.40 +declare typerep_point''_ext_type_def [code inline]
    3.41 +declare typerep_pol_def [code inline]
    3.42 +declare typerep_polex_def [code inline]
    3.43 +
    3.44 +(*avoid popular infixes*)
    3.45 +code_reserved SML union inter upto
    3.46 +
    3.47 +end
     4.1 --- a/src/HOL/ex/Codegenerator_Pretty.thy	Tue Jun 02 15:53:05 2009 +0200
     4.2 +++ b/src/HOL/ex/Codegenerator_Pretty.thy	Tue Jun 02 15:53:07 2009 +0200
     4.3 @@ -1,29 +1,12 @@
     4.4 -(*  Title:      HOL/ex/Codegenerator_Pretty.thy
     4.5 -    Author:     Florian Haftmann, TU Muenchen
     4.6 -*)
     4.7  
     4.8 -header {* Simple examples for pretty numerals and such *}
     4.9 +(* Author: Florian Haftmann, TU Muenchen *)
    4.10 +
    4.11 +header {* Generating code using pretty literals and natural number literals  *}
    4.12  
    4.13  theory Codegenerator_Pretty
    4.14 -imports ExecutableContent Code_Char Efficient_Nat
    4.15 +imports "~~/src/HOL/ex/Codegenerator_Candidates" Code_Char Efficient_Nat
    4.16  begin
    4.17  
    4.18  declare isnorm.simps [code del]
    4.19  
    4.20 -ML {* (*FIXME get rid of this*)
    4.21 -nonfix union;
    4.22 -nonfix inter;
    4.23 -nonfix upto;
    4.24 -*}
    4.25 -
    4.26 -export_code * in SML module_name CodegenTest
    4.27 -  in OCaml module_name CodegenTest file -
    4.28 -  in Haskell file -
    4.29 -
    4.30 -ML {*
    4.31 -infix union;
    4.32 -infix inter;
    4.33 -infix 4 upto;
    4.34 -*}
    4.35 -
    4.36  end
     5.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     5.2 +++ b/src/HOL/ex/Codegenerator_Pretty_Test.thy	Tue Jun 02 15:53:07 2009 +0200
     5.3 @@ -0,0 +1,14 @@
     5.4 +
     5.5 +(* Author: Florian Haftmann, TU Muenchen *)
     5.6 +
     5.7 +header {* Pervasive test of code generator using pretty literals *}
     5.8 +
     5.9 +theory Codegenerator_Pretty_Test
    5.10 +imports Codegenerator_Pretty
    5.11 +begin
    5.12 +
    5.13 +export_code * in SML module_name CodegenTest
    5.14 +  in OCaml module_name CodegenTest file -
    5.15 +  in Haskell file -
    5.16 +
    5.17 +end
     6.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     6.2 +++ b/src/HOL/ex/Codegenerator_Test.thy	Tue Jun 02 15:53:07 2009 +0200
     6.3 @@ -0,0 +1,14 @@
     6.4 +
     6.5 +(* Author: Florian Haftmann, TU Muenchen *)
     6.6 +
     6.7 +header {* Pervasive test of code generator *}
     6.8 +
     6.9 +theory Codegenerator_Test
    6.10 +imports Codegenerator_Candidates
    6.11 +begin
    6.12 +
    6.13 +export_code * in SML module_name CodegenTest
    6.14 +  in OCaml module_name CodegenTest file -
    6.15 +  in Haskell file -
    6.16 +
    6.17 +end
     7.1 --- a/src/HOL/ex/ExecutableContent.thy	Tue Jun 02 15:53:05 2009 +0200
     7.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     7.3 @@ -1,27 +0,0 @@
     7.4 -(*  Author:     Florian Haftmann, TU Muenchen
     7.5 -*)
     7.6 -
     7.7 -header {* A huge set of executable constants *}
     7.8 -
     7.9 -theory ExecutableContent
    7.10 -imports
    7.11 -  Complex_Main
    7.12 -  AssocList
    7.13 -  Binomial
    7.14 -  Commutative_Ring
    7.15 -  Enum
    7.16 -  List_Prefix
    7.17 -  Nat_Infinity
    7.18 -  Nested_Environment
    7.19 -  Option_ord
    7.20 -  Permutation
    7.21 -  Primes
    7.22 -  Product_ord
    7.23 -  SetsAndFunctions
    7.24 -  While_Combinator
    7.25 -  Word
    7.26 -  "~~/src/HOL/ex/Commutative_Ring_Complete"
    7.27 -  "~~/src/HOL/ex/Records"
    7.28 -begin
    7.29 -
    7.30 -end
     8.1 --- a/src/HOL/ex/ROOT.ML	Tue Jun 02 15:53:05 2009 +0200
     8.2 +++ b/src/HOL/ex/ROOT.ML	Tue Jun 02 15:53:07 2009 +0200
     8.3 @@ -11,8 +11,8 @@
     8.4    "Word",
     8.5    "Eval_Examples",
     8.6    "Quickcheck_Generators",
     8.7 -  "Codegenerator",
     8.8 -  "Codegenerator_Pretty",
     8.9 +  "Codegenerator_Test",
    8.10 +  "Codegenerator_Pretty_Test",
    8.11    "NormalForm",
    8.12    "../NumberTheory/Factorization",
    8.13    "Predicate_Compile",