Suppose we declare an array as the following:
dataview myarray
( a:t@ype (* element types *)
, addr (* location *)
, int (* size *)
) =
| {l:addr}
myarray_nil(a, l, 0)
| {l:addr}{n:int}
myarray_cons(a, l, n + 1) of (a@l, myarray(a, l + sizeof(a), n))
I would like to iterate over such an array. I have tried the following way:
fun
{a:t@ype}
myarray_map
{l: addr}{n: nat}
(pf: !myarray(a, l, n) | p0: ptr(l), f:a-<cloref1>a): void = let
prval myarray_cons(pf1, pf2) = pf
val elm = ptr_get<a>(pf1 | p0)
val () = ptr_set<a>(pf1 | p0, f(elm))
val p1 = ptr_succ<a>(p0)
in
(pf:= myarray_cons(pf1, pf2); myarray_map(pf | p1, f))
end
The issue is when I hit the myarray_nil case, the prval becomes unmatched.
Since pf is a linear resource, I cannot do
case+ pf of
| myarray_nil() =>
| myarray_cons(pf1, pf2) =>
Because pf is consumed here but it must be retained according to the function definition. How can I iterate through myarray in this way and ensure that pf is matched exhaustively while not being consumed?
Thank you!
Following the advice given in the comments, I wrote the following which typechecks:
fun
{a:t@ype}
myarray_map
{l: addr}{n: nat | n > 0}
(pf: !myarray(a, l, n) | p0: ptr(l), n: int(n), f:a-<cloref1>a): void = let
prval myarray_cons(pf1, pf2) = pf
val elm = ptr_get<a>(pf1 | p0)
val () = ptr_set<a>(pf1 | p0, f(elm))
val p1 = ptr_succ<a>(p0)
in
if n = 1
then ()
else myarray_map(pf2 | p1, n - 1, f); pf := myarray_cons(pf1, pf2)
end