Data.Seq.Sized

(source)

General purpose two-end finite sequences,
with length in its type.

This is implemented by finger tree.

Reexports

import public Data.Fin
import public Data.Nat
import public Data.Vect
import public Data.Zippable

Definitions

data Seq : Nat -> Type -> Type

  A two-end finite sequence, with length in its type.

Totality: total
Visibility: export
Constructor:

MkSeq : FingerTree (Elem e) -> Seq n e

Hints:

Applicative (Seq n)
Eq a => Eq (Seq n a)
Foldable (Seq n)
Functor (Seq n)
Ord a => Ord (Seq n a)
Show a => Show (Seq n a)
Sized (Seq n a)
Traversable (Seq n)
Zippable (Seq n)

empty : Seq 0 e

  The empty sequence. O(1)

Totality: total
Visibility: export

singleton : e -> Seq 1 e

  A singleton sequence. O(1)

Totality: total
Visibility: export

replicate : (n : Nat) -> e -> Seq n e

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

Totality: total
Visibility: export

length : Seq n a -> Nat

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

Totality: total
Visibility: export

reverse : Seq n a -> Seq n a

  Reverse the sequence. O(n)

Totality: total
Visibility: export

cons : e -> Seq n e -> Seq (S n) e

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

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

snoc : Seq n e -> e -> Seq (S n) e

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

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

(++) : Seq m e -> Seq n e -> Seq (m + n) e

  Concatenate two sequences. O(log(min(m, n)))

Totality: total
Visibility: export
Fixity Declaration: infixr operator, level 7

viewl : Seq (S n) a -> (a, Seq n a)

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

Totality: total
Visibility: export

head : Seq (S n) a -> a

  The first element of the sequence. O(1)

Totality: total
Visibility: export

tail : Seq (S n) a -> Seq n a

  The elements after the head of the sequence. O(1)

Totality: total
Visibility: export

viewr : Seq (S n) a -> (Seq n a, a)

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

Totality: total
Visibility: export

init : Seq (S n) a -> Seq n a

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

Totality: total
Visibility: export

last : Seq (S n) a -> a

  The last element of the sequence. O(1)

Totality: total
Visibility: export

fromVect : Vect n a -> Seq n a

  Turn a vector into a sequence. O(n)

Totality: total
Visibility: export

fromList : (xs : List a) -> Seq (length xs) a

  Turn a list into a sequence. O(n)

Totality: total
Visibility: export

toVect : Seq n a -> Vect n a

  Turn a sequence into a vector. O(n)

Totality: total
Visibility: export

index : (i : Nat) -> Seq n a -> LT i n => a

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

Totality: total
Visibility: export

index' : Seq n a -> Fin n -> a

  The element at the specified position.
  Use Fin n to index instead. O(log(min(i, n-i)))

Totality: total
Visibility: export

adjust : (a -> a) -> (i : Nat) -> Seq n a -> LT i n => Seq n a

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

Totality: total
Visibility: export

update : (i : Nat) -> a -> Seq n a -> LT i n => Seq n a

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

Totality: total
Visibility: export

splitAt : (i : Nat) -> Seq (i + j) a -> (Seq i a, Seq j a)

  Split a sequence at a given position. O(log(min(i, n-i)))

Totality: total
Visibility: export

take : (i : Nat) -> Seq (i + j) a -> Seq i a

  The first i elements of a sequence. O(log(min(i, n-i)))

Totality: total
Visibility: export

drop : (i : Nat) -> Seq (i + j) a -> Seq j a

  Elements of a sequence after the first i. O(log(min(i, n-i)))

Totality: total
Visibility: export

show' : Show a => Seq n a -> String

  Dump the internal structure of the finger tree.

Totality: total
Visibility: export