| Safe Haskell | Safe-Inferred |
|---|---|
| Language | Haskell2010 |
Lang.Crucible.Simulator.SymSequence
Contents
Synopsis
- data SymSequence sym a where
- SymSequenceNil :: SymSequence sym a
- SymSequenceCons :: !(Nonce GlobalNonceGenerator a) -> a -> !(SymSequence sym a) -> SymSequence sym a
- SymSequenceAppend :: !(Nonce GlobalNonceGenerator a) -> !(SymSequence sym a) -> !(SymSequence sym a) -> SymSequence sym a
- SymSequenceMerge :: !(Nonce GlobalNonceGenerator a) -> !(Pred sym) -> !(SymSequence sym a) -> !(SymSequence sym a) -> SymSequence sym a
- nilSymSequence :: sym -> IO (SymSequence sym a)
- consSymSequence :: sym -> a -> SymSequence sym a -> IO (SymSequence sym a)
- appendSymSequence :: sym -> SymSequence sym a -> SymSequence sym a -> IO (SymSequence sym a)
- muxSymSequence :: sym -> Pred sym -> SymSequence sym a -> SymSequence sym a -> IO (SymSequence sym a)
- isNilSymSequence :: forall sym a. IsExprBuilder sym => sym -> SymSequence sym a -> IO (Pred sym)
- lengthSymSequence :: forall sym a. IsExprBuilder sym => sym -> SymSequence sym a -> IO (SymNat sym)
- headSymSequence :: forall sym a. IsExprBuilder sym => sym -> (Pred sym -> a -> a -> IO a) -> SymSequence sym a -> IO (PartExpr (Pred sym) a)
- tailSymSequence :: forall sym a. IsExprBuilder sym => sym -> SymSequence sym a -> IO (PartExpr (Pred sym) (SymSequence sym a))
- unconsSymSequence :: forall sym a. IsExprBuilder sym => sym -> (Pred sym -> a -> a -> IO a) -> SymSequence sym a -> IO (PartExpr (Pred sym) (a, SymSequence sym a))
- traverseSymSequence :: forall m sym a b. MonadIO m => sym -> (a -> m b) -> SymSequence sym a -> m (SymSequence sym b)
- concreteizeSymSequence :: (Pred sym -> IO Bool) -> (a -> IO b) -> SymSequence sym a -> IO [b]
- prettySymSequence :: IsExpr (SymExpr sym) => (a -> Doc ann) -> SymSequence sym a -> Doc ann
- newSeqCache :: IO (SeqCache f)
- evalWithCache :: MonadIO m => SeqCache f -> ((SymSequence sym a -> m (f a)) -> SymSequence sym a -> m (f a)) -> SymSequence sym a -> m (f a)
- evalWithFreshCache :: MonadIO m => ((SymSequence sym a -> m (f a)) -> SymSequence sym a -> m (f a)) -> SymSequence sym a -> m (f a)
Documentation
data SymSequence sym a where Source #
A symbolic sequence of values supporting efficent merge operations. Semantically, these are essentially cons-lists, and designed to support access from the front only. Nodes carry nonce values that allow DAG-based traversal, which efficently supports the common case where merged nodes share a common sublist.
Constructors
| SymSequenceNil :: SymSequence sym a | |
| SymSequenceCons :: !(Nonce GlobalNonceGenerator a) -> a -> !(SymSequence sym a) -> SymSequence sym a | |
| SymSequenceAppend :: !(Nonce GlobalNonceGenerator a) -> !(SymSequence sym a) -> !(SymSequence sym a) -> SymSequence sym a | |
| SymSequenceMerge :: !(Nonce GlobalNonceGenerator a) -> !(Pred sym) -> !(SymSequence sym a) -> !(SymSequence sym a) -> SymSequence sym a |
Instances
| Eq (SymSequence sym a) Source # | |
Defined in Lang.Crucible.Simulator.SymSequence Methods (==) :: SymSequence sym a -> SymSequence sym a -> Bool # (/=) :: SymSequence sym a -> SymSequence sym a -> Bool # | |
| (IsExpr (SymExpr sym), Pretty a) => Pretty (SymSequence sym a) Source # | |
Defined in Lang.Crucible.Simulator.SymSequence | |
nilSymSequence :: sym -> IO (SymSequence sym a) Source #
Generate an empty sequence value
consSymSequence :: sym -> a -> SymSequence sym a -> IO (SymSequence sym a) Source #
Cons a new value onto the front of a sequence
Arguments
| :: sym | |
| -> SymSequence sym a | front sequence |
| -> SymSequence sym a | back sequence |
| -> IO (SymSequence sym a) |
Append two sequences
muxSymSequence :: sym -> Pred sym -> SymSequence sym a -> SymSequence sym a -> IO (SymSequence sym a) Source #
Compute an ifthenelse on symbolic sequences. This will simply produce an internal merge node except in the special case where the then and else branches are sytactically identical.
isNilSymSequence :: forall sym a. IsExprBuilder sym => sym -> SymSequence sym a -> IO (Pred sym) Source #
Test if a sequence is nil (is empty)
lengthSymSequence :: forall sym a. IsExprBuilder sym => sym -> SymSequence sym a -> IO (SymNat sym) Source #
Compute the length of a sequence
Arguments
| :: forall sym a. IsExprBuilder sym | |
| => sym | |
| -> (Pred sym -> a -> a -> IO a) | mux function on values |
| -> SymSequence sym a | |
| -> IO (PartExpr (Pred sym) a) |
Compute the head of a sequence, if it has one
tailSymSequence :: forall sym a. IsExprBuilder sym => sym -> SymSequence sym a -> IO (PartExpr (Pred sym) (SymSequence sym a)) Source #
Compute the tail of a sequence, if it has one
Arguments
| :: forall sym a. IsExprBuilder sym | |
| => sym | |
| -> (Pred sym -> a -> a -> IO a) | mux function on values |
| -> SymSequence sym a | |
| -> IO (PartExpr (Pred sym) (a, SymSequence sym a)) |
Compute both the head and the tail of a sequence, if it is nonempty
traverseSymSequence :: forall m sym a b. MonadIO m => sym -> (a -> m b) -> SymSequence sym a -> m (SymSequence sym b) Source #
Visit every element in the given symbolic sequence, applying the given action, and constructing a new sequence. The traversal is memoized, so any given subsequence will be visited at most once.
concreteizeSymSequence Source #
Arguments
| :: (Pred sym -> IO Bool) | evaluation for booleans |
| -> (a -> IO b) | evaluation for values |
| -> SymSequence sym a | |
| -> IO [b] |
Using the given evaluation function for booleans, and an evaluation function for values, compute a concrete sequence corresponding to the given symbolic sequence.
prettySymSequence :: IsExpr (SymExpr sym) => (a -> Doc ann) -> SymSequence sym a -> Doc ann Source #
Given a pretty printer for elements, print a symbolic sequence.
Low-level evaluation primitives
newSeqCache :: IO (SeqCache f) Source #
evalWithCache :: MonadIO m => SeqCache f -> ((SymSequence sym a -> m (f a)) -> SymSequence sym a -> m (f a)) -> SymSequence sym a -> m (f a) Source #
evalWithFreshCache :: MonadIO m => ((SymSequence sym a -> m (f a)) -> SymSequence sym a -> m (f a)) -> SymSequence sym a -> m (f a) Source #