Data.FastVect.Common

type Append :: forall k. (Int -> k -> Type) -> Int -> Int -> Int -> k -> Typetype Append vect m n m_plus_n elem = Add m n m_plus_n => Compare m NegOne GT => Reflectable m Int => Compare n NegOne GT => vect m elem -> vect n elem -> vect m_plus_n elem

Append two Vects.

as :: Vect 300 String
as = replicate (term :: _ 300) "a"

bs :: Vect 200 String
bs = replicate (term :: _ 200) "b"

cs :: Vect 500 String
cs = append as bs

type Cons :: (Int -> Type -> Type) -> Int -> Int -> Type -> Typetype Cons vect len len_plus_1 elem = Add One len len_plus_1 => Compare len NegOne GT => elem -> vect len elem -> vect len_plus_1 elem

Attaches an element to the front of the Vect, creating a new Vect with size incremented.

type Drop :: forall k. (Int -> k -> Type) -> Int -> Int -> Int -> k -> Typetype Drop vect m n m_plus_n elem = Add m n m_plus_n => Reflectable m Int => Compare m NegOne GT => Compare n NegOne GT => Proxy m -> vect m_plus_n elem -> vect n elem

Safely drop m elements from a Vect. Will result in a compile-time error if you are trying to drop more elements than exist in the vector.

vect :: Vect 300 String
vect = replicate (term :: _ 300) "a"

newVect :: Vect 200 String
newVect = drop (term :: _ 100) vect

type Empty :: forall k1 k2. (Int -> k1 -> k2) -> k1 -> k2type Empty vect elem = vect Zero elem

Creates the empty Vect.

vect :: Vect 0 String
vect = empty

type Generate :: (Int -> Type -> Type) -> Int -> Type -> Typetype Generate vect m elem = Reflectable m Int => Compare m NegOne GT => Proxy m -> (forall i. Compare i NegOne GT => Compare i m LT => Reflectable i Int => Proxy i -> elem) -> vect m elem

type Head :: (Int -> Type -> Type) -> Int -> Type -> Typetype Head vect m elem = Compare m Zero GT => vect m elem -> elem

Safely access the head of a Vect.

vect :: Vect 300 String
vect = replicate (term :: _ 300) "a"

elem :: String
elem = head vect

type HeadM :: (Int -> Type -> Type) -> Int -> Type -> Typetype HeadM vect m elem = Compare m Zero GT => vect m elem -> Maybe elem

type Last :: (Int -> Type -> Type) -> Int -> Type -> Typetype Last vect m elem = Compare m Zero GT => Reflectable m Int => vect m elem -> elem

Safely access the last element of a Vect.

vect :: Vect 300 String
vect = replicate (term :: _ 300) "a"

elem :: String
elem = last vect

type Index :: (Int -> Type -> Type) -> Int -> Int -> Type -> Typetype Index vect m n elem = Reflectable m Int => Compare m NegOne GT => Compare n NegOne GT => Compare m n LT => Proxy m -> vect n elem -> elem

Safely access the i-th element of a Vect.

vect :: Vect 300 String
vect = replicate (term :: _ 300) "a"

elem :: String
elem = index (term :: _ 299) vect

type IndexM :: (Int -> Type -> Type) -> Int -> Int -> Type -> Typetype IndexM vect m n elem = Reflectable m Int => Compare m NegOne GT => Compare n NegOne GT => Compare m n LT => Proxy m -> vect n elem -> Maybe elem

type IndexModulo :: (Int -> Type -> Type) -> Int -> Type -> Typetype IndexModulo vect m elem = Compare m Zero GT => Reflectable m Int => Int -> vect m elem -> elem

Safely access the n-th modulo m element of a Vect.

vect :: Vect 300 String
vect = replicate (term :: _ 300) "a"

elem :: String
elem = indexModulo 5352523 vect

type IndexModuloM :: (Int -> Type -> Type) -> Int -> Type -> Typetype IndexModuloM vect m elem = Compare m Zero GT => Reflectable m Int => Int -> vect m elem -> Maybe elem

