Queue

#include "share/atspre_staload.hats"

staload UN = "prelude/SATS/unsafe.sats"
staload "libats/SATS/deqarray.sats"
staload _ = "libats/DATS/deqarray.dats"

absprop ISNIL (id: int, b: bool)
absprop ISFUL (id: int, b: bool)

absvtype queue_vtype (a: vt@ype+, int) = ptr
vtypedef queue (a: vt@ype, id: int) = queue_vtype (a, id)
vtypedef queue (a: vt@ype) = [id: int] queue (a, id)

extern fun {a: vt@ype} queue_make (cap: intGt(0)): queue (a)
extern fun {a: t@ype} queue_free (que: queue (a)): void

extern fun {a: vt@ype} queue_isnil {id: int} (!queue (a, id)): [b: bool] (ISNIL (id, b) | bool(b))
extern fun {a: vt@ype} queue_isful {id: int} (!queue (a, id)): [b: bool] (ISFUL (id, b) | bool(b))

extern fun {a: vt@ype} queue_insert {id: int} (ISFUL (id, false) | que: !queue (a, id) >> queue (a, id2), x: a) : #[id2: int] void
extern fun {a: vt@ype} queue_remove {id: int} (ISNIL (id, false) | que: !queue (a, id) >> queue (a, id2)) : #[id2: int] a

assume queue_vtype (a: vt@ype, id: int) = deqarray (a)
assume ISNIL (id: int, b: bool) = unit_p
assume ISFUL (id: int, b: bool) = unit_p

implement {a} queue_make (cap) = deqarray_make_cap (i2sz (cap))
implement {a} queue_free (que) = deqarray_free_nil ($UN.castvwtp0 {deqarray (a, 1, 0)} (que))

implement {a} queue_isnil (que) = (unit_p () | deqarray_is_nil (que))
implement {a} queue_isful (que) = (unit_p () | deqarray_is_full (que))

implement {a} queue_insert (pf | que, x) =
{
    prval () = assert (pf) where { extern praxi assert {id: int} (pf: ISFUL (id, false)) : [false] void }
    val () = deqarray_insert_atend<a> (que, x)
}

implement {a} queue_remove (pf | que) = let
    prval () = assert (pf) where { extern praxi assert {id: int} (pf: ISNIL (id, false)) : [false] void }
in
    deqarray_takeout_atbeg<a> (que)
end

implement main0 () = () where
{
    val que = queue_make<int> (3)
    
    val (pff | _) = queue_isful (que)
    val (pfn | _) = queue_isnil (que)
    
    val () = queue_insert<int> (pff | que, 1)
    val () = queue_insert<int> (pff | que, 2)
    val () = println! (queue_remove<int> (pfn | que))
    val () = queue_insert<int> (pff | que, 3)
    val () = println! (queue_remove<int> (pfn | que))
    val () = println! (queue_remove<int> (pfn | que))
    
    val () = queue_free<int> (que)
}