src/HOL/ex/Codegenerator.thy
author haftmann
Mon, 14 Aug 2006 13:46:17 +0200
changeset 20383 58f65fc90cf4
parent 20351 c7658e811ffb
child 20453 855f07fabd76
permissions -rw-r--r--
adaptions to improvements
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
19281
b411f25fff25 added example for operational classes and code generator
haftmann
parents:
diff changeset
     1
(*  ID:         $Id$
b411f25fff25 added example for operational classes and code generator
haftmann
parents:
diff changeset
     2
    Author:     Florian Haftmann, TU Muenchen
b411f25fff25 added example for operational classes and code generator
haftmann
parents:
diff changeset
     3
*)
b411f25fff25 added example for operational classes and code generator
haftmann
parents:
diff changeset
     4
20187
af47971ea304 small adjustments
haftmann
parents: 19888
diff changeset
     5
header {* Test and Examples for code generator *}
19281
b411f25fff25 added example for operational classes and code generator
haftmann
parents:
diff changeset
     6
b411f25fff25 added example for operational classes and code generator
haftmann
parents:
diff changeset
     7
theory Codegenerator
20351
c7658e811ffb added more examples
haftmann
parents: 20187
diff changeset
     8
imports Main "~~/src/HOL/ex/Records"
19281
b411f25fff25 added example for operational classes and code generator
haftmann
parents:
diff changeset
     9
begin
b411f25fff25 added example for operational classes and code generator
haftmann
parents:
diff changeset
    10
b411f25fff25 added example for operational classes and code generator
haftmann
parents:
diff changeset
    11
subsection {* booleans *}
b411f25fff25 added example for operational classes and code generator
haftmann
parents:
diff changeset
    12
b411f25fff25 added example for operational classes and code generator
haftmann
parents:
diff changeset
    13
definition
b411f25fff25 added example for operational classes and code generator
haftmann
parents:
diff changeset
    14
  xor :: "bool \<Rightarrow> bool \<Rightarrow> bool"
b411f25fff25 added example for operational classes and code generator
haftmann
parents:
diff changeset
    15
  "xor p q = ((p | q) & \<not> (p & q))"
b411f25fff25 added example for operational classes and code generator
haftmann
parents:
diff changeset
    16
b411f25fff25 added example for operational classes and code generator
haftmann
parents:
diff changeset
    17
subsection {* natural numbers *}
b411f25fff25 added example for operational classes and code generator
haftmann
parents:
diff changeset
    18
b411f25fff25 added example for operational classes and code generator
haftmann
parents:
diff changeset
    19
definition
b411f25fff25 added example for operational classes and code generator
haftmann
parents:
diff changeset
    20
  one :: nat
b411f25fff25 added example for operational classes and code generator
haftmann
parents:
diff changeset
    21
  "one = 1"
b411f25fff25 added example for operational classes and code generator
haftmann
parents:
diff changeset
    22
  n :: nat
b411f25fff25 added example for operational classes and code generator
haftmann
parents:
diff changeset
    23
  "n = 42"
b411f25fff25 added example for operational classes and code generator
haftmann
parents:
diff changeset
    24
b411f25fff25 added example for operational classes and code generator
haftmann
parents:
diff changeset
    25
subsection {* pairs *}
b411f25fff25 added example for operational classes and code generator
haftmann
parents:
diff changeset
    26
b411f25fff25 added example for operational classes and code generator
haftmann
parents:
diff changeset
    27
definition
b411f25fff25 added example for operational classes and code generator
haftmann
parents:
diff changeset
    28
  swap :: "'a * 'b \<Rightarrow> 'b * 'a"
b411f25fff25 added example for operational classes and code generator
haftmann
parents:
diff changeset
    29
  "swap p = (let (x, y) = p in (y, x))"
b411f25fff25 added example for operational classes and code generator
haftmann
parents:
diff changeset
    30
  swapp :: "'a * 'b \<Rightarrow> 'c * 'd \<Rightarrow> ('a * 'c) * ('b * 'd)"
b411f25fff25 added example for operational classes and code generator
haftmann
parents:
diff changeset
    31
  "swapp = (\<lambda>(x, y) (z, w). ((x, z), (y, w)))"
