# HG changeset patch
# User haftmann
# Date 1155017955 -7200
# Node ID c7658e811ffba6ea2815717feb4eefe15dbad5a1
# Parent  54fe257afd4fd550872adeba7dc34227f9a9bb22
added more examples

diff -r 54fe257afd4f -r c7658e811ffb src/HOL/ex/Codegenerator.thy
--- a/src/HOL/ex/Codegenerator.thy	Tue Aug 08 08:19:11 2006 +0200
+++ b/src/HOL/ex/Codegenerator.thy	Tue Aug 08 08:19:15 2006 +0200
@@ -5,7 +5,7 @@
 header {* Test and Examples for code generator *}
 
 theory Codegenerator
-imports Main
+imports Main "~~/src/HOL/ex/Records"
 begin
 
 subsection {* booleans *}
@@ -14,8 +14,6 @@
   xor :: "bool \<Rightarrow> bool \<Rightarrow> bool"
   "xor p q = ((p | q) & \<not> (p & q))"
 
-code_generate (ml, haskell) xor
-
 subsection {* natural numbers *}
 
 definition
@@ -24,16 +22,6 @@
   n :: nat
   "n = 42"
 
-code_generate (ml, haskell) n
-
-code_generate (ml, haskell)
-  "0::nat" "one" n
-  "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"
-
 subsection {* pairs *}
 
 definition
@@ -44,13 +32,11 @@
   appl :: "('a \<Rightarrow> 'b) * 'a \<Rightarrow> 'b"
   "appl p = (let (f, x) = p in f x)"
 
-code_generate (ml, haskell) Pair fst snd Let split swap swapp appl
-
 subsection {* integers *}
 
 definition
   k :: "int"
-  "k = 42"
+  "k = -42"
 
 consts
   fac :: "int => int"
@@ -58,25 +44,10 @@
 recdef fac "measure nat"
   "fac j = (if j <= 0 then 1 else j * (fac (j - 1)))"
 
-code_generate (ml, haskell)
-  "0::int" 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"  
-
 subsection {* sums *}
 
-code_generate (ml, haskell) Inl Inr
-
 subsection {* options *}
 
-code_generate (ml, haskell) None Some
-
 subsection {* lists *}
 
 definition
@@ -85,8 +56,6 @@
   qs :: "nat list"
   "qs == rev ps"
 
-code_generate (ml, haskell) hd tl "op @" ps qs
-
 subsection {* mutual datatypes *}
 
 datatype mut1 = Tip | Top mut2
@@ -102,22 +71,10 @@
   "mut2 mut2.Tip = mut2.Tip"
   "mut2 (mut2.Top x) = mut2.Top (mut1 x)"
 
-code_generate (ml, haskell) mut1 mut2
+subsection {* records *}
 
 subsection {* equalities *}
 
-code_generate (ml, haskell)
-  "op = :: bool \<Rightarrow> bool \<Rightarrow> bool"
-  "op = :: nat \<Rightarrow> nat \<Rightarrow> bool"
-  "op = :: int \<Rightarrow> int \<Rightarrow> bool"
-  "op = :: 'a * 'b \<Rightarrow> 'a * 'b \<Rightarrow> bool"
-  "op = :: 'a + 'b \<Rightarrow> 'a + 'b \<Rightarrow> bool"
-  "op = :: 'a option \<Rightarrow> 'a option \<Rightarrow> bool"
-  "op = :: 'a list \<Rightarrow> 'a list \<Rightarrow> bool"
-  "op = :: mut1 \<Rightarrow> mut1 \<Rightarrow> bool"
-  "op = :: mut2 \<Rightarrow> mut2 \<Rightarrow> bool"
-
-
 subsection {* heavy usage of names *}
 
 definition
@@ -133,7 +90,73 @@
   "Codegenerator.g" "Mymod.A.f"
   "Codegenerator.h" "Mymod.A.B.f"
 
-code_generate (ml, haskell) f g h
+code_generate (ml, haskell)
+  n one "0::int" "0::nat" "1::int" "1::nat"
+code_generate (ml, haskell)
+  fac
+code_generate (ml, haskell)
+  xor
+code_generate (ml, haskell)
+  "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_generate (ml, haskell)
+  Pair fst snd Let split swap swapp appl
+code_generate (ml, haskell)
+  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_generate (ml, haskell)
+  Inl Inr
+code_generate (ml, haskell)
+  None Some
+code_generate (ml, haskell)
+  hd tl "op @" ps qs
+code_generate (ml, haskell)
+  mut1 mut2
+code_generate (ml, haskell)
+  "op @" filter concat foldl foldr hd tl
+  last butlast list_all2
+  map 
+  nth 
+  list_update
+  take
+  drop
+  takeWhile
+  dropWhile
+  rev
+  zip
+  upt
+  remdups
+  remove1
+  null
+  "distinct"
+  replicate
+  rotate1
+  rotate
+  splice
+code_generate (ml, haskell)
+  foo1 foo3
+code_generate (ml, haskell)
+  "op = :: bool \<Rightarrow> bool \<Rightarrow> bool"
+  "op = :: nat \<Rightarrow> nat \<Rightarrow> bool"
+  "op = :: int \<Rightarrow> int \<Rightarrow> bool"
+  "op = :: 'a * 'b \<Rightarrow> 'a * 'b \<Rightarrow> bool"
+  "op = :: 'a + 'b \<Rightarrow> 'a + 'b \<Rightarrow> bool"
+  "op = :: 'a option \<Rightarrow> 'a option \<Rightarrow> bool"
+  "op = :: 'a list \<Rightarrow> 'a list \<Rightarrow> bool"
+  "op = :: mut1 \<Rightarrow> mut1 \<Rightarrow> bool"
+  "op = :: mut2 \<Rightarrow> mut2 \<Rightarrow> bool"
+code_generate (ml, haskell)
+  f g h
 
 code_serialize ml (-)