src/HOL/ex/Codegenerator.thy
author haftmann
Wed Jun 14 12:13:12 2006 +0200 (2006-06-14)
changeset 19888 2b4c09941e04
parent 19817 bb16bf9ae3fd
child 20187 af47971ea304
permissions -rw-r--r--
slight adaptions
haftmann@19281
     1
(*  ID:         $Id$
haftmann@19281
     2
    Author:     Florian Haftmann, TU Muenchen
haftmann@19281
     3
*)
haftmann@19281
     4
haftmann@19281
     5
header {* Test and Examples for Code Generator *}
haftmann@19281
     6
haftmann@19281
     7
theory Codegenerator
haftmann@19281
     8
imports Main
haftmann@19281
     9
begin
haftmann@19281
    10
haftmann@19281
    11
subsection {* booleans *}
haftmann@19281
    12
haftmann@19281
    13
definition
haftmann@19281
    14
  xor :: "bool \<Rightarrow> bool \<Rightarrow> bool"
haftmann@19281
    15
  "xor p q = ((p | q) & \<not> (p & q))"
haftmann@19281
    16
haftmann@19888
    17
code_generate (ml, haskell) xor
haftmann@19281
    18
haftmann@19281
    19
subsection {* natural numbers *}
haftmann@19281
    20
haftmann@19281
    21
definition
haftmann@19281
    22
  one :: nat
haftmann@19281
    23
  "one = 1"
haftmann@19281
    24
  n :: nat
haftmann@19281
    25
  "n = 42"
haftmann@19281
    26
haftmann@19888
    27
code_generate (ml, haskell) n
haftmann@19817
    28
haftmann@19888
    29
code_generate (ml, haskell)
haftmann@19281
    30
  "0::nat" "one" n
haftmann@19281
    31
  "op + :: nat \<Rightarrow> nat \<Rightarrow> nat"
haftmann@19281
    32
  "op - :: nat \<Rightarrow> nat \<Rightarrow> nat"
haftmann@19281
    33
  "op * :: nat \<Rightarrow> nat \<Rightarrow> nat"
haftmann@19281
    34
  "op < :: nat \<Rightarrow> nat \<Rightarrow> bool"
haftmann@19281
    35
  "op <= :: nat \<Rightarrow> nat \<Rightarrow> bool"
haftmann@19281
    36
haftmann@19281
    37
subsection {* pairs *}
haftmann@19281
    38
haftmann@19281
    39
definition
haftmann@19281
    40
  swap :: "'a * 'b \<Rightarrow> 'b * 'a"
haftmann@19281
    41
  "swap p = (let (x, y) = p in (y, x))"
haftmann@19281
    42
  swapp :: "'a * 'b \<Rightarrow> 'c * 'd \<Rightarrow> ('a * 'c) * ('b * 'd)"
haftmann@19281
    43
  "swapp = (\<lambda>(x, y) (z, w). ((x, z), (y, w)))"
haftmann@19281
    44
  appl :: "('a \<Rightarrow> 'b) * 'a \<Rightarrow> 'b"
haftmann@19281
    45
  "appl p = (let (f, x) = p in f x)"
haftmann@19281
    46
haftmann@19888
    47
code_generate (ml, haskell) Pair fst snd Let split swap swapp appl
haftmann@19281
    48
haftmann@19281
    49
definition
haftmann@19281
    50
  k :: "int"
haftmann@19281
    51
  "k = 42"
haftmann@19281
    52
haftmann@19281
    53
consts
haftmann@19281
    54
  fac :: "int => int"
haftmann@19281
    55
haftmann@19281
    56
recdef fac "measure nat"
haftmann@19281
    57
  "fac j = (if j <= 0 then 1 else j * (fac (j - 1)))"
haftmann@19281
    58
haftmann@19888
    59
code_generate (ml, haskell)
haftmann@19604
    60
  "0::int" k
haftmann@19281
    61
  "op + :: int \<Rightarrow> int \<Rightarrow> int"
haftmann@19281
    62
  "op - :: int \<Rightarrow> int \<Rightarrow> int"
haftmann@19281
    63
  "op * :: int \<Rightarrow> int \<Rightarrow> int"
haftmann@19281
    64
  "op < :: int \<Rightarrow> int \<Rightarrow> bool"
