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
|
import "../mod/libfwdio.so"
import "../mod/libfwdmem.so"
import "../mod/libfwdutil.so"
vec {
u64 n;
u64 s;
*i64 buf;
}
init_vec(u64 n, (vec) ok)
{
ok([n => n, 0 as u64 => s, * => buf] vec);
}
next_s_vec(u64 s, (u64) ok)
{
if s == 0 as u64 {
ok(1 as u64);
} else {
ok(2 as u64 * s);
}
}
reserve_vec(vec v, u64 c, (vec) ok)
{
v => [n => n, s => s, buf => buf];
n + c => nn;
/* expand if we run out of space */
if nn > s {
next_s_vec(s) => s;
/* note that fwdrealloc creates a new closure, meaning that it
* takes ownership of v.buf, so we can't back out and do a
* single ok(v) at the end of the function */
fwdrealloc(buf, s * sizeof(i64)) => nbuf;
ok([nn => n, s => s, nbuf => buf] vec);
} else {
ok([nn => n, s => s, buf => buf] vec);
}
}
set_vec(vec v, i64 i, i64 e, (vec) ok)
{
v => [n => n, s => s, buf => buf];
/* oh wait, this is dumb, of course nbuf will never be null */
buf + i => nbuf;
nil nbuf {
nil nbuf;
fwdfree(buf);
fwdpanic("set_vec, should never happen\n");
} => dst;
/* perform actual store */
e => dst*;
nil nbuf;
ok([n => n, s => s, buf => buf] vec);
}
n_vec(vec v, (vec, u64) ok)
{
v => [n => n, s => s, buf => buf];
ok([n => n, s => s, buf => buf] vec, n);
}
append_vec(vec v, i64 e, (vec) ok)
{
n_vec(v) => v, n;
reserve_vec(v, n + 1 as u64) => v;
set_vec(v, n as i64, e) => v;
ok(v);
}
at_vec(vec v, u64 i, (vec, &i64) ok)
{
v => [n => n, s => s, buf => buf];
guard(i < n) => {
fwdfree(buf);
fwdpanic("at_vec, bounds error\n");
} => ;
buf + i => *i64 nbuf;
nil nbuf {
nil nbuf;
fwdfree(buf);
fwdpanic("at_vec, should never happen\n");
} => &i64 bufr;
nil nbuf;
ok([n => n, s => s, buf => buf] vec, bufr);
}
destroy_vec(vec v)
{
v => [n => n, s => s, buf => buf];
fwdfree(buf);
nil n;
nil s;
}
populate_vec(i64 i, i64 n, vec v, (vec) ok)
{
if i < n {
append_vec(v, i) => vec v;
populate_vec(i + 1, n, v, ok);
} else {
ok(v);
}
}
guard(bool c, () err | () ok)
{
if c {
ok();
} else {
err();
}
}
check_vec(i64 i, i64 n, vec v, (vec) ok)
{
if i < n {
at_vec(v, i as u64) => v, elem;
/* oh, this doesn't really work with the memory analysis, since
* I can destroy `v` but `elem` is still usable. I guess I could
* transform this such that `elem` is only alive within a
* closure? Not sure. */
guard(elem* == i) => {
destroy_vec(v);
fwdpanic("check_vec, vec built wrong\n");
} => ;
check_vec(i + 1, n, v, ok);
} else {
ok(v);
}
}
main()
{
init_vec(0 as u64) => vec v;
populate_vec(0, 10, v) => vec v;
check_vec(0, 10, v) => vec v;
destroy_vec(v);
}
|
