src/HOL/ex/Codegenerator.thy
author haftmann
Fri Sep 01 08:36:51 2006 +0200 (2006-09-01)
changeset 20453 855f07fabd76
parent 20383 58f65fc90cf4
child 20597 65fe827aa595
permissions -rw-r--r--
final syntax for some Isar code generator keywords
     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 "~~/src/HOL/ex/Records"
     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 subsection {* natural numbers *}
    18 
    19 definition
    20   one :: nat
    21   "one = 1"
    22   n :: nat
    23   "n = 42"
    24 
    25 subsection {* pairs *}
    26 
    27 definition
    28   swap :: "'a * 'b \<Rightarrow> 'b * 'a"
    29   "swap p = (let (x, y) = p in (y, x))"
    30   swapp :: "'a * 'b \<Rightarrow> 'c * 'd \<Rightarrow> ('a * 'c) * ('b * 'd)"
    31   "swapp = (\<lambda>(x, y) (z, w). ((x, z), (y, w)))"
    32   appl :: "('a \<Rightarrow> 'b) * 'a \<Rightarrow> 'b"
    33   "appl p = (let (f, x) = p in f x)"
    34 
    35 subsection {* integers *}
    36 
    37 definition
    38   k :: "int"
    39   "k = -42"
    40 
    41 consts
    42   fac :: "int => int"
    43 
    44 recdef fac "measure nat"
    45   "fac j = (if j <= 0 then 1 else j * (fac (j - 1)))"
    46 
    47 subsection {* sums *}
    48 
    49 subsection {* options *}
    50 
    51 subsection {* lists *}
    52 
    53 definition
    54   ps :: "nat list"
    55   "ps = [2, 3, 5, 7, 11]"
    56   qs :: "nat list"
    57   "qs == rev ps"
    58 
    59 subsection {* mutual datatypes *}
    60 
    61 datatype mut1 = Tip | Top mut2
    62   and mut2 = Tip | Top mut1
    63 
    64 consts
    65   mut1 :: "mut1 \<Rightarrow> mut1"
    66   mut2 :: "mut2 \<Rightarrow> mut2"
    67 
    68 primrec
    69   "mut1 mut1.Tip = mut1.Tip"
    70   "mut1 (mut1.Top x) = mut1.Top (mut2 x)"
    71   "mut2 mut2.Tip = mut2.Tip"
    72   "mut2 (mut2.Top x) = mut2.Top (mut1 x)"
    73 
    74 subsection {* records *}
    75 
    76 subsection {* equalities *}
    77 
    78 subsection {* heavy usage of names *}
    79 
    80 definition
    81   f :: nat
    82   "f = 2"
    83   g :: nat
    84   "g = f"
    85   h :: nat
    86   "h = g"
    87 
    88 code_constname
    89   f "Mymod.f"
    90   g "Mymod.A.f"
    91   h "Mymod.A.B.f"
    92 
    93 code_gen xor
    94 code_gen one "0::nat" "1::nat"
    95 code_gen "0::int" "1::int" n fac
    96   (SML) (Haskell)
    97 code_gen
    98   "op + :: nat \<Rightarrow> nat \<Rightarrow> nat"
    99   "op - :: nat \<Rightarrow> nat \<Rightarrow> nat"
   100   "op * :: nat \<Rightarrow> nat \<Rightarrow> nat"
   101   "op < :: nat \<Rightarrow> nat \<Rightarrow> bool"
   102   "op <= :: nat \<Rightarrow> nat \<Rightarrow> bool"
   103 code_gen
   104   Pair fst snd Let split swap swapp appl
   105 code_gen
   106   k
   107   "op + :: int \<Rightarrow> int \<Rightarrow> int"
   108   "op - :: int \<Rightarrow> int \<Rightarrow> int"
   109   "op * :: int \<Rightarrow> int \<Rightarrow> int"
   110   "op < :: int \<Rightarrow> int \<Rightarrow> bool"
   111   "op <= :: int \<Rightarrow> int \<Rightarrow> bool"
   112   fac
   113   "op div :: int \<Rightarrow> int \<Rightarrow> int"
   114   "op mod :: int \<Rightarrow> int \<Rightarrow> int"  
   115   (SML) (Haskell)
   116 code_gen
   117   Inl Inr
   118 code_gen
   119   None Some
   120 code_gen
   121   hd tl "op @" ps qs
   122 code_gen
   123   mut1 mut2
   124 code_gen
   125   "op @" filter concat foldl foldr hd tl
   126   last butlast list_all2
   127   map 
   128   nth 
   129   list_update
   130   take
   131   drop
   132   takeWhile
   133   dropWhile
   134   rev
   135   zip
   136   upt
   137   remdups
   138   remove1
   139   null
   140   "distinct"
   141   replicate
   142   rotate1
   143   rotate
   144   splice
   145   (SML) (Haskell)
   146 code_gen
   147   foo1 foo3
   148 code_gen
   149   "op = :: bool \<Rightarrow> bool \<Rightarrow> bool"
   150   "op = :: nat \<Rightarrow> nat \<Rightarrow> bool"
   151   "op = :: int \<Rightarrow> int \<Rightarrow> bool"
   152   "op = :: 'a * 'b \<Rightarrow> 'a * 'b \<Rightarrow> bool"
   153   "op = :: 'a + 'b \<Rightarrow> 'a + 'b \<Rightarrow> bool"
   154   "op = :: 'a option \<Rightarrow> 'a option \<Rightarrow> bool"
   155   "op = :: 'a list \<Rightarrow> 'a list \<Rightarrow> bool"
   156   "op = :: point \<Rightarrow> point \<Rightarrow> bool"
   157   "op = :: mut1 \<Rightarrow> mut1 \<Rightarrow> bool"
   158   "op = :: mut2 \<Rightarrow> mut2 \<Rightarrow> bool"
   159 code_gen
   160   f g h
   161 
   162 code_gen (SML -)
   163 
   164 end