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

Safe Haskell | Safe-Inferred
Language | Haskell2010

What4.Utils.Serialize

Synopsis

- withRounding :: forall sym tp. IsExprBuilder sym => sym -> SymBV sym 2 -> (RoundingMode -> IO (SymExpr sym tp)) -> IO (SymExpr sym tp)
- makeSymbol :: String -> SolverSymbol
- asyncLinked :: MonadUnliftIO m => m () -> m (Async ())
- withAsyncLinked :: MonadUnliftIO m => m () -> (Async () -> m a) -> m a

# Documentation

withRounding :: forall sym tp. IsExprBuilder sym => sym -> SymBV sym 2 -> (RoundingMode -> IO (SymExpr sym tp)) -> IO (SymExpr sym tp) Source #

makeSymbol :: String -> SolverSymbol Source #

Try converting any `String` into a `SolverSymbol`. If it is an invalid symbol, then error.

asyncLinked :: MonadUnliftIO m => m () -> m (Async ()) Source #

Fork an async action that is linked to the parent thread, but can be safely `cancel`d without also killing the parent thread.

Note that if your async doesn't return unit, then you probably want to `wait` for it instead, which eliminates the need for linking it. Also, if you plan to cancel the async near where you fork it, then `withAsyncLinked` is a better choice than using this function and subsequently canceling, since it ensures cancellation.

See https://github.com/simonmar/async/issues/25 for a perhaps more robust, but also harder to use version of this. The linked version is harder to use because it requires a special version of `cancel`.

withAsyncLinked :: MonadUnliftIO m => m () -> (Async () -> m a) -> m a Source #

A version of `withAsync` that safely links the child. See `asyncLinked`.