src/HOL/ex/Codegenerator.thy
author krauss
Fri Nov 24 13:43:44 2006 +0100 (2006-11-24)
changeset 21511 16c62deb1adf
parent 21460 cda5cd8bfd16
child 21545 54cc492d80a9
permissions -rw-r--r--
The function package declares the [code] attribute automatically again.
haftmann@19281
     1
(*  ID:         $Id$
haftmann@19281
     2
    Author:     Florian Haftmann, TU Muenchen
haftmann@19281
     3
*)
haftmann@19281
     4
haftmann@20187
     5
header {* Test and Examples for code generator *}
haftmann@19281
     6
haftmann@19281
     7
theory Codegenerator
haftmann@21155
     8
imports Main Records
haftmann@19281
     9
begin
haftmann@19281
    10
haftmann@19281
    11
subsection {* booleans *}
haftmann@19281
    12
haftmann@19281
    13
definition
wenzelm@21404
    14
  xor :: "bool \<Rightarrow> bool \<Rightarrow> bool" where
haftmann@19281
    15
  "xor p q = ((p | q) & \<not> (p & q))"
haftmann@19281
    16
haftmann@19281
    17
subsection {* natural numbers *}
haftmann@19281
    18
haftmann@19281
    19
definition
wenzelm@21404
    20
  n :: nat where
haftmann@19281
    21
  "n = 42"
haftmann@19281
    22
haftmann@19281
    23
subsection {* pairs *}
haftmann@19281
    24
haftmann@19281
    25
definition
wenzelm@21404
    26
  swap :: "'a * 'b \<Rightarrow> 'b * 'a" where
haftmann@19281
    27
  "swap p = (let (x, y) = p in (y, x))"
wenzelm@21404
    28
wenzelm@21404
    29
definition
wenzelm@21404
    30
  appl :: "('a \<Rightarrow> 'b) * 'a \<Rightarrow> 'b" where
haftmann@19281
    31
  "appl p = (let (f, x) = p in f x)"
wenzelm@21404
    32
wenzelm@21404
    33
definition
wenzelm@21404
    34
  snd_three :: "'a * 'b * 'c => 'b" where
haftmann@21092
    35
  "snd_three a = id (\<lambda>(a, b, c). b) a"
haftmann@19281
    36
haftmann@20936
    37
lemma [code]:
haftmann@20936
    38
  "swap (x, y) = (y, x)"
haftmann@20936
    39
  unfolding swap_def Let_def by auto
haftmann@20936
    40
haftmann@20936
    41
lemma [code]:
haftmann@20936
    42
  "appl (f, x) = f x"
haftmann@20936
    43
  unfolding appl_def Let_def by auto
haftmann@20936
    44
haftmann@20187
    45
subsection {* integers *}
haftmann@20187
    46
haftmann@19281
    47
definition
wenzelm@21404
    48
  k :: "int" where
haftmann@20351
    49
  "k = -42"
haftmann@19281
    50
haftmann@20968
    51
function
haftmann@20968
    52
  fac :: "int => int" where
haftmann@20968
    53
  "fac j = (if j <= 0 then 1 else j * (fac (j - 1)))"
haftmann@20968
    54
  by pat_completeness auto
krauss@21319
    55
termination by (relation "measure nat") auto
haftmann@19281
    56
haftmann@19281
    57
subsection {* sums *}
haftmann@19281
    58
haftmann@19281
    59
subsection {* options *}
haftmann@19281
    60
haftmann@19281
    61
subsection {* lists *}
haftmann@19281
    62
haftmann@19281
    63
definition
wenzelm@21404
    64
  ps :: "nat list" where
haftmann@19281
    65
  "ps = [2, 3, 5, 7, 11]"
wenzelm@21404
    66
wenzelm@21404
    67
definition
wenzelm@21404
    68
  qs :: "nat list" where
haftmann@19281
    69
  "qs == rev ps"
