hasmtlib-2.5.1: A monad for interfacing with external SMT solvers
Safe HaskellSafe-Inferred
LanguageGHC2021

Language.Hasmtlib.Type.ArrayMap

Synopsis

Documentation

class ArrayMap f k v where Source #

Class that allows access to a map-like array where any value is either the default value or an overwritten values. Every index has a value by default. Values at indices can be overwritten manually.

Based on McCarthy`s basic array theory.

Therefore the following axioms must hold:

  1. forall A i x: arrSelect (store A i x) == x
  2. forall A i j x: i /= j ==> (arrSelect (arrStore A i x) j === arrSelect A j)

Methods

asConst' :: Proxy f -> Proxy k -> v -> f k v Source #

viewConst :: f k v -> v Source #

arrSelect :: f k v -> k -> v Source #

arrStore :: f k v -> k -> v -> f k v Source #

Instances

Instances details
Ord k => ArrayMap ConstArray k v Source # 
Instance details

Defined in Language.Hasmtlib.Type.ArrayMap

Methods

asConst' :: Proxy ConstArray -> Proxy k -> v -> ConstArray k v Source #

viewConst :: ConstArray k v -> v Source #

arrSelect :: ConstArray k v -> k -> v Source #

arrStore :: ConstArray k v -> k -> v -> ConstArray k v Source #

asConst :: forall f k v. ArrayMap f k v => v -> f k v Source #

Wrapper for asConst' which hides the Proxy

data ConstArray k v Source #

A map-like array with a default constant value and partially overwritten values.

Constructors

ConstArray 

Fields

Instances

Instances details
Ord k => ArrayMap ConstArray k v Source # 
Instance details

Defined in Language.Hasmtlib.Type.ArrayMap

Methods

asConst' :: Proxy ConstArray -> Proxy k -> v -> ConstArray k v Source #

viewConst :: ConstArray k v -> v Source #

arrSelect :: ConstArray k v -> k -> v Source #

arrStore :: ConstArray k v -> k -> v -> ConstArray k v Source #

Foldable (ConstArray k) Source # 
Instance details

Defined in Language.Hasmtlib.Type.ArrayMap

Methods

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

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

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

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

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

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

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

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

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

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

null :: ConstArray k a -> Bool #

length :: ConstArray k a -> Int #

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

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

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

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

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

Traversable (ConstArray k) Source # 
Instance details

Defined in Language.Hasmtlib.Type.ArrayMap

Methods

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

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

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

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

Functor (ConstArray k) Source # 
Instance details

Defined in Language.Hasmtlib.Type.ArrayMap

Methods

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

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

(Show v, Show k) => Show (ConstArray k v) Source # 
Instance details

Defined in Language.Hasmtlib.Type.ArrayMap

Methods

showsPrec :: Int -> ConstArray k v -> ShowS #

show :: ConstArray k v -> String #

showList :: [ConstArray k v] -> ShowS #

(Eq v, Eq k) => Eq (ConstArray k v) Source # 
Instance details

Defined in Language.Hasmtlib.Type.ArrayMap

Methods

(==) :: ConstArray k v -> ConstArray k v -> Bool #

(/=) :: ConstArray k v -> ConstArray k v -> Bool #

(Ord v, Ord k) => Ord (ConstArray k v) Source # 
Instance details

Defined in Language.Hasmtlib.Type.ArrayMap

Methods

compare :: ConstArray k v -> ConstArray k v -> Ordering #

(<) :: ConstArray k v -> ConstArray k v -> Bool #

(<=) :: ConstArray k v -> ConstArray k v -> Bool #

(>) :: ConstArray k v -> ConstArray k v -> Bool #

(>=) :: ConstArray k v -> ConstArray k v -> Bool #

max :: ConstArray k v -> ConstArray k v -> ConstArray k v #

min :: ConstArray k v -> ConstArray k v -> ConstArray k v #

stored :: forall k v k. Lens (ConstArray k v) (ConstArray k v) (Map k v) (Map k v) Source #

arrConst :: forall k v. Lens' (ConstArray k v) v Source #