What4.Expr.ArrayUpdateMap

Documentation

data ArrayUpdateMap e ctx tp

Instances

TestEquality e => Eq (ArrayUpdateMap e ctx tp)

Defined in What4.Expr.ArrayUpdateMap

Methods

(==) :: ArrayUpdateMap e ctx tp -> ArrayUpdateMap e ctx tp -> Bool

(/=) :: ArrayUpdateMap e ctx tp -> ArrayUpdateMap e ctx tp -> Bool

TestEquality e => Hashable (ArrayUpdateMap e ctx tp)

Defined in What4.Expr.ArrayUpdateMap

Methods

hashWithSalt :: Int -> ArrayUpdateMap e ctx tp -> Int

hash :: ArrayUpdateMap e ctx tp -> Int

arrayUpdateAbs :: ArrayUpdateMap e ct tp -> Maybe (AbstractValue tp)

empty :: ArrayUpdateMap e ctx tp

null :: ArrayUpdateMap e ctx tp -> Bool

lookup :: Assignment IndexLit ctx -> ArrayUpdateMap e ctx tp -> Maybe (e tp)

filter :: (e tp -> Bool) -> ArrayUpdateMap e ctx tp -> ArrayUpdateMap e ctx tp

singleton :: (HashableF e, HasAbsValue e) => BaseTypeRepr tp -> Assignment IndexLit ctx -> e tp -> ArrayUpdateMap e ctx tp

insert :: (HashableF e, HasAbsValue e) => BaseTypeRepr tp -> Assignment IndexLit ctx -> e tp -> ArrayUpdateMap e ctx tp -> ArrayUpdateMap e ctx tp

delete :: Assignment IndexLit ctx -> ArrayUpdateMap e ctx tp -> ArrayUpdateMap e ctx tp

fromAscList :: (HasAbsValue e, HashableF e) => BaseTypeRepr tp -> [(Assignment IndexLit ctx, e tp)] -> ArrayUpdateMap e ctx tp

toList :: ArrayUpdateMap e ctx tp -> [(Assignment IndexLit ctx, e tp)]

toMap :: ArrayUpdateMap e ctx tp -> Map (Assignment IndexLit ctx) (e tp)

keysSet :: ArrayUpdateMap e ctx tp -> Set (Assignment IndexLit ctx)

traverseArrayUpdateMap :: Applicative m => (e tp -> m (f tp)) -> ArrayUpdateMap e ctx tp -> m (ArrayUpdateMap f ctx tp)

mergeM :: (Applicative m, HashableF g, HasAbsValue g) => BaseTypeRepr tp -> (Assignment IndexLit ctx -> e tp -> f tp -> m (g tp)) -> (Assignment IndexLit ctx -> e tp -> m (g tp)) -> (Assignment IndexLit ctx -> f tp -> m (g tp)) -> ArrayUpdateMap e ctx tp -> ArrayUpdateMap f ctx tp -> m (ArrayUpdateMap g ctx tp)