Copyright	(c) Galois Inc 2022
Safe Haskell	Safe-Inferred
Language	Haskell2010

Data.Parameterized.FinMap.Safe

Contents

Query
Construction
Operations

Description

See Data.Parameterized.FinMap.

Synopsis

data FinMap (n :: Nat) a
null :: FinMap n a -> Bool
lookup :: Fin n -> FinMap n a -> Maybe a
size :: forall n a. FinMap n a -> Fin (n + 1)
incMax :: forall n a. FinMap n a -> FinMap (n + 1) a
embed :: n <= m => NatRepr m -> FinMap n a -> FinMap m a
empty :: KnownNat n => FinMap n a
singleton :: a -> FinMap 1 a
insert :: Fin n -> a -> FinMap n a -> FinMap n a
buildFinMap :: forall m a. NatRepr m -> (forall n. (n + 1) <= m => NatRepr n -> FinMap n a -> FinMap (n + 1) a) -> FinMap m a
append :: NatRepr n -> a -> FinMap n a -> FinMap (n + 1) a
fromVector :: forall n a. Vector n (Maybe a) -> FinMap n a
delete :: Fin n -> FinMap n a -> FinMap n a
decMax :: NatRepr n -> FinMap (n + 1) a -> FinMap n a
mapWithKey :: (Fin n -> a -> b) -> FinMap n a -> FinMap n b
unionWithKey :: (Fin n -> a -> a -> a) -> FinMap n a -> FinMap n a -> FinMap n a
unionWith :: (a -> a -> a) -> FinMap n a -> FinMap n a -> FinMap n a
union :: FinMap n a -> FinMap n a -> FinMap n a

Documentation

data FinMap (n :: Nat) a Source #

FinMap n a is a map with Fin n keys and a values.

Instances

Instances details

Foldable (FinMap n) Source #
Instance details Defined in Data.Parameterized.FinMap.Safe Methods fold :: Monoid m => FinMap n m -> m # foldMap :: Monoid m => (a -> m) -> FinMap n a -> m # foldMap' :: Monoid m => (a -> m) -> FinMap n a -> m # foldr :: (a -> b -> b) -> b -> FinMap n a -> b # foldr' :: (a -> b -> b) -> b -> FinMap n a -> b # foldl :: (b -> a -> b) -> b -> FinMap n a -> b # foldl' :: (b -> a -> b) -> b -> FinMap n a -> b # foldr1 :: (a -> a -> a) -> FinMap n a -> a # foldl1 :: (a -> a -> a) -> FinMap n a -> a # toList :: FinMap n a -> [a] # null :: FinMap n a -> Bool # length :: FinMap n a -> Int # elem :: Eq a => a -> FinMap n a -> Bool # maximum :: Ord a => FinMap n a -> a # minimum :: Ord a => FinMap n a -> a # sum :: Num a => FinMap n a -> a # product :: Num a => FinMap n a -> a #
Traversable (FinMap n) Source #
Instance details Defined in Data.Parameterized.FinMap.Safe Methods traverse :: Applicative f => (a -> f b) -> FinMap n a -> f (FinMap n b) # sequenceA :: Applicative f => FinMap n (f a) -> f (FinMap n a) # mapM :: Monad m => (a -> m b) -> FinMap n a -> m (FinMap n b) # sequence :: Monad m => FinMap n (m a) -> m (FinMap n a) #
Functor (FinMap n) Source #
Instance details Defined in Data.Parameterized.FinMap.Safe Methods fmap :: (a -> b) -> FinMap n a -> FinMap n b # (<$) :: a -> FinMap n b -> FinMap n a #
FoldableWithIndex (Fin n) (FinMap n) Source #
Instance details Defined in Data.Parameterized.FinMap.Safe Methods ifoldMap :: Monoid m => (Fin n -> a -> m) -> FinMap n a -> m # ifoldMap' :: Monoid m => (Fin n -> a -> m) -> FinMap n a -> m # ifoldr :: (Fin n -> a -> b -> b) -> b -> FinMap n a -> b # ifoldl :: (Fin n -> b -> a -> b) -> b -> FinMap n a -> b # ifoldr' :: (Fin n -> a -> b -> b) -> b -> FinMap n a -> b # ifoldl' :: (Fin n -> b -> a -> b) -> b -> FinMap n a -> b #
FunctorWithIndex (Fin n) (FinMap n) Source #
Instance details Defined in Data.Parameterized.FinMap.Safe Methods imap :: (Fin n -> a -> b) -> FinMap n a -> FinMap n b #
KnownNat n => Monoid (FinMap n a) Source #
Instance details Defined in Data.Parameterized.FinMap.Safe Methods mempty :: FinMap n a # mappend :: FinMap n a -> FinMap n a -> FinMap n a # mconcat :: [FinMap n a] -> FinMap n a #
Semigroup (FinMap n a) Source #
Instance details Defined in Data.Parameterized.FinMap.Safe Methods (<>) :: FinMap n a -> FinMap n a -> FinMap n a # sconcat :: NonEmpty (FinMap n a) -> FinMap n a # stimes :: Integral b => b -> FinMap n a -> FinMap n a #
Show a => Show (FinMap n a) Source #	Non-lawful instance, provided for testing
Instance details Defined in Data.Parameterized.FinMap.Safe Methods showsPrec :: Int -> FinMap n a -> ShowS # show :: FinMap n a -> String # showList :: [FinMap n a] -> ShowS #
Eq a => Eq (FinMap n a) Source #
Instance details Defined in Data.Parameterized.FinMap.Safe Methods (==) :: FinMap n a -> FinMap n a -> Bool # (/=) :: FinMap n a -> FinMap n a -> Bool #

Query

null :: FinMap n a -> Bool Source #

O(1). Is the map empty?

lookup :: Fin n -> FinMap n a -> Maybe a Source #

O(log n). Fetch the value at the given key in the map.

size :: forall n a. FinMap n a -> Fin (n + 1) Source #

O(nlog(n)). Number of elements in the map.

This operation is much slower than size because its implementation must provide significant evidence to the type-checker, and the easiest way to do that is fairly inefficient. If speed is a concern, use Data.Parameterized.FinMap.Unsafe.

Construction

incMax :: forall n a. FinMap n a -> FinMap (n + 1) a Source #

O(n log n). Increase maximum key/size by 1.

This does not alter the key-value pairs in the map, but rather increases the maximum number of key-value pairs that the map can hold. See Data.Parameterized.FinMap for more information.

Requires n + 1 < (maxBound :: Int).

embed :: n <= m => NatRepr m -> FinMap n a -> FinMap m a Source #

O(n log n). Increase maximum key/size.

Requires m < (maxBound :: Int).

empty :: KnownNat n => FinMap n a Source #

O(1). The empty map.

singleton :: a -> FinMap 1 a Source #

O(1). A map with one element.

insert :: Fin n -> a -> FinMap n a -> FinMap n a Source #

O(log n).

buildFinMap :: forall m a. NatRepr m -> (forall n. (n + 1) <= m => NatRepr n -> FinMap n a -> FinMap (n + 1) a) -> FinMap m a Source #