~/bend-docscommunity

deque.bend checks

raw source on the hub · import 0xd2d968d969a26029a632a3347c989456/deque.bend as Deque

Deque: a double-ended queue, as a front list and a reversed back list.

Pushing and popping on either end is amortized O(1), in any mix of ends (the refill below says why). Like List, the queries consume the deque: a Data deque is shared with +.

The laws at the bottom are checked every time this file is imported.

1 import
import Base

Laws

law Deque.to_list.new provedsource · line 164 · raw

@-A:Data -> {Deque.to_list(&2, A, Deque.new(&2, A)) == [] : List<&2, A>}

LAW: a new deque reads as the empty list

law Deque.to_list.push_front provedsource · line 172 · raw

@-A:Data -> @-x:A -> @d:Deque<&2, A> -> {Deque.to_list(&2, A, Deque.push_front(&2, A, x, d)) == x <> Deque.to_list(&2, A, d) : List<&2, A>}

LAW: push_front puts the element at the head of the list

law Deque.pop_front.push_front provedsource · line 185 · raw

@-A:Data -> @-x:A -> @d:Deque<&2, A> -> {Deque.pop_front(&2, A, Deque.push_front(&2, A, x, d)) == Some{(x, d)} : Maybe<&1, Pair(A, Deque<&2, A>)>}

LAW: pop_front undoes push_front

law Deque.pop_back.push_back provedsource · line 198 · raw

@-A:Data -> @-x:A -> @d:Deque<&2, A> -> {Deque.pop_back(&2, A, Deque.push_back(&2, A, x, d)) == Some{(x, d)} : Maybe<&1, Pair(A, Deque<&2, A>)>}

LAW: pop_back undoes push_back

law Deque.lemma.append_nil provedsource · line 212 · raw

@-A:Data -> @xs:List<&2, A> -> {List.append(&2, A, xs, []) == xs : List<&2, A>}

law Deque.lemma.append_assoc provedsource · line 226 · raw

@-A:Data -> @xs:List<&2, A> -> @-ys:List<&2, A> -> @-zs:List<&2, A> -> {List.append(&2, A, List.append(&2, A, xs, ys), zs) == List.append(&2, A, xs, List.append(&2, A, ys, zs)) : List<&2, A>}

law Deque.to_list.from_list provedsource · line 244 · raw

@-A:Data -> @xs:List<&2, A> -> {Deque.to_list(&2, A, Deque.from_list(&2, A, xs)) == xs : List<&2, A>}

LAW: a list read into a deque reads back as itself

law Deque.lemma.reverse_go provedsource · line 253 · raw

@-A:Data -> @xs:List<&2, A> -> @-acc:List<&2, A> -> {List.append(&2, A, List.reverse.go(&2, A, xs, []), acc) == List.reverse.go(&2, A, xs, acc) : List<&2, A>}

reversing onto an accumulator is reversing, then appending it

law Deque.to_list.push_back provedsource · line 273 · raw

@-A:Data -> @-x:A -> @d:Deque<&2, A> -> {Deque.to_list(&2, A, Deque.push_back(&2, A, x, d)) == List.append(&2, A, Deque.to_list(&2, A, d), [x]) : List<&2, A>}

LAW: push_back puts the element at the end of the list

Types

type Deque source · line 10 · raw

@-a:Quant -> @-A:Kind(a) -> Kind(a)

Definitions

def Deque.new source · line 13 · raw

@-a:Quant -> @-A:Kind(a) -> Deque<a, A>

def Deque.from_list source · line 17 · raw

@-a:Quant -> @-A:Kind(a) -> @xs:List<a, A> -> Deque<a, A>

the list's first element is the deque's front

def Deque.push_front source · line 20 · raw

@-a:Quant -> @-A:Kind(a) -> @x:A -> @d:Deque<a, A> -> Deque<a, A>

def Deque.push_back source · line 25 · raw

@-a:Quant -> @-A:Kind(a) -> @x:A -> @d:Deque<a, A> -> Deque<a, A>

def Deque.count.put source · line 30 · raw

@-a:Quant -> @-A:Kind(a) -> @h:A -> @rn:Pair(List<a, A>, Nat) -> Pair(List<a, A>, Nat)

def Deque.count source · line 37 · raw

@-a:Quant -> @-A:Kind(a) -> @xs:List<a, A> -> Pair(List<a, A>, Nat)

a list and its length, in one pass that hands the list back

def Deque.half source · line 44 · raw

@n:Nat -> Nat

def Deque.split.put source · line 55 · raw

@-a:Quant -> @-A:Kind(a) -> @h:A -> @lr:Pair(List<a, A>, List<a, A>) -> Pair(List<a, A>, List<a, A>)

def Deque.split source · line 62 · raw

@-a:Quant -> @-A:Kind(a) -> @n:Nat -> @xs:List<a, A> -> Pair(List<a, A>, List<a, A>)

the first n elements, and the rest

def Deque.pop_front.go source · line 79 · raw

@-a:Quant -> @-A:Kind(a) -> @xs:List<a, A> -> @b:List<a, A> -> Maybe<&1, Pair(A, Deque<a, A>)>

def Deque.pop_front.halves source · line 88 · raw

@-a:Quant -> @-A:Kind(a) -> @sm:Pair(List<a, A>, List<a, A>) -> Maybe<&1, Pair(A, Deque<a, A>)>

def Deque.pop_front.refill source · line 94 · raw

@-a:Quant -> @-A:Kind(a) -> @bn:Pair(List<a, A>, Nat) -> Maybe<&1, Pair(A, Deque<a, A>)>

def Deque.pop_front source · line 100 · raw

@-a:Quant -> @-A:Kind(a) -> @d:Deque<a, A> -> Maybe<&1, Pair(A, Deque<a, A>)>

def Deque.pop_back.go source · line 111 · raw

@-a:Quant -> @-A:Kind(a) -> @xs:List<a, A> -> @f:List<a, A> -> Maybe<&1, Pair(A, Deque<a, A>)>

def Deque.pop_back.halves source · line 120 · raw

@-a:Quant -> @-A:Kind(a) -> @sm:Pair(List<a, A>, List<a, A>) -> Maybe<&1, Pair(A, Deque<a, A>)>

def Deque.pop_back.refill source · line 126 · raw

@-a:Quant -> @-A:Kind(a) -> @fn:Pair(List<a, A>, Nat) -> Maybe<&1, Pair(A, Deque<a, A>)>

def Deque.pop_back source · line 132 · raw

@-a:Quant -> @-A:Kind(a) -> @d:Deque<a, A> -> Maybe<&1, Pair(A, Deque<a, A>)>

def Deque.to_list source · line 144 · raw

@-a:Quant -> @-A:Kind(a) -> @d:Deque<a, A> -> List<a, A>

the elements, front to back

def Deque.length source · line 149 · raw

@-a:Quant -> @-A:Kind(a) -> @d:Deque<a, A> -> Nat

def Deque.is_empty source · line 154 · raw

@-a:Quant -> @-A:Kind(a) -> @d:Deque<a, A> -> Bool