Как я могу получить сегмент списка в 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