parameterized-utils-2.1.11.0: Classes and data structures for working with data-kind indexed types

Copyright | (c) Galois Inc 2022
Safe Haskell | None
Language | Haskell2010

Data.Parameterized.FinMap.Safe

Contents

- Query
- Construction
- Operations

Description

See Data.Parameterized.FinMap.

Synopsis

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

Functor (FinMap n) Source # |
Instance details Defined in Data.Parameterized.FinMap.Safe Methods fmap :: (a -> b) -> FinMap n a -> FinMap n b Source # (<$) :: a -> FinMap n b -> FinMap n a Source #
Foldable (FinMap n) Source # |

Instance details

Defined in Data.Parameterized.FinMap.Safe

Methods

fold :: Monoid m => FinMap n m -> m Source #

foldMap :: Monoid m => (a -> m) -> FinMap n a -> m Source #

foldMap' :: Monoid m => (a -> m) -> FinMap n a -> m Source #

foldr :: (a -> b -> b) -> b -> FinMap n a -> b Source #

foldr' :: (a -> b -> b) -> b -> FinMap n a -> b Source #

foldl :: (b -> a -> b) -> b -> FinMap n a -> b Source #

foldl' :: (b -> a -> b) -> b -> FinMap n a -> b Source #

foldr1 :: (a -> a -> a) -> FinMap n a -> a Source #

foldl1 :: (a -> a -> a) -> FinMap n a -> a Source #

toList :: FinMap n a -> [a] Source #

null :: FinMap n a -> Bool Source #

length :: FinMap n a -> Int Source #

elem :: Eq a => a -> FinMap n a -> Bool Source #

maximum :: Ord a => FinMap n a -> a Source #

minimum :: Ord a => FinMap n a -> a Source #

sum :: Num a => FinMap n a -> a Source #

product :: Num a => FinMap n a -> a Source #

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) Source # sequenceA :: Applicative f => FinMap n (f a) -> f (FinMap n a) Source # mapM :: Monad m => (a -> m b) -> FinMap n a -> m (FinMap n b) Source # sequence :: Monad m => FinMap n (m a) -> m (FinMap n a) Source #
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 Source #

ifoldMap' :: Monoid m => (Fin n -> a -> m) -> FinMap n a -> m Source #

ifoldr :: (Fin n -> a -> b -> b) -> b -> FinMap n a -> b Source #

ifoldl :: (Fin n -> b -> a -> b) -> b -> FinMap n a -> b Source #

ifoldr' :: (Fin n -> a -> b -> b) -> b -> FinMap n a -> b Source #

ifoldl' :: (Fin n -> b -> a -> b) -> b -> FinMap n a -> b Source #

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 Source #
KnownNat n => Monoid (FinMap n a) Source # |
Instance details Defined in Data.Parameterized.FinMap.Safe Methods mempty :: FinMap n a Source # mappend :: FinMap n a -> FinMap n a -> FinMap n a Source # mconcat :: [FinMap n a] -> FinMap n a Source #
Semigroup (FinMap n a) Source # |
Instance details Defined in Data.Parameterized.FinMap.Safe Methods (<>) :: FinMap n a -> FinMap n a -> FinMap n a Source # sconcat :: NonEmpty (FinMap n a) -> FinMap n a Source # stimes :: Integral b => b -> FinMap n a -> FinMap n a Source #
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 Source # show :: FinMap n a -> String Source # showList :: [FinMap n a] -> ShowS Source #
Eq a => Eq (FinMap n a) Source # |
Instance details Defined in Data.Parameterized.FinMap.Safe Methods (==) :: FinMap n a -> FinMap n a -> Bool Source # (/=) :: FinMap n a -> FinMap n a -> Bool Source #

# Query

null :: forall (n :: Nat) a. FinMap n a -> Bool Source #

O(1). Is the map empty?

lookup :: forall (n :: Natural) a. Fin n -> FinMap n a -> Maybe a Source #

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

size :: forall (n :: Nat) 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 :: Nat) 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 :: forall (n :: Nat) (m :: Nat) a. n <= m => NatRepr m -> FinMap n a -> FinMap m a Source #

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

Requires `m < (maxBound :: Int)`.

empty :: forall (n :: Nat) a. 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 :: forall (n :: Natural) a. Fin n -> a -> FinMap n a -> FinMap n a Source #

O(log n).

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

append :: forall (n :: Nat) a. NatRepr n -> a -> FinMap n a -> FinMap (n + 1) a Source #

O(min(n,W)).

fromVector :: forall (n :: Natural) a. Vector n (Maybe a) -> FinMap n a Source #

# Operations

delete :: forall (n :: Natural) a. Fin n -> FinMap n a -> FinMap n a Source #

O(log n).

decMax :: forall (n :: Nat) a. NatRepr n -> FinMap (n + 1) a -> FinMap n a Source #

Decrement the key/size, removing the item at key `n + 1` if present.

mapWithKey :: forall (n :: Natural) a b. (Fin n -> a -> b) -> FinMap n a -> FinMap n b Source #

unionWithKey :: forall (n :: Natural) a. (Fin n -> a -> a -> a) -> FinMap n a -> FinMap n a -> FinMap n a Source #

O(n+m).

unionWith :: forall a (n :: Nat). (a -> a -> a) -> FinMap n a -> FinMap n a -> FinMap n a Source #

O(n+m).

union :: forall (n :: Nat) a. FinMap n a -> FinMap n a -> FinMap n a Source #

O(n+m). Left-biased union, i.e. (``union` == `unionWith` `const``).