b411f25fff25 added example for operational classes and code generator
haftmann
parents:
diff changeset
    32
  appl :: "('a \<Rightarrow> 'b) * 'a \<Rightarrow> 'b"
b411f25fff25 added example for operational classes and code generator
haftmann
parents:
diff changeset
    33
  "appl p = (let (f, x) = p in f x)"
b411f25fff25 added example for operational classes and code generator
haftmann
parents:
diff changeset
    34
20187
af47971ea304 small adjustments
haftmann
parents: 19888
diff changeset
    35
subsection {* integers *}
af47971ea304 small adjustments
haftmann
parents: 19888
diff changeset
    36
19281
b411f25fff25 added example for operational classes and code generator
haftmann
parents:
diff changeset
    37
definition
b411f25fff25 added example for operational classes and code generator
haftmann
parents:
diff changeset
    38
  k :: "int"
20351
c7658e811ffb added more examples
haftmann
parents: 20187
diff changeset
    39
  "k = -42"
19281
b411f25fff25 added example for operational classes and code generator
haftmann
parents:
diff changeset
    40
b411f25fff25 added example for operational classes and code generator
haftmann
parents:
diff changeset
    41
consts
b411f25fff25 added example for operational classes and code generator
haftmann
parents:
diff changeset
    42
  fac :: "int => int"
b411f25fff25 added example for operational classes and code generator
haftmann
parents:
diff changeset
    43
b411f25fff25 added example for operational classes and code generator
haftmann
parents:
diff changeset
    44
recdef fac "measure nat"
b411f25fff25 added example for operational classes and code generator
haftmann
parents:
diff changeset
    45
  "fac j = (if j <= 0 then 1 else j * (fac (j - 1)))"
b411f25fff25 added example for operational classes and code generator
haftmann
parents:
diff changeset
    46
b411f25fff25 added example for operational classes and code generator
haftmann
parents:
diff changeset
    47
subsection {* sums *}
b411f25fff25 added example for operational classes and code generator
haftmann
parents:
diff changeset
    48
b411f25fff25 added example for operational classes and code generator
haftmann
parents:
diff changeset
    49
subsection {* options *}
b411f25fff25 added example for operational classes and code generator
haftmann
parents:
diff changeset
    50
b411f25fff25 added example for operational classes and code generator
haftmann
parents:
diff changeset
    51
subsection {* lists *}
b411f25fff25 added example for operational classes and code generator
haftmann
parents:
diff changeset
    52
b411f25fff25 added example for operational classes and code generator
haftmann
parents:
diff changeset
    53
definition
b411f25fff25 added example for operational classes and code generator
haftmann
parents:
diff changeset
    54
  ps :: "nat list"
b411f25fff25 added example for operational classes and code generator
haftmann
parents:
diff changeset
    55
  "ps = [2, 3, 5, 7, 11]"
b411f25fff25 added example for operational classes and code generator
haftmann
parents:
diff changeset
    56
  qs :: "nat list"
b411f25fff25 added example for operational classes and code generator
haftmann
parents:
diff changeset
    57
  "qs == rev ps"
b411f25fff25 added example for operational classes and code generator
haftmann
parents:
diff changeset
    58
b411f25fff25 added example for operational classes and code generator
haftmann
parents:
diff changeset
    59
subsection {* mutual datatypes *}
b411f25fff25 added example for operational classes and code generator
haftmann
parents:
diff changeset
    60
b411f25fff25 added example for operational classes and code generator
haftmann
parents:
diff changeset
    61
datatype mut1 = Tip | Top mut2
b411f25fff25 added example for operational classes and code generator
haftmann
parents:
diff changeset
    62
  and mut2 = Tip | Top mut1
b411f25fff25 added example for operational classes and code generator
haftmann
parents:
diff changeset
    63
b411f25fff25 added example for operational classes and code generator
haftmann
parents:
diff changeset
    64
consts
b411f25fff25 added example for operational classes and code generator
haftmann
parents:
diff changeset
    65
  mut1 :: "mut1 \<Rightarrow> mut1"