haftmann@19281
    70
haftmann@19281
    71
subsection {* mutual datatypes *}
haftmann@19281
    72
haftmann@19281
    73
datatype mut1 = Tip | Top mut2
haftmann@19281
    74
  and mut2 = Tip | Top mut1
haftmann@19281
    75
haftmann@19281
    76
consts
haftmann@19281
    77
  mut1 :: "mut1 \<Rightarrow> mut1"
haftmann@19281
    78
  mut2 :: "mut2 \<Rightarrow> mut2"
haftmann@19281
    79
haftmann@19281
    80
primrec
haftmann@19281
    81
  "mut1 mut1.Tip = mut1.Tip"
haftmann@19281
    82
  "mut1 (mut1.Top x) = mut1.Top (mut2 x)"
haftmann@19281
    83
  "mut2 mut2.Tip = mut2.Tip"
haftmann@19281
    84
  "mut2 (mut2.Top x) = mut2.Top (mut1 x)"
haftmann@19281
    85
haftmann@20351
    86
subsection {* records *}
haftmann@19281
    87
haftmann@19281
    88
subsection {* equalities *}
haftmann@19281
    89
haftmann@20702
    90
subsection {* strings *}
haftmann@20702
    91
haftmann@20702
    92
definition
haftmann@20702
    93
  "mystring = ''my home is my castle''"
haftmann@20702
    94
haftmann@20968
    95
subsection {* nested lets and such *}
haftmann@20968
    96
haftmann@20968
    97
definition
haftmann@20968
    98
  "abs_let x = (let (y, z) = x in (\<lambda>u. case u of () \<Rightarrow> (y + y)))"
haftmann@20968
    99
haftmann@20968
   100
definition
haftmann@20968
   101
  "nested_let x = (let (y, z) = x in let w = y z in w * w)"
haftmann@20968
   102
haftmann@20968
   103
definition
haftmann@20968
   104
  "case_let x = (let (y, z) = x in case y of () => z)"
haftmann@20968
   105
haftmann@21155
   106
definition
haftmann@21155
   107
  "base_case f = f list_case"
haftmann@21155
   108
haftmann@20702
   109
definition
haftmann@20702
   110
  "apply_tower = (\<lambda>x. x (\<lambda>x. x (\<lambda>x. x)))"
haftmann@20702
   111
haftmann@20702
   112
definition
haftmann@20702
   113
  "keywords fun datatype class instance funa classa =
haftmann@20702
   114
    Suc fun + datatype * class mod instance - funa - classa"
haftmann@20702
   115
haftmann@20702
   116
hide (open) const keywords
haftmann@20702
   117
haftmann@20702
   118
definition
haftmann@20702
   119
  "shadow keywords = keywords @ [Codegenerator.keywords 0 0 0 0 0 0]"
haftmann@20702
   120
haftmann@20713
   121
code_gen
haftmann@20713
   122
  xor
haftmann@20713
   123
code_gen
haftmann@20713
   124
  "0::nat" "1::nat"
haftmann@20702
   125
code_gen
haftmann@21092
   126
  Pair fst snd Let split swap snd_three
haftmann@20453
   127
code_gen
haftmann@20351
   128
  "op + :: nat \<Rightarrow> nat \<Rightarrow> nat"
haftmann@20351
   129
  "op - :: nat \<Rightarrow> nat \<Rightarrow> nat"
haftmann@20351
   130
  "op * :: nat \<Rightarrow> nat \<Rightarrow> nat"
haftmann@20351
   131
  "op < :: nat \<Rightarrow> nat \<Rightarrow> bool"
haftmann@20351
   132
  "op <= :: nat \<Rightarrow> nat \<Rightarrow> bool"
haftmann@20453
   133
code_gen
haftmann@20597
   134
  appl
haftmann@20453
   135
code_gen
haftmann@20351
   136
  Inl Inr
