author haftmann Mon, 18 Dec 2006 08:21:33 +0100 changeset 21877 e871f57b1adb parent 21876 96a601bc59d8 child 21878 cfc07819bb47
now testing executable content of nearly all HOL
```--- 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
+  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
-code_gen
-  abs_let nested_let case_let
-code_gen "0::int" "1::int"
-code_gen n
-code_gen fac
-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"
-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"
-