added more examples
authorhaftmann
Tue Aug 08 08:19:15 2006 +0200 (2006-08-08)
changeset 20351c7658e811ffb
parent 20350 54fe257afd4f
child 20352 bb56a6cbacac
added more examples
src/HOL/ex/Codegenerator.thy
     1.1 --- a/src/HOL/ex/Codegenerator.thy	Tue Aug 08 08:19:11 2006 +0200
     1.2 +++ b/src/HOL/ex/Codegenerator.thy	Tue Aug 08 08:19:15 2006 +0200
     1.3 @@ -5,7 +5,7 @@
     1.4  header {* Test and Examples for code generator *}
     1.5  
     1.6  theory Codegenerator
     1.7 -imports Main
     1.8 +imports Main "~~/src/HOL/ex/Records"
     1.9  begin
    1.10  
    1.11  subsection {* booleans *}
    1.12 @@ -14,8 +14,6 @@
    1.13    xor :: "bool \<Rightarrow> bool \<Rightarrow> bool"
    1.14    "xor p q = ((p | q) & \<not> (p & q))"
    1.15  
    1.16 -code_generate (ml, haskell) xor
    1.17 -
    1.18  subsection {* natural numbers *}
    1.19  
    1.20  definition
    1.21 @@ -24,16 +22,6 @@
    1.22    n :: nat
    1.23    "n = 42"
    1.24  
    1.25 -code_generate (ml, haskell) n
    1.26 -
    1.27 -code_generate (ml, haskell)
    1.28 -  "0::nat" "one" n
    1.29 -  "op + :: nat \<Rightarrow> nat \<Rightarrow> nat"
    1.30 -  "op - :: nat \<Rightarrow> nat \<Rightarrow> nat"
    1.31 -  "op * :: nat \<Rightarrow> nat \<Rightarrow> nat"
    1.32 -  "op < :: nat \<Rightarrow> nat \<Rightarrow> bool"
    1.33 -  "op <= :: nat \<Rightarrow> nat \<Rightarrow> bool"
    1.34 -
    1.35  subsection {* pairs *}
    1.36  
    1.37  definition
    1.38 @@ -44,13 +32,11 @@
    1.39    appl :: "('a \<Rightarrow> 'b) * 'a \<Rightarrow> 'b"
    1.40    "appl p = (let (f, x) = p in f x)"
    1.41  
    1.42 -code_generate (ml, haskell) Pair fst snd Let split swap swapp appl
    1.43 -
    1.44  subsection {* integers *}
    1.45  
    1.46  definition
    1.47    k :: "int"
    1.48 -  "k = 42"
    1.49 +  "k = -42"
    1.50  
    1.51  consts
    1.52    fac :: "int => int"
    1.53 @@ -58,25 +44,10 @@
    1.54  recdef fac "measure nat"
    1.55    "fac j = (if j <= 0 then 1 else j * (fac (j - 1)))"
    1.56  
    1.57 -code_generate (ml, haskell)
    1.58 -  "0::int" k
    1.59 -  "op + :: int \<Rightarrow> int \<Rightarrow> int"
    1.60 -  "op - :: int \<Rightarrow> int \<Rightarrow> int"
    1.61 -  "op * :: int \<Rightarrow> int \<Rightarrow> int"
    1.62 -  "op < :: int \<Rightarrow> int \<Rightarrow> bool"
    1.63 -  "op <= :: int \<Rightarrow> int \<Rightarrow> bool"
    1.64 -  fac
    1.65 -  "op div :: int \<Rightarrow> int \<Rightarrow> int"
    1.66 -  "op mod :: int \<Rightarrow> int \<Rightarrow> int"  
    1.67 -
    1.68  subsection {* sums *}
    1.69  
    1.70 -code_generate (ml, haskell) Inl Inr
    1.71 -
    1.72  subsection {* options *}
    1.73  
    1.74 -code_generate (ml, haskell) None Some
    1.75 -
    1.76  subsection {* lists *}
    1.77  
    1.78  definition
    1.79 @@ -85,8 +56,6 @@
    1.80    qs :: "nat list"
    1.81    "qs == rev ps"
    1.82  
    1.83 -code_generate (ml, haskell) hd tl "op @" ps qs
    1.84 -
    1.85  subsection {* mutual datatypes *}
    1.86  
    1.87  datatype mut1 = Tip | Top mut2
    1.88 @@ -102,22 +71,10 @@
    1.89    "mut2 mut2.Tip = mut2.Tip"
    1.90    "mut2 (mut2.Top x) = mut2.Top (mut1 x)"
    1.91  
    1.92 -code_generate (ml, haskell) mut1 mut2
    1.93 +subsection {* records *}
    1.94  
    1.95  subsection {* equalities *}
    1.96  
    1.97 -code_generate (ml, haskell)
    1.98 -  "op = :: bool \<Rightarrow> bool \<Rightarrow> bool"
    1.99 -  "op = :: nat \<Rightarrow> nat \<Rightarrow> bool"
   1.100 -  "op = :: int \<Rightarrow> int \<Rightarrow> bool"
   1.101 -  "op = :: 'a * 'b \<Rightarrow> 'a * 'b \<Rightarrow> bool"
   1.102 -  "op = :: 'a + 'b \<Rightarrow> 'a + 'b \<Rightarrow> bool"
   1.103 -  "op = :: 'a option \<Rightarrow> 'a option \<Rightarrow> bool"
   1.104 -  "op = :: 'a list \<Rightarrow> 'a list \<Rightarrow> bool"
   1.105 -  "op = :: mut1 \<Rightarrow> mut1 \<Rightarrow> bool"
   1.106 -  "op = :: mut2 \<Rightarrow> mut2 \<Rightarrow> bool"
   1.107 -
   1.108 -
   1.109  subsection {* heavy usage of names *}
   1.110  
   1.111  definition
   1.112 @@ -133,7 +90,73 @@
   1.113    "Codegenerator.g" "Mymod.A.f"
   1.114    "Codegenerator.h" "Mymod.A.B.f"
   1.115  
   1.116 -code_generate (ml, haskell) f g h
   1.117 +code_generate (ml, haskell)
   1.118 +  n one "0::int" "0::nat" "1::int" "1::nat"
   1.119 +code_generate (ml, haskell)
   1.120 +  fac
   1.121 +code_generate (ml, haskell)
   1.122 +  xor
   1.123 +code_generate (ml, haskell)
   1.124 +  "op + :: nat \<Rightarrow> nat \<Rightarrow> nat"
   1.125 +  "op - :: nat \<Rightarrow> nat \<Rightarrow> nat"
   1.126 +  "op * :: nat \<Rightarrow> nat \<Rightarrow> nat"
   1.127 +  "op < :: nat \<Rightarrow> nat \<Rightarrow> bool"
   1.128 +  "op <= :: nat \<Rightarrow> nat \<Rightarrow> bool"
   1.129 +code_generate (ml, haskell)
   1.130 +  Pair fst snd Let split swap swapp appl
   1.131 +code_generate (ml, haskell)
   1.132 +  k
   1.133 +  "op + :: int \<Rightarrow> int \<Rightarrow> int"
   1.134 +  "op - :: int \<Rightarrow> int \<Rightarrow> int"
   1.135 +  "op * :: int \<Rightarrow> int \<Rightarrow> int"
   1.136 +  "op < :: int \<Rightarrow> int \<Rightarrow> bool"
   1.137 +  "op <= :: int \<Rightarrow> int \<Rightarrow> bool"
   1.138 +  fac
   1.139 +  "op div :: int \<Rightarrow> int \<Rightarrow> int"
   1.140 +  "op mod :: int \<Rightarrow> int \<Rightarrow> int"  
   1.141 +code_generate (ml, haskell)
   1.142 +  Inl Inr
   1.143 +code_generate (ml, haskell)
   1.144 +  None Some
   1.145 +code_generate (ml, haskell)
   1.146 +  hd tl "op @" ps qs
   1.147 +code_generate (ml, haskell)
   1.148 +  mut1 mut2
   1.149 +code_generate (ml, haskell)
   1.150 +  "op @" filter concat foldl foldr hd tl
   1.151 +  last butlast list_all2
   1.152 +  map 
   1.153 +  nth 
   1.154 +  list_update
   1.155 +  take
   1.156 +  drop
   1.157 +  takeWhile
   1.158 +  dropWhile
   1.159 +  rev
   1.160 +  zip
   1.161 +  upt
   1.162 +  remdups
   1.163 +  remove1
   1.164 +  null
   1.165 +  "distinct"
   1.166 +  replicate
   1.167 +  rotate1
   1.168 +  rotate
   1.169 +  splice
   1.170 +code_generate (ml, haskell)
   1.171 +  foo1 foo3
   1.172 +code_generate (ml, haskell)
   1.173 +  "op = :: bool \<Rightarrow> bool \<Rightarrow> bool"
   1.174 +  "op = :: nat \<Rightarrow> nat \<Rightarrow> bool"
   1.175 +  "op = :: int \<Rightarrow> int \<Rightarrow> bool"
   1.176 +  "op = :: 'a * 'b \<Rightarrow> 'a * 'b \<Rightarrow> bool"
   1.177 +  "op = :: 'a + 'b \<Rightarrow> 'a + 'b \<Rightarrow> bool"
   1.178 +  "op = :: 'a option \<Rightarrow> 'a option \<Rightarrow> bool"
   1.179 +  "op = :: 'a list \<Rightarrow> 'a list \<Rightarrow> bool"
   1.180 +  "op = :: mut1 \<Rightarrow> mut1 \<Rightarrow> bool"
   1.181 +  "op = :: mut2 \<Rightarrow> mut2 \<Rightarrow> bool"
   1.182 +code_generate (ml, haskell)
   1.183 +  f g h
   1.184  
   1.185  code_serialize ml (-)
   1.186