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