author  haftmann 
Mon, 14 Aug 2006 13:46:17 +0200  
changeset 20383  58f65fc90cf4 
parent 20351  c7658e811ffb 
child 20453  855f07fabd76 
permissions  rwrr 
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 
20351  8 
imports Main "~~/src/HOL/ex/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 
one :: nat 
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset

21 
"one = 1" 
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset

22 
n :: nat 
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset

23 
"n = 42" 
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 
subsection {* pairs *} 
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 
definition 
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset

28 
swap :: "'a * 'b \<Rightarrow> 'b * 'a" 
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset

29 
"swap p = (let (x, y) = p in (y, x))" 
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset

30 
swapp :: "'a * 'b \<Rightarrow> 'c * 'd \<Rightarrow> ('a * 'c) * ('b * 'd)" 
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset

31 
"swapp = (\<lambda>(x, y) (z, w). ((x, z), (y, w)))" 
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset

32 
appl :: "('a \<Rightarrow> 'b) * 'a \<Rightarrow> 'b" 
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset

33 
"appl p = (let (f, x) = p in f x)" 
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset

34 

20187  35 
subsection {* integers *} 
36 

19281
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 
k :: "int" 
20351  39 
"k = 42" 
19281
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset

40 

b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset

41 
consts 
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset

42 
fac :: "int => int" 
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset

43 

b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset

44 
recdef fac "measure nat" 
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset

45 
"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

46 

b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset

47 
subsection {* sums *} 
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset

48 

b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset

49 
subsection {* options *} 
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 
subsection {* lists *} 
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset

52 

b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset

53 
definition 
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset

54 
ps :: "nat list" 
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset

55 
"ps = [2, 3, 5, 7, 11]" 
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset

56 
qs :: "nat list" 
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset

57 
"qs == rev ps" 
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 {* mutual datatypes *} 
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 
datatype mut1 = Tip  Top mut2 
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset

62 
and mut2 = Tip  Top mut1 
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset

63 

b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset

64 
consts 
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset

65 
mut1 :: "mut1 \<Rightarrow> mut1" 
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset

66 
mut2 :: "mut2 \<Rightarrow> mut2" 
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 
primrec 
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset

69 
"mut1 mut1.Tip = mut1.Tip" 
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset

70 
"mut1 (mut1.Top x) = mut1.Top (mut2 x)" 
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset

71 
"mut2 mut2.Tip = mut2.Tip" 
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset

72 
"mut2 (mut2.Top x) = mut2.Top (mut1 x)" 
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset

73 

20351  74 
subsection {* records *} 
19281
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 
subsection {* equalities *} 
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset

77 

19789  78 
subsection {* heavy usage of names *} 
19281
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset

79 

b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset

80 
definition 
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset

81 
f :: nat 
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset

82 
"f = 2" 
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset

83 
g :: nat 
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset

84 
"g = f" 
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset

85 
h :: nat 
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset

86 
"h = g" 
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset

87 

20383  88 
code_constname 
89 
f "Mymod.f" 

90 
g "Mymod.A.f" 

91 
h "Mymod.A.B.f" 

19281
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset

92 

20351  93 
code_generate (ml, haskell) 
94 
n one "0::int" "0::nat" "1::int" "1::nat" 

95 
code_generate (ml, haskell) 

96 
fac 

20383  97 
code_generate 
20351  98 
xor 
20383  99 
code_generate 
20351  100 
"op + :: nat \<Rightarrow> nat \<Rightarrow> nat" 
101 
"op  :: nat \<Rightarrow> nat \<Rightarrow> nat" 

102 
"op * :: nat \<Rightarrow> nat \<Rightarrow> nat" 

103 
"op < :: nat \<Rightarrow> nat \<Rightarrow> bool" 

104 
"op <= :: nat \<Rightarrow> nat \<Rightarrow> bool" 

20383  105 
code_generate 
20351  106 
Pair fst snd Let split swap swapp appl 
107 
code_generate (ml, haskell) 

108 
k 

109 
"op + :: int \<Rightarrow> int \<Rightarrow> int" 

110 
"op  :: int \<Rightarrow> int \<Rightarrow> int" 

111 
"op * :: int \<Rightarrow> int \<Rightarrow> int" 

112 
"op < :: int \<Rightarrow> int \<Rightarrow> bool" 

113 
"op <= :: int \<Rightarrow> int \<Rightarrow> bool" 

114 
fac 

115 
"op div :: int \<Rightarrow> int \<Rightarrow> int" 

116 
"op mod :: int \<Rightarrow> int \<Rightarrow> int" 

20383  117 
code_generate 
20351  118 
Inl Inr 
20383  119 
code_generate 
20351  120 
None Some 
20383  121 
code_generate 
20351  122 
hd tl "op @" ps qs 
20383  123 
code_generate 
20351  124 
mut1 mut2 
125 
code_generate (ml, haskell) 

126 
"op @" filter concat foldl foldr hd tl 

127 
last butlast list_all2 

128 
map 

129 
nth 

130 
list_update 

131 
take 

132 
drop 

133 
takeWhile 

134 
dropWhile 

135 
rev 

136 
zip 

137 
upt 

138 
remdups 

139 
remove1 

140 
null 

141 
"distinct" 

142 
replicate 

143 
rotate1 

144 
rotate 

145 
splice 

20383  146 
code_generate 
20351  147 
foo1 foo3 
148 
code_generate (ml, haskell) 

149 
"op = :: bool \<Rightarrow> bool \<Rightarrow> bool" 

150 
"op = :: nat \<Rightarrow> nat \<Rightarrow> bool" 

151 
"op = :: int \<Rightarrow> int \<Rightarrow> bool" 

152 
"op = :: 'a * 'b \<Rightarrow> 'a * 'b \<Rightarrow> bool" 

153 
"op = :: 'a + 'b \<Rightarrow> 'a + 'b \<Rightarrow> bool" 

154 
"op = :: 'a option \<Rightarrow> 'a option \<Rightarrow> bool" 

155 
"op = :: 'a list \<Rightarrow> 'a list \<Rightarrow> bool" 

20383  156 
"op = :: point \<Rightarrow> point \<Rightarrow> bool" 
20351  157 
"op = :: mut1 \<Rightarrow> mut1 \<Rightarrow> bool" 
158 
"op = :: mut2 \<Rightarrow> mut2 \<Rightarrow> bool" 

20383  159 
code_generate 
20351  160 
f g h 
19281
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset

161 

b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset

162 
code_serialize ml () 
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset

163 

b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset

164 
end 