src/HOL/ex/Codegenerator.thy
author haftmann
Mon Sep 25 17:04:19 2006 +0200 (2006-09-25)
changeset 20702 8b79d853eabb
parent 20597 65fe827aa595
child 20713 823967ef47f1
permissions -rw-r--r--
added examples for variable name handling
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@20351
     8
imports Main "~~/src/HOL/ex/Records"
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@19281
    17
subsection {* natural numbers *}
haftmann@19281
    18
haftmann@19281
    19
definition
haftmann@19281
    20
  one :: nat
haftmann@19281
    21
  "one = 1"
haftmann@19281
    22
  n :: nat
haftmann@19281
    23
  "n = 42"
haftmann@19281
    24
haftmann@19281
    25
subsection {* pairs *}
haftmann@19281
    26
haftmann@19281
    27
definition
haftmann@19281
    28
  swap :: "'a * 'b \<Rightarrow> 'b * 'a"
haftmann@19281
    29
  "swap p = (let (x, y) = p in (y, x))"
haftmann@19281
    30
  appl :: "('a \<Rightarrow> 'b) * 'a \<Rightarrow> 'b"
haftmann@19281
    31
  "appl p = (let (f, x) = p in f x)"
haftmann@19281
    32
haftmann@20187
    33
subsection {* integers *}
haftmann@20187
    34
haftmann@19281
    35
definition
haftmann@19281
    36
  k :: "int"
haftmann@20351
    37
  "k = -42"
haftmann@19281
    38
haftmann@19281
    39
consts
haftmann@19281
    40
  fac :: "int => int"
haftmann@19281
    41
haftmann@19281
    42
recdef fac "measure nat"
haftmann@19281
    43
  "fac j = (if j <= 0 then 1 else j * (fac (j - 1)))"
haftmann@19281
    44
haftmann@19281
    45
subsection {* sums *}
haftmann@19281
    46
haftmann@19281
    47
subsection {* options *}
haftmann@19281
    48
haftmann@19281
    49
subsection {* lists *}
haftmann@19281
    50
haftmann@19281
    51
definition
haftmann@19281
    52
  ps :: "nat list"
haftmann@19281
    53
  "ps = [2, 3, 5, 7, 11]"
haftmann@19281
    54
  qs :: "nat list"
haftmann@19281
    55
  "qs == rev ps"
haftmann@19281
    56
haftmann@19281
    57
subsection {* mutual datatypes *}
haftmann@19281
    58
haftmann@19281
    59
datatype mut1 = Tip | Top mut2
haftmann@19281
    60
  and mut2 = Tip | Top mut1
haftmann@19281
    61
haftmann@19281
    62
consts
haftmann@19281
    63
  mut1 :: "mut1 \<Rightarrow> mut1"
haftmann@19281
    64
  mut2 :: "mut2 \<Rightarrow> mut2"
haftmann@19281
    65
haftmann@19281
    66
primrec
haftmann@19281
    67
  "mut1 mut1.Tip = mut1.Tip"
haftmann@19281
    68
  "mut1 (mut1.Top x) = mut1.Top (mut2 x)"
haftmann@19281
    69
  "mut2 mut2.Tip = mut2.Tip"
haftmann@19281
    70
  "mut2 (mut2.Top x) = mut2.Top (mut1 x)"
haftmann@19281
    71
haftmann@20351
    72
subsection {* records *}
haftmann@19281
    73
haftmann@19281
    74
subsection {* equalities *}
haftmann@19281
    75
haftmann@20702
    76
subsection {* strings *}
haftmann@20702
    77
haftmann@20702
    78
definition
haftmann@20702
    79
  "mystring = ''my home is my castle''"
haftmann@20702
    80
haftmann@19789
    81
subsection {* heavy usage of names *}
haftmann@19281
    82
haftmann@19281
    83
definition
haftmann@19281
    84
  f :: nat
haftmann@19281
    85
  "f = 2"
haftmann@19281
    86
  g :: nat
haftmann@19281
    87
  "g = f"
haftmann@19281
    88
  h :: nat
haftmann@19281
    89
  "h = g"
haftmann@19281
    90
haftmann@20383
    91
code_constname
haftmann@20383
    92
  f "Mymod.f"
haftmann@20383
    93
  g "Mymod.A.f"
haftmann@20383
    94
  h "Mymod.A.B.f"
haftmann@19281
    95
haftmann@20702
    96
definition
haftmann@20702
    97
  "apply_tower = (\<lambda>x. x (\<lambda>x. x (\<lambda>x. x)))"
haftmann@20702
    98
haftmann@20702
    99
definition
haftmann@20702
   100
  "keywords fun datatype class instance funa classa =
haftmann@20702
   101
    Suc fun + datatype * class mod instance - funa - classa"
haftmann@20702
   102
haftmann@20702
   103
hide (open) const keywords
haftmann@20702
   104
haftmann@20702
   105
definition
haftmann@20702
   106
  "shadow keywords = keywords @ [Codegenerator.keywords 0 0 0 0 0 0]"
