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
|
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];
buf + (n - 1 as u64) => nbuf;
nil nbuf {
nil nbuf;
fwdfree(buf);
fwdpanic("should never happen");
} => 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 - 1, 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("bounds error");
} => ;
buf + i => *i64 nbuf;
nil nbuf {
nil nbuf;
fwdfree(buf);
fwdpanic("should never happen");
} => &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 {
err();
} else {
ok();
}
}
check_vec(i64 i, i64 n, vec v, (vec) ok)
{
if i < n {
at_vec(v, i as u64) => v, elem;
guard(elem* != i) => {
destroy_vec(v);
fwdpanic("vec built wrong");
} => ;
check_vec(i + 1, n, v, ok);
} else {
ok(v);
}
}
main()
{
init_vec(0 as u64) => vec v;
populate_vec(0, 1000000, v) => vec v;
check_vec(0, 1000000, v) => vec v;
destroy_vec(v);
}
|
