--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Codegenerator_Test/Candidates.thy Fri Jul 02 14:23:18 2010 +0200
@@ -0,0 +1,25 @@
+
+(* Author: Florian Haftmann, TU Muenchen *)
+
+header {* A huge collection of equations to generate code from *}
+
+theory Candidates
+imports
+ Complex_Main
+ Library
+ List_Prefix
+ "~~/src/HOL/Number_Theory/Primes"
+ "~~/src/HOL/ex/Records"
+begin
+
+inductive sublist :: "'a list \<Rightarrow> 'a list \<Rightarrow> bool" where
+ empty: "sublist [] xs"
+ | drop: "sublist ys xs \<Longrightarrow> sublist ys (x # xs)"
+ | take: "sublist ys xs \<Longrightarrow> sublist (x # ys) (x # xs)"
+
+code_pred sublist .
+
+(*avoid popular infix*)
+code_reserved SML upto
+
+end
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Codegenerator_Test/Candidates_Pretty.thy Fri Jul 02 14:23:18 2010 +0200
@@ -0,0 +1,10 @@
+
+(* Author: Florian Haftmann, TU Muenchen *)
+
+header {* Generating code using pretty literals and natural number literals *}
+
+theory Candidates_Pretty
+imports Candidates Code_Char Efficient_Nat
+begin
+
+end
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Codegenerator_Test/Generate.thy Fri Jul 02 14:23:18 2010 +0200
@@ -0,0 +1,15 @@
+
+(* Author: Florian Haftmann, TU Muenchen *)
+
+header {* Pervasive test of code generator *}
+
+theory Generate
+imports Candidates
+begin
+
+export_code * in SML module_name Code_Test
+ in OCaml module_name Code_Test file -
+ in Haskell file -
+ in Scala file -
+
+end
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Codegenerator_Test/Generate_Pretty.thy Fri Jul 02 14:23:18 2010 +0200
@@ -0,0 +1,20 @@
+
+(* Author: Florian Haftmann, TU Muenchen *)
+
+header {* Pervasive test of code generator using pretty literals *}
+
+theory Generate_Pretty
+imports Candidates_Pretty
+begin
+
+lemma [code, code del]: "nat_of_char = nat_of_char" ..
+lemma [code, code del]: "char_of_nat = char_of_nat" ..
+lemma [code, code del]: "(less_eq :: char \<Rightarrow> _) = less_eq" ..
+lemma [code, code del]: "(less :: char \<Rightarrow> _) = less" ..
+
+export_code * in SML module_name Code_Test
+ in OCaml module_name Code_Test file -
+ in Haskell file -
+ in Scala file -
+
+end
--- a/src/HOL/ex/Codegenerator_Candidates.thy Fri Jul 02 14:23:17 2010 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,39 +0,0 @@
-
-(* Author: Florian Haftmann, TU Muenchen *)
-
-header {* A huge collection of equations to generate code from *}
-
-theory Codegenerator_Candidates
-imports
- Complex_Main
- AssocList
- Binomial
- "~~/src/HOL/Decision_Procs/Commutative_Ring_Complete"
- Dlist
- Fset
- Enum
- List_Prefix
- More_List
- Nat_Infinity
- Nested_Environment
- Option_ord
- Permutation
- "~~/src/HOL/Number_Theory/Primes"
- Product_ord
- "~~/src/HOL/ex/Records"
- RBT
- SetsAndFunctions
- While_Combinator
-begin
-
-inductive sublist :: "'a list \<Rightarrow> 'a list \<Rightarrow> bool" where
- empty: "sublist [] xs"
- | drop: "sublist ys xs \<Longrightarrow> sublist ys (x # xs)"
- | take: "sublist ys xs \<Longrightarrow> sublist (x # ys) (x # xs)"
-
-code_pred sublist .
-
-(*avoid popular infix*)
-code_reserved SML upto
-
-end
--- a/src/HOL/ex/Codegenerator_Pretty.thy Fri Jul 02 14:23:17 2010 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,12 +0,0 @@
-
-(* Author: Florian Haftmann, TU Muenchen *)
-
-header {* Generating code using pretty literals and natural number literals *}
-
-theory Codegenerator_Pretty
-imports "~~/src/HOL/ex/Codegenerator_Candidates" Code_Char Efficient_Nat
-begin
-
-declare isnorm.simps [code del]
-
-end
--- a/src/HOL/ex/Codegenerator_Pretty_Test.thy Fri Jul 02 14:23:17 2010 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,15 +0,0 @@
-
-(* 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 -
- in Scala file -
-
-end
--- a/src/HOL/ex/Codegenerator_Test.thy Fri Jul 02 14:23:17 2010 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,15 +0,0 @@
-
-(* 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 -
- in Scala file -
-
-end
--- a/src/HOL/ex/ROOT.ML Fri Jul 02 14:23:17 2010 +0200
+++ b/src/HOL/ex/ROOT.ML Fri Jul 02 14:23:18 2010 +0200
@@ -8,8 +8,6 @@
"Efficient_Nat_examples",
"FuncSet",
"Eval_Examples",
- "Codegenerator_Test",
- "Codegenerator_Pretty_Test",
"NormalForm"
];