How can I get a segment of a list in ATS?

Question

Basically, what I need is a function of the following type:

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)

where i is the starting index of the segment and j the length of the segment.

Answer 1

I was able to do it with the following code

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