-- |
-- 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)

-- | A computation that returns an already-evaluated value.
ready :: a -> Eval a
ready :: 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.
type CallStack = Seq (Name, Range)

-- | 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 = [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 (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
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 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 :: Eval a -> Eval (Maybe a)
maybeReady (Ready a
a) = Maybe a -> Eval (Maybe 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 (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
     Forced a
a -> Maybe a -> IO (Maybe 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 (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 (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 :: 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 (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 (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 :: Eval a -> Eval (Eval a)
evalSpark e :: Eval a
e@(Ready a
_) = Eval a -> Eval (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 (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
    Forced a
x     -> Eval a -> IO (Eval 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 (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 (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 (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 :: 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 (m :: * -> *) a. Monad m => a -> m a
return ()
                 ThunkState a -> STM (ThunkState 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 (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 (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 :: 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 (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 :: 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 (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
    Forced a
x -> 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 (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 (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 (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 (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 (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 (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 :: 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 :: (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 -> Eval a -> IO a
forall a. CallStack -> Eval a -> IO a
runEval CallStack
stk' Eval a
m

-- | Execute the given evaluation action.
runEval :: CallStack -> Eval a -> IO a
runEval :: CallStack -> Eval a -> IO a
runEval CallStack
_   (Ready a
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 evalBind #-}
evalBind :: Eval a -> (a -> Eval b) -> Eval b
evalBind :: 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 (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 (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 :: (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 :: a -> Eval a
pure  = a -> Eval a
forall (m :: * -> *) a. Monad m => a -> m a
return
  <*> :: 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 :: a -> Eval a
return = a -> Eval a
forall a. a -> Eval a
Ready
  >>= :: 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 :: 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 :: 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 :: 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.
    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

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
stk 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
    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
showList :: [Unsupported] -> String -> String
$cshowList :: [Unsupported] -> String -> String
show :: Unsupported -> String
$cshow :: Unsupported -> String
showsPrec :: Int -> Unsupported -> String -> String
$cshowsPrec :: Int -> 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 :: 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