#include "share/atspre_staload.hats"
staload UN = "prelude/SATS/unsafe.sats"

absvtype stream_vt = ptr // for string streams

extern fun create_stream_vt(): stream_vt
extern fun inc_stream_vt(stream: !stream_vt >> _): void
extern fun free_stream_vt(stream: stream_vt): void

local
  vtypedef stream_struct_vt(n:int) = @{
    data= Strptr1,
    size= size_t(n),
    pos= sizeLte(n)
  }
  vtypedef stream_struct_vt = [n:nat] stream_struct_vt(n)

  assume stream_vt = [l:addr] (stream_struct_vt@l, mfree_gc_v(l) | ptr(l))
in
  implement create_stream_vt() = let
    val (pf, pfgc | p) = ptr_alloc<stream_struct_vt(0)> ()
    val () = p->data := string0_copy("content of a text file")
    val () = p->size := i2sz(13)
    val () = p->pos := i2sz(0)
  in
    $UN.castvwtp0{stream_vt}((pf, pfgc | p))
  end

  implement inc_stream_vt(stream) = let
    val (pf, pfgc | p) = stream
    val () = p->pos := p->pos + 1
    val () = assertloc (p->pos <= p->size)
    val () = stream := (pf, pfgc | p)
  in
  end

  implement free_stream_vt(stream) = let
    val (pf, pfgc | p) = stream
    val () = strptr_free(p->data)
  in
    ptr_free{stream_struct_vt(0)?}(pfgc, pf| p)
  end
end

implement main0(argc, argv) = let
  val stream = create_stream_vt()
  val () = inc_stream_vt(stream)
in
  free_stream_vt(stream)
end