    -- |
    -- Module      :  Cryptol.Backend.Monad
    -- Copyright   :  (c) 2013-2020 Galois, Inc.
    -- License     :  BSD3
    -- Maintainer  :  cryptol@galois.com
    -- Stability   :  provisional
    -- Portability :  portable

    {-# LANGUAGE Safe #-}
    {-# LANGUAGE DeriveDataTypeable #-}
    {-# LANGUAGE DeriveFunctor #-}
    {-# LANGUAGE LambdaCase #-}
    {-# LANGUAGE OverloadedStrings #-}

    module Cryptol.Backend.Monad
    ( -- * Evaluation monad
      Eval(..)
    , runEval
    , io
    , delayFill
    , ready
    , blackhole
    , evalSpark
    , maybeReady
      -- * Call stacks
    , CallStack
    , getCallStack
    , withCallStack
    , modifyCallStack
    , combineCallStacks
    , pushCallFrame
    , displayCallStack
      -- * Error reporting
    , Unsupported(..)
    , EvalError(..)
    , EvalErrorEx(..)
    , evalPanic
    , wordTooWide
    , WordTooWide(..)
    ) where

    import           Control.Concurrent
    import           Control.Concurrent.STM

    import           Control.Monad
    import           Control.Monad.IO.Class
    import           Data.Foldable (toList)
    import           Data.Sequence (Seq)
    import qualified Data.Sequence as Seq
    import           Data.Typeable (Typeable)
    import qualified Control.Exception as X

    import Cryptol.Parser.Position
    import Cryptol.Utils.Panic
    import Cryptol.Utils.PP
    import Cryptol.TypeCheck.AST(Name, TParam)

    -- | A computation that returns an already-evaluated value.
    ready :: a -> Eval a
    ready :: forall a. a -> Eval a
    ready a
    a = a -> Eval a
    forall a. a -> Eval a
    Ready a
    a

    -- | The type of dynamic call stacks for the interpreter.
    --   New frames are pushed onto the right side of the sequence.
    data CallStack
      = EmptyCallStack
      | CombineCallStacks !CallStack !CallStack
      | PushCallFrame !Name !Range !CallStack

    instance Semigroup CallStack where
      <> :: CallStack -> CallStack -> CallStack
    (<>) = CallStack -> CallStack -> CallStack
    CombineCallStacks

    instance Monoid CallStack where
      mempty :: CallStack
    mempty = CallStack
    EmptyCallStack

    type CallStack' = Seq (Name, Range)

    evalCallStack :: CallStack -> CallStack'
    evalCallStack :: CallStack -> CallStack'
    evalCallStack CallStack
    stk =
      case CallStack
    stk of
        CallStack
    EmptyCallStack -> CallStack'
    forall a. Monoid a => a
    mempty
        CombineCallStacks CallStack
    appstk CallStack
    fnstk -> CallStack' -> CallStack' -> CallStack'
    combineCallStacks' (CallStack -> CallStack'
    evalCallStack CallStack
    appstk) (CallStack -> CallStack'
    evalCallStack CallStack
    fnstk)
        PushCallFrame Name
    n Range
    r CallStack
    stk1 -> Name -> Range -> CallStack' -> CallStack'
    pushCallFrame' Name
    n Range
    r (CallStack -> CallStack'
    evalCallStack CallStack
    stk1)

    -- | Pretty print a call stack with each call frame on a separate
    --   line, with most recent call frames at the top.
    displayCallStack :: CallStack -> Doc
    displayCallStack :: CallStack -> Doc
    displayCallStack = CallStack' -> Doc
    displayCallStack' (CallStack' -> Doc)
    -> (CallStack -> CallStack') -> CallStack -> Doc
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . CallStack -> CallStack'
    evalCallStack

    displayCallStack' :: CallStack' -> Doc
    displayCallStack' :: CallStack' -> Doc
    displayCallStack' = [Doc] -> Doc
    vcat ([Doc] -> Doc) -> (CallStack' -> [Doc]) -> CallStack' -> Doc
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . ((Name, Range) -> Doc) -> [(Name, Range)] -> [Doc]
    forall a b. (a -> b) -> [a] -> [b]
    map (Name, Range) -> Doc
    forall {a}. PP a => (a, Range) -> Doc
    f ([(Name, Range)] -> [Doc])
    -> (CallStack' -> [(Name, Range)]) -> CallStack' -> [Doc]
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . CallStack' -> [(Name, Range)]
    forall a. Seq a -> [a]
    forall (t :: * -> *) a. Foldable t => t a -> [a]
    toList (CallStack' -> [(Name, Range)])
    -> (CallStack' -> CallStack') -> CallStack' -> [(Name, Range)]
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . CallStack' -> CallStack'
    forall a. Seq a -> Seq a
    Seq.reverse
      where
      f :: (a, Range) -> Doc
    f (a
    nm,Range
    rng)
        | Range
    rng Range -> Range -> Bool
    forall a. Eq a => a -> a -> Bool
    == Range
    emptyRange = a -> Doc
    forall a. PP a => a -> Doc
    pp a
    nm
        | Bool
    otherwise = a -> Doc
    forall a. PP a => a -> Doc
    pp a
    nm Doc -> Doc -> Doc
    <+> String -> Doc
    text String
    "called at" Doc -> Doc -> Doc
    <+> Range -> Doc
    forall a. PP a => a -> Doc
    pp Range
    rng

    -- | Combine the call stack of a function value with the call
    --   stack of the current calling context.  This algorithm is
    --   the same one GHC uses to compute profiling calling contexts.
    --
    --   The algorithm is as follows.
    --
    --        ccs ++> ccsfn  =  ccs ++ dropCommonPrefix ccs ccsfn
    --
    --      where
    --
    --        dropCommonPrefix A B
    --           -- returns the suffix of B after removing any prefix common
    --           -- to both A and B.
    combineCallStacks ::
      CallStack {- ^ call stack of the application context -} ->
      CallStack {- ^ call stack of the function being applied -} ->
      CallStack
    combineCallStacks :: CallStack -> CallStack -> CallStack
    combineCallStacks CallStack
    appstk CallStack
    EmptyCallStack = CallStack
    appstk
    combineCallStacks CallStack
    EmptyCallStack CallStack
    fnstk = CallStack
    fnstk
    combineCallStacks CallStack
    appstk CallStack
    fnstk = CallStack -> CallStack -> CallStack
    CombineCallStacks CallStack
    appstk CallStack
    fnstk

    combineCallStacks' ::
      CallStack' {- ^ call stack of the application context -} ->
      CallStack' {- ^ call stack of the function being applied -} ->
      CallStack'
    combineCallStacks' :: CallStack' -> CallStack' -> CallStack'
    combineCallStacks' CallStack'
    appstk CallStack'
    fnstk = CallStack'
    appstk CallStack' -> CallStack' -> CallStack'
    forall a. Semigroup a => a -> a -> a
    <> CallStack' -> CallStack' -> CallStack'
    forall {a}. Eq a => Seq a -> Seq a -> Seq a
    dropCommonPrefix CallStack'
    appstk CallStack'
    fnstk
      where
      dropCommonPrefix :: Seq a -> Seq a -> Seq a
    dropCommonPrefix Seq a
    _  Seq a
    Seq.Empty = Seq a
    forall a. Seq a
    Seq.Empty
      dropCommonPrefix Seq a
    Seq.Empty Seq a
    fs = Seq a
    fs
      dropCommonPrefix (a
    a Seq.:<| Seq a
    as) xs :: Seq a
    xs@(a
    f Seq.:<| Seq a
    fs)
        | a
    a a -> a -> Bool
    forall a. Eq a => a -> a -> Bool
    == a
    f    = Seq a -> Seq a -> Seq a
    dropCommonPrefix Seq a
    as Seq a
    fs
        | Bool
    otherwise = Seq a
    xs

    -- | Add a call frame to the top of a call stack
    pushCallFrame :: Name -> Range -> CallStack -> CallStack
    pushCallFrame :: Name -> Range -> CallStack -> CallStack
    pushCallFrame Name
    nm Range
    rng CallStack
    stk = Name -> Range -> CallStack -> CallStack
    PushCallFrame Name
    nm Range
    rng CallStack
    stk

    pushCallFrame' :: Name -> Range -> CallStack' -> CallStack'
    pushCallFrame' :: Name -> Range -> CallStack' -> CallStack'
    pushCallFrame' Name
    nm Range
    rng stk :: CallStack'
    stk@( CallStack'
    _ Seq.:|> (Name
    nm',Range
    rng'))
      | Name
    nm Name -> Name -> Bool
    forall a. Eq a => a -> a -> Bool
    == Name
    nm', Range
    rng Range -> Range -> Bool
    forall a. Eq a => a -> a -> Bool
    == Range
    rng' = CallStack'
    stk
    pushCallFrame' Name
    nm Range
    rng CallStack'
    stk = CallStack'
    stk CallStack' -> (Name, Range) -> CallStack'
    forall a. Seq a -> a -> Seq a
    Seq.:|> (Name
    nm,Range
    rng)

    -- | The monad for Cryptol evaluation.
    --   A computation is either "ready", which means it represents
    --   only trivial computation, or is an "eval" action which must
    --   be computed to get the answer, or it is a "thunk", which
    --   represents a delayed, shared computation.
    data Eval a
       = Ready !a
       | Eval !(CallStack -> IO a)
       | Thunk !(TVar (ThunkState a))

    -- | This datastructure tracks the lifecycle of a thunk.
    --
    --   Thunks are used for basically three use cases.  First,
    --   we use thunks to preserve sharing.  Basically every
    --   cryptol expression that is bound to a name, and is not
    --   already obviously a value (and in a few other places as
    --   well) will get turned into a thunk in order to avoid
    --   recomputation.  These thunks will start in the `Unforced`
    --   state, and have a backup computation that just raises
    --   the `LoopError` exception.
    --
    --   Secondly, thunks are used to cut cycles when evaluating
    --   recursive definition groups.  Every named clause in a
    --   recursive definition is thunked so that the value can appear
    --   in its definition.  Such thunks start in the `Void` state,
    --   as they must exist before we have a definition to assign them.
    --   Forcing a thunk in the `Void` state is a programmer error (panic).
    --   Once the body of a definition is ready, we replace the
    --   thunk with the relevant computation, going to the `Unforced` state.
    --
    --   In the third case, we are using thunks to provide an optimistic
    --   shortcut for evaluation.  In these cases we first try to run a
    --   computation that is stricter than the semantics actually allows.
    --   If it succeeds, all is well an we continue.  However, if it tight
    --   loops, we fall back on a lazier (and generally more expensive)
    --   version, which is the "backup" computation referred to above.
    data ThunkState a
      = Void !String
           -- ^ This thunk has not yet been initialized
      | Unforced !(IO a) !(Maybe (IO a)) !String !CallStack
           -- ^ This thunk has not yet been forced.  We keep track of the "main"
           --   computation to run and an optional "backup" computation to run if we
           --   detect a tight loop when evaluating the first one.
           --   The final two arguments are used to throw a loop exception
           --   if the backup computation also causes a tight loop.
      | UnderEvaluation !ThreadId !(Maybe (IO a)) !String !CallStack
           -- ^ This thunk is currently being evaluated by the thread with the given
           --   thread ID.  We track an optional "backup" computation to run if we detect
           --   a tight loop evaluating this thunk.  If the thunk is being evaluated
           --   by some other thread, the current thread will await its completion.
           --   The final two arguments are used to throw a loop exception
           --   if the backup computation also causes a tight loop.
      | ForcedErr !EvalErrorEx
           -- ^ This thunk has been forced, and its evaluation results in an exception
      | Forced !a
           -- ^ This thunk has been forced to the given value

    -- | Test if a value is "ready", which means that
    --   it requires no computation to return.
    maybeReady :: Eval a -> Eval (Maybe a)
    maybeReady :: forall a. Eval a -> Eval (Maybe a)
    maybeReady (Ready a
    a) = Maybe a -> Eval (Maybe a)
    forall a. a -> Eval a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (a -> Maybe a
    forall a. a -> Maybe a
    Just a
    a)
    maybeReady (Thunk TVar (ThunkState a)
    tv) = (CallStack -> IO (Maybe a)) -> Eval (Maybe a)
    forall a. (CallStack -> IO a) -> Eval a
    Eval ((CallStack -> IO (Maybe a)) -> Eval (Maybe a))
    -> (CallStack -> IO (Maybe a)) -> Eval (Maybe a)
    forall a b. (a -> b) -> a -> b
    $ \CallStack
    _ ->
      TVar (ThunkState a) -> IO (ThunkState a)
    forall a. TVar a -> IO a
    readTVarIO TVar (ThunkState a)
    tv IO (ThunkState a) -> (ThunkState a -> IO (Maybe a)) -> IO (Maybe a)
    forall a b. IO a -> (a -> IO b) -> IO b
    forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
    >>= \case
         Forced a
    a -> Maybe a -> IO (Maybe a)
    forall a. a -> IO a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (a -> Maybe a
    forall a. a -> Maybe a
    Just a
    a)
         ThunkState a
    _ -> Maybe a -> IO (Maybe a)
    forall a. a -> IO a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure Maybe a
    forall a. Maybe a
    Nothing
    maybeReady (Eval CallStack -> IO a
    _) = Maybe a -> Eval (Maybe a)
    forall a. a -> Eval a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure Maybe a
    forall a. Maybe a
    Nothing

    {-# INLINE delayFill #-}

    -- | Delay the given evaluation computation, returning a thunk
    --   which will run the computation when forced.  Run the 'retry'
    --   computation instead if the resulting thunk is forced during
    --   its own evaluation.
    delayFill ::
      Eval a {- ^ Computation to delay -} ->
      Maybe (Eval a) {- ^ Optional backup computation to run if a tight loop is detected -} ->
      String {- ^ message for the <<loop>> exception if a tight loop is detected -} ->
      Eval (Eval a)
    delayFill :: forall a. Eval a -> Maybe (Eval a) -> String -> Eval (Eval a)
    delayFill e :: Eval a
    e@(Ready a
    _) Maybe (Eval a)
    _ String
    _ = Eval a -> Eval (Eval a)
    forall a. a -> Eval a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Eval a
    e
    delayFill e :: Eval a
    e@(Thunk TVar (ThunkState a)
    _) Maybe (Eval a)
    _ String
    _ = Eval a -> Eval (Eval a)
    forall a. a -> Eval a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Eval a
    e
    delayFill (Eval CallStack -> IO a
    x) Maybe (Eval a)
    backup String
    msg =
      (CallStack -> IO (Eval a)) -> Eval (Eval a)
    forall a. (CallStack -> IO a) -> Eval a
    Eval (\CallStack
    stk -> TVar (ThunkState a) -> Eval a
    forall a. TVar (ThunkState a) -> Eval a
    Thunk (TVar (ThunkState a) -> Eval a)
    -> IO (TVar (ThunkState a)) -> IO (Eval a)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> ThunkState a -> IO (TVar (ThunkState a))
    forall a. a -> IO (TVar a)
    newTVarIO (IO a -> Maybe (IO a) -> String -> CallStack -> ThunkState a
    forall a.
    IO a -> Maybe (IO a) -> String -> CallStack -> ThunkState a
    Unforced (CallStack -> IO a
    x CallStack
    stk) (CallStack -> Eval a -> IO a
    forall a. CallStack -> Eval a -> IO a
    runEval CallStack
    stk (Eval a -> IO a) -> Maybe (Eval a) -> Maybe (IO a)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Maybe (Eval a)
    backup) String
    msg CallStack
    stk))

    -- | Begin executing the given operation in a separate thread,
    --   returning a thunk which will await the completion of
    --   the computation when forced.
    evalSpark ::
      Eval a ->
      Eval (Eval a)

    -- Ready computations need no additional evaluation.
    evalSpark :: forall a. Eval a -> Eval (Eval a)
    evalSpark e :: Eval a
    e@(Ready a
    _) = Eval a -> Eval (Eval a)
    forall a. a -> Eval a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Eval a
    e

    -- A thunked computation might already have
    -- been forced.  If so, return the result.  Otherwise,
    -- fork a thread to force this computation and return
    -- the thunk.
    evalSpark (Thunk TVar (ThunkState a)
    tv)  = (CallStack -> IO (Eval a)) -> Eval (Eval a)
    forall a. (CallStack -> IO a) -> Eval a
    Eval ((CallStack -> IO (Eval a)) -> Eval (Eval a))
    -> (CallStack -> IO (Eval a)) -> Eval (Eval a)
    forall a b. (a -> b) -> a -> b
    $ \CallStack
    _stk ->
      TVar (ThunkState a) -> IO (ThunkState a)
    forall a. TVar a -> IO a
    readTVarIO TVar (ThunkState a)
    tv IO (ThunkState a) -> (ThunkState a -> IO (Eval a)) -> IO (Eval a)
    forall a b. IO a -> (a -> IO b) -> IO b
    forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
    >>= \case
        Forced a
    x     -> Eval a -> IO (Eval a)
    forall a. a -> IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (a -> Eval a
    forall a. a -> Eval a
    Ready a
    x)
        ForcedErr EvalErrorEx
    ex -> Eval a -> IO (Eval a)
    forall a. a -> IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return ((CallStack -> IO a) -> Eval a
    forall a. (CallStack -> IO a) -> Eval a
    Eval ((CallStack -> IO a) -> Eval a) -> (CallStack -> IO a) -> Eval a
    forall a b. (a -> b) -> a -> b
    $ \CallStack
    _ -> (EvalErrorEx -> IO a
    forall e a. Exception e => e -> IO a
    X.throwIO EvalErrorEx
    ex))
        ThunkState a
    _ ->
           do ThreadId
    _ <- IO () -> IO ThreadId
    forkIO (TVar (ThunkState a) -> IO ()
    forall a. TVar (ThunkState a) -> IO ()
    sparkThunk TVar (ThunkState a)
    tv)
              Eval a -> IO (Eval a)
    forall a. a -> IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (TVar (ThunkState a) -> Eval a
    forall a. TVar (ThunkState a) -> Eval a
    Thunk TVar (ThunkState a)
    tv)

    -- If the computation is nontrivial but not already a thunk,
    -- create a thunk and fork a thread to force it.
    evalSpark (Eval CallStack -> IO a
    x) = (CallStack -> IO (Eval a)) -> Eval (Eval a)
    forall a. (CallStack -> IO a) -> Eval a
    Eval ((CallStack -> IO (Eval a)) -> Eval (Eval a))
    -> (CallStack -> IO (Eval a)) -> Eval (Eval a)
    forall a b. (a -> b) -> a -> b
    $ \CallStack
    stk ->
      do TVar (ThunkState a)
    tv <- ThunkState a -> IO (TVar (ThunkState a))
    forall a. a -> IO (TVar a)
    newTVarIO (IO a -> Maybe (IO a) -> String -> CallStack -> ThunkState a
    forall a.
    IO a -> Maybe (IO a) -> String -> CallStack -> ThunkState a
    Unforced (CallStack -> IO a
    x CallStack
    stk) Maybe (IO a)
    forall a. Maybe a
    Nothing String
    "" CallStack
    stk)
         ThreadId
    _ <- IO () -> IO ThreadId
    forkIO (TVar (ThunkState a) -> IO ()
    forall a. TVar (ThunkState a) -> IO ()
    sparkThunk TVar (ThunkState a)
    tv)
         Eval a -> IO (Eval a)
    forall a. a -> IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (TVar (ThunkState a) -> Eval a
    forall a. TVar (ThunkState a) -> Eval a
    Thunk TVar (ThunkState a)
    tv)

    -- | To the work of forcing a thunk. This is the worker computation
    --   that is forked off via @evalSpark@.
    sparkThunk :: TVar (ThunkState a) -> IO ()
    sparkThunk :: forall a. TVar (ThunkState a) -> IO ()
    sparkThunk TVar (ThunkState a)
    tv =
      do ThreadId
    tid <- IO ThreadId
    myThreadId
         -- Try to claim the thunk.  If it is still in the @Void@ state, wait
         -- until it is in some other state.  If it is @Unforced@ claim the thunk.
         -- Otherwise, it is already evaluated or under evaluation by another thread,
         -- and we have no work to do.
         ThunkState a
    st <- STM (ThunkState a) -> IO (ThunkState a)
    forall a. STM a -> IO a
    atomically (STM (ThunkState a) -> IO (ThunkState a))
    -> STM (ThunkState a) -> IO (ThunkState a)
    forall a b. (a -> b) -> a -> b
    $
                  do ThunkState a
    st <- TVar (ThunkState a) -> STM (ThunkState a)
    forall a. TVar a -> STM a
    readTVar TVar (ThunkState a)
    tv
                     case ThunkState a
    st of
                       Void String
    _ -> STM ()
    forall a. STM a
    retry
                       Unforced IO a
    _ Maybe (IO a)
    backup String
    msg CallStack
    stk -> TVar (ThunkState a) -> ThunkState a -> STM ()
    forall a. TVar a -> a -> STM ()
    writeTVar TVar (ThunkState a)
    tv (ThreadId -> Maybe (IO a) -> String -> CallStack -> ThunkState a
    forall a.
    ThreadId -> Maybe (IO a) -> String -> CallStack -> ThunkState a
    UnderEvaluation ThreadId
    tid Maybe (IO a)
    backup String
    msg CallStack
    stk)
                       ThunkState a
    _ -> () -> STM ()
    forall a. a -> STM a
    forall (m :: * -> *) a. Monad m => a -> m a
    return ()
                     ThunkState a -> STM (ThunkState a)
    forall a. a -> STM a
    forall (m :: * -> *) a. Monad m => a -> m a
    return ThunkState a
    st
         -- If we successfully claimed the thunk to work on, run the computation and
         -- update the thunk state with the result.
         case ThunkState a
    st of
           Unforced IO a
    work Maybe (IO a)
    _ String
    _ CallStack
    _ ->
             IO a -> IO (Either EvalErrorEx a)
    forall e a. Exception e => IO a -> IO (Either e a)
    X.try IO a
    work IO (Either EvalErrorEx a)
    -> (Either EvalErrorEx a -> IO ()) -> IO ()
    forall a b. IO a -> (a -> IO b) -> IO b
    forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
    >>= \case
               Left EvalErrorEx
    err -> STM () -> IO ()
    forall a. STM a -> IO a
    atomically (TVar (ThunkState a) -> ThunkState a -> STM ()
    forall a. TVar a -> a -> STM ()
    writeTVar TVar (ThunkState a)
    tv (EvalErrorEx -> ThunkState a
    forall a. EvalErrorEx -> ThunkState a
    ForcedErr EvalErrorEx
    err))
               Right a
    a  -> STM () -> IO ()
    forall a. STM a -> IO a
    atomically (TVar (ThunkState a) -> ThunkState a -> STM ()
    forall a. TVar a -> a -> STM ()
    writeTVar TVar (ThunkState a)
    tv (a -> ThunkState a
    forall a. a -> ThunkState a
    Forced a
    a))
           ThunkState a
    _ -> () -> IO ()
    forall a. a -> IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return ()

    -- | Produce a thunk value which can be filled with its associated computation
    --   after the fact.  A preallocated thunk is returned, along with an operation to
    --   fill the thunk with the associated computation.
    --   This is used to implement recursive declaration groups.
    blackhole ::
      String {- ^ A name to associate with this thunk. -} ->
      Eval (Eval a, Eval a -> Eval ())
    blackhole :: forall a. String -> Eval (Eval a, Eval a -> Eval ())
    blackhole String
    msg = (CallStack -> IO (Eval a, Eval a -> Eval ()))
    -> Eval (Eval a, Eval a -> Eval ())
    forall a. (CallStack -> IO a) -> Eval a
    Eval ((CallStack -> IO (Eval a, Eval a -> Eval ()))
     -> Eval (Eval a, Eval a -> Eval ()))
    -> (CallStack -> IO (Eval a, Eval a -> Eval ()))
    -> Eval (Eval a, Eval a -> Eval ())
    forall a b. (a -> b) -> a -> b
    $ \CallStack
    stk ->
      do TVar (ThunkState a)
    tv <- ThunkState a -> IO (TVar (ThunkState a))
    forall a. a -> IO (TVar a)
    newTVarIO (String -> ThunkState a
    forall a. String -> ThunkState a
    Void String
    msg)
         let set :: Eval a -> Eval ()
    set (Ready a
    x)  = IO () -> Eval ()
    forall a. IO a -> Eval a
    io (IO () -> Eval ()) -> IO () -> Eval ()
    forall a b. (a -> b) -> a -> b
    $ STM () -> IO ()
    forall a. STM a -> IO a
    atomically (TVar (ThunkState a) -> ThunkState a -> STM ()
    forall a. TVar a -> a -> STM ()
    writeTVar TVar (ThunkState a)
    tv (a -> ThunkState a
    forall a. a -> ThunkState a
    Forced a
    x))
             set Eval a
    m          = IO () -> Eval ()
    forall a. IO a -> Eval a
    io (IO () -> Eval ()) -> IO () -> Eval ()
    forall a b. (a -> b) -> a -> b
    $ STM () -> IO ()
    forall a. STM a -> IO a
    atomically (TVar (ThunkState a) -> ThunkState a -> STM ()
    forall a. TVar a -> a -> STM ()
    writeTVar TVar (ThunkState a)
    tv (IO a -> Maybe (IO a) -> String -> CallStack -> ThunkState a
    forall a.
    IO a -> Maybe (IO a) -> String -> CallStack -> ThunkState a
    Unforced (CallStack -> Eval a -> IO a
    forall a. CallStack -> Eval a -> IO a
    runEval CallStack
    stk Eval a
    m) Maybe (IO a)
    forall a. Maybe a
    Nothing String
    msg CallStack
    stk))
         (Eval a, Eval a -> Eval ()) -> IO (Eval a, Eval a -> Eval ())
    forall a. a -> IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (TVar (ThunkState a) -> Eval a
    forall a. TVar (ThunkState a) -> Eval a
    Thunk TVar (ThunkState a)
    tv, Eval a -> Eval ()
    set)

    -- | Force a thunk to get the result.
    unDelay :: TVar (ThunkState a) -> IO a
    unDelay :: forall a. TVar (ThunkState a) -> IO a
    unDelay TVar (ThunkState a)
    tv =
      -- First, check if the thunk is in an evaluated state,
      -- and return the value if so.
      TVar (ThunkState a) -> IO (ThunkState a)
    forall a. TVar a -> IO a
    readTVarIO TVar (ThunkState a)
    tv IO (ThunkState a) -> (ThunkState a -> IO a) -> IO a
    forall a b. IO a -> (a -> IO b) -> IO b
    forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
    >>= \case
        Forced a
    x -> a -> IO a
    forall a. a -> IO a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure a
    x
        ForcedErr EvalErrorEx
    e -> EvalErrorEx -> IO a
    forall e a. Exception e => e -> IO a
    X.throwIO EvalErrorEx
    e
        ThunkState a
    _ ->
          -- Otherwise, try to claim the thunk to work on.
          do ThreadId
    tid <- IO ThreadId
    myThreadId
             ThunkState a
    res <- STM (ThunkState a) -> IO (ThunkState a)
    forall a. STM a -> IO a
    atomically (STM (ThunkState a) -> IO (ThunkState a))
    -> STM (ThunkState a) -> IO (ThunkState a)
    forall a b. (a -> b) -> a -> b
    $ do
                      ThunkState a
    res <- TVar (ThunkState a) -> STM (ThunkState a)
    forall a. TVar a -> STM a
    readTVar TVar (ThunkState a)
    tv
                      case ThunkState a
    res of
                        -- In this case, we claim the thunk.  Update the state to indicate
                        -- that we are working on it.
                        Unforced IO a
    _ Maybe (IO a)
    backup String
    msg CallStack
    stk -> TVar (ThunkState a) -> ThunkState a -> STM ()
    forall a. TVar a -> a -> STM ()
    writeTVar TVar (ThunkState a)
    tv (ThreadId -> Maybe (IO a) -> String -> CallStack -> ThunkState a
    forall a.
    ThreadId -> Maybe (IO a) -> String -> CallStack -> ThunkState a
    UnderEvaluation ThreadId
    tid Maybe (IO a)
    backup String
    msg CallStack
    stk)

                        -- In this case, the thunk is already being evaluated.  If it is
                        -- under evaluation by this thread, we have to run the backup computation,
                        -- and "consume" it by updating the backup computation to one that throws
                        -- a loop error.  If some other thread is evaluating, reset the
                        -- transaction to await completion of the thunk.
                        UnderEvaluation ThreadId
    t Maybe (IO a)
    backup String
    msg CallStack
    stk
                          | ThreadId
    tid ThreadId -> ThreadId -> Bool
    forall a. Eq a => a -> a -> Bool
    == ThreadId
    t  ->
                              case Maybe (IO a)
    backup of
                                Just IO a
    _  -> TVar (ThunkState a) -> ThunkState a -> STM ()
    forall a. TVar a -> a -> STM ()
    writeTVar TVar (ThunkState a)
    tv (ThreadId -> Maybe (IO a) -> String -> CallStack -> ThunkState a
    forall a.
    ThreadId -> Maybe (IO a) -> String -> CallStack -> ThunkState a
    UnderEvaluation ThreadId
    tid Maybe (IO a)
    forall a. Maybe a
    Nothing String
    msg CallStack
    stk)
                                Maybe (IO a)
    Nothing -> TVar (ThunkState a) -> ThunkState a -> STM ()
    forall a. TVar a -> a -> STM ()
    writeTVar TVar (ThunkState a)
    tv (EvalErrorEx -> ThunkState a
    forall a. EvalErrorEx -> ThunkState a
    ForcedErr (CallStack -> EvalError -> EvalErrorEx
    EvalErrorEx CallStack
    stk (String -> EvalError
    LoopError String
    msg)))
                          | Bool
    otherwise -> STM ()
    forall a. STM a
    retry -- wait, if some other thread is evaluating
                        ThunkState a
    _ -> () -> STM ()
    forall a. a -> STM a
    forall (m :: * -> *) a. Monad m => a -> m a
    return ()

                      -- Return the original thunk state so we can decide what work to do
                      -- after the transaction completes.
                      ThunkState a -> STM (ThunkState a)
    forall a. a -> STM a
    forall (m :: * -> *) a. Monad m => a -> m a
    return ThunkState a
    res

             -- helper for actually doing the work
             let doWork :: IO a -> IO a
    doWork IO a
    work =
                   IO a -> IO (Either EvalErrorEx a)
    forall e a. Exception e => IO a -> IO (Either e a)
    X.try IO a
    work IO (Either EvalErrorEx a) -> (Either EvalErrorEx a -> IO a) -> IO a
    forall a b. IO a -> (a -> IO b) -> IO b
    forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
    >>= \case
                     Left EvalErrorEx
    ex -> do STM () -> IO ()
    forall a. STM a -> IO a
    atomically (TVar (ThunkState a) -> ThunkState a -> STM ()
    forall a. TVar a -> a -> STM ()
    writeTVar TVar (ThunkState a)
    tv (EvalErrorEx -> ThunkState a
    forall a. EvalErrorEx -> ThunkState a
    ForcedErr EvalErrorEx
    ex))
                                   EvalErrorEx -> IO a
    forall e a. Exception e => e -> IO a
    X.throwIO EvalErrorEx
    ex
                     Right a
    a -> do STM () -> IO ()
    forall a. STM a -> IO a
    atomically (TVar (ThunkState a) -> ThunkState a -> STM ()
    forall a. TVar a -> a -> STM ()
    writeTVar TVar (ThunkState a)
    tv (a -> ThunkState a
    forall a. a -> ThunkState a
    Forced a
    a))
                                   a -> IO a
    forall a. a -> IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return a
    a

             -- Now, examine the thunk state and decide what to do.
             case ThunkState a
    res of
               Void String
    msg -> String -> [String] -> IO a
    forall a. HasCallStack => String -> [String] -> a
    evalPanic String
    "unDelay" [String
    "Thunk forced before it was initialized", String
    msg]
               Forced a
    x -> a -> IO a
    forall a. a -> IO a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure a
    x
               ForcedErr EvalErrorEx
    e -> EvalErrorEx -> IO a
    forall e a. Exception e => e -> IO a
    X.throwIO EvalErrorEx
    e
               -- this thread was already evaluating this thunk
               UnderEvaluation ThreadId
    _ (Just IO a
    backup) String
    _ CallStack
    _ -> IO a -> IO a
    doWork IO a
    backup
               UnderEvaluation ThreadId
    _ Maybe (IO a)
    Nothing String
    msg CallStack
    stk -> EvalErrorEx -> IO a
    forall e a. Exception e => e -> IO a
    X.throwIO (CallStack -> EvalError -> EvalErrorEx
    EvalErrorEx CallStack
    stk (String -> EvalError
    LoopError String
    msg))
               Unforced IO a
    work Maybe (IO a)
    _ String
    _ CallStack
    _ -> IO a -> IO a
    doWork IO a
    work

    -- | Get the current call stack
    getCallStack :: Eval CallStack
    getCallStack :: Eval CallStack
    getCallStack = (CallStack -> IO CallStack) -> Eval CallStack
    forall a. (CallStack -> IO a) -> Eval a
    Eval (\CallStack
    stk -> CallStack -> IO CallStack
    forall a. a -> IO a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure CallStack
    stk)

    -- | Execute the action with the given call stack
    withCallStack :: CallStack -> Eval a -> Eval a
    withCallStack :: forall a. CallStack -> Eval a -> Eval a
    withCallStack CallStack
    stk Eval a
    m = (CallStack -> IO a) -> Eval a
    forall a. (CallStack -> IO a) -> Eval a
    Eval (\CallStack
    _ -> CallStack -> Eval a -> IO a
    forall a. CallStack -> Eval a -> IO a
    runEval CallStack
    stk Eval a
    m)

    -- | Run the given action with a modify call stack
    modifyCallStack :: (CallStack -> CallStack) -> Eval a -> Eval a
    modifyCallStack :: forall a. (CallStack -> CallStack) -> Eval a -> Eval a
    modifyCallStack CallStack -> CallStack
    f Eval a
    m =
      (CallStack -> IO a) -> Eval a
    forall a. (CallStack -> IO a) -> Eval a
    Eval ((CallStack -> IO a) -> Eval a) -> (CallStack -> IO a) -> Eval a
    forall a b. (a -> b) -> a -> b
    $ \CallStack
    stk ->
        do let stk' :: CallStack
    stk' = CallStack -> CallStack
    f CallStack
    stk
           -- putStrLn $ unwords ["Pushing call stack", show (displayCallStack stk')]
           CallStack -> IO a -> IO a
    forall a b. a -> b -> b
    seq CallStack
    stk' (CallStack -> Eval a -> IO a
    forall a. CallStack -> Eval a -> IO a
    runEval CallStack
    stk' Eval a
    m)
    {-# INLINE modifyCallStack #-}

    -- | Execute the given evaluation action.
    runEval :: CallStack -> Eval a -> IO a
    runEval :: forall a. CallStack -> Eval a -> IO a
    runEval CallStack
    _   (Ready a
    a)  = a -> IO a
    forall a. a -> IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return a
    a
    runEval CallStack
    stk (Eval CallStack -> IO a
    x)   = CallStack -> IO a
    x CallStack
    stk
    runEval CallStack
    _   (Thunk TVar (ThunkState a)
    tv) = TVar (ThunkState a) -> IO a
    forall a. TVar (ThunkState a) -> IO a
    unDelay TVar (ThunkState a)
    tv
    {-# INLINE runEval #-}

    {-# INLINE evalBind #-}
    evalBind :: Eval a -> (a -> Eval b) -> Eval b
    evalBind :: forall a b. Eval a -> (a -> Eval b) -> Eval b
    evalBind (Ready a
    a) a -> Eval b
    f  = a -> Eval b
    f a
    a
    evalBind (Eval CallStack -> IO a
    x)  a -> Eval b
    f  = (CallStack -> IO b) -> Eval b
    forall a. (CallStack -> IO a) -> Eval a
    Eval (\CallStack
    stk -> CallStack -> IO a
    x CallStack
    stk IO a -> (a -> IO b) -> IO b
    forall a b. IO a -> (a -> IO b) -> IO b
    forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
    >>= CallStack -> Eval b -> IO b
    forall a. CallStack -> Eval a -> IO a
    runEval CallStack
    stk (Eval b -> IO b) -> (a -> Eval b) -> a -> IO b
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . a -> Eval b
    f)
    evalBind (Thunk TVar (ThunkState a)
    x) a -> Eval b
    f  = (CallStack -> IO b) -> Eval b
    forall a. (CallStack -> IO a) -> Eval a
    Eval (\CallStack
    stk -> TVar (ThunkState a) -> IO a
    forall a. TVar (ThunkState a) -> IO a
    unDelay TVar (ThunkState a)
    x IO a -> (a -> IO b) -> IO b
    forall a b. IO a -> (a -> IO b) -> IO b
    forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
    >>= CallStack -> Eval b -> IO b
    forall a. CallStack -> Eval a -> IO a
    runEval CallStack
    stk (Eval b -> IO b) -> (a -> Eval b) -> a -> IO b
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . a -> Eval b
    f)

    instance Functor Eval where
      fmap :: forall a b. (a -> b) -> Eval a -> Eval b
    fmap a -> b
    f (Ready a
    x)   = b -> Eval b
    forall a. a -> Eval a
    Ready (a -> b
    f a
    x)
      fmap a -> b
    f (Eval CallStack -> IO a
    m)    = (CallStack -> IO b) -> Eval b
    forall a. (CallStack -> IO a) -> Eval a
    Eval (\CallStack
    stk -> a -> b
    f (a -> b) -> IO a -> IO b
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> CallStack -> IO a
    m CallStack
    stk)
      fmap a -> b
    f (Thunk TVar (ThunkState a)
    tv)  = (CallStack -> IO b) -> Eval b
    forall a. (CallStack -> IO a) -> Eval a
    Eval (\CallStack
    _   -> a -> b
    f (a -> b) -> IO a -> IO b
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> TVar (ThunkState a) -> IO a
    forall a. TVar (ThunkState a) -> IO a
    unDelay TVar (ThunkState a)
    tv)
      {-# INLINE fmap #-}

    instance Applicative Eval where
      pure :: forall a. a -> Eval a
    pure  = a -> Eval a
    forall a. a -> Eval a
    Ready
      <*> :: forall a b. Eval (a -> b) -> Eval a -> Eval b
    (<*>) = Eval (a -> b) -> Eval a -> Eval b
    forall (m :: * -> *) a b. Monad m => m (a -> b) -> m a -> m b
    ap
      {-# INLINE pure #-}
      {-# INLINE (<*>) #-}

    instance Monad Eval where
      return :: forall a. a -> Eval a
    return = a -> Eval a
    forall a. a -> Eval a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure
      >>= :: forall a b. Eval a -> (a -> Eval b) -> Eval b
    (>>=)  = Eval a -> (a -> Eval b) -> Eval b
    forall a b. Eval a -> (a -> Eval b) -> Eval b
    evalBind
      {-# INLINE return #-}
      {-# INLINE (>>=) #-}

    instance MonadIO Eval where
      liftIO :: forall a. IO a -> Eval a
    liftIO = IO a -> Eval a
    forall a. IO a -> Eval a
    io

    -- | Lift an 'IO' computation into the 'Eval' monad.
    io :: IO a -> Eval a
    io :: forall a. IO a -> Eval a
    io IO a
    m = (CallStack -> IO a) -> Eval a
    forall a. (CallStack -> IO a) -> Eval a
    Eval (\CallStack
    _stk -> IO a
    m)
    {-# INLINE io #-}

    -- Errors ----------------------------------------------------------------------

    -- | Panic from an @Eval@ context.
    evalPanic :: HasCallStack => String -> [String] -> a
    evalPanic :: forall a. HasCallStack => String -> [String] -> a
    evalPanic String
    cxt = String -> [String] -> a
    forall a. HasCallStack => String -> [String] -> a
    panic (String
    "[Eval] " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    cxt)

    -- | Data type describing errors that can occur during evaluation.
    data EvalError
      = InvalidIndex (Maybe Integer)         -- ^ Out-of-bounds index
      | DivideByZero                         -- ^ Division or modulus by 0
      | NegativeExponent                     -- ^ Exponentiation by negative integer
      | LogNegative                          -- ^ Logarithm of a negative integer
      | UserError String                     -- ^ Call to the Cryptol @error@ primitive
      | LoopError String                     -- ^ Detectable nontermination
      | NoPrim Name                          -- ^ Primitive with no implementation
      | BadRoundingMode Integer              -- ^ Invalid rounding mode
      | BadValue String                      -- ^ Value outside the domain of a partial function.
      | NoMatchingPropGuardCase String    -- ^ No prop guard holds for the given type variables.
      | FFINotSupported Name                 -- ^ Foreign function cannot be called
      | FFITypeNumTooBig Name TParam Integer -- ^ Number passed to foreign function
                                             --   as a type argument is too large
      deriving Typeable

    instance PP EvalError where
      ppPrec :: Int -> EvalError -> Doc
    ppPrec Int
    _ EvalError
    e = case EvalError
    e of
        InvalidIndex (Just Integer
    i) -> String -> Doc
    text String
    "invalid sequence index:" Doc -> Doc -> Doc
    <+> Integer -> Doc
    integer Integer
    i
        InvalidIndex Maybe Integer
    Nothing  -> String -> Doc
    text String
    "invalid sequence index"
        EvalError
    DivideByZero -> String -> Doc
    text String
    "division by 0"
        EvalError
    NegativeExponent -> String -> Doc
    text String
    "negative exponent"
        EvalError
    LogNegative -> String -> Doc
    text String
    "logarithm of negative"
        UserError String
    x -> String -> Doc
    text String
    "Run-time error:" Doc -> Doc -> Doc
    <+> String -> Doc
    text String
    x
        LoopError String
    x -> [Doc] -> Doc
    vcat [ String -> Doc
    text String
    "<<loop>>" Doc -> Doc -> Doc
    <+> String -> Doc
    text String
    x
                            , String -> Doc
    text String
    "This usually occurs due to an improper recursive definition,"
                            , String -> Doc
    text String
    "but may also result from retrying a previously interrupted"
                            , String -> Doc
    text String
    "computation (e.g., after CTRL^C). In that case, you may need to"
                            , String -> Doc
    text String
    "`:reload` the current module to reset to a good state."
                            ]
        BadRoundingMode Integer
    r -> Doc
    "invalid rounding mode" Doc -> Doc -> Doc
    <+> Integer -> Doc
    integer Integer
    r
        BadValue String
    x -> Doc
    "invalid input for" Doc -> Doc -> Doc
    <+> Doc -> Doc
    backticks (String -> Doc
    text String
    x)
        NoPrim Name
    x -> String -> Doc
    text String
    "unimplemented primitive:" Doc -> Doc -> Doc
    <+> Name -> Doc
    forall a. PP a => a -> Doc
    pp Name
    x
        NoMatchingPropGuardCase String
    msg -> String -> Doc
    text (String -> Doc) -> String -> Doc
    forall a b. (a -> b) -> a -> b
    $ String
    "No matching constraint guard; " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    msg
        FFINotSupported Name
    x -> [Doc] -> Doc
    vcat
          [ String -> Doc
    text String
    "cannot call foreign function" Doc -> Doc -> Doc
    <+> Name -> Doc
    forall a. PP a => a -> Doc
    pp Name
    x
          , String -> Doc
    text String
    "FFI calls are not supported in this context"
          , String -> Doc
    text String
    "If you are trying to evaluate an expression, try rebuilding"
          , String -> Doc
    text String
    "  Cryptol with FFI support enabled."
          ]
        FFITypeNumTooBig Name
    f TParam
    p Integer
    n -> [Doc] -> Doc
    vcat
          [ String -> Doc
    text String
    "numeric type argument to foreign function is too large:"
            Doc -> Doc -> Doc
    <+> Integer -> Doc
    integer Integer
    n
          , String -> Doc
    text String
    "in type parameter" Doc -> Doc -> Doc
    <+> TParam -> Doc
    forall a. PP a => a -> Doc
    pp TParam
    p Doc -> Doc -> Doc
    <+> Doc
    "of function" Doc -> Doc -> Doc
    <+> Name -> Doc
    forall a. PP a => a -> Doc
    pp Name
    f
          , String -> Doc
    text String
    "type arguments must fit in a C `size_t`" ]

    instance Show EvalError where
      show :: EvalError -> String
    show = Doc -> String
    forall a. Show a => a -> String
    show (Doc -> String) -> (EvalError -> Doc) -> EvalError -> String
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . EvalError -> Doc
    forall a. PP a => a -> Doc
    pp

    data EvalErrorEx =
      EvalErrorEx CallStack EvalError
     deriving Typeable

    instance PP EvalErrorEx where
      ppPrec :: Int -> EvalErrorEx -> Doc
    ppPrec Int
    _ (EvalErrorEx CallStack
    stk0 EvalError
    ex) = [Doc] -> Doc
    vcat ([ EvalError -> Doc
    forall a. PP a => a -> Doc
    pp EvalError
    ex ] [Doc] -> [Doc] -> [Doc]
    forall a. [a] -> [a] -> [a]
    ++ [Doc]
    callStk)

       where
        stk :: CallStack'
    stk = CallStack -> CallStack'
    evalCallStack CallStack
    stk0
        callStk :: [Doc]
    callStk | CallStack' -> Bool
    forall a. Seq a -> Bool
    Seq.null CallStack'
    stk = []
                | Bool
    otherwise = [ String -> Doc
    text String
    "-- Backtrace --", CallStack' -> Doc
    displayCallStack' CallStack'
    stk ]

    instance Show EvalErrorEx where
      show :: EvalErrorEx -> String
    show = Doc -> String
    forall a. Show a => a -> String
    show (Doc -> String) -> (EvalErrorEx -> Doc) -> EvalErrorEx -> String
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . EvalErrorEx -> Doc
    forall a. PP a => a -> Doc
    pp

    instance X.Exception EvalErrorEx

    data Unsupported
      = UnsupportedSymbolicOp String  -- ^ Operation cannot be supported in the symbolic simulator
        deriving (Typeable,Int -> Unsupported -> String -> String
    [Unsupported] -> String -> String
    Unsupported -> String
    (Int -> Unsupported -> String -> String)
    -> (Unsupported -> String)
    -> ([Unsupported] -> String -> String)
    -> Show Unsupported
    forall a.
    (Int -> a -> String -> String)
    -> (a -> String) -> ([a] -> String -> String) -> Show a
    $cshowsPrec :: Int -> Unsupported -> String -> String
    showsPrec :: Int -> Unsupported -> String -> String
    $cshow :: Unsupported -> String
    show :: Unsupported -> String
    $cshowList :: [Unsupported] -> String -> String
    showList :: [Unsupported] -> String -> String
    Show)

    instance PP Unsupported where
      ppPrec :: Int -> Unsupported -> Doc
    ppPrec Int
    _ Unsupported
    e = case Unsupported
    e of
        UnsupportedSymbolicOp String
    nm -> String -> Doc
    text String
    "operation can not be supported on symbolic values:" Doc -> Doc -> Doc
    <+> String -> Doc
    text String
    nm

    instance X.Exception Unsupported

    -- | For when we know that a word is too wide and will exceed gmp's
    -- limits (though words approaching this size will probably cause the
    -- system to crash anyway due to lack of memory).
    wordTooWide :: Integer -> a
    wordTooWide :: forall a. Integer -> a
    wordTooWide Integer
    w = WordTooWide -> a
    forall a e. Exception e => e -> a
    X.throw (Integer -> WordTooWide
    WordTooWide Integer
    w)

    data WordTooWide = WordTooWide Integer -- ^ Bitvector too large
     deriving Typeable

    instance PP WordTooWide where
      ppPrec :: Int -> WordTooWide -> Doc
    ppPrec Int
    _ (WordTooWide Integer
    w) =
          String -> Doc
    text String
    "word too wide for memory:" Doc -> Doc -> Doc
    <+> Integer -> Doc
    integer Integer
    w Doc -> Doc -> Doc
    <+> String -> Doc
    text String
    "bits"

    instance Show WordTooWide where
      show :: WordTooWide -> String
    show = Doc -> String
    forall a. Show a => a -> String
    show (Doc -> String) -> (WordTooWide -> Doc) -> WordTooWide -> String
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . WordTooWide -> Doc
    forall a. PP a => a -> Doc
    pp

    instance X.Exception WordTooWide