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