Data.Seq1.Unsized

General purpose linear two-end finite sequences.

This is implemented by finger tree.

Reexports

Definitions

data Seq1 : Type -> Type -> Type

  A linear two-end finite sequence.

Totality: total
Visibility: export
Constructor: 

MkSeq1 : Ref s (FingerTree (Elem e)) -> Seq1 s e

empty : F1 s (Seq1 s e)

  O(1). The empty sequence.

Totality: total
Visibility: export

singleton : e -> F1 s (Seq1 s e)

  O(1). A singleton sequence.

Totality: total
Visibility: export

replicate : Nat -> e -> F1 s (Seq1 s e)

  O(n). A sequence of length n with a the value of every element.

Totality: total
Visibility: export

length : Seq1 s a -> F1 s Nat

  O(1). The number of elements in the sequence.

Totality: total
Visibility: export

reverse : Seq1 s a -> F1' s

  O(n). Reverse the sequence.

Totality: total
Visibility: export

cons : e -> Seq1 s e -> F1' s

  O(1). Add an element to the left end of a sequence.

Totality: total
Visibility: export
Fixity Declarations:
infixr operator, level 5
infixr operator, level 5
infixr operator, level 5

snoc : Seq1 s e -> e -> F1' s

  O(1). Add an element to the right end of a sequence.

Totality: total
Visibility: export
Fixity Declarations:
infixl operator, level 5
infixl operator, level 5
infixl operator, level 5

viewl : Seq1 s e -> F1 s (Maybe (e, Seq1 s e))

  O(1). View from the left of the sequence.

Totality: total
Visibility: export

head : Seq1 s e -> F1 s (Maybe e)

  O(1). The first element of the sequence.

Totality: total
Visibility: export

tail : Seq1 s e -> F1' s

  O(1). The elements after the head of the sequence.
  Returns an empty sequence when the sequence is empty.

Totality: total
Visibility: export

viewr : Seq1 s e -> F1 s (Maybe (Seq1 s e, e))

  O(1). View from the right of the sequence.

Totality: total
Visibility: export

init : Seq1 s e -> F1' s

  O(1). The elements before the last element of the sequence.
  Returns an empty sequence when the sequence is empty.

Totality: total
Visibility: export

last : Seq1 s e -> F1 s (Maybe e)

  O(1). The last element of the sequence.

Totality: total
Visibility: export

fromList : List e -> F1 s (Seq1 s e)

  O(n). Turn a list into a sequence.

Totality: total
Visibility: export

toList : Seq1 s e -> F1 s (List e)

  Turn a sequence into a list. O(n)

Totality: total
Visibility: export

index : Nat -> Seq1 s e -> F1 s (Maybe e)

  O(log(min(i, n-i))). The element at the specified position.

Totality: total
Visibility: export

adjust : (e -> e) -> Nat -> Seq1 s e -> F1' s

  O(log(min(i, n-i))). Update the element at the specified position.
  If the position is out of range, the original sequence is returned.

Totality: total
Visibility: export

update : Nat -> e -> Seq1 s e -> F1' s

  O(log(min(i, n-i))). Replace the element at the specified position.
  If the position is out of range, the original sequence is returned.

Totality: total
Visibility: export

show' : Show e => Seq1 s e -> F1 s String

  Dump the internal structure of the finger tree.

Totality: total
Visibility: export