Safe Haskell	None
Language	Haskell2010

Vector.Int

Contents

Primitives
Ranges
Freeze
Copy
Composite
Ordered
Index
Unsafe
Hide Length
Recover Length

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
data Vector_ (a :: TYPE R) where
- Vector_ :: forall (a :: TYPE R) (n :: Nat). Nat# n -> Vector# n a -> Vector_ a
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) (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
initialized :: forall s (n :: Nat) (a :: TYPE R). Nat# n -> a -> ST s (MutableVector s n a)
unsafeCoerceLength :: forall (n :: Nat) (m :: Nat) (a :: TYPE R). Nat n -> Vector m a -> Vector n 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)
thaw :: forall (n :: Nat) (a :: TYPE R) s. Nat# n -> Vector n a -> ST s (MutableVector s n a)
tail :: forall (n :: Nat) (a :: TYPE R). Nat# n -> Vector (n + 1) a -> Vector n a
cons :: forall (n :: Nat) (a :: TYPE R). Nat# n -> Vector n a -> a -> Vector (n + 1) a
snoc :: forall (n :: Nat) (a :: TYPE R). Nat# n -> Vector n a -> a -> Vector (n + 1) a
replaceAt :: forall (n :: Nat) (a :: TYPE R). Nat# n -> Vector n a -> Fin# n -> a -> Vector n a
findIndex :: forall (n :: Nat) (a :: TYPE R). (a -> Bool) -> Nat# n -> Vector n a -> MaybeFin# n
map :: forall (a :: TYPE R) (n :: Nat). (a -> a) -> Vector n a -> Nat# n -> Vector n a
all :: forall (a :: TYPE R) (n :: Nat). (a -> Bool) -> Nat# n -> Vector n a -> Bool
any :: forall (a :: TYPE R) (n :: Nat). (a -> Bool) -> Nat# n -> Vector n a -> Bool
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 ()
foldlM :: forall (n :: Nat) m (a :: TYPE R) b. Monad m => (b -> a -> m b) -> b -> Nat# n -> Vector n a -> m b
foldr :: forall (n :: Nat) (a :: TYPE R) b. (a -> b -> b) -> b -> Nat# n -> Vector n a -> 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
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
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
construct6 :: forall (a :: TYPE R). a -> a -> a -> a -> a -> a -> Vector 6 a
construct7 :: forall (a :: TYPE R). a -> a -> a -> a -> a -> a -> a -> Vector 7 a
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
construct7# :: forall (a :: TYPE R). a -> a -> a -> a -> a -> a -> a -> Vector# 7 a
construct1_ :: forall (a :: TYPE R). a -> Vector_ a
construct2_ :: forall (a :: TYPE R). a -> a -> Vector_ a
construct3_ :: forall (a :: TYPE R). a -> a -> a -> Vector_ a
construct4_ :: forall (a :: TYPE R). a -> a -> a -> a -> Vector_ a
construct7_ :: forall (a :: TYPE R). a -> a -> a -> a -> a -> a -> a -> Vector_ 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
unique :: forall (n :: Nat) (a :: TYPE R). Nat# n -> Vector n a -> Bounded n a
equals :: forall (n :: Nat) (a :: TYPE R). Nat# n -> Vector n a -> Vector n a -> Bool
elem :: forall (n :: Nat) (a :: TYPE R). Nat# n -> a -> Vector n a -> Bool
findIndexEq :: forall (n :: Nat) (a :: TYPE R). Nat# n -> a -> Vector n a -> MaybeFin# n
maximum :: forall (n :: Nat) (a :: TYPE R). Nat# n -> (0 <# n) -> Vector n a -> a
maximumSlice :: forall (i :: Nat) (m :: Nat) (n :: Nat) (a :: TYPE R). ((i + n) <=# m) -> (0 <# n) -> Vector m a -> Nat# i -> Nat# n -> a
maximumSliceInitial :: forall (i :: Nat) (m :: Nat) (n :: Nat) (a :: TYPE R). ((i + n) <=# m) -> a -> Vector m a -> Nat# i -> Nat# n -> a
bubbleSort :: forall (n :: Nat) (a :: TYPE R). Nat# n -> Vector n a -> Vector n a
bubbleSortSlice :: forall (i :: Natural) (n :: Natural) (m :: Nat) (a :: TYPE R). ((i + n) <=# m) -> Vector m a -> Nat# i -> Nat# n -> Vector n a
bubbleSortSliceInPlace :: forall (i :: Natural) (n :: Natural) (m :: Nat) (a :: TYPE R) s. ((i + n) <=# m) -> MutableVector s m a -> Nat# i -> Nat# n -> ST s ()
mapEq :: forall (n :: Nat) (a :: TYPE R). Nat# n -> a -> Vector n a -> Vector n Bool#
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
unsafeCoerceVector :: forall (a :: TYPE R) (b :: TYPE R) (n :: Nat). Vector n a -> Vector n b
vector_ :: forall (n :: Nat) (a :: TYPE R). Nat# n -> Vector n a -> Vector_ a
length :: forall (n :: Nat) (a :: TYPE R). Vector n a -> Nat# n

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

data Vector_ (a :: TYPE R) where #

Constructors

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

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) (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 #

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

unsafeCoerceLength :: forall (n :: Nat) (m :: Nat) (a :: TYPE R). Nat n -> Vector m a -> Vector n 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) #

Copy

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

Composite

tail :: forall (n :: Nat) (a :: TYPE R). Nat# n -> Vector (n + 1) a -> Vector n a #

cons :: forall (n :: Nat) (a :: TYPE R). Nat# n -> Vector n a -> a -> Vector (n + 1) a #

snoc :: forall (n :: Nat) (a :: TYPE R). Nat# n -> Vector n a -> a -> Vector (n + 1) a #

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

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

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

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

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

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 () #

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

foldr :: forall (n :: Nat) (a :: TYPE R) b. (a -> b -> b) -> b -> Nat# n -> Vector n a -> 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 #

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 #

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 #

construct6 :: forall (a :: TYPE R). a -> a -> a -> a -> a -> a -> Vector 6 a #

construct7 :: forall (a :: TYPE R). a -> a -> a -> a -> a -> a -> a -> Vector 7 a #

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 #

construct7# :: forall (a :: TYPE R). a -> a -> a -> a -> a -> a -> a -> Vector# 7 a #

construct1_ :: forall (a :: TYPE R). a -> Vector_ a #

construct2_ :: forall (a :: TYPE R). a -> a -> Vector_ a #

construct3_ :: forall (a :: TYPE R). a -> a -> a -> Vector_ a #

construct4_ :: forall (a :: TYPE R). a -> a -> a -> a -> Vector_ a #

construct7_ :: forall (a :: TYPE R). a -> a -> a -> a -> a -> a -> a -> Vector_ 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 #

Ordered

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

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

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

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

maximum :: forall (n :: Nat) (a :: TYPE R). Nat# n -> (0 <# n) -> Vector n a -> a #

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

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

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

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

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

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

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 #

Unsafe

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

Hide Length

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

Recover Length

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