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