b411f25fff25 added example for operational classes and code generator
haftmann
parents:
diff changeset
    66
  mut2 :: "mut2 \<Rightarrow> mut2"
b411f25fff25 added example for operational classes and code generator
haftmann
parents:
diff changeset
    67
b411f25fff25 added example for operational classes and code generator
haftmann
parents:
diff changeset
    68
primrec
b411f25fff25 added example for operational classes and code generator
haftmann
parents:
diff changeset
    69
  "mut1 mut1.Tip = mut1.Tip"
b411f25fff25 added example for operational classes and code generator
haftmann
parents:
diff changeset
    70
  "mut1 (mut1.Top x) = mut1.Top (mut2 x)"
b411f25fff25 added example for operational classes and code generator
haftmann
parents:
diff changeset
    71
  "mut2 mut2.Tip = mut2.Tip"
b411f25fff25 added example for operational classes and code generator
haftmann
parents:
diff changeset
    72
  "mut2 (mut2.Top x) = mut2.Top (mut1 x)"
b411f25fff25 added example for operational classes and code generator
haftmann
parents:
diff changeset
    73
20351
c7658e811ffb added more examples
haftmann
parents: 20187
diff changeset
    74
subsection {* records *}
19281
b411f25fff25 added example for operational classes and code generator
haftmann
parents:
diff changeset
    75
b411f25fff25 added example for operational classes and code generator
haftmann
parents:
diff changeset
    76
subsection {* equalities *}
b411f25fff25 added example for operational classes and code generator
haftmann
parents:
diff changeset
    77
19789
c08c9f9ea9a5 small fix
haftmann
parents: 19604
diff changeset
    78
subsection {* heavy usage of names *}
19281
b411f25fff25 added example for operational classes and code generator
haftmann
parents:
diff changeset
    79
b411f25fff25 added example for operational classes and code generator
haftmann
parents:
diff changeset
    80
definition
b411f25fff25 added example for operational classes and code generator
haftmann
parents:
diff changeset
    81
  f :: nat
b411f25fff25 added example for operational classes and code generator
haftmann
parents:
diff changeset
    82
  "f = 2"
b411f25fff25 added example for operational classes and code generator
haftmann
parents:
diff changeset
    83
  g :: nat
b411f25fff25 added example for operational classes and code generator
haftmann
parents:
diff changeset
    84
  "g = f"
b411f25fff25 added example for operational classes and code generator
haftmann
parents:
diff changeset
    85
  h :: nat
b411f25fff25 added example for operational classes and code generator
haftmann
parents:
diff changeset
    86
  "h = g"
b411f25fff25 added example for operational classes and code generator
haftmann
parents:
diff changeset
    87
20383
58f65fc90cf4 adaptions to improvements
haftmann
parents: 20351
diff changeset
    88
code_constname
58f65fc90cf4 adaptions to improvements
haftmann
parents: 20351
diff changeset
    89
  f "Mymod.f"
58f65fc90cf4 adaptions to improvements
haftmann
parents: 20351
diff changeset
    90
  g "Mymod.A.f"
58f65fc90cf4 adaptions to improvements
haftmann
parents: 20351
diff changeset
    91
  h "Mymod.A.B.f"
19281
b411f25fff25 added example for operational classes and code generator
haftmann
parents:
diff changeset
    92
20351
c7658e811ffb added more examples
haftmann
parents: 20187
diff changeset
    93
code_generate (ml, haskell)
c7658e811ffb added more examples
haftmann
parents: 20187
diff changeset
    94
  n one "0::int" "0::nat" "1::int" "1::nat"
c7658e811ffb added more examples
haftmann
parents: 20187
diff changeset
    95
code_generate (ml, haskell)
c7658e811ffb added more examples
haftmann
parents: 20187
diff changeset
    96
  fac
20383
58f65fc90cf4 adaptions to improvements
haftmann
parents: 20351
diff changeset
    97
code_generate
20351
c7658e811ffb added more examples
haftmann
parents: 20187
diff changeset
    98
  xor
20383
58f65fc90cf4 adaptions to improvements
haftmann
parents: 20351
diff changeset
    99
