Safe Haskell	None
Language	Haskell2010

Vector.Bit

Contents

Primitives
Ranges
Freeze
Copy
Composite
Index
Equality
Custom

Synopsis

data Vector (a :: Nat) (b :: TYPE R) where
- Vector :: forall (a :: Nat) (b :: TYPE R). Vector# a b -> Vector a b
data Vector# (a :: Nat) (b :: TYPE R) :: UnliftedType
data MutableVector a (b :: Nat) (c :: TYPE R) where
- MutableVector :: forall a (b :: Nat) (c :: TYPE R). MutableVector# a b c -> MutableVector a b c
data MutableVector# a (b :: Nat) (c :: TYPE R) :: UnliftedType
data Bounded (a :: Nat) (b :: TYPE R) where
- Bounded :: forall (b :: TYPE R) (a :: Nat) (m :: Nat). Nat# m -> (m <=# a) -> Vector# m b -> Bounded a b
write# :: forall s (n :: Nat) (a :: TYPE R). MutableVector# s n a -> Fin# n -> a -> State# s -> State# s
write :: forall s (n :: Nat) (a :: TYPE R). MutableVector s n a -> Fin# n -> a -> ST s ()
read :: forall s (n :: Nat). MutableVector s n Bool# -> Fin# n -> ST s Bool
read# :: forall s (n :: Nat) (a :: TYPE R). MutableVector# s n a -> Fin# n -> State# s -> (# State# s, a #)
index# :: forall (n :: Nat) (a :: TYPE R). Vector# n a -> Fin# n -> a
index :: forall (n :: Nat) (a :: TYPE R). Vector n a -> Fin# n -> a
unlift :: forall (n :: Nat) (a :: TYPE R). Vector n a -> Vector# n a
substitute :: forall (m :: Nat) (n :: Nat) (a :: TYPE R). (m :=:# n) -> Vector m a -> Vector n a
substitute# :: forall (m :: Nat) (n :: Nat) (a :: TYPE R). (m :=:# n) -> Vector# m a -> Vector# n a
initialized :: forall s (n :: Nat) (a :: TYPE R). Nat# n -> a -> ST s (MutableVector s n a)
initialized# :: forall s (n :: Nat) (a :: TYPE R). Nat# n -> a -> State# s -> (# State# s, MutableVector# s n a #)
unsafeCoerceLength :: forall (n :: Nat) (m :: Nat) (a :: TYPE R). Nat n -> Vector m a -> Vector n a
expose :: forall (n :: Nat) (a :: TYPE R). Vector n a -> A# a
expose# :: forall (n :: Nat) (a :: TYPE R). Vector# n a -> A# a
set :: forall s (n :: Nat) (a :: TYPE R). MutableVector s n a -> Nat# n -> a -> ST s ()
setSlice :: forall (i :: Natural) (n :: Natural) (m :: Nat) s (a :: TYPE R). ((i + n) <=# m) -> MutableVector s n a -> Nat# i -> Nat# m -> a -> ST s ()
unsafeShrinkFreeze :: forall s (n0 :: Nat) (n1 :: Nat) (a :: TYPE R). (n1 <=# n0) -> MutableVector s n0 a -> Nat# n1 -> ST s (Vector n1 a)
unsafeFreeze :: forall s (n :: Nat) (a :: TYPE R). MutableVector s n a -> ST s (Vector n a)
freeze :: forall (n :: Nat) s (a :: TYPE R). Nat# n -> MutableVector s n a -> ST s (Vector n a)
freezeSlice :: forall (i :: Natural) (n :: Natural) (m :: Nat) s (a :: TYPE R). ((i + n) <=# m) -> MutableVector s m a -> Nat# i -> Nat# n -> ST s (Vector n a)
freeze# :: forall (n :: Nat) s (a :: TYPE R). Nat# n -> MutableVector# s n a -> State# s -> (# State# s, Vector# n a #)
freezeSlice# :: forall (i :: Natural) (n :: Natural) (m :: Nat) s (a :: TYPE R). ((i + n) <=# m) -> MutableVector# s m a -> Nat# i -> Nat# n -> State# s -> (# State# s, Vector# n a #)
thaw :: forall (n :: Nat) (a :: TYPE R) s. Nat# n -> Vector n a -> ST s (MutableVector s n a)
map :: forall (a :: TYPE R) (n :: Nat). (a -> a) -> Vector n a -> Nat# n -> Vector n a
traverse_ :: forall (n :: Nat) m (a :: TYPE R) b. Monad m => (a -> m b) -> Nat# n -> Vector n a -> m ()
itraverse_ :: forall (n :: Nat) m (a :: TYPE R) b. Monad m => (Fin# n -> a -> m b) -> Nat# n -> Vector n a -> m ()
itraverse_# :: forall (n :: Nat) m (a :: TYPE R) b. Monad m => (Fin# n -> a -> m b) -> Nat# n -> Vector# n a -> m ()
traverseST# :: forall (n :: Nat) s (a :: TYPE R) (b :: TYPE R). (a -> State# s -> (# State# s, b #)) -> Nat# n -> Vector# n a -> State# s -> (# State# s, Vector# n b #)
ifoldl' :: forall (n :: Nat) (a :: TYPE R) b. (b -> Fin# n -> a -> b) -> b -> Nat# n -> Vector n a -> b
ifoldlSlice' :: forall (i :: Nat) (m :: Nat) (n :: Nat) (a :: TYPE R) b. ((i + n) <= m) -> (b -> Fin# (i + n) -> a -> b) -> b -> Vector m a -> Nat# i -> Nat# n -> b
construct1 :: forall (a :: TYPE R). a -> Vector 1 a
construct2 :: forall (a :: TYPE R). a -> a -> Vector 2 a
construct3 :: forall (a :: TYPE R). a -> a -> a -> Vector 3 a
construct4 :: forall (a :: TYPE R). a -> a -> a -> a -> Vector 4 a
construct5 :: forall (a :: TYPE R). a -> a -> a -> a -> a -> Vector 5 a
replicate :: forall (n :: Nat) (a :: TYPE R). Nat# n -> a -> Vector n a
empty :: forall (a :: TYPE R). Vector 0 a
empty_ :: forall (a :: TYPE R). Vector_ a
empty# :: forall (a :: TYPE R). (# #) -> Vector# 0 a
append :: forall (n :: Nat) (m :: Nat) (a :: TYPE R). Nat# n -> Nat# m -> Vector n a -> Vector m a -> Vector (n + m) a
clone :: forall (n :: Nat) (a :: TYPE R). Nat# n -> Vector n a -> Vector n a
cloneSlice :: forall (i :: Natural) (n :: Natural) (m :: Nat) (a :: TYPE R). ((i + n) <=# m) -> Vector m a -> Nat# i -> Nat# n -> Vector n a
index0 :: forall (n :: Natural) (a :: TYPE R). CmpNat 0 n ~ 'LT => Vector n a -> a
index1 :: forall (n :: Natural) (a :: TYPE R). CmpNat 1 n ~ 'LT => Vector n a -> a
index2 :: forall (n :: Natural) (a :: TYPE R). CmpNat 2 n ~ 'LT => Vector n a -> a
index3 :: forall (n :: Natural) (a :: TYPE R). CmpNat 3 n ~ 'LT => Vector n a -> a
equals :: forall (n :: Nat) (a :: TYPE R). Nat# n -> Vector n a -> Vector n a -> Bool
zipAnd :: forall (n :: Nat). Nat# n -> Vector n Bool# -> Vector n Bool# -> Vector n Bool#
zipOr :: forall (n :: Nat). Nat# n -> Vector n Bool# -> Vector n Bool# -> Vector n Bool#
allEqTrue :: forall (n :: Nat). Nat# n -> Vector n Bool# -> Bool

Documentation

data Vector (a :: Nat) (b :: TYPE R) where #

Constructors

Vector :: forall (a :: Nat) (b :: TYPE R). Vector# a b -> Vector a b

data Vector# (a :: Nat) (b :: TYPE R) :: UnliftedType #

data MutableVector a (b :: Nat) (c :: TYPE R) where #

Constructors

MutableVector :: forall a (b :: Nat) (c :: TYPE R). MutableVector# a b c -> MutableVector a b c

data MutableVector# a (b :: Nat) (c :: TYPE R) :: UnliftedType #

data Bounded (a :: Nat) (b :: TYPE R) where #

Constructors

Bounded :: forall (b :: TYPE R) (a :: Nat) (m :: Nat). Nat# m -> (m <=# a) -> Vector# m b -> Bounded a b

Primitives

write# :: forall s (n :: Nat) (a :: TYPE R). MutableVector# s n a -> Fin# n -> a -> State# s -> State# s #

write :: forall s (n :: Nat) (a :: TYPE R). MutableVector s n a -> Fin# n -> a -> ST s () #

read :: forall s (n :: Nat). MutableVector s n Bool# -> Fin# n -> ST s Bool Source #

read# :: forall s (n :: Nat) (a :: TYPE R). MutableVector# s n a -> Fin# n -> State# s -> (# State# s, a #) #

index# :: forall (n :: Nat) (a :: TYPE R). Vector# n a -> Fin# n -> a #

index :: forall (n :: Nat) (a :: TYPE R). Vector n a -> Fin# n -> a #

unlift :: forall (n :: Nat) (a :: TYPE R). Vector n a -> Vector# n a #

substitute :: forall (m :: Nat) (n :: Nat) (a :: TYPE R). (m :=:# n) -> Vector m a -> Vector n a #

substitute# :: forall (m :: Nat) (n :: Nat) (a :: TYPE R). (m :=:# n) -> Vector# m a -> Vector# n a #

initialized :: forall s (n :: Nat) (a :: TYPE R). Nat# n -> a -> ST s (MutableVector s n a) #

initialized# :: forall s (n :: Nat) (a :: TYPE R). Nat# n -> a -> State# s -> (# State# s, MutableVector# s n a #) #

unsafeCoerceLength :: forall (n :: Nat) (m :: Nat) (a :: TYPE R). Nat n -> Vector m a -> Vector n a #

expose :: forall (n :: Nat) (a :: TYPE R). Vector n a -> A# a #

expose# :: forall (n :: Nat) (a :: TYPE R). Vector# n a -> A# a #

Ranges

set :: forall s (n :: Nat) (a :: TYPE R). MutableVector s n a -> Nat# n -> a -> ST s () #

setSlice :: forall (i :: Natural) (n :: Natural) (m :: Nat) s (a :: TYPE R). ((i + n) <=# m) -> MutableVector s n a -> Nat# i -> Nat# m -> a -> ST s () #

Freeze

unsafeShrinkFreeze :: forall s (n0 :: Nat) (n1 :: Nat) (a :: TYPE R). (n1 <=# n0) -> MutableVector s n0 a -> Nat# n1 -> ST s (Vector n1 a) #

unsafeFreeze :: forall s (n :: Nat) (a :: TYPE R). MutableVector s n a -> ST s (Vector n a) #

freeze :: forall (n :: Nat) s (a :: TYPE R). Nat# n -> MutableVector s n a -> ST s (Vector n a) #

freezeSlice :: forall (i :: Natural) (n :: Natural) (m :: Nat) s (a :: TYPE R). ((i + n) <=# m) -> MutableVector s m a -> Nat# i -> Nat# n -> ST s (Vector n a) #

freeze# :: forall (n :: Nat) s (a :: TYPE R). Nat# n -> MutableVector# s n a -> State# s -> (# State# s, Vector# n a #) #

freezeSlice# :: forall (i :: Natural) (n :: Natural) (m :: Nat) s (a :: TYPE R). ((i + n) <=# m) -> MutableVector# s m a -> Nat# i -> Nat# n -> State# s -> (# State# s, Vector# n a #) #

Copy

thaw :: forall (n :: Nat) (a :: TYPE R) s. Nat# n -> Vector n a -> ST s (MutableVector s n a) #

Composite

map :: forall (a :: TYPE R) (n :: Nat). (a -> a) -> Vector n a -> Nat# n -> Vector n a #

traverse_ :: forall (n :: Nat) m (a :: TYPE R) b. Monad m => (a -> m b) -> Nat# n -> Vector n a -> m () #

itraverse_ :: forall (n :: Nat) m (a :: TYPE R) b. Monad m => (Fin# n -> a -> m b) -> Nat# n -> Vector n a -> m () #

itraverse_# :: forall (n :: Nat) m (a :: TYPE R) b. Monad m => (Fin# n -> a -> m b) -> Nat# n -> Vector# n a -> m () #

traverseST# :: forall (n :: Nat) s (a :: TYPE R) (b :: TYPE R). (a -> State# s -> (# State# s, b #)) -> Nat# n -> Vector# n a -> State# s -> (# State# s, Vector# n b #) #

ifoldl' :: forall (n :: Nat) (a :: TYPE R) b. (b -> Fin# n -> a -> b) -> b -> Nat# n -> Vector n a -> b #

ifoldlSlice' :: forall (i :: Nat) (m :: Nat) (n :: Nat) (a :: TYPE R) b. ((i + n) <= m) -> (b -> Fin# (i + n) -> a -> b) -> b -> Vector m a -> Nat# i -> Nat# n -> b #

construct1 :: forall (a :: TYPE R). a -> Vector 1 a #

construct2 :: forall (a :: TYPE R). a -> a -> Vector 2 a #

construct3 :: forall (a :: TYPE R). a -> a -> a -> Vector 3 a #

construct4 :: forall (a :: TYPE R). a -> a -> a -> a -> Vector 4 a #

construct5 :: forall (a :: TYPE R). a -> a -> a -> a -> a -> Vector 5 a #

replicate :: forall (n :: Nat) (a :: TYPE R). Nat# n -> a -> Vector n a #

empty :: forall (a :: TYPE R). Vector 0 a #

empty_ :: forall (a :: TYPE R). Vector_ a #

empty# :: forall (a :: TYPE R). (# #) -> Vector# 0 a #

append :: forall (n :: Nat) (m :: Nat) (a :: TYPE R). Nat# n -> Nat# m -> Vector n a -> Vector m a -> Vector (n + m) a #

clone :: forall (n :: Nat) (a :: TYPE R). Nat# n -> Vector n a -> Vector n a #

cloneSlice :: forall (i :: Natural) (n :: Natural) (m :: Nat) (a :: TYPE R). ((i + n) <=# m) -> Vector m a -> Nat# i -> Nat# n -> Vector n a #

Index

index0 :: forall (n :: Natural) (a :: TYPE R). CmpNat 0 n ~ 'LT => Vector n a -> a #

index1 :: forall (n :: Natural) (a :: TYPE R). CmpNat 1 n ~ 'LT => Vector n a -> a #

index2 :: forall (n :: Natural) (a :: TYPE R). CmpNat 2 n ~ 'LT => Vector n a -> a #

index3 :: forall (n :: Natural) (a :: TYPE R). CmpNat 3 n ~ 'LT => Vector n a -> a #

Equality

equals :: forall (n :: Nat) (a :: TYPE R). Nat# n -> Vector n a -> Vector n a -> Bool #

Custom

zipAnd :: forall (n :: Nat). Nat# n -> Vector n Bool# -> Vector n Bool# -> Vector n Bool# Source #

zipOr :: forall (n :: Nat). Nat# n -> Vector n Bool# -> Vector n Bool# -> Vector n Bool# Source #

allEqTrue :: forall (n :: Nat). Nat# n -> Vector n Bool# -> Bool Source #