std.deque

Double-ended queues: a sequence pushed onto and popped from at either end, persistent. Two lists, the front and the back the other way round, each with its length: where one would be left empty while the other has two or more, the other is cut in halves, one turned round for it. So a push, a pop and a peek at either end take a step each, amortised (where a deque is used once: a pop that cuts the halves, popped again from an older deque, cuts them again), and its size one. Import it by a name, import std.deque as Deque, as the list module has a null. The deque comes first, as a set’s does: Deque.pushFront d x, Deque.pushBack d x.

import std.deque as Deque

-- | the last of a list moved to its front
-- | >>> rotated [1, 2, 3]
-- | Cons 3 (Cons 1 (Cons 2 Nil))
rotated : List Int -> List Int
rotated xs =
  let d : Deque.Deque Int = Deque.fromList xs
  in Deque.toList
    (maybe d (\p -> Deque.pushFront (snd p) (fst p)) (Deque.popBack d))

Deque

data Deque a

A deque: how many are at the front and the front, first first, and how many are at the back and the back, last first. Each has an element where there are two or more in all.

empty

empty : {a : Type} -> Deque a

The deque of nothing.

null

null : {a : Type} -> Deque a -> Bool

Whether it holds nothing.

size

size : {a : Type} -> Deque a -> Int

How many elements it holds: kept with each side, so a step.

pushFront

pushFront : {a : Type} -> Deque a -> a -> Deque a

The deque with x at its front.

pushBack

pushBack : {a : Type} -> Deque a -> a -> Deque a

The deque with x at its back.

popFront

popFront : {a : Type} -> Deque a -> Maybe (a, Deque a)

Its first element and the deque without it, if it is not empty.

>>> maybe 0 (\p -> fst p) (popFront (pushBack (pushBack empty 1) 2))
1
>>> maybe (-1) (\p -> size (snd p)) (popFront (pushFront empty 1))
0

popBack

popBack : {a : Type} -> Deque a -> Maybe (a, Deque a)

Its last element and the deque without it, if it is not empty.

>>> maybe 0 (\p -> fst p) (popBack (pushBack (pushBack empty 1) 2))
2

peekFront

peekFront : {a : Type} -> Deque a -> Maybe a

Its first element, if it is not empty.

>>> peekFront (pushBack (pushBack empty 1) 2)
Just 1
>>> peekFront (empty : Deque Int)
Nothing

peekBack

peekBack : {a : Type} -> Deque a -> Maybe a

Its last element, if it is not empty.

>>> peekBack (pushBack (pushBack empty 1) 2)
Just 2

fromList

fromList : {a : Type} -> List a -> Deque a

The deque of a list’s elements, its first at the front.

>>> peekBack (fromList [1, 2, 3])
Just 3

toList

toList : {a : Type} -> Deque a -> List a

The elements, the front’s first.

>>> toList (pushFront (pushBack (fromList [1, 2, 3]) 4) 0)
Cons 0 (Cons 1 (Cons 2 (Cons 3 (Cons 4 Nil))))
>>> toList (maybe empty (\p -> snd p) (popBack (fromList [1, 2, 3])))
Cons 1 (Cons 2 Nil)