{-# LANGUAGE Safe #-}
{-# LANGUAGE DeriveDataTypeable #-}
{-# LANGUAGE DeriveFunctor #-}
module Cryptol.Eval.Monad
(
Eval(..)
, runEval
, EvalOpts(..)
, getEvalOpts
, PPOpts(..)
, io
, delay
, delayFill
, ready
, blackhole
, EvalError(..)
, evalPanic
, typeCannotBeDemoted
, divideByZero
, negativeExponent
, logNegative
, wordTooWide
, cryUserError
, cryLoopError
, cryNoPrimError
, invalidIndex
) where
import Control.DeepSeq
import Control.Monad
import Control.Monad.Fix
import Control.Monad.IO.Class
import Data.IORef
import Data.Typeable (Typeable)
import qualified Control.Exception as X
import Cryptol.Utils.Panic
import Cryptol.Utils.PP
import Cryptol.Utils.Logger(Logger)
import Cryptol.TypeCheck.AST(Type,Name)
ready :: a -> Eval a
ready :: a -> Eval a
ready a :: a
a = a -> Eval a
forall a. a -> Eval a
Ready a
a
data PPOpts = PPOpts
{ PPOpts -> Bool
useAscii :: Bool
, PPOpts -> Int
useBase :: Int
, PPOpts -> Int
useInfLength :: Int
}
data EvalOpts = EvalOpts
{ EvalOpts -> Logger
evalLogger :: Logger
, EvalOpts -> PPOpts
evalPPOpts :: PPOpts
}
data Eval a
= Ready !a
| Thunk !(EvalOpts -> IO a)
data ThunkState a
= Unforced
| BlackHole
| Forced !(Either EvalError a)
getEvalOpts :: Eval EvalOpts
getEvalOpts :: Eval EvalOpts
getEvalOpts = (EvalOpts -> IO EvalOpts) -> Eval EvalOpts
forall a. (EvalOpts -> IO a) -> Eval a
Thunk EvalOpts -> IO EvalOpts
forall (m :: * -> *) a. Monad m => a -> m a
return
{-# INLINE delay #-}
delay :: Maybe String
-> Eval a
-> Eval (Eval a)
delay :: Maybe String -> Eval a -> Eval (Eval a)
delay _ (Ready a :: a
a) = Eval a -> Eval (Eval a)
forall a. a -> Eval a
Ready (a -> Eval a
forall a. a -> Eval a
Ready a
a)
delay msg :: Maybe String
msg (Thunk x :: EvalOpts -> IO a
x) = (EvalOpts -> IO (Eval a)) -> Eval (Eval a)
forall a. (EvalOpts -> IO a) -> Eval a
Thunk ((EvalOpts -> IO (Eval a)) -> Eval (Eval a))
-> (EvalOpts -> IO (Eval a)) -> Eval (Eval a)
forall a b. (a -> b) -> a -> b
$ \opts :: EvalOpts
opts -> do
let msg' :: String
msg' = String -> (String -> String) -> Maybe String -> String
forall b a. b -> (a -> b) -> Maybe a -> b
maybe "" ("while evaluating "String -> String -> String
forall a. [a] -> [a] -> [a]
++) Maybe String
msg
let retry :: Eval a
retry = String -> Eval a
forall a. String -> Eval a
cryLoopError String
msg'
IORef (ThunkState a)
r <- ThunkState a -> IO (IORef (ThunkState a))
forall a. a -> IO (IORef a)
newIORef ThunkState a
forall a. ThunkState a
Unforced
Eval a -> IO (Eval a)
forall (m :: * -> *) a. Monad m => a -> m a
return (Eval a -> IO (Eval a)) -> Eval a -> IO (Eval a)
forall a b. (a -> b) -> a -> b
$ Eval a -> IORef (ThunkState a) -> IO a -> Eval a
forall a. Eval a -> IORef (ThunkState a) -> IO a -> Eval a
unDelay Eval a
forall a. Eval a
retry IORef (ThunkState a)
r (EvalOpts -> IO a
x EvalOpts
opts)
{-# INLINE delayFill #-}
delayFill :: Eval a
-> Eval a
-> Eval (Eval a)
delayFill :: Eval a -> Eval a -> Eval (Eval a)
delayFill (Ready x :: a
x) _ = Eval a -> Eval (Eval a)
forall a. a -> Eval a
Ready (a -> Eval a
forall a. a -> Eval a
Ready a
x)
delayFill (Thunk x :: EvalOpts -> IO a
x) retry :: Eval a
retry = (EvalOpts -> IO (Eval a)) -> Eval (Eval a)
forall a. (EvalOpts -> IO a) -> Eval a
Thunk ((EvalOpts -> IO (Eval a)) -> Eval (Eval a))
-> (EvalOpts -> IO (Eval a)) -> Eval (Eval a)
forall a b. (a -> b) -> a -> b
$ \opts :: EvalOpts
opts -> do
IORef (ThunkState a)
r <- ThunkState a -> IO (IORef (ThunkState a))
forall a. a -> IO (IORef a)
newIORef ThunkState a
forall a. ThunkState a
Unforced
Eval a -> IO (Eval a)
forall (m :: * -> *) a. Monad m => a -> m a
return (Eval a -> IO (Eval a)) -> Eval a -> IO (Eval a)
forall a b. (a -> b) -> a -> b
$ Eval a -> IORef (ThunkState a) -> IO a -> Eval a
forall a. Eval a -> IORef (ThunkState a) -> IO a -> Eval a
unDelay Eval a
retry IORef (ThunkState a)
r (EvalOpts -> IO a
x EvalOpts
opts)
blackhole :: String
-> Eval (Eval a, Eval a -> Eval ())
blackhole :: String -> Eval (Eval a, Eval a -> Eval ())
blackhole msg :: String
msg = do
IORef (Eval a)
r <- IO (IORef (Eval a)) -> Eval (IORef (Eval a))
forall a. IO a -> Eval a
io (IO (IORef (Eval a)) -> Eval (IORef (Eval a)))
-> IO (IORef (Eval a)) -> Eval (IORef (Eval a))
forall a b. (a -> b) -> a -> b
$ Eval a -> IO (IORef (Eval a))
forall a. a -> IO (IORef a)
newIORef (String -> Eval a
forall (m :: * -> *) a. MonadFail m => String -> m a
fail String
msg)
let get :: Eval a
get = Eval (Eval a) -> Eval a
forall (m :: * -> *) a. Monad m => m (m a) -> m a
join (IO (Eval a) -> Eval (Eval a)
forall a. IO a -> Eval a
io (IO (Eval a) -> Eval (Eval a)) -> IO (Eval a) -> Eval (Eval a)
forall a b. (a -> b) -> a -> b
$ IORef (Eval a) -> IO (Eval a)
forall a. IORef a -> IO a
readIORef IORef (Eval a)
r)
let set :: Eval a -> Eval ()
set = IO () -> Eval ()
forall a. IO a -> Eval a
io (IO () -> Eval ()) -> (Eval a -> IO ()) -> Eval a -> Eval ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. IORef (Eval a) -> Eval a -> IO ()
forall a. IORef a -> a -> IO ()
writeIORef IORef (Eval a)
r
(Eval a, Eval a -> Eval ()) -> Eval (Eval a, Eval a -> Eval ())
forall (m :: * -> *) a. Monad m => a -> m a
return (Eval a
get, Eval a -> Eval ()
set)
unDelay :: Eval a -> IORef (ThunkState a) -> IO a -> Eval a
unDelay :: Eval a -> IORef (ThunkState a) -> IO a -> Eval a
unDelay retry :: Eval a
retry r :: IORef (ThunkState a)
r x :: IO a
x = do
ThunkState a
rval <- IO (ThunkState a) -> Eval (ThunkState a)
forall a. IO a -> Eval a
io (IO (ThunkState a) -> Eval (ThunkState a))
-> IO (ThunkState a) -> Eval (ThunkState a)
forall a b. (a -> b) -> a -> b
$ IORef (ThunkState a) -> IO (ThunkState a)
forall a. IORef a -> IO a
readIORef IORef (ThunkState a)
r
case ThunkState a
rval of
Forced val :: Either EvalError a
val -> IO a -> Eval a
forall a. IO a -> Eval a
io (Either EvalError a -> IO a
forall e a. Exception e => Either e a -> IO a
toVal Either EvalError a
val)
BlackHole ->
Eval a
retry
Unforced -> IO a -> Eval a
forall a. IO a -> Eval a
io (IO a -> Eval a) -> IO a -> Eval a
forall a b. (a -> b) -> a -> b
$ do
IORef (ThunkState a) -> ThunkState a -> IO ()
forall a. IORef a -> a -> IO ()
writeIORef IORef (ThunkState a)
r ThunkState a
forall a. ThunkState a
BlackHole
Either EvalError a
val <- IO a -> IO (Either EvalError a)
forall e a. Exception e => IO a -> IO (Either e a)
X.try IO a
x
IORef (ThunkState a) -> ThunkState a -> IO ()
forall a. IORef a -> a -> IO ()
writeIORef IORef (ThunkState a)
r (Either EvalError a -> ThunkState a
forall a. Either EvalError a -> ThunkState a
Forced Either EvalError a
val)
Either EvalError a -> IO a
forall e a. Exception e => Either e a -> IO a
toVal Either EvalError a
val
where
toVal :: Either e a -> IO a
toVal mbV :: Either e a
mbV = case Either e a
mbV of
Right a :: a
a -> a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure a
a
Left e :: e
e -> e -> IO a
forall e a. Exception e => e -> IO a
X.throwIO e
e
runEval :: EvalOpts -> Eval a -> IO a
runEval :: EvalOpts -> Eval a -> IO a
runEval _ (Ready a :: a
a) = a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return a
a
runEval opts :: EvalOpts
opts (Thunk x :: EvalOpts -> IO a
x) = EvalOpts -> IO a
x EvalOpts
opts
{-# INLINE evalBind #-}
evalBind :: Eval a -> (a -> Eval b) -> Eval b
evalBind :: Eval a -> (a -> Eval b) -> Eval b
evalBind (Ready a :: a
a) f :: a -> Eval b
f = a -> Eval b
f a
a
evalBind (Thunk x :: EvalOpts -> IO a
x) f :: a -> Eval b
f = (EvalOpts -> IO b) -> Eval b
forall a. (EvalOpts -> IO a) -> Eval a
Thunk ((EvalOpts -> IO b) -> Eval b) -> (EvalOpts -> IO b) -> Eval b
forall a b. (a -> b) -> a -> b
$ \opts :: EvalOpts
opts -> EvalOpts -> IO a
x EvalOpts
opts IO a -> (a -> IO b) -> IO b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= EvalOpts -> Eval b -> IO b
forall a. EvalOpts -> Eval a -> IO a
runEval EvalOpts
opts (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 f :: a -> b
f (Ready x :: a
x) = b -> Eval b
forall a. a -> Eval a
Ready (a -> b
f a
x)
fmap f :: a -> b
f (Thunk m :: EvalOpts -> IO a
m) = (EvalOpts -> IO b) -> Eval b
forall a. (EvalOpts -> IO a) -> Eval a
Thunk ((EvalOpts -> IO b) -> Eval b) -> (EvalOpts -> IO b) -> Eval b
forall a b. (a -> b) -> a -> b
$ \opts :: EvalOpts
opts -> a -> b
f (a -> b) -> IO a -> IO b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> EvalOpts -> IO a
m EvalOpts
opts
{-# 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 MonadFail Eval where
fail :: String -> Eval a
fail x :: String
x = (EvalOpts -> IO a) -> Eval a
forall a. (EvalOpts -> IO a) -> Eval a
Thunk (\_ -> String -> IO a
forall (m :: * -> *) a. MonadFail m => String -> m a
fail String
x)
instance MonadIO Eval where
liftIO :: IO a -> Eval a
liftIO = IO a -> Eval a
forall a. IO a -> Eval a
io
instance NFData a => NFData (Eval a) where
rnf :: Eval a -> ()
rnf (Ready a :: a
a) = a -> ()
forall a. NFData a => a -> ()
rnf a
a
rnf (Thunk _) = ()
instance MonadFix Eval where
mfix :: (a -> Eval a) -> Eval a
mfix f :: a -> Eval a
f = (EvalOpts -> IO a) -> Eval a
forall a. (EvalOpts -> IO a) -> Eval a
Thunk ((EvalOpts -> IO a) -> Eval a) -> (EvalOpts -> IO a) -> Eval a
forall a b. (a -> b) -> a -> b
$ \opts :: EvalOpts
opts -> (a -> IO a) -> IO a
forall (m :: * -> *) a. MonadFix m => (a -> m a) -> m a
mfix (\x :: a
x -> EvalOpts -> Eval a -> IO a
forall a. EvalOpts -> Eval a -> IO a
runEval EvalOpts
opts (a -> Eval a
f a
x))
io :: IO a -> Eval a
io :: IO a -> Eval a
io m :: IO a
m = (EvalOpts -> IO a) -> Eval a
forall a. (EvalOpts -> IO a) -> Eval a
Thunk (\_ -> IO a
m)
{-# INLINE io #-}
evalPanic :: HasCallStack => String -> [String] -> a
evalPanic :: String -> [String] -> a
evalPanic cxt :: String
cxt = String -> [String] -> a
forall a. HasCallStack => String -> [String] -> a
panic ("[Eval] " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
cxt)
data EvalError
= InvalidIndex Integer
| TypeCannotBeDemoted Type
| DivideByZero
| NegativeExponent
| LogNegative
| WordTooWide Integer
| UserError String
| LoopError String
| NoPrim Name
deriving (Typeable,Int -> EvalError -> String -> String
[EvalError] -> String -> String
EvalError -> String
(Int -> EvalError -> String -> String)
-> (EvalError -> String)
-> ([EvalError] -> String -> String)
-> Show EvalError
forall a.
(Int -> a -> String -> String)
-> (a -> String) -> ([a] -> String -> String) -> Show a
showList :: [EvalError] -> String -> String
$cshowList :: [EvalError] -> String -> String
show :: EvalError -> String
$cshow :: EvalError -> String
showsPrec :: Int -> EvalError -> String -> String
$cshowsPrec :: Int -> EvalError -> String -> String
Show)
instance PP EvalError where
ppPrec :: Int -> EvalError -> Doc
ppPrec _ e :: EvalError
e = case EvalError
e of
InvalidIndex i :: Integer
i -> String -> Doc
text "invalid sequence index:" Doc -> Doc -> Doc
<+> Integer -> Doc
integer Integer
i
TypeCannotBeDemoted t :: Type
t -> String -> Doc
text "type cannot be demoted:" Doc -> Doc -> Doc
<+> Type -> Doc
forall a. PP a => a -> Doc
pp Type
t
DivideByZero -> String -> Doc
text "division by 0"
NegativeExponent -> String -> Doc
text "negative exponent"
LogNegative -> String -> Doc
text "logarithm of negative"
WordTooWide w :: Integer
w ->
String -> Doc
text "word too wide for memory:" Doc -> Doc -> Doc
<+> Integer -> Doc
integer Integer
w Doc -> Doc -> Doc
<+> String -> Doc
text "bits"
UserError x :: String
x -> String -> Doc
text "Run-time error:" Doc -> Doc -> Doc
<+> String -> Doc
text String
x
LoopError x :: String
x -> String -> Doc
text "<<loop>>" Doc -> Doc -> Doc
<+> String -> Doc
text String
x
NoPrim x :: Name
x -> String -> Doc
text "unimplemented primitive:" Doc -> Doc -> Doc
<+> Name -> Doc
forall a. PP a => a -> Doc
pp Name
x
instance X.Exception EvalError
typeCannotBeDemoted :: Type -> a
typeCannotBeDemoted :: Type -> a
typeCannotBeDemoted t :: Type
t = EvalError -> a
forall a e. Exception e => e -> a
X.throw (Type -> EvalError
TypeCannotBeDemoted Type
t)
divideByZero :: Eval a
divideByZero :: Eval a
divideByZero = IO a -> Eval a
forall a. IO a -> Eval a
io (EvalError -> IO a
forall e a. Exception e => e -> IO a
X.throwIO EvalError
DivideByZero)
negativeExponent :: Eval a
negativeExponent :: Eval a
negativeExponent = IO a -> Eval a
forall a. IO a -> Eval a
io (EvalError -> IO a
forall e a. Exception e => e -> IO a
X.throwIO EvalError
NegativeExponent)
logNegative :: Eval a
logNegative :: Eval a
logNegative = IO a -> Eval a
forall a. IO a -> Eval a
io (EvalError -> IO a
forall e a. Exception e => e -> IO a
X.throwIO EvalError
LogNegative)
wordTooWide :: Integer -> a
wordTooWide :: Integer -> a
wordTooWide w :: Integer
w = EvalError -> a
forall a e. Exception e => e -> a
X.throw (Integer -> EvalError
WordTooWide Integer
w)
cryUserError :: String -> Eval a
cryUserError :: String -> Eval a
cryUserError msg :: String
msg = IO a -> Eval a
forall a. IO a -> Eval a
io (EvalError -> IO a
forall e a. Exception e => e -> IO a
X.throwIO (String -> EvalError
UserError String
msg))
cryNoPrimError :: Name -> Eval a
cryNoPrimError :: Name -> Eval a
cryNoPrimError x :: Name
x = IO a -> Eval a
forall a. IO a -> Eval a
io (EvalError -> IO a
forall e a. Exception e => e -> IO a
X.throwIO (Name -> EvalError
NoPrim Name
x))
cryLoopError :: String -> Eval a
cryLoopError :: String -> Eval a
cryLoopError msg :: String
msg = IO a -> Eval a
forall a. IO a -> Eval a
io (EvalError -> IO a
forall e a. Exception e => e -> IO a
X.throwIO (String -> EvalError
LoopError String
msg))
invalidIndex :: Integer -> Eval a
invalidIndex :: Integer -> Eval a
invalidIndex i :: Integer
i = IO a -> Eval a
forall a. IO a -> Eval a
io (EvalError -> IO a
forall e a. Exception e => e -> IO a
X.throwIO (Integer -> EvalError
InvalidIndex Integer
i))