--- 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 \
--- 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
--- /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
--- 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
--- /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
--- /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
--- 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
--- 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",