#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)
}
PATSCC=$(PATSHOME)/bin/patscc
main: main.dats; $(PATSCC) -DATS_MEMALLOC_LIBC -o $@ $< -latslib && ./main && rm -f ./main_dats.c && rm -f ./main