code_generate
20351
c7658e811ffb added more examples
haftmann
parents: 20187
diff changeset
   100
  "op + :: nat \<Rightarrow> nat \<Rightarrow> nat"
c7658e811ffb added more examples
haftmann
parents: 20187
diff changeset
   101
  "op - :: nat \<Rightarrow> nat \<Rightarrow> nat"
c7658e811ffb added more examples
haftmann
parents: 20187
diff changeset
   102
  "op * :: nat \<Rightarrow> nat \<Rightarrow> nat"
c7658e811ffb added more examples
haftmann
parents: 20187
diff changeset
   103
  "op < :: nat \<Rightarrow> nat \<Rightarrow> bool"
c7658e811ffb added more examples
haftmann
parents: 20187
diff changeset
   104
  "op <= :: nat \<Rightarrow> nat \<Rightarrow> bool"
20383
58f65fc90cf4 adaptions to improvements
haftmann
parents: 20351
diff changeset
   105
code_generate
20351
c7658e811ffb added more examples
haftmann
parents: 20187
diff changeset
   106
  Pair fst snd Let split swap swapp appl
c7658e811ffb added more examples
haftmann
parents: 20187
diff changeset
   107
code_generate (ml, haskell)
c7658e811ffb added more examples
haftmann
parents: 20187
diff changeset
   108
  k
c7658e811ffb added more examples
haftmann
parents: 20187
diff changeset
   109
  "op + :: int \<Rightarrow> int \<Rightarrow> int"
c7658e811ffb added more examples
haftmann
parents: 20187
diff changeset
   110
  "op - :: int \<Rightarrow> int \<Rightarrow> int"
c7658e811ffb added more examples
haftmann
parents: 20187
diff changeset
   111
  "op * :: int \<Rightarrow> int \<Rightarrow> int"
c7658e811ffb added more examples
haftmann
parents: 20187
diff changeset
   112
  "op < :: int \<Rightarrow> int \<Rightarrow> bool"
c7658e811ffb added more examples
haftmann
parents: 20187
diff changeset
   113
  "op <= :: int \<Rightarrow> int \<Rightarrow> bool"
c7658e811ffb added more examples
haftmann
parents: 20187
diff changeset
   114
  fac
c7658e811ffb added more examples
haftmann
parents: 20187
diff changeset
   115
  "op div :: int \<Rightarrow> int \<Rightarrow> int"
c7658e811ffb added more examples
haftmann
parents: 20187
diff changeset
   116
  "op mod :: int \<Rightarrow> int \<Rightarrow> int"  
20383
58f65fc90cf4 adaptions to improvements
haftmann
parents: 20351
diff changeset
   117
code_generate
20351
c7658e811ffb added more examples
haftmann
parents: 20187
diff changeset
   118
  Inl Inr
20383
58f65fc90cf4 adaptions to improvements
haftmann
parents: 20351
diff changeset
   119
code_generate
20351
c7658e811ffb added more examples
haftmann
parents: 20187
diff changeset
   120
  None Some
20383
58f65fc90cf4 adaptions to improvements
haftmann
parents: 20351
diff changeset
   121
code_generate
20351
c7658e811ffb added more examples
haftmann
parents: 20187
diff changeset
   122
  hd tl "op @" ps qs
20383
58f65fc90cf4 adaptions to improvements
haftmann
parents: 20351
diff changeset
   123
code_generate
20351
c7658e811ffb added more examples
haftmann
parents: 20187
diff changeset
   124
  mut1 mut2
c7658e811ffb added more examples
haftmann
parents: 20187
diff changeset
   125
code_generate (ml, haskell)
c7658e811ffb added more examples
haftmann
parents: 20187
diff changeset
   126
  "op @" filter concat foldl foldr hd tl
c7658e811ffb added more examples
haftmann
parents: 20187
diff changeset
   127
  last butlast list_all2
c7658e811ffb added more examples
haftmann
parents: 20187
diff changeset
   128
  map 
c7658e811ffb added more examples
haftmann
parents: 20187
diff changeset
   129
  nth 
c7658e811ffb added more examples
haftmann
parents: 20187
diff changeset
   130
  list_update
c7658e811ffb added more examples
haftmann
parents: 20187
diff changeset
   131
  take
