Data.FVect

Fin-based vects encode not just their current size but also their
largest size. See also Data.FVect.Capacity for a view that is
useful when determining if you want to add to an FVect depending
on whether or not it is full.

Reexports

Definitions

data FVect : (capacity : Nat) -> Fin (S capacity) -> Type -> Type

  A Fin-based Vect. Can be thought of as a Vect with both a length
  and a maximum capacity. Operations like filtering can reduce the
  length without affecting maximum capacity which provides proof
  that a Vect's length has not increased over the course of a series
  of operations.

Totality: total
Visibility: public export
Constructors:

Nil : FVect capacity FZ elem

(::) : elem -> FVect capacity len elem -> FVect (S capacity) (FS len) elem

  Cons an element to the FVect, increasing its capacity.
  See (:::) for an operator that conses an element without
  increasing capacity.

Hints:

Applicative (FVect capacity l)

DecEq elem => DecEq (FVect c l elem)

Eq elem => Eq (FVect c l elem)

Foldable (FVect c l)

Functor (FVect c l)

Uninhabited (FVect 0 (FS l) e)

consWeaker : elem -> FVect (S n) (weaken len') elem -> FVect (S n) (FS len') elem

  Cons an element without increasing the capacity of the FVect. You
  must make sure the capacity and length of the FVect being consed
  onto are accessible in the context where you call this.
  
  The function signature is a bit tricky because it needs to ensure
  you are going from length of type Fin n to length of type Fin n
  but calling Fin's FS constructor increments n. To increment the
  value stored without weakening the bounds of the Fin, we go from
  (weaken (Fin (S n))) to (FS (Fin (S n))).
  
  In other words, we go from a weaker input Fin to the succesor of a
  stronger bounded Fin.

Totality: total
Visibility: public export

strengthenLT : (j : Fin (S n)) -> {auto 0 _ : LT (finToNat j) n} -> Fin n

Totality: total
Visibility: public export

consLT : {auto 0 ltPrf : LT (finToNat len) (S n)} -> elem -> FVect (S n) len elem -> FVect (S n) (FS (strengthenLT len)) elem

  Like `consWeaker`, cons an element onto an FVect without changing
  its capacity.
  
  You need only know that the existing FVect is not at capacity to
  know that an element can be consed onto it without increasing the
  capacity.

Totality: total
Visibility: public export

(:::) : {auto 0 ltPrf : LT (finToNat len) (S n)} -> elem -> FVect (S n) len elem -> FVect (S n) (FS (strengthenLT len)) elem

  Like `consWeaker`, cons an element onto an FVect without changing
  its capacity.
  
  You need only know that the existing FVect is not at capacity to
  know that an element can be consed onto it without increasing the
  capacity.

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

empty : (capacity : Nat) -> FVect capacity FZ elem

  Create an empty FVect with the given capacity.

Totality: total
Visibility: export

replicate : (l : Fin (S capacity)) -> elem -> FVect capacity l elem

  Create an FVect by replicating the given element enough to fill
  the needed length.

Totality: total
Visibility: export

addCapacity : FVect c l a -> FVect (S c) (weaken l) a

  Allow FVect to hold one more element. 
  Do not change the elements currently in the FVect.

Totality: total
Visibility: public export

addCapacityN : (n : Nat) -> FVect capacity l a -> FVect (capacity + n) (weakenN n l) a

  Allow FVect to hold n more elements. 
  Do not change the elements currently in the FVect.

Totality: total
Visibility: public export

removeCapacity : FVect (S n) (weaken len') a -> FVect n len' a

  Reduce the FVect's capacity to hold elements.

Totality: total
Visibility: public export

length : FVect capacity l a -> Nat

  Calculate the length of the FVect.

Totality: total
Visibility: export

fromVect : Vect l a -> FVect l last a

  Get the smallest FVect that can contain the given Vect.

Totality: total
Visibility: export

toVect : FVect c l elem -> Vect (finToNat l) elem

Totality: total
Visibility: export

tail : FVect c (FS l) elem -> FVect c (weaken l) elem

  All but the first element of the FVect.
  This operation does not change capacity. This means you can carry
  out this operation and retain proof that the new FVect length is
  less than or equal to the original FVect (although in this case
  the length is exactly one less than before the call to tail).

Totality: total
Visibility: public export

dropFirst : FVect (S c) (FS l) elem -> FVect c l elem

  Like tail but reduces the capacity by 1 in addition
  to dropping the first element.

Totality: total
Visibility: public export

head : FVect c (FS l) elem -> elem

Totality: total
Visibility: public export

last : FVect c (FS l) elem -> elem

Totality: total
Visibility: public export

init : FVect c (FS l) elem -> FVect c (weaken l) elem

  All but the last element of the FVect.
  This operation does not change capacity. This means you can carry
  out this operation and retain proof that the new FVect length is
  less than or equal to the original FVect (although in this case
  the length is exactly one less than before the call to tail).

Totality: total
Visibility: public export

dropLast : FVect (S c) (FS l) elem -> FVect c l elem

  Like init but reduces the capacity by 1 in addition to removing
  the last element.

Totality: total
Visibility: public export

fVectInjective : x :: xs = y :: ys -> (x = y, xs = ys)

  If two FVects are equal, their heads and tails are equal.

Totality: total
Visibility: export

addRemoveCapacityInverse : (xs : FVect c l elem) -> removeCapacity (addCapacity xs) = xs

  If you add and then remove capacity, you are left with the
  original capacity.
  In fact, you are left with exactly the original FVect.

Totality: total
Visibility: export

lengthReifies : (v : FVect c l elem) -> length v = finToNat l

  The calculated length of an FVect reifies the erased length of the
  FVect.

Totality: total
Visibility: export

catMaybes : FVect capacity len (Maybe elem) -> (len' : Fin (S capacity) ** FVect capacity len' elem)

  Remove all Nothings from the FVect.
  This operation does not change capacity. That means you can carry
  out this operation and retain proof that the new FVect length is
  less than or equal to that of the original FVect.

Totality: total
Visibility: export

mapMaybes : (elem -> Maybe elem') -> FVect capacity len elem -> (len' : Fin (S capacity) ** FVect capacity len' elem')

  Map all elements, removing any Nothings along the way.
  This operation does not change capacity. That means you can carry
  out this operation and retain proof that the new FVect length is
  less than or equal to that of the original FVect.

Totality: total
Visibility: export

filter : (elem -> Bool) -> FVect capacity len elem -> (len' : Fin (S capacity) ** FVect capacity len' elem)

  Filter down to only elements matching the predicate.
  This operation does not change capacity. That means you can carry
  out this operation and retain proof that the new FVect length is
  less than or equal to that of the original FVect.

Totality: total
Visibility: export