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

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

module Cryptol.Eval.Monad
( -- * Evaluation monad
  Eval(..)
, runEval
, EvalOpts(..)
, getEvalOpts
, PPOpts(..)
, io
, delay
, delayFill
, ready
, blackhole
  -- * Error reporting
, 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)

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

-- | How to pretty print things when evaluating
data PPOpts = PPOpts
  { PPOpts -> Bool
useAscii     :: Bool
  , PPOpts -> Int
useBase      :: Int
  , PPOpts -> Int
useInfLength :: Int
  }

-- | Some options for evalutaion
data EvalOpts = EvalOpts
  { EvalOpts -> Logger
evalLogger :: Logger    -- ^ Where to print stuff (e.g., for @trace@)
  , EvalOpts -> PPOpts
evalPPOpts :: PPOpts    -- ^ How to pretty print things.
  }


-- | The monad for Cryptol evaluation.
data Eval a
   = Ready !a
   | Thunk !(EvalOpts -> IO a)

data ThunkState a
  = Unforced        -- ^ This thunk has not yet been forced
  | BlackHole       -- ^ This thunk is currently being evaluated
  | Forced !(Either EvalError a)
    -- ^ This thunk has previously been forced,
    -- and has the given value, or evaluation resulted in an error.


-- | Access the evaluation options.
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 the given evaluation computation, returning a thunk
--   which will run the computation when forced.  Raise a loop
--   error if the resulting thunk is forced during its own evaluation.
delay :: Maybe String     -- ^ Optional name to print if a loop is detected
      -> Eval a           -- ^ Computation to delay
      -> 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 #-}

-- | 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
          -> Eval a        -- ^ Backup computation to run if a tight loop is detected
          -> 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)

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

-- | Execute the given evaluation action.
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))

-- | Lift an 'IO' computation into the 'Eval' monad.
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 #-}


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

-- | Panic from an @Eval@ context.
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 type describing errors that can occur during evaluation.
data EvalError
  = InvalidIndex Integer          -- ^ Out-of-bounds index
  | TypeCannotBeDemoted Type      -- ^ Non-numeric type passed to @number@ function
  | DivideByZero                  -- ^ Division or modulus by 0
  | NegativeExponent              -- ^ Exponentiation by negative integer
  | LogNegative                   -- ^ Logarithm of a negative integer
  | WordTooWide Integer           -- ^ Bitvector too large
  | UserError String              -- ^ Call to the Cryptol @error@ primitive
  | LoopError String              -- ^ Detectable nontermination
  | NoPrim Name                   -- ^ Primitive with no implementation
    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

-- | For things like @`(inf)@ or @`(0-1)@.
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)

-- | For division by 0.
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)

-- | For exponentiation by a negative integer.
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)

-- | For logarithm of a negative integer.
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)

-- | 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 w :: Integer
w = EvalError -> a
forall a e. Exception e => e -> a
X.throw (Integer -> EvalError
WordTooWide Integer
w)

-- | For the Cryptol @error@ function.
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))

-- | For cases where we can detect tight loops.
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))

-- | A sequencing operation has gotten an invalid index.
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))