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];

	/* expand if we run out of space */
	if c > 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([c => n, s => s, nbuf => buf] vec);
	} else {
		/* if this were a generic vector we'd have to worry about
		 * destroying the elements, but since we're just dealing with
		 * integers this is fine */
		ok([c => 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, 1000000, v) => vec v;
	check_vec(0, 1000000, v) => vec v;
	destroy_vec(v);
}