author | haftmann |
Fri, 03 Nov 2006 14:22:41 +0100 | |
changeset 21155 | 95142d816793 |
parent 21125 | 9b7d35ca1eef |
child 21191 | c00161fbf990 |
permissions | -rw-r--r-- |
19281
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
1 |
(* ID: $Id$ |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
2 |
Author: Florian Haftmann, TU Muenchen |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
3 |
*) |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
4 |
|
20187 | 5 |
header {* Test and Examples for code generator *} |
19281
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
6 |
|
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
7 |
theory Codegenerator |
21155
95142d816793
added particular test for partially applied case constants
haftmann
parents:
21125
diff
changeset
|
8 |
imports Main Records |
19281
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
9 |
begin |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
10 |
|
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
11 |
subsection {* booleans *} |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
12 |
|
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
13 |
definition |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
14 |
xor :: "bool \<Rightarrow> bool \<Rightarrow> bool" |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
15 |
"xor p q = ((p | q) & \<not> (p & q))" |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
16 |
|
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
17 |
subsection {* natural numbers *} |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
18 |
|
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
19 |
definition |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
20 |
n :: nat |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
21 |
"n = 42" |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
22 |
|
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
23 |
subsection {* pairs *} |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
24 |
|
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
25 |
definition |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
26 |
swap :: "'a * 'b \<Rightarrow> 'b * 'a" |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
27 |
"swap p = (let (x, y) = p in (y, x))" |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
28 |
appl :: "('a \<Rightarrow> 'b) * 'a \<Rightarrow> 'b" |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
29 |
"appl p = (let (f, x) = p in f x)" |
21092 | 30 |
snd_three :: "'a * 'b * 'c => 'b" |
31 |
"snd_three a = id (\<lambda>(a, b, c). b) a" |
|
19281
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
32 |
|
20936 | 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 |
||
20187 | 41 |
subsection {* integers *} |
42 |
||
19281
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
43 |
definition |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
44 |
k :: "int" |
20351 | 45 |
"k = -42" |
19281
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
46 |
|
20968 | 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") |
|
19281
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
52 |
|
20968 | 53 |
declare fac.simps [code] |
19281
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
54 |
|
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
55 |
subsection {* sums *} |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
56 |
|
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
57 |
subsection {* options *} |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
58 |
|
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
59 |
subsection {* lists *} |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
60 |
|
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
61 |
definition |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
62 |
ps :: "nat list" |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
63 |
"ps = [2, 3, 5, 7, 11]" |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
64 |
qs :: "nat list" |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
65 |
"qs == rev ps" |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
66 |
|
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
67 |
subsection {* mutual datatypes *} |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
68 |
|
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
69 |
datatype mut1 = Tip | Top mut2 |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
70 |
and mut2 = Tip | Top mut1 |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
71 |
|
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
72 |
consts |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
73 |
mut1 :: "mut1 \<Rightarrow> mut1" |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
74 |
mut2 :: "mut2 \<Rightarrow> mut2" |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
75 |
|
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
76 |
primrec |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
77 |
"mut1 mut1.Tip = mut1.Tip" |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
78 |
"mut1 (mut1.Top x) = mut1.Top (mut2 x)" |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
79 |
"mut2 mut2.Tip = mut2.Tip" |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
80 |
"mut2 (mut2.Top x) = mut2.Top (mut1 x)" |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
81 |
|
20351 | 82 |
subsection {* records *} |
19281
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
83 |
|
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
84 |
subsection {* equalities *} |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
85 |
|
20702 | 86 |
subsection {* strings *} |
87 |
||
88 |
definition |
|
89 |
"mystring = ''my home is my castle''" |
|
90 |
||
20968 | 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 |
||
21155
95142d816793
added particular test for partially applied case constants
haftmann
parents:
21125
diff
changeset
|
102 |
definition |
95142d816793
added particular test for partially applied case constants
haftmann
parents:
21125
diff
changeset
|
103 |
"base_case f = f list_case" |
95142d816793
added particular test for partially applied case constants
haftmann
parents:
21125
diff
changeset
|
104 |
|
19789 | 105 |
subsection {* heavy usage of names *} |
19281
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
106 |
|
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
107 |
definition |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
108 |
f :: nat |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
109 |
"f = 2" |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
110 |
g :: nat |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
111 |
"g = f" |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
112 |
h :: nat |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
113 |
"h = g" |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
114 |
|
20383 | 115 |
code_constname |
20936 | 116 |
f "MymodA.f" |
117 |
g "MymodB.f" |
|
118 |
h "MymodC.f" |
|
19281
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
119 |
|
20702 | 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 |
||
20713
823967ef47f1
renamed 0 and 1 to HOL.zero and HOL.one respectivly; introduced corresponding syntactic classes
haftmann
parents:
20702
diff
changeset
|
132 |
code_gen |
823967ef47f1
renamed 0 and 1 to HOL.zero and HOL.one respectivly; introduced corresponding syntactic classes
haftmann
parents:
20702
diff
changeset
|
133 |
xor |
823967ef47f1
renamed 0 and 1 to HOL.zero and HOL.one respectivly; introduced corresponding syntactic classes
haftmann
parents:
20702
diff
changeset
|
134 |
code_gen |
823967ef47f1
renamed 0 and 1 to HOL.zero and HOL.one respectivly; introduced corresponding syntactic classes
haftmann
parents:
20702
diff
changeset
|
135 |
"0::nat" "1::nat" |
20702 | 136 |
code_gen |
21092 | 137 |
Pair fst snd Let split swap snd_three |
20453
855f07fabd76
final syntax for some Isar code generator keywords
haftmann
parents:
20383
diff
changeset
|
138 |
code_gen |
20351 | 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" |
|
20453
855f07fabd76
final syntax for some Isar code generator keywords
haftmann
parents:
20383
diff
changeset
|
144 |
code_gen |
20597 | 145 |
appl |
20453
855f07fabd76
final syntax for some Isar code generator keywords
haftmann
parents:
20383
diff
changeset
|
146 |
code_gen |
20351 | 147 |
Inl Inr |
20453
855f07fabd76
final syntax for some Isar code generator keywords
haftmann
parents:
20383
diff
changeset
|
148 |
code_gen |
20351 | 149 |
None Some |
20453
855f07fabd76
final syntax for some Isar code generator keywords
haftmann
parents:
20383
diff
changeset
|
150 |
code_gen |
20351 | 151 |
hd tl "op @" ps qs |
20453
855f07fabd76
final syntax for some Isar code generator keywords
haftmann
parents:
20383
diff
changeset
|
152 |
code_gen |
20351 | 153 |
mut1 mut2 |
20453
855f07fabd76
final syntax for some Isar code generator keywords
haftmann
parents:
20383
diff
changeset
|
154 |
code_gen |
20351 | 155 |
remove1 |
156 |
null |
|
157 |
replicate |
|
158 |
rotate1 |
|
159 |
rotate |
|
160 |
splice |
|
20597 | 161 |
code_gen |
162 |
remdups |
|
163 |
"distinct" |
|
21155
95142d816793
added particular test for partially applied case constants
haftmann
parents:
21125
diff
changeset
|
164 |
filter |
20453
855f07fabd76
final syntax for some Isar code generator keywords
haftmann
parents:
20383
diff
changeset
|
165 |
code_gen |
20351 | 166 |
foo1 foo3 |
20453
855f07fabd76
final syntax for some Isar code generator keywords
haftmann
parents:
20383
diff
changeset
|
167 |
code_gen |
20936 | 168 |
mystring |
169 |
code_gen |
|
170 |
f g h |
|
171 |
code_gen |
|
21155
95142d816793
added particular test for partially applied case constants
haftmann
parents:
21125
diff
changeset
|
172 |
apply_tower Codegenerator.keywords shadow base_case |
20968 | 173 |
code_gen |
174 |
abs_let nested_let case_let |
|
20936 | 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 |
|
21046
fe1db2f991a7
moved HOL code generator setup to Code_Generator
haftmann
parents:
20968
diff
changeset
|
193 |
"Code_Generator.eq :: bool \<Rightarrow> bool \<Rightarrow> bool" |
fe1db2f991a7
moved HOL code generator setup to Code_Generator
haftmann
parents:
20968
diff
changeset
|
194 |
"Code_Generator.eq :: nat \<Rightarrow> nat \<Rightarrow> bool" |
fe1db2f991a7
moved HOL code generator setup to Code_Generator
haftmann
parents:
20968
diff
changeset
|
195 |
"Code_Generator.eq :: int \<Rightarrow> int \<Rightarrow> bool" |
fe1db2f991a7
moved HOL code generator setup to Code_Generator
haftmann
parents:
20968
diff
changeset
|
196 |
"Code_Generator.eq :: ('a\<Colon>eq) * ('b\<Colon>eq) \<Rightarrow> 'a * 'b \<Rightarrow> bool" |
fe1db2f991a7
moved HOL code generator setup to Code_Generator
haftmann
parents:
20968
diff
changeset
|
197 |
"Code_Generator.eq :: ('a\<Colon>eq) + ('b\<Colon>eq) \<Rightarrow> 'a + 'b \<Rightarrow> bool" |
fe1db2f991a7
moved HOL code generator setup to Code_Generator
haftmann
parents:
20968
diff
changeset
|
198 |
"Code_Generator.eq :: ('a\<Colon>eq) option \<Rightarrow> 'a option \<Rightarrow> bool" |
fe1db2f991a7
moved HOL code generator setup to Code_Generator
haftmann
parents:
20968
diff
changeset
|
199 |
"Code_Generator.eq :: ('a\<Colon>eq) list \<Rightarrow> 'a list \<Rightarrow> bool" |
fe1db2f991a7
moved HOL code generator setup to Code_Generator
haftmann
parents:
20968
diff
changeset
|
200 |
"Code_Generator.eq :: mut1 \<Rightarrow> mut1 \<Rightarrow> bool" |
fe1db2f991a7
moved HOL code generator setup to Code_Generator
haftmann
parents:
20968
diff
changeset
|
201 |
"Code_Generator.eq :: mut2 \<Rightarrow> mut2 \<Rightarrow> bool" |
fe1db2f991a7
moved HOL code generator setup to Code_Generator
haftmann
parents:
20968
diff
changeset
|
202 |
"Code_Generator.eq :: ('a\<Colon>eq) point_scheme \<Rightarrow> 'a point_scheme \<Rightarrow> bool" |
19281
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
203 |
|
21125 | 204 |
code_gen (SML *) |
21080 | 205 |
code_gen (Haskell -) |
19281
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
206 |
|
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
207 |
end |