我如何在ATS中获取列表的细分市场

Question

基本上，我需要的是以下类型的函数：

fun
{a:t@ype}
{n:int}
{i,j:nat | i+j <= n}
list_get_segment(list(a, n), int(i), int(j)): list(a, j)

其中 i是该段的起始索引，而 j的长度是段的长度。

Answer 1

我能够使用以下代码

进行操作

fun {a:t@ype} takefirst {n, j:nat | j <= n} (ls: list(a, n), j:int(j)): list(a, j) =
  if j = 0
  then
        list_nil()
  else
        let
          val+ list_cons(head,tail) = ls
        in
          list_cons(head,takefirst(tail, j-1))
        end
fun {a:t@ype} list_get_segment {n, i, j:nat | i+j <= n} (ls: list(a, n), i:int(i), j:int(j)): list(a, j) =
  if i = 0
  then
        takefirst(ls, j)
  else
        let
          val+ list_cons(head,tail) = ls
        in
          list_get_segment(tail,i-1, j)
        end