haftmann@19281
    65
  "op <= :: int \<Rightarrow> int \<Rightarrow> bool"
haftmann@19281
    66
  fac
haftmann@19281
    67
haftmann@19281
    68
subsection {* sums *}
haftmann@19281
    69
haftmann@19888
    70
code_generate (ml, haskell) Inl Inr
haftmann@19281
    71
haftmann@19281
    72
subsection {* options *}
haftmann@19281
    73
haftmann@19888
    74
code_generate (ml, haskell) None Some
haftmann@19281
    75
haftmann@19281
    76
subsection {* lists *}
haftmann@19281
    77
haftmann@19281
    78
definition
haftmann@19281
    79
  ps :: "nat list"
haftmann@19281
    80
  "ps = [2, 3, 5, 7, 11]"
haftmann@19281
    81
  qs :: "nat list"
haftmann@19281
    82
  "qs == rev ps"
haftmann@19281
    83
haftmann@19888
    84
code_generate (ml, haskell) hd tl "op @" ps qs
haftmann@19281
    85
haftmann@19281
    86
subsection {* mutual datatypes *}
haftmann@19281
    87
haftmann@19281
    88
datatype mut1 = Tip | Top mut2
haftmann@19281
    89
  and mut2 = Tip | Top mut1
haftmann@19281
    90
haftmann@19281
    91
consts
haftmann@19281
    92
  mut1 :: "mut1 \<Rightarrow> mut1"
haftmann@19281
    93
  mut2 :: "mut2 \<Rightarrow> mut2"
haftmann@19281
    94
haftmann@19281
    95
primrec
haftmann@19281
    96
  "mut1 mut1.Tip = mut1.Tip"
haftmann@19281
    97
  "mut1 (mut1.Top x) = mut1.Top (mut2 x)"
haftmann@19281
    98
  "mut2 mut2.Tip = mut2.Tip"
haftmann@19281
    99
  "mut2 (mut2.Top x) = mut2.Top (mut1 x)"
haftmann@19281
   100
haftmann@19888
   101
code_generate (ml, haskell) mut1 mut2
haftmann@19281
   102
haftmann@19281
   103
subsection {* equalities *}
haftmann@19281
   104
haftmann@19888
   105
code_generate (ml, haskell)
haftmann@19281
   106
  "op = :: bool \<Rightarrow> bool \<Rightarrow> bool"
haftmann@19281
   107
  "op = :: nat \<Rightarrow> nat \<Rightarrow> bool"
haftmann@19281
   108
  "op = :: int \<Rightarrow> int \<Rightarrow> bool"
haftmann@19281
   109
  "op = :: 'a * 'b \<Rightarrow> 'a * 'b \<Rightarrow> bool"
haftmann@19281
   110
  "op = :: 'a + 'b \<Rightarrow> 'a + 'b \<Rightarrow> bool"
haftmann@19281
   111
  "op = :: 'a option \<Rightarrow> 'a option \<Rightarrow> bool"
haftmann@19281
   112
  "op = :: 'a list \<Rightarrow> 'a list \<Rightarrow> bool"
haftmann@19281
   113
  "op = :: mut1 \<Rightarrow> mut1 \<Rightarrow> bool"
haftmann@19281
   114
  "op = :: mut2 \<Rightarrow> mut2 \<Rightarrow> bool"
haftmann@19281
   115
haftmann@19817
   116
haftmann@19789
   117
subsection {* heavy usage of names *}
haftmann@19281
   118
haftmann@19281
   119
definition
haftmann@19281
   120
  f :: nat
haftmann@19281
   121
  "f = 2"
haftmann@19281
   122
  g :: nat
haftmann@19281
   123
  "g = f"
haftmann@19281
   124
  h :: nat
haftmann@19281
   125
  "h = g"
haftmann@19281
   126
haftmann@19281
   127
code_alias
haftmann@19281
   128
  "Codegenerator.f" "Mymod.f"
haftmann@19281
   129
  "Codegenerator.g" "Mymod.A.f"
haftmann@19281
   130
  "Codegenerator.h" "Mymod.A.B.f"
haftmann@19281
   131
haftmann@19888
   132
code_generate (ml, haskell) f g h
haftmann@19281
   133
haftmann@19281
   134
code_serialize ml (-)
haftmann@19281
   135
haftmann@19281
   136
end