如何在 ATS 中使用（或迭代）数组

Question

假设我们声明一个数组如下：

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))

我想遍历这样一个数组。我试过以下方法：

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

问题是当我遇到 myarray_nil 情况时，prval 变得不匹配。

因为pf是线性资源，我做不到

case+ pf of
| myarray_nil() =>
| myarray_cons(pf1, pf2) =>

因为这里消耗了pf但是根据函数定义必须保留。如何以这种方式遍历 myarray 并确保 pf 在不被消耗的情况下进行详尽匹配？

谢谢！

Answer 1

根据评论中给出的建议，我写了以下内容进行类型检查：

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

如何在 ATS 中使用（或迭代）数组

How to consume (or iterate over) an array in ATS

ats