291 lines
7.2 KiB
Plaintext
291 lines
7.2 KiB
Plaintext
(* NOTE: Others are treating more negative numbers as the higher
|
|
priority, but I think it is pretty clear that making tea and
|
|
feeding the cat are higher in priority than solving RC tasks.
|
|
|
|
So I treat more positive numbers as higher priority.
|
|
|
|
But see a note below on how easy it is to reverse that. *)
|
|
|
|
#include "share/atspre_staload.hats"
|
|
staload UN = "prelude/SATS/unsafe.sats"
|
|
|
|
(* For the sake of the task, use a heap implementation that comes with
|
|
the ATS distribution. *)
|
|
staload H = "libats/ATS1/SATS/funheap_binomial.sats"
|
|
|
|
(* #include instead of anonymous staload, to work around an
|
|
inconvenience in the distributed code: funheap_is_empty and
|
|
funheap_isnot_empty are functions rather than template
|
|
functions. One could instead compile funheap_binomial.dats
|
|
separately. Or one could copy and modify the distributed code to
|
|
one's own taste. (The heap code is GPL-3+) *)
|
|
#include "libats/ATS1/DATS/funheap_binomial.dats"
|
|
|
|
#define NIL list_nil ()
|
|
#define :: list_cons
|
|
|
|
abstype pqueue (a : t@ype+) = ptr
|
|
|
|
extern fn {}
|
|
pqueue_make_empty :
|
|
{a : t@ype}
|
|
() -<> pqueue a
|
|
|
|
extern fn {}
|
|
pqueue_is_empty :
|
|
{a : t@ype}
|
|
pqueue (INV(a)) -<> [b : bool] bool
|
|
|
|
extern fn {}
|
|
pqueue_isnot_empty :
|
|
{a : t@ype}
|
|
pqueue (INV(a)) -<> [b : bool] bool
|
|
|
|
extern fn {a : t@ype}
|
|
pqueue_size :
|
|
pqueue (INV(a)) -<> [n : nat] size_t n
|
|
|
|
extern fn {a : t@ype}
|
|
pqueue_insert :
|
|
(&pqueue (INV(a)) >> _, int, a) -< !wrt > void
|
|
|
|
extern fn {a : t@ype}
|
|
pqueue_delete :
|
|
(&pqueue (INV(a)) >> _) -< !wrt > Option a
|
|
|
|
extern fn {a : t@ype}
|
|
pqueue_peek :
|
|
(pqueue (INV(a))) -< !wrt > Option a
|
|
|
|
extern fn {a : t@ype}
|
|
pqueue_merge :
|
|
(pqueue (INV(a)), pqueue a) -< !wrt > pqueue a
|
|
|
|
local
|
|
|
|
typedef heap_elt (a : t@ype+) =
|
|
'{
|
|
(* The "priority" field must come first. We take advantage of
|
|
the layout of a '{..} being that of a C struct. *)
|
|
priority = int,
|
|
value = a
|
|
}
|
|
|
|
fn {a : t@ype}
|
|
heap_elt_get_priority (elt : heap_elt a)
|
|
:<> int =
|
|
let
|
|
typedef prio_t = '{ priority = int }
|
|
val prio = $UN.cast{prio_t} elt
|
|
in
|
|
prio.priority
|
|
end
|
|
|
|
extern castfn
|
|
pqueue2heap :
|
|
{a : t@ype}
|
|
pqueue a -<> $H.heap (heap_elt a)
|
|
|
|
extern castfn
|
|
heap2pqueue :
|
|
{a : t@ype}
|
|
$H.heap (heap_elt a) -<> pqueue a
|
|
|
|
macdef p2h = pqueue2heap
|
|
macdef h2p = heap2pqueue
|
|
|
|
macdef comparison_cloref =
|
|
lam (x, y) =<cloref>
|
|
let
|
|
val px = heap_elt_get_priority x
|
|
and py = heap_elt_get_priority y
|
|
in
|
|
(* NOTE: Reverse the order of the arguments, if you want more
|
|
negative numbers to represent higher priorities. *)
|
|
compare (py, px)
|
|
end
|
|
|
|
fn {a : t@ype}
|
|
funheap_getmin_opt (heap : $H.heap (INV(a)),
|
|
cmp : $H.cmp a)
|
|
:<!wrt> Option_vt a =
|
|
let
|
|
var result : a?
|
|
val success = $H.funheap_getmin<a> (heap, cmp, result)
|
|
in
|
|
if success then
|
|
let
|
|
prval () = opt_unsome{a} result
|
|
in
|
|
Some_vt{a} result
|
|
end
|
|
else
|
|
let
|
|
prval () = opt_unnone{a} result
|
|
in
|
|
None_vt{a} ()
|
|
end
|
|
end
|
|
|
|
in
|
|
|
|
implement {}
|
|
pqueue_make_empty {a} () =
|
|
h2p{a} ($H.funheap_make_nil {heap_elt a} ())
|
|
|
|
implement {}
|
|
pqueue_is_empty {a} pq =
|
|
$H.funheap_is_empty {heap_elt a} (p2h{a} pq)
|
|
|
|
implement {}
|
|
pqueue_isnot_empty {a} pq =
|
|
$H.funheap_isnot_empty {heap_elt a} (p2h{a} pq)
|
|
|
|
implement {a}
|
|
pqueue_size pq =
|
|
$H.funheap_size<heap_elt a> (p2h{a} pq)
|
|
|
|
implement {a}
|
|
pqueue_insert (pq, priority, x) =
|
|
let
|
|
val elt =
|
|
'{
|
|
priority = priority,
|
|
value = x
|
|
} : heap_elt a
|
|
and compare = comparison_cloref
|
|
var heap = p2h{a} pq
|
|
val () = $H.funheap_insert (heap, elt, compare)
|
|
in
|
|
pq := h2p{a} heap
|
|
end
|
|
|
|
implement {a}
|
|
pqueue_delete pq =
|
|
let
|
|
typedef t = heap_elt a
|
|
val compare = comparison_cloref
|
|
var heap = p2h{a} pq
|
|
val elt_opt = $H.funheap_delmin_opt<heap_elt a> (heap, compare)
|
|
in
|
|
pq := h2p{a} heap;
|
|
case+ elt_opt of
|
|
| ~ Some_vt elt => Some (elt.value)
|
|
| ~ None_vt () => None ()
|
|
end
|
|
|
|
implement {a}
|
|
pqueue_peek pq =
|
|
let
|
|
typedef t = heap_elt a
|
|
val compare = comparison_cloref
|
|
and heap = p2h{a} pq
|
|
val elt_opt = funheap_getmin_opt<heap_elt a> (heap, compare)
|
|
in
|
|
case+ elt_opt of
|
|
| ~ Some_vt elt => Some (elt.value)
|
|
| ~ None_vt () => None ()
|
|
end
|
|
|
|
implement {a}
|
|
pqueue_merge (pq1, pq2) =
|
|
let
|
|
val heap1 = p2h{a} pq1
|
|
and heap2 = p2h{a} pq2
|
|
and compare = comparison_cloref
|
|
in
|
|
h2p{a} ($H.funheap_merge<heap_elt a> (heap1, heap2, compare))
|
|
end
|
|
|
|
overload iseqz with pqueue_is_empty
|
|
overload isneqz with pqueue_isnot_empty
|
|
overload size with pqueue_size
|
|
overload insert with pqueue_insert
|
|
overload delete with pqueue_delete
|
|
overload peek with pqueue_peek
|
|
overload merge with pqueue_merge
|
|
|
|
end
|
|
|
|
implement
|
|
main0 () =
|
|
let
|
|
var pq = pqueue_make_empty{string} ()
|
|
val () = print! (" ", iseqz pq)
|
|
val () = print! (" ", isneqz pq)
|
|
val () = print! (" ", "size:", size pq)
|
|
val () = insert (pq, 3, "3")
|
|
val () = insert (pq, 4, "4")
|
|
val () = insert (pq, 2, "2")
|
|
val () = insert (pq, 5, "5")
|
|
val () = insert (pq, 1, "1")
|
|
val () = print! (" ", iseqz pq)
|
|
val () = print! (" ", isneqz pq)
|
|
val () = print! (" ", "size:", size pq)
|
|
|
|
var pq2 = pqueue_make_empty{string} ()
|
|
val () = insert (pq, 6, "6")
|
|
val () = insert (pq, 4, "4a")
|
|
|
|
val () = pq := merge (pq, pq2)
|
|
val () = print! (" ", iseqz pq)
|
|
val () = print! (" ", isneqz pq)
|
|
val () = print! (" ", "size:", size pq)
|
|
|
|
val- Some x = peek pq
|
|
val () = print! (" ", x)
|
|
val- Some x = peek pq
|
|
val () = print! (" ", x)
|
|
val- Some x = peek pq
|
|
val () = print! (" ", x)
|
|
val- Some x = peek pq
|
|
val () = print! (" ", x)
|
|
val- Some x = delete pq
|
|
val () = print! (" ", x)
|
|
val- Some x = delete pq
|
|
val () = print! (" ", x)
|
|
val- Some x = peek pq
|
|
val () = print! (" ", x)
|
|
val- Some x = peek pq
|
|
val () = print! (" ", x)
|
|
val- Some x = delete pq
|
|
val () = print! (" ", x)
|
|
val- Some x = peek pq
|
|
val () = print! (" ", x)
|
|
val- Some x = peek pq
|
|
val () = print! (" ", x)
|
|
val- Some x = peek pq
|
|
val () = print! (" ", x)
|
|
val- Some x = peek pq
|
|
val () = print! (" ", x)
|
|
val- Some x = delete pq
|
|
val () = print! (" ", x)
|
|
val- Some x = delete pq
|
|
val () = print! (" ", x)
|
|
val- Some x = delete pq
|
|
val () = print! (" ", x)
|
|
val- Some x = delete pq
|
|
val () = print! (" ", x)
|
|
val- None () = delete pq
|
|
|
|
val () = println! ()
|
|
|
|
var pq2 = pqueue_make_empty{string} ()
|
|
val () = insert (pq2, 3, "Clear drains")
|
|
val () = insert (pq2, 4, "Feed cat")
|
|
val () = insert (pq2, 5, "Make tea")
|
|
val () = insert (pq2, 1, "Solve RC tasks")
|
|
val () = insert (pq2, 2, "Tax return")
|
|
val- Some x = delete pq2
|
|
val () = println! ("|", x, "|")
|
|
val- Some x = delete pq2
|
|
val () = println! ("|", x, "|")
|
|
val- Some x = delete pq2
|
|
val () = println! ("|", x, "|")
|
|
val- Some x = delete pq2
|
|
val () = println! ("|", x, "|")
|
|
val- Some x = delete pq2
|
|
val () = println! ("|", x, "|")
|
|
in
|
|
end
|