1.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
1.2 +++ b/src/HOL/Codegenerator_Test/Candidates.thy Fri Jul 02 14:23:18 2010 +0200
1.3 @@ -0,0 +1,25 @@
1.4 +
1.5 +(* Author: Florian Haftmann, TU Muenchen *)
1.6 +
1.7 +header {* A huge collection of equations to generate code from *}
1.8 +
1.9 +theory Candidates
1.10 +imports
1.11 + Complex_Main
1.12 + Library
1.13 + List_Prefix
1.14 + "~~/src/HOL/Number_Theory/Primes"
1.15 + "~~/src/HOL/ex/Records"
1.16 +begin
1.17 +
1.18 +inductive sublist :: "'a list \<Rightarrow> 'a list \<Rightarrow> bool" where
1.19 + empty: "sublist [] xs"
1.20 + | drop: "sublist ys xs \<Longrightarrow> sublist ys (x # xs)"
1.21 + | take: "sublist ys xs \<Longrightarrow> sublist (x # ys) (x # xs)"
1.22 +
1.23 +code_pred sublist .
1.24 +
1.25 +(*avoid popular infix*)
1.26 +code_reserved SML upto
1.27 +
1.28 +end
2.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
2.2 +++ b/src/HOL/Codegenerator_Test/Candidates_Pretty.thy Fri Jul 02 14:23:18 2010 +0200
2.3 @@ -0,0 +1,10 @@
2.4 +
2.5 +(* Author: Florian Haftmann, TU Muenchen *)
2.6 +
2.7 +header {* Generating code using pretty literals and natural number literals *}
2.8 +
2.9 +theory Candidates_Pretty
2.10 +imports Candidates Code_Char Efficient_Nat
2.11 +begin
2.12 +
2.13 +end
3.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
3.2 +++ b/src/HOL/Codegenerator_Test/Generate.thy Fri Jul 02 14:23:18 2010 +0200
3.3 @@ -0,0 +1,15 @@
3.4 +
3.5 +(* Author: Florian Haftmann, TU Muenchen *)
3.6 +
3.7 +header {* Pervasive test of code generator *}
3.8 +
3.9 +theory Generate
3.10 +imports Candidates
3.11 +begin
3.12 +
3.13 +export_code * in SML module_name Code_Test
3.14 + in OCaml module_name Code_Test file -
3.15 + in Haskell file -
3.16 + in Scala file -
3.17 +
3.18 +end
4.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
4.2 +++ b/src/HOL/Codegenerator_Test/Generate_Pretty.thy Fri Jul 02 14:23:18 2010 +0200
4.3 @@ -0,0 +1,20 @@
4.4 +
4.5 +(* Author: Florian Haftmann, TU Muenchen *)
4.6 +
4.7 +header {* Pervasive test of code generator using pretty literals *}
4.8 +
4.9 +theory Generate_Pretty
4.10 +imports Candidates_Pretty
4.11 +begin
4.12 +
4.13 +lemma [code, code del]: "nat_of_char = nat_of_char" ..
4.14 +lemma [code, code del]: "char_of_nat = char_of_nat" ..
4.15 +lemma [code, code del]: "(less_eq :: char \<Rightarrow> _) = less_eq" ..
4.16 +lemma [code, code del]: "(less :: char \<Rightarrow> _) = less" ..
4.17 +
4.18 +export_code * in SML module_name Code_Test
4.19 + in OCaml module_name Code_Test file -
4.20 + in Haskell file -
4.21 + in Scala file -
4.22 +
4.23 +end
5.1 --- a/src/HOL/ex/Codegenerator_Candidates.thy Fri Jul 02 14:23:17 2010 +0200
5.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
5.3 @@ -1,39 +0,0 @@
5.4 -
5.5 -(* Author: Florian Haftmann, TU Muenchen *)
5.6 -
5.7 -header {* A huge collection of equations to generate code from *}
5.8 -
5.9 -theory Codegenerator_Candidates
5.10 -imports
5.11 - Complex_Main
5.12 - AssocList
5.13 - Binomial
5.14 - "~~/src/HOL/Decision_Procs/Commutative_Ring_Complete"
5.15 - Dlist
5.16 - Fset
5.17 - Enum
5.18 - List_Prefix
5.19 - More_List
5.20 - Nat_Infinity
5.21 - Nested_Environment
5.22 - Option_ord
5.23 - Permutation
5.24 - "~~/src/HOL/Number_Theory/Primes"
5.25 - Product_ord
5.26 - "~~/src/HOL/ex/Records"
5.27 - RBT
5.28 - SetsAndFunctions
5.29 - While_Combinator
5.30 -begin
5.31 -
5.32 -inductive sublist :: "'a list \<Rightarrow> 'a list \<Rightarrow> bool" where
5.33 - empty: "sublist [] xs"
5.34 - | drop: "sublist ys xs \<Longrightarrow> sublist ys (x # xs)"
5.35 - | take: "sublist ys xs \<Longrightarrow> sublist (x # ys) (x # xs)"
5.36 -
5.37 -code_pred sublist .
5.38 -
5.39 -(*avoid popular infix*)
5.40 -code_reserved SML upto
5.41 -
5.42 -end
6.1 --- a/src/HOL/ex/Codegenerator_Pretty.thy Fri Jul 02 14:23:17 2010 +0200
6.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
6.3 @@ -1,12 +0,0 @@
6.4 -
6.5 -(* Author: Florian Haftmann, TU Muenchen *)
6.6 -
6.7 -header {* Generating code using pretty literals and natural number literals *}
6.8 -
6.9 -theory Codegenerator_Pretty
6.10 -imports "~~/src/HOL/ex/Codegenerator_Candidates" Code_Char Efficient_Nat
6.11 -begin
6.12 -
6.13 -declare isnorm.simps [code del]
6.14 -
6.15 -end
7.1 --- a/src/HOL/ex/Codegenerator_Pretty_Test.thy Fri Jul 02 14:23:17 2010 +0200
7.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
7.3 @@ -1,15 +0,0 @@
7.4 -
7.5 -(* Author: Florian Haftmann, TU Muenchen *)
7.6 -
7.7 -header {* Pervasive test of code generator using pretty literals *}
7.8 -
7.9 -theory Codegenerator_Pretty_Test
7.10 -imports Codegenerator_Pretty
7.11 -begin
7.12 -
7.13 -export_code * in SML module_name CodegenTest
7.14 - in OCaml module_name CodegenTest file -
7.15 - in Haskell file -
7.16 - in Scala file -
7.17 -
7.18 -end
8.1 --- a/src/HOL/ex/Codegenerator_Test.thy Fri Jul 02 14:23:17 2010 +0200
8.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
8.3 @@ -1,15 +0,0 @@
8.4 -
8.5 -(* Author: Florian Haftmann, TU Muenchen *)
8.6 -
8.7 -header {* Pervasive test of code generator *}
8.8 -
8.9 -theory Codegenerator_Test
8.10 -imports Codegenerator_Candidates
8.11 -begin
8.12 -
8.13 -export_code * in SML module_name CodegenTest
8.14 - in OCaml module_name CodegenTest file -
8.15 - in Haskell file -
8.16 - in Scala file -
8.17 -
8.18 -end
9.1 --- a/src/HOL/ex/ROOT.ML Fri Jul 02 14:23:17 2010 +0200
9.2 +++ b/src/HOL/ex/ROOT.ML Fri Jul 02 14:23:18 2010 +0200
9.3 @@ -8,8 +8,6 @@
9.4 "Efficient_Nat_examples",
9.5 "FuncSet",
9.6 "Eval_Examples",
9.7 - "Codegenerator_Test",
9.8 - "Codegenerator_Pretty_Test",
9.9 "NormalForm"
9.10 ];
9.11