Queue/Definition: Difference between revisions
→{{header|AutoHotkey}}
(→{{header|BQN}}: Link to linked-list queue example in documentation) |
|||
Line 1,287:
Error detected !!!!.
=={{header|ATS}}==
=== A linear linked list as a queue ===
<lang ATS>(*------------------------------------------------------------------*)
#define ATS_DYNLOADFLAG 0
#include "share/atspre_staload.hats"
staload UN = "prelude/SATS/unsafe.sats"
(*------------------------------------------------------------------*)
vtypedef queue_t (vt : vt@ype+, n : int) =
(* A list that forms the queue, and a pointer to its last node. *)
@(list_vt (vt, n), ptr)
#define NIL list_vt_nil ()
#define :: list_vt_cons
fn {}
queue_t_nil {vt : vt@ype}
() :
queue_t (vt, 0) =
@(NIL, the_null_ptr)
fn {}
queue_t_is_empty
{n : int}
{vt : vt@ype}
(q : !queue_t (vt, n)) :
[is_empty : bool | is_empty == (n == 0)]
bool is_empty =
case+ q.0 of
| NIL => true
| _ :: _ => false
fn {vt : vt@ype}
queue_t_enqueue
{n : int}
(q : queue_t (vt, n),
x : vt) :
(* Returns the new queue. *)
[m : int | 1 <= m; m == n + 1]
queue_t (vt, m) =
let
val @(lst, tail_ptr) = q
prval _ = lemma_list_vt_param lst
in
case+ lst of
| ~ NIL =>
let
val lst = x :: NIL
val tail_ptr = $UN.castvwtp1{ptr} lst
in
@(lst, tail_ptr)
end
| _ :: _ =>
let
val old_tail = $UN.castvwtp0{list_vt (vt, 1)} tail_ptr
val+ @ (hd :: tl) = old_tail
(* Extend the list by one node, at its tail end. *)
val new_tail : list_vt (vt, 1) = x :: NIL
val tail_ptr = $UN.castvwtp1{ptr} new_tail
prval _ = $UN.castvwtp0{void} tl
val _ = tl := new_tail
prval _ = fold@ old_tail
prval _ = $UN.castvwtp0{void} old_tail
(* Let us cheat and simply *assert* (rather than prove) that
the list has grown by one node. *)
val lst = $UN.castvwtp0{list_vt (vt, n + 1)} lst
in
@(lst, tail_ptr)
end
end
(* The dequeue routine simply CANNOT BE CALLED with an empty queue.
It requires a queue of type queue_t (vt, n) where n is positive. *)
fn {vt : vt@ype}
queue_t_dequeue
{n : int | 1 <= n}
(q : queue_t (vt, n)) :
(* Returns a tuple: the dequeued element and the new queue. *)
[m : int | 0 <= m; m == n - 1]
@(vt, queue_t (vt, m)) =
case+ q.0 of
| ~ (x :: lst) => @(x, @(lst, q.1))
(* queue_t is a linear type that must be freed. *)
extern fun {vt : vt@ype}
queue_t$element_free : vt -> void
fn {vt : vt@ype}
queue_t_free {n : int}
(q : queue_t (vt, n)) :
void =
let
fun
loop {n : nat} .<n>. (lst : list_vt (vt, n)) : void =
case+ lst of
| ~ NIL => begin end
| ~ (hd :: tl) =>
begin
queue_t$element_free<vt> hd;
loop tl
end
prval _ = lemma_list_vt_param (q.0)
in
loop (q.0)
end
(*------------------------------------------------------------------*)
(* An example: a queue of nonlinear strings. *)
vtypedef strq_t (n : int) = queue_t (string, n)
fn {} (* A parameterless template, for efficiency. *)
strq_t_nil () : strq_t 0 =
queue_t_nil ()
fn {} (* A parameterless template, for efficiency. *)
strq_t_is_empty {n : int} (q : !strq_t n) :
[is_empty : bool | is_empty == (n == 0)] bool is_empty =
queue_t_is_empty<> q
fn
strq_t_enqueue {n : int} (q : strq_t n, x : string) :
[m : int | 1 <= m; m == n + 1] strq_t m =
queue_t_enqueue<string> (q, x)
fn (* Impossible to... VVVVVV ...call with an empty queue. *)
strq_t_dequeue {n : int | 1 <= n} (q : strq_t n) :
[m : int | 0 <= m; m == n - 1] @(string, strq_t m) =
queue_t_dequeue<string> q
fn
strq_t_free {n : int} (q : strq_t n) : void =
let
implement
queue_t$element_free<string> x =
(* A nonlinear string will be allowed to leak. (It might be
collected as garbage, however.) *)
begin end
in
queue_t_free<string> q
end
macdef qnil = strq_t_nil ()
overload iseqz with strq_t_is_empty
overload << with strq_t_enqueue
overload pop with strq_t_dequeue
overload free with strq_t_free
implement
main0 () =
{
val q = qnil
val _ = println! ("val q = qnil")
val _ = println! ("iseqz q = ", iseqz q)
val _ = println! ("val q = q << \"one\" << \"two\" << \"three\"")
val q = q << "one" << "two" << "three"
val _ = println! ("iseqz q = ", iseqz q)
val _ = println! ("val (x, q) = pop q")
val (x, q) = pop q
val _ = println! ("x = ", x)
val _ = println! ("val (x, q) = pop q")
val (x, q) = pop q
val _ = println! ("x = ", x)
val _ = println! ("val q = q << \"four\"")
val q = q << "four"
val _ = println! ("val (x, q) = pop q")
val (x, q) = pop q
val _ = println! ("x = ", x)
val _ = println! ("val (x, q) = pop q")
val (x, q) = pop q
val _ = println! ("x = ", x)
val _ = println! ("iseqz q = ", iseqz q)
//val (x, q) = pop q // If you uncomment this you cannot compile!
val _ = free q
}
(*------------------------------------------------------------------*)</lang>
{{out}}
<pre>$ patscc -O2 -DATS_MEMALLOC_GCBDW queues-postiats.dats -lgc && ./a.out
val q = qnil
iseqz q = true
val q = q << "one" << "two" << "three"
iseqz q = false
val (x, q) = pop q
x = one
val (x, q) = pop q
x = two
val q = q << "four"
val (x, q) = pop q
x = three
val (x, q) = pop q
x = four
iseqz q = true</pre>
=={{header|AutoHotkey}}==
| |||