type MapWithTerm :: (Int -> Type -> Type) -> Int -> Type -> Type -> Typetype MapWithTerm vect m elem elem' = Reflectable m Int => Compare m NegOne GT => (forall i. Compare i NegOne GT => Compare i m LT => Reflectable i Int => Proxy i -> elem -> elem') -> vect m elem -> vect m elem'

type Modify :: (Int -> Type -> Type) -> Int -> Int -> Type -> Typetype Modify vect m n elem = Reflectable m Int => Compare m NegOne GT => Compare n NegOne GT => Compare m n LT => Proxy m -> (elem -> elem) -> vect n elem -> vect n elem

Safely modify element m from a Vect.

vect :: Vect 300 String
vect = replicate (term :: _ 300) "a"

newVect :: Vect 100 String
newVect = modify (term :: _ 100) (append "b") vect

type NegOne :: Inttype NegOne = -1

type One :: Inttype One = 1

type Replicate :: (Int -> Type -> Type) -> Int -> Type -> Typetype Replicate vect len elem = Compare len NegOne GT => Reflectable len Int => Proxy len -> elem -> vect len elem

Create a Vect by replicating len times the given element

vect :: Vect 300 String
vect = replicate (term :: _ 300) "a"

type Set :: (Int -> Type -> Type) -> Int -> Int -> Type -> Typetype Set vect m n elem = Reflectable m Int => Compare m NegOne GT => Compare n NegOne GT => Compare m n LT => Proxy m -> elem -> vect n elem -> vect n elem

Safely set element m from a Vect.

vect :: Vect 300 String
vect = replicate (term :: _ 300) "a"

newVect :: Vect 100 String
newVect = modify (term :: _ 100) "b" vect
`

type Singleton :: (Int -> Type -> Type) -> Type -> Typetype Singleton vect elem = elem -> vect One elem

Create a Vect of one element.

vect :: Vect 1 String
vect = singleton "a"

type Snoc :: (Int -> Type -> Type) -> Int -> Int -> Type -> Typetype Snoc vect len len_plus_1 elem = Add One len len_plus_1 => Reflectable len Int => Compare len NegOne GT => vect len elem -> elem -> vect len_plus_1 elem

Attaches an element to the end of the Vect, creating a new Vect with size incremented.

type Sparse :: forall k1 k2 k3. (k1 -> k2 -> k3) -> k1 -> k2 -> k3type Sparse vect n elem = vect n elem

Creates the sparse Vect.

vect :: Vect 40 String
vect = sparse

type SplitAt :: forall k. (Int -> k -> Type) -> Int -> Int -> Int -> k -> Typetype SplitAt vect m n m_plus_n elem = Add m n m_plus_n => Reflectable m Int => Compare m NegOne GT => Compare n NegOne GT => Proxy m -> vect m_plus_n elem -> { after :: vect n elem, before :: vect m elem }

Split the Vect into two sub vectors before and after, where before contains up to m elements.

vect :: Vect 10 String
vect = replicate (term :: _ 10) "a"

split ::
  { after :: Vect 7 String
  , before :: Vect 3 String
  }
split = splitAt (term :: _ 3) vect

type Take :: forall k. (Int -> k -> Type) -> Int -> Int -> Int -> k -> Typetype Take vect m n m_plus_n elem = Add m n m_plus_n => Reflectable m Int => Compare m NegOne GT => Compare n NegOne GT => Proxy m -> vect m_plus_n elem -> vect m elem

Safely take m elements from a Vect. Will result in a compile-time error if you are trying to take more elements than exist in the vector.

vect :: Vect 300 String
vect = replicate (term :: _ 300) "a"

newVect :: Vect 100 String
newVect = take (term :: _ 100) vect

type Zero :: Inttype Zero = 0

class IsVect :: (Type -> Type) -> Constraintclass (TraversableWithIndex Int f) <= IsVect f 

term :: forall (i :: Int). Proxy i

Create a term for the index of a vector.

toInt :: forall (len :: Int). Reflectable len Int => Proxy len -> Int

Convert a term to an Int