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
|
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 {fwdpanic("should never happen");} => dst;
e => dst*;
ok([n => n, s => s, nbuf => 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];
if i >= n {fwdpanic("bounds error");}
fwdptradd(buf, (i * sizeof(i64)) as i64) => *i64 buf;
nil buf {fwdpanic("should never happen");} => &i64 bufr;
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);
}
|
