#include
"share/atspre_staload.hats"
(* ****** ****** *)
(* intrusive node type *)
typedef slseg_node = @(int, ptr)
typedef slseg_node (l:addr) = @(int, ptr l)
viewdef slseg_node_v (l1: addr, l2: addr) = slseg_node (l1) @ l2
extern
fun{}
slseg_node_set_next {l1,l2,l3:addr} (!slseg_node_v (l1, l2) >> slseg_node_v (l3, l2) | ptr l2, ptr l3): void
extern
fun{}
slseg_node_get_next {l1,l2:addr} (!slseg_node_v (l1, l2) | ptr l2): ptr l1
implement
slseg_node_set_next<> {l1,l2,l3} (pf_at | p, p2) = !p.1 := p2
implement
slseg_node_get_next<> {l1,l2} (pf_at | p) = !p.1
overload set_next with slseg_node_set_next
overload get_next with slseg_node_get_next
(* ***** ****** *)
(* dataview for singly-linked list segment
* (adapted from ATS1 code by Hongwei Xi)
*)
dataview slseg_v
(addr(*self*), addr(*last node's [next]*), int(*segment length*)) =
| {n:nat} {l1,l2,l3:addr}
slseg_v_cons (l1, l3, n+1) of (
mfree_gc_v (l1), slseg_node_v (l2, l1), slseg_v (l2, l3, n)
) // end of [slseg_v_cons]
| {l:addr} slseg_v_nil (l, l, 0)
// end of [slseg_v]
extern
prfun
slseg_v_lemma_size {l1,l2:addr}{n:int} (!slseg_v (l1, l2, n)): [n>=0] void
extern
prfun slseg_v_extend
{l1,l2,l3:addr} {n:nat} (
pf_sl: slseg_v (l1, l2, n)
, pf_gc: mfree_gc_v (l2)
, pf_at: slseg_node_v (l3, l2)
) :<prf> slseg_v (l1, l3, n+1)
extern
prfun slseg_v_append
{l1,l2,l3:addr} {n1,n2:nat} (
pf1_sl: slseg_v (l1, l2, n1), pf2_sl: slseg_v (l2, l3, n2)
) :<prf> slseg_v (l1, l3, n1+n2) // end of [slseg_v_append]
(* ****** ****** *)
(* functions for constructing slseg values *)
// nil/empty list segment
extern
castfn
slseg_nil {l1,l2:addr} (
mfree_gc_v (l1), slseg_node_v (l2, l1) | p1: ptr l1, p2: ptr l2
) : (slseg_v (l1, l2, 1) | void)
// slseg cons -- insert before the first elt
extern
fun{}
slseg_cons {p_nxt0,p_slf,p_fst,p_lst:addr}{n:int} (
mfree_gc_v (p_slf), slseg_node_v (p_nxt0, p_slf)
, slseg_v (p_fst, p_lst, n)
| ptr p_slf, ptr p_fst
): (slseg_v (p_slf, p_lst, n+1) | void)
// slseg extend -- insert after the last elt
extern
castfn
slseg_snoc {p_nxt0,p_fst,p_lst:addr}{n:int} (
mfree_gc_v (p_lst), slseg_node_v (p_nxt0, p_lst)
, slseg_v (p_fst, p_lst, n)
| ptr p_lst
): (slseg_v (p_fst, p_nxt0, n+1) | void)
extern
fun{}
slseg_free {l1,l2:addr} {n:int} (
slseg_v (l1, l2, n) | ptr l1, int n
): void
(* ****** ****** *)
(* slseg functions: implementations *)
implement
slseg_nil (pf_gc, pf_at | p1, p2) = let
prval pf_res = slseg_v_cons (pf_gc, pf_at, slseg_v_nil ())
in
(pf_res | ((*void*)))
end
implement
slseg_cons<> {p_nxt0,p_slf,p_fst,p_lst} (pf_gc, pf_at, pf_seg | p_slf, p_seg) = let
val () = set_next (pf_at | p_slf, p_seg)
prval () = slseg_v_lemma_size (pf_seg)
prval pf_seg = slseg_v_cons (pf_gc, pf_at, pf_seg)
in
(pf_seg | ((*void*)))
end
implement
slseg_snoc {p_nxt0,p_fst,p_lst} (pf_gc, pf_at, pf_seg | p_lst) = let
prval () = slseg_v_lemma_size (pf_seg)
prval pf_seg = slseg_v_extend (pf_seg, pf_gc, pf_at)
in
(pf_seg | ((*void*)))
end
implement
slseg_free<> {l1,l2} {n} (pf_seg | p_seg, n) = let
var i: int = n
prval () = slseg_v_lemma_size (pf_seg)
var p = p_seg
prvar pf0 = pf_seg
//
val () =
while* {i:nat; l1,l2:addr | i <= n} .<i>. (
i: int (i)
, p: ptr (l1)
, pf0: slseg_v (l1, l2, i)
) : [l3,l4:addr] (
pf0: slseg_v (l3, l4, 0)
) => (
i > 0
) {
//
prval slseg_v_cons (pf_gc, pf_at, pf1_seg) = pf0
prval () = pf0 := pf1_seg
//
val p1 = get_next (pf_at | p)
val () = ptr_free {slseg_node} (pf_gc, pf_at | p) // TODO: move this into node API
val () = p := p1
//
val () = i := i - 1
//
} // end of [val]
//
prval slseg_v_nil () = pf0
//
in
end // end of [slseg_free]
(* ****** ****** *)
(* queue abstract type: this one is based on singly-linked lists
* (adapted from ATS1 code by Hongwei Xi)
*)
absvtype linqueuelst_vt (n:int(*size*)) = ptr
stadef queue = linqueuelst_vt
extern
fun{}
linqueuelst_is_nil
{n:nat} (xs: !queue (n)):<> bool (n==0)
extern
fun{}
linqueuelst_is_cons
{n:nat} (xs: !queue (n)):<> bool (n > 0)
extern fun{}
linqueuelst_nil ():<> queue (0)
extern fun{}
linqueuelst_enqueue {n:nat} // O(1)
(xs: &queue (n) >> queue (n+1), x: int): void
extern fun{}
linqueuelst_dequeue {n:pos} // O(1)
(xs: &queue (n) >> queue (n-1)): int
extern fun{}
linqueuelst_free {n:int} (xs: queue (n)): void
(* ****** ****** *)
local
datavtype queuelst_vt (int) =
| {n:nat} {l1,l2,l3:addr}
queuelst_vt_some (n+1) of (
slseg_v (l1, l2, n), mfree_gc_v (l2), slseg_node_v (null, l2) | int n, ptr l1, ptr l2
) // end of [queuelst_vt_some]
| queuelst_vt_none (0) of ()
assume linqueuelst_vt (n: int) = queuelst_vt (n)
in
implement{}
linqueuelst_nil () = queuelst_vt_none ()
implement{}
linqueuelst_is_nil (xs) = (
case+ xs of
| queuelst_vt_some (_, _, _| _, _, _) => false
| queuelst_vt_none () => true
) (* end of [linqueuelst_is_nil] *)
implement{}
linqueuelst_is_cons (xs) = (
case+ xs of
| queuelst_vt_some (_, _, _ | _, _, _) => true
| queuelst_vt_none () => false
) (* end of [linqueuelst_is_cons] *)
implement{}
linqueuelst_enqueue (xs, x) = let
// TODO: move this logic out into slseg node API
val (pf_at_new, pf_gc_new | p_new) = ptr_alloc<slseg_node> ()
val () = p_new->0 := x
val () = p_new->1 := the_null_ptr
in
case+ xs of
| @queuelst_vt_some
(pf_seg, pf_gc, pf_at | n, p1, p2) => let
prval [l2:addr] EQADDR () = ptr_get_index (p2)
val () = set_next (pf_at | p2, p_new)
prval pf_seg_new = slseg_v_extend (pf_seg, pf_gc, pf_at)
prval () = begin
pf_seg := pf_seg_new; pf_gc := pf_gc_new; pf_at := pf_at_new
end // end of [prval]
in
n := n + 1;
p2 := p_new;
fold@ xs;
end // end of [queuelst_vt_some]
| ~queuelst_vt_none () => begin
xs := queuelst_vt_some (slseg_v_nil (), pf_gc_new, pf_at_new | 0, p_new, p_new)
end // end of [queuelst_vt_none]
end // end of [linqueuelst_enqueue]
implement{}
linqueuelst_dequeue (xs) = let
val+ @queuelst_vt_some (pf_seg, pf_gc, pf_at | n, p1, p2) = xs
in
if n > 0 then let
prval slseg_v_cons (pf_gc, pf_at, pf1_seg) = pf_seg
val x = p1->0 // TODO: move this out into slseg node API
val p1_ = p1
val () = p1 := get_next (pf_at | p1)
// TODO: move this out into slseg node API
val () = ptr_free {slseg_node} (pf_gc, pf_at | p1_)
in
pf_seg := pf1_seg;
n := n - 1;
fold@ xs;
x
end else let
prval slseg_v_nil () = pf_seg
val x = p2->0 // TODO: move this out into slseg node API
val () = ptr_free {slseg_node} (pf_gc, pf_at | p2)
in
free@ {0} (xs);
xs := queuelst_vt_none ();
x
end // end of [if]
end // end of [linqueuelst_deqeue]
implement{}
linqueuelst_free (xs) = case+ xs of
| ~queuelst_vt_some (pf_seg, pf_gc, pf_at | n, p1, p2) => let
val () = ptr_free {slseg_node} (pf_gc, pf_at | p2)
in
slseg_free<> (pf_seg | p1, n)
end // end of [queuelst_vt_some]
| ~queuelst_vt_none () => ()
// end of [linqueuelst_free]
end
overload queue_create with linqueuelst_nil
overload enqueue with linqueuelst_enqueue
overload dequeue with linqueuelst_dequeue
overload queue_free with linqueuelst_free
implement
main0 () = let
var xs = queue_create()
val () = enqueue(xs, 1)
val () = enqueue(xs, 2)
val () = print(dequeue(xs)) // print 1
val () = print_newline ()
val () = enqueue(xs,3)
val () = print(dequeue(xs)) // print 2
val () = print_newline ()
val () = print(dequeue(xs)) // print 3
val () = print_newline ()
val () = queue_free (xs)
in
end
