Interactive session for insert-full.mz

 - 
 
Non-duplicable permissions
Duplicable permissions
mutable data fifo a =
  | Empty { head: (); tail: () }
  | NonEmpty { head: dynamic; tail: dynamic }
adopts cell a

mutable data cell a =
  | Cell { contents: a; next: dynamic }

(* Insert [x] into [f]. *)
val insert [a] (consumes x: a, f: fifo a): () =
  let c = Cell { contents = x; next = () } in
  c.next <- c;
  give c to f;
  match f with
  | Empty ->
      tag of f <- NonEmpty;
      f.head <- c;
      f.tail <- c
  | NonEmpty { tail } ->
      take tail from f;
      tail.next <- c;
      give tail to f;
      f.tail <- c
  end