haftmann@20453
   137
code_gen
haftmann@20351
   138
  None Some
haftmann@20453
   139
code_gen
haftmann@20351
   140
  hd tl "op @" ps qs
haftmann@20453
   141
code_gen
haftmann@20351
   142
  mut1 mut2
haftmann@20453
   143
code_gen
haftmann@20351
   144
  remove1
haftmann@20351
   145
  null
haftmann@20351
   146
  replicate
haftmann@20351
   147
  rotate1
haftmann@20351
   148
  rotate
haftmann@20351
   149
  splice
haftmann@20597
   150
code_gen
haftmann@20597
   151
  remdups
haftmann@20597
   152
  "distinct"
haftmann@21155
   153
  filter
haftmann@20453
   154
code_gen
haftmann@20351
   155
  foo1 foo3
haftmann@20453
   156
code_gen
haftmann@20936
   157
  mystring
haftmann@20936
   158
code_gen
haftmann@21155
   159
  apply_tower Codegenerator.keywords shadow base_case
haftmann@20968
   160
code_gen
haftmann@20968
   161
  abs_let nested_let case_let
haftmann@20936
   162
code_gen "0::int" "1::int"
haftmann@20936
   163
  (SML) (Haskell)
haftmann@20936
   164
code_gen n
haftmann@20936
   165
  (SML) (Haskell)
haftmann@20936
   166
code_gen fac
haftmann@20936
   167
  (SML) (Haskell)
haftmann@20936
   168
code_gen
haftmann@20936
   169
  k
haftmann@20936
   170
  "op + :: int \<Rightarrow> int \<Rightarrow> int"
haftmann@20936
   171
  "op - :: int \<Rightarrow> int \<Rightarrow> int"
haftmann@20936
   172
  "op * :: int \<Rightarrow> int \<Rightarrow> int"
haftmann@20936
   173
  "op < :: int \<Rightarrow> int \<Rightarrow> bool"
haftmann@20936
   174
  "op <= :: int \<Rightarrow> int \<Rightarrow> bool"
haftmann@20936
   175
  fac
haftmann@20936
   176
  "op div :: int \<Rightarrow> int \<Rightarrow> int"
haftmann@20936
   177
  "op mod :: int \<Rightarrow> int \<Rightarrow> int"  
haftmann@20936
   178
  (SML) (Haskell)
haftmann@20936
   179
code_gen
haftmann@21460
   180
  "op = :: bool \<Rightarrow> bool \<Rightarrow> bool"
haftmann@21460
   181
  "op = :: nat \<Rightarrow> nat \<Rightarrow> bool"
haftmann@21460
   182
  "op = :: int \<Rightarrow> int \<Rightarrow> bool"
haftmann@21460
   183
  "op = :: ('a\<Colon>eq) * ('b\<Colon>eq) \<Rightarrow> 'a * 'b \<Rightarrow> bool"
haftmann@21460
   184
  "op = :: ('a\<Colon>eq) + ('b\<Colon>eq) \<Rightarrow> 'a + 'b \<Rightarrow> bool"
haftmann@21460
   185
  "op = :: ('a\<Colon>eq) option \<Rightarrow> 'a option \<Rightarrow> bool"
haftmann@21460
   186
  "op = :: ('a\<Colon>eq) list \<Rightarrow> 'a list \<Rightarrow> bool"
haftmann@21460
   187
  "op = :: mut1 \<Rightarrow> mut1 \<Rightarrow> bool"
haftmann@21460
   188
  "op = :: mut2 \<Rightarrow> mut2 \<Rightarrow> bool"
haftmann@21460
   189
  "op = :: ('a\<Colon>eq) point_scheme \<Rightarrow> 'a point_scheme \<Rightarrow> bool"
haftmann@19281
   190
haftmann@21420
   191
code_gen (SML *) (Haskell -)
haftmann@19281
   192
haftmann@19281
   193
end