Queue/Definition: Difference between revisions

(*------------------------------------------------------------------*)

 

(* A list that forms the queue, and a pointer to its last node. *)

@(list_vt (vt, n), ptr)

 

fn {}

() :

@(NIL, the_null_ptr)

 

fn {}

{vt : vt@ype}

[is_empty : bool | is_empty == (n == 0)]

bool is_empty =

 

fn {vt : vt@ype}

{n : int}

x : vt) :

(* Returns the new queue. *)

[m : int | 1 <= m; m == n + 1]

let

val @(lst, tail_ptr) = q

 

(* The dequeue routine simply CANNOT BE CALLED with an empty queue.

fn {vt : vt@ype}

{n : int | 1 <= n}

(* Returns a tuple: the dequeued element and the new queue. *)

[m : int | 0 <= m; m == n - 1]

case+ q.0 of

| ~ (x :: lst) => @(x, @(lst, q.1))

 

extern fun {vt : vt@ype}

fn {vt : vt@ype}

void =

let

| ~ (hd :: tl) =>

begin

loop tl

end

(* An example: a queue of nonlinear strings. *)

 

 

fn {} (* A parameterless template, for efficiency. *)

 

fn {} (* A parameterless template, for efficiency. *)

[is_empty : bool | is_empty == (n == 0)] bool is_empty =

 

fn

 

 

fn

let

implement

(* A nonlinear string will be allowed to leak. (It might be

collected as garbage, however.) *)

begin end

in

end

 

 

implement

x = four

iseqz q = true</pre>

 

=={{header|AutoHotkey}}==