-
Notifications
You must be signed in to change notification settings - Fork 0
/
Copy pathaccount.verona
179 lines (151 loc) · 4.66 KB
/
account.verona
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
/* Example accessing two accounts and transfering money.
* Demonstrates safe exclusive mutable access, without locking, transaction or two-phase commit
*/
use "common/bool.verona"
use "common/callbacks.verona"
class Account {
_balance: U64 & imm;
_frozen: Bool & imm;
create(opening: U64 & imm): Account & iso {
var result = new Account;
result._balance = opening;
result._frozen = Bool.false();
result
}
balance(self: mut): U64 & imm {
self._balance
}
withdraw(self: mut, amount: U64 & imm) {
self._balance = self._balance - amount;
}
deposit(self: mut, amount: U64 & imm) {
self._balance = self._balance + amount;
}
freeze(self: mut) {
self._frozen = Bool.true();
}
unfreeze(self: mut) {
self._frozen = Bool.false();
}
frozen(self: mut): Bool & imm {
self._frozen
}
}
class FreezeTask {
_account: cown[Account] & imm;
create(account: cown[Account] & imm): FreezeTask & iso {
var result = new FreezeTask;
result._account = account;
result
}
apply(self: mut) {
when(var account = self._account) {
Builtin.print("Freezing dst\n");
account.freeze()
}
}
}
class Main {
main_with_transfer() {
var src = cown.create(Account.create(0));
var dst = cown.create(Account.create(0));
when(src) {
Builtin.print("Depositing 200 into src\n\n");
src.deposit(200)
};
when(src, dst) {
var amount = 50;
if (((src.frozen()).or(dst.frozen())).apply()) {
Builtin.print1("tansferring from src to dst failed\n\n", amount);
} else {
Builtin.print1("tansferring {:#} from src to dst\n\n", amount);
src.withdraw(amount);
dst.deposit(amount);
}
};
}
main_with_ordering_problem() {
var src = cown.create(Account.create(0));
var dst = cown.create(Account.create(0));
when(src) {
Builtin.print("Depositing 200 into src\n\n");
src.deposit(200)
};
when(src, dst) {
var amount = 50;
if (((src.frozen()).or(dst.frozen())).apply()) {
Builtin.print1("tansferring from src to dst failed\n\n", amount);
} else {
Builtin.print1("tansferring {:#} from src to dst\n\n", amount);
src.withdraw(amount);
dst.deposit(amount);
}
};
// This freeze can happen before the transfer takes place, this can be fixed by
// placing the behaviour creation inside the previous behaviour, but after the transfer
when(dst) {
Builtin.print("Freezing dst\n");
dst.freeze();
}
}
// Hoist the transfer with a callback into a seperate method
// The callback will get called after the transfer has completed
transfer_with_callback(src: cown[Account] & imm, dst: cown[Account] & imm, amount: U64 & imm, callback: Callback & iso) {
when(src, dst) {
if (((src.frozen()).or(dst.frozen())).apply()) {
Builtin.print1("tansferring from src to dst failed\n\n", amount);
} else {
Builtin.print1("tansferring {:#} from src to dst\n\n", amount);
src.withdraw(amount);
dst.deposit(amount);
};
(mut-view callback).apply()
};
}
main_with_transfer_with_callback() {
var src = cown.create(Account.create(0));
var dst = cown.create(Account.create(0));
when(src) {
Builtin.print("Depositing 200 into src\n\n");
src.deposit(200)
};
Main.transfer_with_callback(src, dst, 50, FreezeTask.create(dst));
}
transfer_with_promise(src: cown[Account] & imm, dst: cown[Account] & imm, amount: U64 & imm): cown[None] & imm {
var p = Promise.create();
var f = (mut-view p).wait_handle();
when(src, dst) {
if (((src.frozen()).or(dst.frozen())).apply()) {
Builtin.print1("tansferring from src to dst failed\n\n", amount);
} else {
Builtin.print1("tansferring {:#} from src to dst\n\n", amount);
src.withdraw(amount);
dst.deposit(amount);
};
p.fulfill(new None);
};
f
}
main_with_transfer_with_promise() {
var src = cown.create(Account.create(0));
var dst = cown.create(Account.create(0));
when(src) {
Builtin.print("Depositing 200 into src\n\n");
src.deposit(200)
};
when(var _ = Main.transfer_with_promise(src, dst, 50)) {
// FIXME: We should be able to put dst in the cown request here but it causes a runtime error
when(dst) {
Builtin.print("Freezing dst\n");
dst.freeze()
}
};
}
main() {
// Comment and uncomment diffenr implementations to see how they run
// Main.main_with_transfer();
// Main.main_with_ordering_problem();
// Main.main_with_transfer_with_callback();
Main.main_with_transfer_with_promise();
}
}