author | haftmann |
Tue, 06 Jun 2006 15:01:09 +0200 | |
changeset 19789 | c08c9f9ea9a5 |
parent 19604 | 02f5fbdd5c54 |
child 19817 | bb16bf9ae3fd |
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 |
|
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
5 |
header {* Test and Examples for Code Generator *} |
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 |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
8 |
imports Main |
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 |
code_generate xor |
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 |
subsection {* natural numbers *} |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
20 |
|
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
21 |
definition |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
22 |
one :: nat |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
23 |
"one = 1" |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
24 |
n :: nat |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
25 |
"n = 42" |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
26 |
|
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
27 |
code_generate |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
28 |
"0::nat" "one" n |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
29 |
"op + :: nat \<Rightarrow> nat \<Rightarrow> nat" |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
30 |
"op - :: nat \<Rightarrow> nat \<Rightarrow> nat" |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
31 |
"op * :: nat \<Rightarrow> nat \<Rightarrow> nat" |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
32 |
"op < :: nat \<Rightarrow> nat \<Rightarrow> bool" |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
33 |
"op <= :: nat \<Rightarrow> nat \<Rightarrow> bool" |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
34 |
|
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
35 |
subsection {* pairs *} |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
36 |
|
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
37 |
definition |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
38 |
swap :: "'a * 'b \<Rightarrow> 'b * 'a" |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
39 |
"swap p = (let (x, y) = p in (y, x))" |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
40 |
swapp :: "'a * 'b \<Rightarrow> 'c * 'd \<Rightarrow> ('a * 'c) * ('b * 'd)" |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
41 |
"swapp = (\<lambda>(x, y) (z, w). ((x, z), (y, w)))" |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
42 |
appl :: "('a \<Rightarrow> 'b) * 'a \<Rightarrow> 'b" |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
43 |
"appl p = (let (f, x) = p in f x)" |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
44 |
|
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
45 |
code_generate Pair fst snd Let split swap swapp appl |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
46 |
|
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
47 |
definition |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
48 |
k :: "int" |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
49 |
"k = 42" |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
50 |
|
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
51 |
consts |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
52 |
fac :: "int => int" |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
53 |
|
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
54 |
recdef fac "measure nat" |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
55 |
"fac j = (if j <= 0 then 1 else j * (fac (j - 1)))" |
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 |
code_generate |
19604 | 58 |
"0::int" k |
19281
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
59 |
"op + :: int \<Rightarrow> int \<Rightarrow> int" |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
60 |
"op - :: int \<Rightarrow> int \<Rightarrow> int" |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
61 |
"op * :: int \<Rightarrow> int \<Rightarrow> int" |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
62 |
"op < :: int \<Rightarrow> int \<Rightarrow> bool" |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
63 |
"op <= :: int \<Rightarrow> int \<Rightarrow> bool" |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
64 |
fac |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
65 |
|
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
66 |
subsection {* sums *} |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
67 |
|
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
68 |
code_generate Inl Inr |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
69 |
|
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
70 |
subsection {* options *} |
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 |
code_generate None Some |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
73 |
|
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
74 |
subsection {* lists *} |
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 |
definition |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
77 |
ps :: "nat list" |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
78 |
"ps = [2, 3, 5, 7, 11]" |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
79 |
qs :: "nat list" |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
80 |
"qs == rev ps" |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
81 |
|
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
82 |
code_generate hd tl "op @" ps qs |
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 {* mutual datatypes *} |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
85 |
|
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
86 |
datatype mut1 = Tip | Top mut2 |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
87 |
and mut2 = Tip | Top mut1 |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
88 |
|
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
89 |
consts |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
90 |
mut1 :: "mut1 \<Rightarrow> mut1" |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
91 |
mut2 :: "mut2 \<Rightarrow> mut2" |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
92 |
|
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
93 |
primrec |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
94 |
"mut1 mut1.Tip = mut1.Tip" |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
95 |
"mut1 (mut1.Top x) = mut1.Top (mut2 x)" |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
96 |
"mut2 mut2.Tip = mut2.Tip" |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
97 |
"mut2 (mut2.Top x) = mut2.Top (mut1 x)" |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
98 |
|
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
99 |
code_generate mut1 mut2 |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
100 |
|
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
101 |
subsection {* equalities *} |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
102 |
|
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
103 |
code_generate |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
104 |
"op = :: bool \<Rightarrow> bool \<Rightarrow> bool" |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
105 |
"op = :: nat \<Rightarrow> nat \<Rightarrow> bool" |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
106 |
"op = :: int \<Rightarrow> int \<Rightarrow> bool" |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
107 |
"op = :: 'a * 'b \<Rightarrow> 'a * 'b \<Rightarrow> bool" |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
108 |
"op = :: 'a + 'b \<Rightarrow> 'a + 'b \<Rightarrow> bool" |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
109 |
"op = :: 'a option \<Rightarrow> 'a option \<Rightarrow> bool" |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
110 |
"op = :: 'a list \<Rightarrow> 'a list \<Rightarrow> bool" |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
111 |
"op = :: mut1 \<Rightarrow> mut1 \<Rightarrow> bool" |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
112 |
"op = :: mut2 \<Rightarrow> mut2 \<Rightarrow> bool" |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
113 |
|
19789 | 114 |
subsection {* heavy usage of names *} |
19281
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
115 |
|
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
116 |
definition |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
117 |
f :: nat |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
118 |
"f = 2" |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
119 |
g :: nat |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
120 |
"g = f" |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
121 |
h :: nat |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
122 |
"h = g" |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
123 |
|
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
124 |
code_alias |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
125 |
"Codegenerator.f" "Mymod.f" |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
126 |
"Codegenerator.g" "Mymod.A.f" |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
127 |
"Codegenerator.h" "Mymod.A.B.f" |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
128 |
|
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
129 |
code_generate f g h |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
130 |
|
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
131 |
code_serialize ml (-) |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
132 |
|
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
133 |
end |