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

Copyright | (c) Galois Inc 2019-2020
License | BSD3
Maintainer | rdockins@galois.com
Safe Haskell | None
Language | Haskell2010

What4.Expr.ArrayUpdateMap

Description

# Documentation

data ArrayUpdateMap (e :: BaseType -> Type) (ctx :: Ctx BaseType) (tp :: BaseType) Source #

#### Instances

Instances details

TestEquality e => Eq (ArrayUpdateMap e ctx tp) Source # |
Instance details Defined in What4.Expr.ArrayUpdateMap Methods (==) :: ArrayUpdateMap e ctx tp -> ArrayUpdateMap e ctx tp -> Bool Source # (/=) :: ArrayUpdateMap e ctx tp -> ArrayUpdateMap e ctx tp -> Bool Source #
TestEquality e => Hashable (ArrayUpdateMap e ctx tp) Source # |
Instance details Defined in What4.Expr.ArrayUpdateMap Methods hashWithSalt :: Int -> ArrayUpdateMap e ctx tp -> Int Source # hash :: ArrayUpdateMap e ctx tp -> Int Source #

arrayUpdateAbs :: forall (e :: BaseType -> Type) (ct :: Ctx BaseType) (tp :: BaseType). ArrayUpdateMap e ct tp -> Maybe (AbstractValue tp) Source #

empty :: forall (e :: BaseType -> Type) (ctx :: Ctx BaseType) (tp :: BaseType). ArrayUpdateMap e ctx tp Source #

null :: forall (e :: BaseType -> Type) (ctx :: Ctx BaseType) (tp :: BaseType). ArrayUpdateMap e ctx tp -> Bool Source #

lookup :: forall (ctx :: Ctx BaseType) e (tp :: BaseType). Assignment IndexLit ctx -> ArrayUpdateMap e ctx tp -> Maybe (e tp) Source #

filter :: forall e (tp :: BaseType) (ctx :: Ctx BaseType). (e tp -> Bool) -> ArrayUpdateMap e ctx tp -> ArrayUpdateMap e ctx tp Source #

singleton :: forall e (tp :: BaseType) (ctx :: Ctx BaseType). (HashableF e, HasAbsValue e) => BaseTypeRepr tp -> Assignment IndexLit ctx -> e tp -> ArrayUpdateMap e ctx tp Source #

insert :: forall e (tp :: BaseType) (ctx :: Ctx BaseType). (HashableF e, HasAbsValue e) => BaseTypeRepr tp -> Assignment IndexLit ctx -> e tp -> ArrayUpdateMap e ctx tp -> ArrayUpdateMap e ctx tp Source #

delete :: forall (ctx :: Ctx BaseType) (e :: BaseType -> Type) (tp :: BaseType). Assignment IndexLit ctx -> ArrayUpdateMap e ctx tp -> ArrayUpdateMap e ctx tp Source #

fromAscList :: forall e (tp :: BaseType) (ctx :: Ctx BaseType). (HasAbsValue e, HashableF e) => BaseTypeRepr tp -> [(Assignment IndexLit ctx, e tp)] -> ArrayUpdateMap e ctx tp Source #

toList :: forall e (ctx :: Ctx BaseType) (tp :: BaseType). ArrayUpdateMap e ctx tp -> [(Assignment IndexLit ctx, e tp)] Source #

toMap :: forall e (ctx :: Ctx BaseType) (tp :: BaseType). ArrayUpdateMap e ctx tp -> Map (Assignment IndexLit ctx) (e tp) Source #

keysSet :: forall (e :: BaseType -> Type) (ctx :: Ctx BaseType) (tp :: BaseType). ArrayUpdateMap e ctx tp -> Set (Assignment IndexLit ctx) Source #

traverseArrayUpdateMap :: forall m e (tp :: BaseType) f (ctx :: Ctx BaseType). Applicative m => (e tp -> m (f tp)) -> ArrayUpdateMap e ctx tp -> m (ArrayUpdateMap f ctx tp) Source #

mergeM :: forall m g (tp :: BaseType) (ctx :: Ctx BaseType) e f. (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) Source #