Description

This module provides an implementation of a First-In, First-Out (FIFO) queue based on Okasaki's "Purely Functional Data Structures." Ch.3. This Okasaki Queue version data structure ensures amortized constant-time performance for basic operations such as push, pop, and front. The Okasaki Queue consists of two lists (front and back) to separate the concerns of adding and removing elements for ensuring efficient performance.

Definitions

type Queue (A : Type)Source #

A first-in-first-out data structure

Constructors

mkQueue@{ front : List A; back : List A; }

empty {A} : Queue ASource #

𝒪(1). The empty Queue.

isEmpty {A} (queue : Queue A) : BoolSource #

𝒪(1). Returns true when the Queue has no elements.

head {A} (queue : Queue A) : Maybe ASource #

𝒪(1). Returns first element of the Queue, if any.

tail {A} (queue : Queue A) : Maybe (Queue A)Source #

𝒪(1). Removes the first element from the Queue. If the Queue is empty

check {A} (queue : Queue A) : Queue ASource #

𝒪(n) worst-case, but 𝒪(1) amortized

pop {A} (queue : Queue A) : Maybe (Pair A (Queue A))Source #

𝒪(n) worst-case, but 𝒪(1) amortized. Returns the first element and the

push {A} (x : A) (queue : Queue A) : Queue ASource #

𝒪(1). Adds an element to the end of the Queue.

pushMany {A} (list : List A) (queue : Queue A) : Queue ASource #

𝒪(n). Adds a list of elements to the end of the Queue.

fromList {A} (list : List A) : Queue ASource #

𝒪(n). Build a Queue from a List.

toList {A} (queue : Queue A) : List ASource #

toList: O(n). Returns a List of the elements in the Queue. The elements are in the same order as they appear in the Queue (i.e. the first element of the Queue is the first element of the List).

size {A} (queue : Queue A) : NatSource #

𝒪(n). Returns the number of elements in the Queue.

instance eqQueueI {A} {{Eq A}} : Eq (Queue A)Source #

instance showQueueI {A} {{Show A}} : Show (Queue A)Source #

instance ordQueueI {A} {{Ord A}} : Ord (Queue A)Source #