src/HOL/ex/Codegenerator.thy
author wenzelm
Fri Nov 17 02:20:03 2006 +0100 (2006-11-17)
changeset 21404 eb85850d3eb7
parent 21319 cf814e36f788
child 21420 8b15e5e66813
permissions -rw-r--r--
more robust syntax for definition/abbreviation/notation;
     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 Records
     9 begin
    10 
    11 subsection {* booleans *}
    12 
    13 definition
    14   xor :: "bool \<Rightarrow> bool \<Rightarrow> bool" where
    15   "xor p q = ((p | q) & \<not> (p & q))"
    16 
    17 subsection {* natural numbers *}
    18 
    19 definition
    20   n :: nat where
    21   "n = 42"
    22 
    23 subsection {* pairs *}
    24 
    25 definition
    26   swap :: "'a * 'b \<Rightarrow> 'b * 'a" where
    27   "swap p = (let (x, y) = p in (y, x))"
    28 
    29 definition
    30   appl :: "('a \<Rightarrow> 'b) * 'a \<Rightarrow> 'b" where
    31   "appl p = (let (f, x) = p in f x)"
    32 
    33 definition
    34   snd_three :: "'a * 'b * 'c => 'b" where
    35   "snd_three a = id (\<lambda>(a, b, c). b) a"
    36 
    37 lemma [code]:
    38   "swap (x, y) = (y, x)"
    39   unfolding swap_def Let_def by auto
    40 
    41 lemma [code]:
    42   "appl (f, x) = f x"
    43   unfolding appl_def Let_def by auto
    44 
    45 subsection {* integers *}
    46 
    47 definition
    48   k :: "int" where
    49   "k = -42"
    50 
    51 function
    52   fac :: "int => int" where
    53   "fac j = (if j <= 0 then 1 else j * (fac (j - 1)))"
    54   by pat_completeness auto
    55 termination by (relation "measure nat") auto
    56 
    57 declare fac.simps [code]
    58 
    59 subsection {* sums *}
    60 
    61 subsection {* options *}
    62 
    63 subsection {* lists *}
    64 
    65 definition
    66   ps :: "nat list" where
    67   "ps = [2, 3, 5, 7, 11]"
    68 
    69 definition
    70   qs :: "nat list" where
    71   "qs == rev ps"
    72 
    73 subsection {* mutual datatypes *}
    74 
    75 datatype mut1 = Tip | Top mut2
    76   and mut2 = Tip | Top mut1
    77 
    78 consts
    79   mut1 :: "mut1 \<Rightarrow> mut1"
    80   mut2 :: "mut2 \<Rightarrow> mut2"
    81 
    82 primrec
    83   "mut1 mut1.Tip = mut1.Tip"
    84   "mut1 (mut1.Top x) = mut1.Top (mut2 x)"
    85   "mut2 mut2.Tip = mut2.Tip"
    86   "mut2 (mut2.Top x) = mut2.Top (mut1 x)"
    87 
    88 subsection {* records *}
    89 
    90 subsection {* equalities *}
    91 
    92 subsection {* strings *}
    93 
    94 definition
    95   "mystring = ''my home is my castle''"
    96 
    97 subsection {* nested lets and such *}
    98 
    99 definition
   100   "abs_let x = (let (y, z) = x in (\<lambda>u. case u of () \<Rightarrow> (y + y)))"
   101 
   102 definition
   103   "nested_let x = (let (y, z) = x in let w = y z in w * w)"
   104 
   105 definition
   106   "case_let x = (let (y, z) = x in case y of () => z)"
   107 
   108 definition
   109   "base_case f = f list_case"
   110 
   111 definition
   112   "apply_tower = (\<lambda>x. x (\<lambda>x. x (\<lambda>x. x)))"
   113 
   114 definition
   115   "keywords fun datatype class instance funa classa =
   116     Suc fun + datatype * class mod instance - funa - classa"
   117 
   118 hide (open) const keywords
   119 
   120 definition
   121   "shadow keywords = keywords @ [Codegenerator.keywords 0 0 0 0 0 0]"
   122 
   123 code_gen
   124   xor
   125 code_gen
   126   "0::nat" "1::nat"
   127 code_gen
   128   Pair fst snd Let split swap snd_three
   129 code_gen
   130   "op + :: nat \<Rightarrow> nat \<Rightarrow> nat"
   131   "op - :: nat \<Rightarrow> nat \<Rightarrow> nat"
   132   "op * :: nat \<Rightarrow> nat \<Rightarrow> nat"
   133   "op < :: nat \<Rightarrow> nat \<Rightarrow> bool"
   134   "op <= :: nat \<Rightarrow> nat \<Rightarrow> bool"
   135 code_gen
   136   appl
   137 code_gen
   138   Inl Inr
   139 code_gen
   140   None Some
   141 code_gen
   142   hd tl "op @" ps qs
   143 code_gen
   144   mut1 mut2
   145 code_gen
   146   remove1
   147   null
   148   replicate
   149   rotate1
   150   rotate
   151   splice
   152 code_gen
   153   remdups
   154   "distinct"
   155   filter
   156 code_gen
   157   foo1 foo3
   158 code_gen
   159   mystring
   160 code_gen
   161   apply_tower Codegenerator.keywords shadow base_case
   162 code_gen
   163   abs_let nested_let case_let
   164 code_gen "0::int" "1::int"
   165   (SML) (Haskell)
   166 code_gen n
   167   (SML) (Haskell)
   168 code_gen fac
   169   (SML) (Haskell)
   170 code_gen
   171   k
   172   "op + :: int \<Rightarrow> int \<Rightarrow> int"
   173   "op - :: int \<Rightarrow> int \<Rightarrow> int"
   174   "op * :: int \<Rightarrow> int \<Rightarrow> int"
   175   "op < :: int \<Rightarrow> int \<Rightarrow> bool"
   176   "op <= :: int \<Rightarrow> int \<Rightarrow> bool"
   177   fac
   178   "op div :: int \<Rightarrow> int \<Rightarrow> int"
   179   "op mod :: int \<Rightarrow> int \<Rightarrow> int"  
   180   (SML) (Haskell)
   181 code_gen
   182   "Code_Generator.eq :: bool \<Rightarrow> bool \<Rightarrow> bool"
   183   "Code_Generator.eq :: nat \<Rightarrow> nat \<Rightarrow> bool"
   184   "Code_Generator.eq :: int \<Rightarrow> int \<Rightarrow> bool"
   185   "Code_Generator.eq :: ('a\<Colon>eq) * ('b\<Colon>eq) \<Rightarrow> 'a * 'b \<Rightarrow> bool"
   186   "Code_Generator.eq :: ('a\<Colon>eq) + ('b\<Colon>eq) \<Rightarrow> 'a + 'b \<Rightarrow> bool"
   187   "Code_Generator.eq :: ('a\<Colon>eq) option \<Rightarrow> 'a option \<Rightarrow> bool"
   188   "Code_Generator.eq :: ('a\<Colon>eq) list \<Rightarrow> 'a list \<Rightarrow> bool"
   189   "Code_Generator.eq :: mut1 \<Rightarrow> mut1 \<Rightarrow> bool"
   190   "Code_Generator.eq :: mut2 \<Rightarrow> mut2 \<Rightarrow> bool"
   191   "Code_Generator.eq :: ('a\<Colon>eq) point_scheme \<Rightarrow> 'a point_scheme \<Rightarrow> bool"
   192 
   193 code_gen (SML *)
   194 code_gen (Haskell -)
   195 
   196 end