c7658e811ffb added more examples
haftmann
parents: 20187
diff changeset
   132
  drop
c7658e811ffb added more examples
haftmann
parents: 20187
diff changeset
   133
  takeWhile
c7658e811ffb added more examples
haftmann
parents: 20187
diff changeset
   134
  dropWhile
c7658e811ffb added more examples
haftmann
parents: 20187
diff changeset
   135
  rev
c7658e811ffb added more examples
haftmann
parents: 20187
diff changeset
   136
  zip
c7658e811ffb added more examples
haftmann
parents: 20187
diff changeset
   137
  upt
c7658e811ffb added more examples
haftmann
parents: 20187
diff changeset
   138
  remdups
c7658e811ffb added more examples
haftmann
parents: 20187
diff changeset
   139
  remove1
c7658e811ffb added more examples
haftmann
parents: 20187
diff changeset
   140
  null
c7658e811ffb added more examples
haftmann
parents: 20187
diff changeset
   141
  "distinct"
c7658e811ffb added more examples
haftmann
parents: 20187
diff changeset
   142
  replicate
c7658e811ffb added more examples
haftmann
parents: 20187
diff changeset
   143
  rotate1
c7658e811ffb added more examples
haftmann
parents: 20187
diff changeset
   144
  rotate
c7658e811ffb added more examples
haftmann
parents: 20187
diff changeset
   145
  splice
20383
58f65fc90cf4 adaptions to improvements
haftmann
parents: 20351
diff changeset
   146
code_generate
20351
c7658e811ffb added more examples
haftmann
parents: 20187
diff changeset
   147
  foo1 foo3
c7658e811ffb added more examples
haftmann
parents: 20187
diff changeset
   148
code_generate (ml, haskell)
c7658e811ffb added more examples
haftmann
parents: 20187
diff changeset
   149
  "op = :: bool \<Rightarrow> bool \<Rightarrow> bool"
c7658e811ffb added more examples
haftmann
parents: 20187
diff changeset
   150
  "op = :: nat \<Rightarrow> nat \<Rightarrow> bool"
c7658e811ffb added more examples
haftmann
parents: 20187
diff changeset
   151
  "op = :: int \<Rightarrow> int \<Rightarrow> bool"
c7658e811ffb added more examples
haftmann
parents: 20187
diff changeset
   152
  "op = :: 'a * 'b \<Rightarrow> 'a * 'b \<Rightarrow> bool"
c7658e811ffb added more examples
haftmann
parents: 20187
diff changeset
   153
  "op = :: 'a + 'b \<Rightarrow> 'a + 'b \<Rightarrow> bool"
c7658e811ffb added more examples
haftmann
parents: 20187
diff changeset
   154
  "op = :: 'a option \<Rightarrow> 'a option \<Rightarrow> bool"
c7658e811ffb added more examples
haftmann
parents: 20187
diff changeset
   155
  "op = :: 'a list \<Rightarrow> 'a list \<Rightarrow> bool"
20383
58f65fc90cf4 adaptions to improvements
haftmann
parents: 20351
diff changeset
   156
  "op = :: point \<Rightarrow> point \<Rightarrow> bool"
20351
c7658e811ffb added more examples
haftmann
parents: 20187
diff changeset
   157
  "op = :: mut1 \<Rightarrow> mut1 \<Rightarrow> bool"
c7658e811ffb added more examples
haftmann
parents: 20187
diff changeset
   158
  "op = :: mut2 \<Rightarrow> mut2 \<Rightarrow> bool"
20383
58f65fc90cf4 adaptions to improvements
haftmann
parents: 20351
diff changeset
   159
code_generate
20351
c7658e811ffb added more examples
haftmann
parents: 20187
diff changeset
   160
  f g h
19281
b411f25fff25 added example for operational classes and code generator
haftmann
parents:
diff changeset
   161
b411f25fff25 added example for operational classes and code generator
haftmann
parents:
diff changeset
   162
code_serialize ml (-)
b411f25fff25 added example for operational classes and code generator
haftmann
parents:
diff changeset
   163
b411f25fff25 added example for operational classes and code generator
haftmann
parents:
diff changeset
   164
end