--- a/src/HOL/ex/Codegenerator.thy Mon Dec 18 08:21:32 2006 +0100
+++ b/src/HOL/ex/Codegenerator.thy Mon Dec 18 08:21:33 2006 +0100
@@ -2,74 +2,38 @@
Author: Florian Haftmann, TU Muenchen
*)
-header {* Test and Examples for code generator *}
+header {* Tests and examples for code generator *}
theory Codegenerator
-imports Main Records
+imports
+ Main
+ Records
+ AssocList
+ Binomial
+ Commutative_Ring
+ GCD
+ List_Prefix
+ Nat_Infinity
+ NatPair
+ Nested_Environment
+ Permutation
+ Primes
+ Product_ord
+ SetsAndFunctions
+ State_Monad
+ While_Combinator
+ Word
+ (*a lot of stuff to test*)
begin
-subsection {* booleans *}
-
-definition
- xor :: "bool \<Rightarrow> bool \<Rightarrow> bool" where
- "xor p q = ((p | q) & \<not> (p & q))"
-
-subsection {* natural numbers *}
-
definition
n :: nat where
"n = 42"
-subsection {* pairs *}
-
-definition
- swap :: "'a * 'b \<Rightarrow> 'b * 'a" where
- "swap p = (let (x, y) = p in (y, x))"
-
-definition
- appl :: "('a \<Rightarrow> 'b) * 'a \<Rightarrow> 'b" where
- "appl p = (let (f, x) = p in f x)"
-
-definition
- snd_three :: "'a * 'b * 'c => 'b" where
- "snd_three a = id (\<lambda>(a, b, c). b) a"
-
-lemma [code]:
- "swap (x, y) = (y, x)"
- unfolding swap_def Let_def by auto
-
-lemma [code]:
- "appl (f, x) = f x"
- unfolding appl_def Let_def by auto
-
-subsection {* integers *}
-
definition
k :: "int" where
"k = -42"
-function
- fac :: "int => int" where
- "fac j = (if j <= 0 then 1 else j * (fac (j - 1)))"
- by pat_completeness auto
-termination by (relation "measure nat") auto
-
-subsection {* sums *}
-
-subsection {* options *}
-
-subsection {* lists *}
-
-definition
- ps :: "nat list" where
- "ps = [2, 3, 5, 7, 11]"
-
-definition
- qs :: "nat list" where
- "qs == rev ps"
-
-subsection {* mutual datatypes *}
-
datatype mut1 = Tip | Top mut2
and mut2 = Tip | Top mut1
@@ -83,16 +47,10 @@
"mut2 mut2.Tip = mut2.Tip"
"mut2 (mut2.Top x) = mut2.Top (mut1 x)"
-subsection {* records *}
-
-subsection {* equalities *}
-
-subsection {* strings *}
-
definition
"mystring = ''my home is my castle''"
-subsection {* nested lets and such *}
+text {* nested lets and such *}
definition
"abs_let x = (let (y, z) = x in (\<lambda>u. case u of () \<Rightarrow> (y + y)))"
@@ -110,84 +68,14 @@
"apply_tower = (\<lambda>x. x (\<lambda>x. x (\<lambda>x. x)))"
definition
- "keywords fun datatype class instance funa classa =
- Suc fun + datatype * class mod instance - funa - classa"
+ "keywords fun datatype x instance funa classa =
+ Suc fun + datatype * x mod instance - funa - classa"
hide (open) const keywords
definition
"shadow keywords = keywords @ [Codegenerator.keywords 0 0 0 0 0 0]"
-code_gen
- xor
-code_gen
- "0::nat" "1::nat"
-code_gen
- Pair fst snd Let split swap snd_three
-code_gen
- "op + :: nat \<Rightarrow> nat \<Rightarrow> nat"
- "op - :: nat \<Rightarrow> nat \<Rightarrow> nat"
- "op * :: nat \<Rightarrow> nat \<Rightarrow> nat"
- "op < :: nat \<Rightarrow> nat \<Rightarrow> bool"
- "op <= :: nat \<Rightarrow> nat \<Rightarrow> bool"
-code_gen
- appl
-code_gen
- Inl Inr
-code_gen
- None Some
-code_gen
- hd tl "op @" ps qs
-code_gen
- mut1 mut2
-code_gen
- remove1
- null
- replicate
- rotate1
- rotate
- splice
-code_gen
- remdups
- "distinct"
- filter
-code_gen
- foo1 foo3
-code_gen
- mystring
-code_gen
- apply_tower Codegenerator.keywords shadow base_case
-code_gen
- abs_let nested_let case_let
-code_gen "0::int" "1::int"
- (SML) (Haskell)
-code_gen n
- (SML) (Haskell)
-code_gen fac
- (SML) (Haskell)
-code_gen
- k
- "op + :: int \<Rightarrow> int \<Rightarrow> int"
- "op - :: int \<Rightarrow> int \<Rightarrow> int"
- "op * :: int \<Rightarrow> int \<Rightarrow> int"
- "op < :: int \<Rightarrow> int \<Rightarrow> bool"
- "op <= :: int \<Rightarrow> int \<Rightarrow> bool"
- fac
- "op div :: int \<Rightarrow> int \<Rightarrow> int"
- "op mod :: int \<Rightarrow> int \<Rightarrow> int"
- (SML) (Haskell)
-code_gen
- "op = :: bool \<Rightarrow> bool \<Rightarrow> bool"
- "op = :: nat \<Rightarrow> nat \<Rightarrow> bool"
- "op = :: int \<Rightarrow> int \<Rightarrow> bool"
- "op = :: ('a\<Colon>eq) * ('b\<Colon>eq) \<Rightarrow> 'a * 'b \<Rightarrow> bool"
- "op = :: ('a\<Colon>eq) + ('b\<Colon>eq) \<Rightarrow> 'a + 'b \<Rightarrow> bool"
- "op = :: ('a\<Colon>eq) option \<Rightarrow> 'a option \<Rightarrow> bool"
- "op = :: ('a\<Colon>eq) list \<Rightarrow> 'a list \<Rightarrow> bool"
- "op = :: mut1 \<Rightarrow> mut1 \<Rightarrow> bool"
- "op = :: mut2 \<Rightarrow> mut2 \<Rightarrow> bool"
- "op = :: ('a\<Colon>eq) point_scheme \<Rightarrow> 'a point_scheme \<Rightarrow> bool"
-
-code_gen (SML #) (Haskell -)
+code_gen "*" (Haskell -) (SML #)
end
\ No newline at end of file