Reputation: 265
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.
Upvotes: 1
Views: 45
Reputation: 2799
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
Upvotes: 2