open list

val convert (): () = ()
alias convertible (p: perm) (q: perm): perm = convert @ (| consumes p) -> (| q)

data mutable iterator a (hole: perm) (post: perm) = Iterator {
  content: {p: perm} (
    l: list a
    | p * convertible (p * hole * l @ list a) post
  )
}

data offer a (post: perm) =
| None { | post }
| Some { x: a }

val next [a, hole: perm, post: perm] (consumes (it: iterator a hole post | hole)):
  offer (x: a | it @ iterator a (x @ a) post) post =
  match it.content with
  | Nil ->
    convert ();
    None
  | Cons { head; tail } ->
    it.content <- tail;
    Some { x = head }
  end 

val stop [a, hole: perm, post: perm] (consumes (it: iterator a hole post | hole)): (| post) =
  convert ()

val new [a] (consumes l: list a): iterator a empty (l @ list a) =
  Iterator { content = l }

(* -------------------------------------------- *)

val rec loop [a, hole: perm, post: perm]
  (consumes (it: iterator a hole post | hole), f: a -> ()): (| post) =

  match next [hole = hole] it with
  | None ->
    assert post;
    ()
  | Some { x } ->
    f x;
    loop [hole = (x @ a)] (it, f)
  end

val rec nth [a, hole: perm, post: perm] (consumes it: (iterator a hole post | hole), n: int):
  offer (x: a | it @ iterator a (x @ a) post) post =

  match next [hole = hole] it with
  | None ->
    None
  | Some { x } ->
    if n <= 0 then (
      Some { x = x }
    ) else (
      nth [a = a, hole = (x @ a)] (it, n-1)
    )
  end

val _ =
  let l = three (1, 2, 3) in
  let it = new l in
  match nth [hole = empty] (it, 1) with
  | None ->
    ()
  | Some { x } ->
    (* Do stuff on x *)
    print x;

    (* Give (x @ int) back to the list, close the iteration *)
    stop it
  end
  (* l @ list int *)