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