haftmann@20702
   107
haftmann@20453
   108
code_gen xor
haftmann@20597
   109
code_gen one
haftmann@20702
   110
code_gen
haftmann@20702
   111
  Pair fst snd Let split swap
haftmann@20597
   112
code_gen "0::int" "1::int"
haftmann@20597
   113
  (SML) (Haskell)
haftmann@20597
   114
code_gen n
haftmann@20597
   115
  (SML) (Haskell)
haftmann@20597
   116
code_gen fac
haftmann@20597
   117
  (SML) (Haskell)
haftmann@20453
   118
code_gen
haftmann@20351
   119
  "op + :: nat \<Rightarrow> nat \<Rightarrow> nat"
haftmann@20351
   120
  "op - :: nat \<Rightarrow> nat \<Rightarrow> nat"
haftmann@20351
   121
  "op * :: nat \<Rightarrow> nat \<Rightarrow> nat"
haftmann@20351
   122
  "op < :: nat \<Rightarrow> nat \<Rightarrow> bool"
haftmann@20351
   123
  "op <= :: nat \<Rightarrow> nat \<Rightarrow> bool"
haftmann@20453
   124
code_gen
haftmann@20597
   125
  appl
haftmann@20453
   126
code_gen
haftmann@20351
   127
  k
haftmann@20351
   128
  "op + :: int \<Rightarrow> int \<Rightarrow> int"
haftmann@20351
   129
  "op - :: int \<Rightarrow> int \<Rightarrow> int"
haftmann@20351
   130
  "op * :: int \<Rightarrow> int \<Rightarrow> int"
haftmann@20351
   131
  "op < :: int \<Rightarrow> int \<Rightarrow> bool"
haftmann@20351
   132
  "op <= :: int \<Rightarrow> int \<Rightarrow> bool"
haftmann@20351
   133
  fac
haftmann@20351
   134
  "op div :: int \<Rightarrow> int \<Rightarrow> int"
haftmann@20351
   135
  "op mod :: int \<Rightarrow> int \<Rightarrow> int"  
haftmann@20453
   136
  (SML) (Haskell)
haftmann@20453
   137
code_gen
haftmann@20351
   138
  Inl Inr
haftmann@20453
   139
code_gen
haftmann@20351
   140
  None Some
haftmann@20453
   141
code_gen
haftmann@20351
   142
  hd tl "op @" ps qs
haftmann@20453
   143
code_gen
haftmann@20351
   144
  mut1 mut2
haftmann@20453
   145
code_gen
haftmann@20351
   146
  remove1
haftmann@20351
   147
  null
haftmann@20351
   148
  replicate
haftmann@20351
   149
  rotate1
haftmann@20351
   150
  rotate
haftmann@20351
   151
  splice
haftmann@20597
   152
code_gen
haftmann@20597
   153
  remdups
haftmann@20597
   154
  "distinct"
haftmann@20453
   155
code_gen
haftmann@20351
   156
  foo1 foo3
haftmann@20453
   157
code_gen
haftmann@20597
   158
  "OperationalEquality.eq :: bool \<Rightarrow> bool \<Rightarrow> bool"
haftmann@20597
   159
  "OperationalEquality.eq :: nat \<Rightarrow> nat \<Rightarrow> bool"
haftmann@20597
   160
  "OperationalEquality.eq :: int \<Rightarrow> int \<Rightarrow> bool"
haftmann@20597
   161
  "OperationalEquality.eq :: ('a\<Colon>eq) * ('b\<Colon>eq) \<Rightarrow> 'a * 'b \<Rightarrow> bool"
haftmann@20597
   162
  "OperationalEquality.eq :: ('a\<Colon>eq) + ('b\<Colon>eq) \<Rightarrow> 'a + 'b \<Rightarrow> bool"
haftmann@20597
   163
  "OperationalEquality.eq :: ('a\<Colon>eq) option \<Rightarrow> 'a option \<Rightarrow> bool"
haftmann@20597
   164
  "OperationalEquality.eq :: ('a\<Colon>eq) list \<Rightarrow> 'a list \<Rightarrow> bool"
haftmann@20597
   165
  "OperationalEquality.eq :: mut1 \<Rightarrow> mut1 \<Rightarrow> bool"
haftmann@20597
   166
  "OperationalEquality.eq :: mut2 \<Rightarrow> mut2 \<Rightarrow> bool"
haftmann@20597
   167
  "OperationalEquality.eq :: ('a\<Colon>eq) point_scheme \<Rightarrow> 'a point_scheme \<Rightarrow> bool"
haftmann@20453
   168
code_gen
haftmann@20702
   169
  mystring
haftmann@20702
   170
code_gen
haftmann@20351
   171
  f g h
haftmann@20702
   172
code_gen
haftmann@20702
   173
  apply_tower Codegenerator.keywords shadow
haftmann@19281
   174
haftmann@20702
   175
code_gen (SML -)
haftmann@19281
   176
haftmann@19281
   177
end