what4-1.0: Solver-agnostic symbolic values support for issuing queries

Copyright(c) Galois Inc 2015-2020
LicenseBSD3
MaintainerJoe Hendrix <jhendrix@galois.com>
Safe HaskellSafe
LanguageHaskell2010

What4.Utils.LeqMap

Description

This module defines a strict map.

It is similiar to Data.Map.Strict, but provides some additional operations including splitEntry, splitLeq, fromDistinctDescList.

Synopsis

Documentation

data LeqMap k p Source #

Instances
Functor (LeqMap k) Source # 
Instance details

Defined in What4.Utils.LeqMap

Methods

fmap :: (a -> b) -> LeqMap k a -> LeqMap k b #

(<$) :: a -> LeqMap k b -> LeqMap k a #

Foldable (LeqMap k) Source # 
Instance details

Defined in What4.Utils.LeqMap

Methods

fold :: Monoid m => LeqMap k m -> m #

foldMap :: Monoid m => (a -> m) -> LeqMap k a -> m #

foldr :: (a -> b -> b) -> b -> LeqMap k a -> b #

foldr' :: (a -> b -> b) -> b -> LeqMap k a -> b #

foldl :: (b -> a -> b) -> b -> LeqMap k a -> b #

foldl' :: (b -> a -> b) -> b -> LeqMap k a -> b #

foldr1 :: (a -> a -> a) -> LeqMap k a -> a #

foldl1 :: (a -> a -> a) -> LeqMap k a -> a #

toList :: LeqMap k a -> [a] #

null :: LeqMap k a -> Bool #

length :: LeqMap k a -> Int #

elem :: Eq a => a -> LeqMap k a -> Bool #

maximum :: Ord a => LeqMap k a -> a #

minimum :: Ord a => LeqMap k a -> a #

sum :: Num a => LeqMap k a -> a #

product :: Num a => LeqMap k a -> a #

Traversable (LeqMap k) Source # 
Instance details

Defined in What4.Utils.LeqMap

Methods

traverse :: Applicative f => (a -> f b) -> LeqMap k a -> f (LeqMap k b) #

sequenceA :: Applicative f => LeqMap k (f a) -> f (LeqMap k a) #

mapM :: Monad m => (a -> m b) -> LeqMap k a -> m (LeqMap k b) #

sequence :: Monad m => LeqMap k (m a) -> m (LeqMap k a) #

(Ord k, Eq p) => Eq (LeqMap k p) Source # 
Instance details

Defined in What4.Utils.LeqMap

Methods

(==) :: LeqMap k p -> LeqMap k p -> Bool #

(/=) :: LeqMap k p -> LeqMap k p -> Bool #

toList :: LeqMap k p -> [(k, p)] Source #

findMin :: LeqMap k p -> (k, p) Source #

findMax :: LeqMap k p -> (k, p) Source #

null :: LeqMap k p -> Bool Source #

empty :: LeqMap k p Source #

Return the empty map

mapKeysMonotonic :: (k1 -> k2) -> LeqMap k1 p -> LeqMap k2 p Source #

union :: Ord k => LeqMap k p -> LeqMap k p -> LeqMap k p Source #

fromDistinctAscList :: [(k, p)] -> LeqMap k p Source #

fromDistinctDescList :: [(k, p)] -> LeqMap k p Source #

Create a map from a list of keys in descending order.

toDescList :: LeqMap k p -> [(k, p)] Source #

deleteFindMin :: LeqMap k p -> ((k, p), LeqMap k p) Source #

deleteFindMax :: LeqMap k p -> ((k, p), LeqMap k p) Source #

minViewWithKey :: LeqMap k p -> Maybe ((k, p), LeqMap k p) Source #

filterGt :: Ord k => k -> LeqMap k p -> LeqMap k p Source #

filterLt :: Ord k => k -> LeqMap k p -> LeqMap k p Source #

insert :: Ord k => k -> p -> LeqMap k p -> LeqMap k p Source #

lookupLE :: Ord k => k -> LeqMap k p -> Maybe (k, p) Source #

Find largest element that is less than or equal to key (if any).

lookupLT :: Ord k => k -> LeqMap k p -> Maybe (k, p) Source #

Find less than element that is less than key (if any).

lookupGE :: Ord k => k -> LeqMap k p -> Maybe (k, p) Source #

Find largest element that is at least key (if any).

lookupGT :: Ord k => k -> LeqMap k p -> Maybe (k, p) Source #

Find less than element that is less than key (if any).

keys :: LeqMap k p -> [k] Source #

mergeWithKey :: forall a b c. (a -> b -> IO c) -> (a -> IO c) -> (b -> IO c) -> LeqMap Integer a -> LeqMap Integer b -> IO (LeqMap Integer c) Source #

singleton :: k -> p -> LeqMap k p Source #

foldlWithKey' :: (a -> k -> b -> a) -> a -> LeqMap k b -> a Source #

size :: LeqMap k p -> Int Source #

splitEntry :: LeqMap k p -> Maybe (LeqMap k p, (k, p), LeqMap k p) Source #

splitLeq :: Ord k => k -> LeqMap k p -> (LeqMap k p, LeqMap k p) Source #