src/HOL/ex/Codegenerator.thy
changeset 19281 b411f25fff25
child 19604 02f5fbdd5c54
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/ex/Codegenerator.thy	Fri Mar 17 14:20:24 2006 +0100
     1.3 @@ -0,0 +1,133 @@
     1.4 +(*  ID:         $Id$
     1.5 +    Author:     Florian Haftmann, TU Muenchen
     1.6 +*)
     1.7 +
     1.8 +header {* Test and Examples for Code Generator *}
     1.9 +
    1.10 +theory Codegenerator
    1.11 +imports Main
    1.12 +begin
    1.13 +
    1.14 +subsection {* booleans *}
    1.15 +
    1.16 +definition
    1.17 +  xor :: "bool \<Rightarrow> bool \<Rightarrow> bool"
    1.18 +  "xor p q = ((p | q) & \<not> (p & q))"
    1.19 +
    1.20 +code_generate xor
    1.21 +
    1.22 +subsection {* natural numbers *}
    1.23 +
    1.24 +definition
    1.25 +  one :: nat
    1.26 +  "one = 1"
    1.27 +  n :: nat
    1.28 +  "n = 42"
    1.29 +
    1.30 +code_generate
    1.31 +  "0::nat" "one" n
    1.32 +  "op + :: nat \<Rightarrow> nat \<Rightarrow> nat"
    1.33 +  "op - :: nat \<Rightarrow> nat \<Rightarrow> nat"
    1.34 +  "op * :: nat \<Rightarrow> nat \<Rightarrow> nat"
    1.35 +  "op < :: nat \<Rightarrow> nat \<Rightarrow> bool"
    1.36 +  "op <= :: nat \<Rightarrow> nat \<Rightarrow> bool"
    1.37 +
    1.38 +subsection {* pairs *}
    1.39 +
    1.40 +definition
    1.41 +  swap :: "'a * 'b \<Rightarrow> 'b * 'a"
    1.42 +  "swap p = (let (x, y) = p in (y, x))"
    1.43 +  swapp :: "'a * 'b \<Rightarrow> 'c * 'd \<Rightarrow> ('a * 'c) * ('b * 'd)"
    1.44 +  "swapp = (\<lambda>(x, y) (z, w). ((x, z), (y, w)))"
    1.45 +  appl :: "('a \<Rightarrow> 'b) * 'a \<Rightarrow> 'b"
    1.46 +  "appl p = (let (f, x) = p in f x)"
    1.47 +
    1.48 +code_generate Pair fst snd Let split swap swapp appl
    1.49 +
    1.50 +definition
    1.51 +  k :: "int"
    1.52 +  "k = 42"
    1.53 +
    1.54 +consts
    1.55 +  fac :: "int => int"
    1.56 +
    1.57 +recdef fac "measure nat"
    1.58 +  "fac j = (if j <= 0 then 1 else j * (fac (j - 1)))"
    1.59 +
    1.60 +code_generate
    1.61 +  "0::int" "1::int" k
    1.62 +  "op + :: int \<Rightarrow> int \<Rightarrow> int"
    1.63 +  "op - :: int \<Rightarrow> int \<Rightarrow> int"
    1.64 +  "op * :: int \<Rightarrow> int \<Rightarrow> int"
    1.65 +  "op < :: int \<Rightarrow> int \<Rightarrow> bool"
    1.66 +  "op <= :: int \<Rightarrow> int \<Rightarrow> bool"
    1.67 +  fac
    1.68 +
    1.69 +subsection {* sums *}
    1.70 +
    1.71 +code_generate Inl Inr
    1.72 +
    1.73 +subsection {* options *}
    1.74 +
    1.75 +code_generate None Some
    1.76 +
    1.77 +subsection {* lists *}
    1.78 +
    1.79 +definition
    1.80 +  ps :: "nat list"
    1.81 +  "ps = [2, 3, 5, 7, 11]"
    1.82 +  qs :: "nat list"
    1.83 +  "qs == rev ps"
    1.84 +
    1.85 +code_generate hd tl "op @" ps qs
    1.86 +
    1.87 +subsection {* mutual datatypes *}
    1.88 +
    1.89 +datatype mut1 = Tip | Top mut2
    1.90 +  and mut2 = Tip | Top mut1
    1.91 +
    1.92 +consts
    1.93 +  mut1 :: "mut1 \<Rightarrow> mut1"
    1.94 +  mut2 :: "mut2 \<Rightarrow> mut2"
    1.95 +
    1.96 +primrec
    1.97 +  "mut1 mut1.Tip = mut1.Tip"
    1.98 +  "mut1 (mut1.Top x) = mut1.Top (mut2 x)"
    1.99 +  "mut2 mut2.Tip = mut2.Tip"
   1.100 +  "mut2 (mut2.Top x) = mut2.Top (mut1 x)"
   1.101 +
   1.102 +code_generate mut1 mut2
   1.103 +
   1.104 +subsection {* equalities *}
   1.105 +
   1.106 +code_generate
   1.107 +  "op = :: bool \<Rightarrow> bool \<Rightarrow> bool"
   1.108 +  "op = :: nat \<Rightarrow> nat \<Rightarrow> bool"
   1.109 +  "op = :: int \<Rightarrow> int \<Rightarrow> bool"
   1.110 +  "op = :: 'a * 'b \<Rightarrow> 'a * 'b \<Rightarrow> bool"
   1.111 +  "op = :: 'a + 'b \<Rightarrow> 'a + 'b \<Rightarrow> bool"
   1.112 +  "op = :: 'a option \<Rightarrow> 'a option \<Rightarrow> bool"
   1.113 +  "op = :: 'a list \<Rightarrow> 'a list \<Rightarrow> bool"
   1.114 +  "op = :: mut1 \<Rightarrow> mut1 \<Rightarrow> bool"
   1.115 +  "op = :: mut2 \<Rightarrow> mut2 \<Rightarrow> bool"
   1.116 +
   1.117 +subsection {* heavy use of names *}
   1.118 +
   1.119 +definition
   1.120 +  f :: nat
   1.121 +  "f = 2"
   1.122 +  g :: nat
   1.123 +  "g = f"
   1.124 +  h :: nat
   1.125 +  "h = g"
   1.126 +
   1.127 +code_alias
   1.128 +  "Codegenerator.f" "Mymod.f"
   1.129 +  "Codegenerator.g" "Mymod.A.f"
   1.130 +  "Codegenerator.h" "Mymod.A.B.f"
   1.131 +
   1.132 +code_generate f g h
   1.133 +
   1.134 +code_serialize ml (-)
   1.135 +
   1.136 +end
   1.137 \ No newline at end of file