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

{-# LANGUAGE DeriveDataTypeable #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE PatternGuards #-}
{-# LANGUAGE RecordWildCards #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE ViewPatterns #-}
{-# LANGUAGE FlexibleInstances #-}

module Cryptol.REPL.Monad (
    -- * REPL Monad
    REPL(..), runREPL
  , io
  , raise
  , stop
  , catch
  , finally
  , rPutStrLn
  , rPutStr
  , rPrint

    -- ** Errors
  , REPLException(..)
  , rethrowEvalError

    -- ** Environment
  , getFocusedEnv
  , getModuleEnv, setModuleEnv
  , getDynEnv, setDynEnv
  , uniqify, freshName
  , getTSyns, getNewtypes, getVars
  , whenDebug
  , getExprNames
  , getTypeNames
  , getPropertyNames
  , getModNames
  , LoadedModule(..), getLoadedMod, setLoadedMod, clearLoadedMod
  , setEditPath, getEditPath, clearEditPath
  , setSearchPath, prependSearchPath
  , getPrompt
  , shouldContinue
  , unlessBatch
  , asBatch
  , disableLet
  , enableLet
  , getLetEnabled
  , validEvalContext
  , updateREPLTitle
  , setUpdateREPLTitle

    -- ** Config Options
  , EnvVal(..)
  , OptionDescr(..)
  , setUser, getUser, getKnownUser, tryGetUser
  , userOptions
  , getUserSatNum
  , getUserShowProverStats
  , getUserProverValidate

    -- ** Configurable Output
  , getPutStr
  , getLogger
  , setPutStr

    -- ** Smoke Test
  , smokeTest
  , Smoke(..)

  ) where

import Cryptol.REPL.Trie

import Cryptol.Eval (EvalError)
import qualified Cryptol.ModuleSystem as M
import qualified Cryptol.ModuleSystem.Env as M
import qualified Cryptol.ModuleSystem.Name as M
import qualified Cryptol.ModuleSystem.NamingEnv as M
import Cryptol.Parser (ParseError,ppError)
import Cryptol.Parser.NoInclude (IncludeError,ppIncludeError)
import Cryptol.Parser.NoPat (Error)
import Cryptol.Parser.Position (emptyRange, Range(from))
import qualified Cryptol.TypeCheck.AST as T
import qualified Cryptol.TypeCheck as T
import qualified Cryptol.IR.FreeVars as T
import qualified Cryptol.Utils.Ident as I
import Cryptol.Utils.PP
import Cryptol.Utils.Panic (panic)
import Cryptol.Utils.Logger(Logger, logPutStr, funLogger)
import qualified Cryptol.Parser.AST as P
import Cryptol.Symbolic (proverNames, lookupProver, SatNum(..))

import Control.Monad (ap,unless,when)
import Control.Monad.Base
import Control.Monad.IO.Class
import Control.Monad.Trans.Control
import Data.Char (isSpace)
import Data.IORef
    (IORef,newIORef,readIORef,modifyIORef,atomicModifyIORef)
import Data.List (intercalate, isPrefixOf, unfoldr, sortBy)
import Data.Maybe (catMaybes)
import Data.Ord (comparing)
import Data.Typeable (Typeable)
import System.Directory (findExecutable)
import qualified Control.Exception as X
import qualified Data.Map as Map
import qualified Data.Set as Set
import Text.Read (readMaybe)

import Data.SBV.Dynamic (sbvCheckSolverInstallation)

import Prelude ()
import Prelude.Compat

-- REPL Environment ------------------------------------------------------------

-- | This indicates what the user would like to work on.
data LoadedModule = LoadedModule
  { LoadedModule -> Maybe ModName
lName :: Maybe P.ModName  -- ^ Working on this module.
  , LoadedModule -> ModulePath
lPath :: M.ModulePath     -- ^ Working on this file.
  }

-- | REPL RW Environment.
data RW = RW
  { RW -> Maybe LoadedModule
eLoadedMod   :: Maybe LoadedModule
    -- ^ This is the name of the currently "focused" module.
    -- This is what we reload (:r)

  , RW -> Maybe FilePath
eEditFile :: Maybe FilePath
    -- ^ This is what we edit (:e)

  , RW -> Bool
eContinue    :: Bool
    -- ^ Should we keep going when we encounter an error, or give up.

  , RW -> Bool
eIsBatch     :: Bool
    -- ^ Are we in batch mode.

  , RW -> ModuleEnv
eModuleEnv   :: M.ModuleEnv
    -- ^ The current environment of all things loaded.

  , RW -> UserEnv
eUserEnv     :: UserEnv
    -- ^ User settings

  , RW -> Logger
eLogger      :: Logger
    -- ^ Use this to send messages to the user

  , RW -> Bool
eLetEnabled  :: Bool
    -- ^ Should we allow `let` on the command line

  , RW -> REPL ()
eUpdateTitle :: REPL ()
    -- ^ Execute this every time we load a module.
    -- This is used to change the title of terminal when loading a module.
  }

-- | Initial, empty environment.
defaultRW :: Bool -> Logger -> IO RW
defaultRW :: Bool -> Logger -> IO RW
defaultRW isBatch :: Bool
isBatch l :: Logger
l = do
  ModuleEnv
env <- IO ModuleEnv
M.initialModuleEnv
  RW -> IO RW
forall (m :: * -> *) a. Monad m => a -> m a
return RW :: Maybe LoadedModule
-> Maybe FilePath
-> Bool
-> Bool
-> ModuleEnv
-> UserEnv
-> Logger
-> Bool
-> REPL ()
-> RW
RW
    { eLoadedMod :: Maybe LoadedModule
eLoadedMod   = Maybe LoadedModule
forall a. Maybe a
Nothing
    , eEditFile :: Maybe FilePath
eEditFile    = Maybe FilePath
forall a. Maybe a
Nothing
    , eContinue :: Bool
eContinue    = Bool
True
    , eIsBatch :: Bool
eIsBatch     = Bool
isBatch
    , eModuleEnv :: ModuleEnv
eModuleEnv   = ModuleEnv
env
    , eUserEnv :: UserEnv
eUserEnv     = OptionMap -> UserEnv
mkUserEnv OptionMap
userOptions
    , eLogger :: Logger
eLogger      = Logger
l
    , eLetEnabled :: Bool
eLetEnabled  = Bool
True
    , eUpdateTitle :: REPL ()
eUpdateTitle = () -> REPL ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
    }

-- | Build up the prompt for the REPL.
mkPrompt :: RW -> String
mkPrompt :: RW -> FilePath
mkPrompt rw :: RW
rw
  | RW -> Bool
eIsBatch RW
rw = ""
  | Bool
detailedPrompt = FilePath
withEdit FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ "> "
  | Bool
otherwise      = FilePath
modLn FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ "> "
  where
  detailedPrompt :: Bool
detailedPrompt = Bool
False

  modLn :: FilePath
modLn   =
    case LoadedModule -> Maybe ModName
lName (LoadedModule -> Maybe ModName)
-> Maybe LoadedModule -> Maybe ModName
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< RW -> Maybe LoadedModule
eLoadedMod RW
rw of
      Nothing -> Doc -> FilePath
forall a. Show a => a -> FilePath
show (ModName -> Doc
forall a. PP a => a -> Doc
pp ModName
I.preludeName)
      Just m :: ModName
m
        | ModName -> LoadedModules -> Bool
M.isLoadedParamMod ModName
m (ModuleEnv -> LoadedModules
M.meLoadedModules (RW -> ModuleEnv
eModuleEnv RW
rw)) ->
                 FilePath
modName FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ "(parameterized)"
        | Bool
otherwise -> FilePath
modName
        where modName :: FilePath
modName = ModName -> FilePath
forall a. PP a => a -> FilePath
pretty ModName
m

  withFocus :: FilePath
withFocus =
    case RW -> Maybe LoadedModule
eLoadedMod RW
rw of
      Nothing -> FilePath
modLn
      Just m :: LoadedModule
m ->
        case (LoadedModule -> Maybe ModName
lName LoadedModule
m, LoadedModule -> ModulePath
lPath LoadedModule
m) of
          (Nothing, M.InFile f :: FilePath
f) -> ":r to reload " FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ FilePath -> FilePath
forall a. Show a => a -> FilePath
show FilePath
f FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ "\n" FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ FilePath
modLn
          _ -> FilePath
modLn

  withEdit :: FilePath
withEdit =
    case RW -> Maybe FilePath
eEditFile RW
rw of
      Nothing -> FilePath
withFocus
      Just e :: FilePath
e
        | Just (M.InFile f :: FilePath
f) <- LoadedModule -> ModulePath
lPath (LoadedModule -> ModulePath)
-> Maybe LoadedModule -> Maybe ModulePath
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> RW -> Maybe LoadedModule
eLoadedMod RW
rw
        , FilePath
f FilePath -> FilePath -> Bool
forall a. Eq a => a -> a -> Bool
== FilePath
e -> FilePath
withFocus
        | Bool
otherwise -> ":e to edit " FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ FilePath
e FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ "\n" FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ FilePath
withFocus



-- REPL Monad ------------------------------------------------------------------

-- | REPL_ context with InputT handling.
newtype REPL a = REPL { REPL a -> IORef RW -> IO a
unREPL :: IORef RW -> IO a }

-- | Run a REPL action with a fresh environment.
runREPL :: Bool -> Logger -> REPL a -> IO a
runREPL :: Bool -> Logger -> REPL a -> IO a
runREPL isBatch :: Bool
isBatch l :: Logger
l m :: REPL a
m = do
  IORef RW
ref <- RW -> IO (IORef RW)
forall a. a -> IO (IORef a)
newIORef (RW -> IO (IORef RW)) -> IO RW -> IO (IORef RW)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Bool -> Logger -> IO RW
defaultRW Bool
isBatch Logger
l
  REPL a -> IORef RW -> IO a
forall a. REPL a -> IORef RW -> IO a
unREPL REPL a
m IORef RW
ref

instance Functor REPL where
  {-# INLINE fmap #-}
  fmap :: (a -> b) -> REPL a -> REPL b
fmap f :: a -> b
f m :: REPL a
m = (IORef RW -> IO b) -> REPL b
forall a. (IORef RW -> IO a) -> REPL a
REPL (\ ref :: IORef RW
ref -> (a -> b) -> IO a -> IO b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap a -> b
f (REPL a -> IORef RW -> IO a
forall a. REPL a -> IORef RW -> IO a
unREPL REPL a
m IORef RW
ref))

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

instance Monad REPL where
  {-# INLINE return #-}
  return :: a -> REPL a
return x :: a
x = (IORef RW -> IO a) -> REPL a
forall a. (IORef RW -> IO a) -> REPL a
REPL (\_ -> a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return a
x)

  {-# INLINE (>>=) #-}
  m :: REPL a
m >>= :: REPL a -> (a -> REPL b) -> REPL b
>>= f :: a -> REPL b
f = (IORef RW -> IO b) -> REPL b
forall a. (IORef RW -> IO a) -> REPL a
REPL ((IORef RW -> IO b) -> REPL b) -> (IORef RW -> IO b) -> REPL b
forall a b. (a -> b) -> a -> b
$ \ref :: IORef RW
ref -> do
    a
x <- REPL a -> IORef RW -> IO a
forall a. REPL a -> IORef RW -> IO a
unREPL REPL a
m IORef RW
ref
    REPL b -> IORef RW -> IO b
forall a. REPL a -> IORef RW -> IO a
unREPL (a -> REPL b
f a
x) IORef RW
ref

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

instance MonadBase IO REPL where
  liftBase :: IO α -> REPL α
liftBase = IO α -> REPL α
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO

instance MonadBaseControl IO REPL where
  type StM REPL a = a
  liftBaseWith :: (RunInBase REPL IO -> IO a) -> REPL a
liftBaseWith f :: RunInBase REPL IO -> IO a
f = (IORef RW -> IO a) -> REPL a
forall a. (IORef RW -> IO a) -> REPL a
REPL ((IORef RW -> IO a) -> REPL a) -> (IORef RW -> IO a) -> REPL a
forall a b. (a -> b) -> a -> b
$ \ref :: IORef RW
ref ->
    RunInBase REPL IO -> IO a
f (RunInBase REPL IO -> IO a) -> RunInBase REPL IO -> IO a
forall a b. (a -> b) -> a -> b
$ \m :: REPL a
m -> REPL a -> IORef RW -> IO a
forall a. REPL a -> IORef RW -> IO a
unREPL REPL a
m IORef RW
ref
  restoreM :: StM REPL a -> REPL a
restoreM x :: StM REPL a
x = a -> REPL a
forall (m :: * -> *) a. Monad m => a -> m a
return a
StM REPL a
x

instance M.FreshM REPL where
  liftSupply :: (Supply -> (a, Supply)) -> REPL a
liftSupply f :: Supply -> (a, Supply)
f = (RW -> (RW, a)) -> REPL a
forall a. (RW -> (RW, a)) -> REPL a
modifyRW ((RW -> (RW, a)) -> REPL a) -> (RW -> (RW, a)) -> REPL a
forall a b. (a -> b) -> a -> b
$ \ RW { .. } ->
    let (a :: a
a,s' :: Supply
s') = Supply -> (a, Supply)
f (ModuleEnv -> Supply
M.meSupply ModuleEnv
eModuleEnv)
     in (RW :: Maybe LoadedModule
-> Maybe FilePath
-> Bool
-> Bool
-> ModuleEnv
-> UserEnv
-> Logger
-> Bool
-> REPL ()
-> RW
RW { eModuleEnv :: ModuleEnv
eModuleEnv = ModuleEnv
eModuleEnv { meSupply :: Supply
M.meSupply = Supply
s' }, .. },a
a)

-- Exceptions ------------------------------------------------------------------

-- | REPL exceptions.
data REPLException
  = ParseError ParseError
  | FileNotFound FilePath
  | DirectoryNotFound FilePath
  | NoPatError [Error]
  | NoIncludeError [IncludeError]
  | EvalError EvalError
  | ModuleSystemError NameDisp M.ModuleError
  | EvalPolyError T.Schema
  | TypeNotTestable T.Type
  | EvalInParamModule [M.Name]
  | SBVError String
    deriving (Int -> REPLException -> FilePath -> FilePath
[REPLException] -> FilePath -> FilePath
REPLException -> FilePath
(Int -> REPLException -> FilePath -> FilePath)
-> (REPLException -> FilePath)
-> ([REPLException] -> FilePath -> FilePath)
-> Show REPLException
forall a.
(Int -> a -> FilePath -> FilePath)
-> (a -> FilePath) -> ([a] -> FilePath -> FilePath) -> Show a
showList :: [REPLException] -> FilePath -> FilePath
$cshowList :: [REPLException] -> FilePath -> FilePath
show :: REPLException -> FilePath
$cshow :: REPLException -> FilePath
showsPrec :: Int -> REPLException -> FilePath -> FilePath
$cshowsPrec :: Int -> REPLException -> FilePath -> FilePath
Show,Typeable)

instance X.Exception REPLException

instance PP REPLException where
  ppPrec :: Int -> REPLException -> Doc
ppPrec _ re :: REPLException
re = case REPLException
re of
    ParseError e :: ParseError
e         -> ParseError -> Doc
ppError ParseError
e
    FileNotFound path :: FilePath
path    -> [Doc] -> Doc
sep [ FilePath -> Doc
text "File"
                                , FilePath -> Doc
text ("`" FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ FilePath
path FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ "'")
                                , FilePath -> Doc
text"not found"
                                ]
    DirectoryNotFound path :: FilePath
path -> [Doc] -> Doc
sep [ FilePath -> Doc
text "Directory"
                                  , FilePath -> Doc
text ("`" FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ FilePath
path FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ "'")
                                  , FilePath -> Doc
text"not found or not a directory"
                                  ]
    NoPatError es :: [Error]
es        -> [Doc] -> Doc
vcat ((Error -> Doc) -> [Error] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map Error -> Doc
forall a. PP a => a -> Doc
pp [Error]
es)
    NoIncludeError es :: [IncludeError]
es    -> [Doc] -> Doc
vcat ((IncludeError -> Doc) -> [IncludeError] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map IncludeError -> Doc
ppIncludeError [IncludeError]
es)
    ModuleSystemError ns :: NameDisp
ns me :: ModuleError
me -> NameDisp -> Doc -> Doc
fixNameDisp NameDisp
ns (ModuleError -> Doc
forall a. PP a => a -> Doc
pp ModuleError
me)
    EvalError e :: EvalError
e          -> EvalError -> Doc
forall a. PP a => a -> Doc
pp EvalError
e
    EvalPolyError s :: Schema
s      -> FilePath -> Doc
text "Cannot evaluate polymorphic value."
                         Doc -> Doc -> Doc
$$ FilePath -> Doc
text "Type:" Doc -> Doc -> Doc
<+> Schema -> Doc
forall a. PP a => a -> Doc
pp Schema
s
    TypeNotTestable t :: Type
t    -> FilePath -> Doc
text "The expression is not of a testable type."
                         Doc -> Doc -> Doc
$$ FilePath -> Doc
text "Type:" Doc -> Doc -> Doc
<+> Type -> Doc
forall a. PP a => a -> Doc
pp Type
t
    EvalInParamModule xs :: [Name]
xs ->
      FilePath -> Doc
text "Expression depends on definitions from a parameterized module:"
        Doc -> Doc -> Doc
$$ Int -> Doc -> Doc
nest 2 ([Doc] -> Doc
vcat ((Name -> Doc) -> [Name] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map Name -> Doc
forall a. PP a => a -> Doc
pp [Name]
xs))
    SBVError s :: FilePath
s           -> FilePath -> Doc
text "SBV error:" Doc -> Doc -> Doc
$$ FilePath -> Doc
text FilePath
s

-- | Raise an exception.
raise :: REPLException -> REPL a
raise :: REPLException -> REPL a
raise exn :: REPLException
exn = IO a -> REPL a
forall a. IO a -> REPL a
io (REPLException -> IO a
forall e a. Exception e => e -> IO a
X.throwIO REPLException
exn)


catch :: REPL a -> (REPLException -> REPL a) -> REPL a
catch :: REPL a -> (REPLException -> REPL a) -> REPL a
catch m :: REPL a
m k :: REPLException -> REPL a
k = (IORef RW -> IO a) -> REPL a
forall a. (IORef RW -> IO a) -> REPL a
REPL (\ ref :: IORef RW
ref -> IO a -> IO a
forall a. IO a -> IO a
rethrowEvalError (REPL a -> IORef RW -> IO a
forall a. REPL a -> IORef RW -> IO a
unREPL REPL a
m IORef RW
ref) IO a -> (REPLException -> IO a) -> IO a
forall e a. Exception e => IO a -> (e -> IO a) -> IO a
`X.catch` \ e :: REPLException
e -> REPL a -> IORef RW -> IO a
forall a. REPL a -> IORef RW -> IO a
unREPL (REPLException -> REPL a
k REPLException
e) IORef RW
ref)

finally :: REPL a -> REPL b -> REPL a
finally :: REPL a -> REPL b -> REPL a
finally m1 :: REPL a
m1 m2 :: REPL b
m2 = (IORef RW -> IO a) -> REPL a
forall a. (IORef RW -> IO a) -> REPL a
REPL (\ref :: IORef RW
ref -> REPL a -> IORef RW -> IO a
forall a. REPL a -> IORef RW -> IO a
unREPL REPL a
m1 IORef RW
ref IO a -> IO b -> IO a
forall a b. IO a -> IO b -> IO a
`X.finally` REPL b -> IORef RW -> IO b
forall a. REPL a -> IORef RW -> IO a
unREPL REPL b
m2 IORef RW
ref)


rethrowEvalError :: IO a -> IO a
rethrowEvalError :: IO a -> IO a
rethrowEvalError m :: IO a
m = IO a
run IO a -> (EvalError -> IO a) -> IO a
forall e a. Exception e => IO a -> (e -> IO a) -> IO a
`X.catch` EvalError -> IO a
forall a. EvalError -> IO a
rethrow
  where
  run :: IO a
run = do
    a
a <- IO a
m
    a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (a -> IO a) -> a -> IO a
forall a b. (a -> b) -> a -> b
$! a
a

  rethrow :: EvalError -> IO a
  rethrow :: EvalError -> IO a
rethrow exn :: EvalError
exn = REPLException -> IO a
forall e a. Exception e => e -> IO a
X.throwIO (EvalError -> REPLException
EvalError EvalError
exn)




-- Primitives ------------------------------------------------------------------


io :: IO a -> REPL a
io :: IO a -> REPL a
io m :: IO a
m = (IORef RW -> IO a) -> REPL a
forall a. (IORef RW -> IO a) -> REPL a
REPL (\ _ -> IO a
m)

getRW :: REPL RW
getRW :: REPL RW
getRW  = (IORef RW -> IO RW) -> REPL RW
forall a. (IORef RW -> IO a) -> REPL a
REPL IORef RW -> IO RW
forall a. IORef a -> IO a
readIORef

modifyRW :: (RW -> (RW,a)) -> REPL a
modifyRW :: (RW -> (RW, a)) -> REPL a
modifyRW f :: RW -> (RW, a)
f = (IORef RW -> IO a) -> REPL a
forall a. (IORef RW -> IO a) -> REPL a
REPL (\ ref :: IORef RW
ref -> IORef RW -> (RW -> (RW, a)) -> IO a
forall a b. IORef a -> (a -> (a, b)) -> IO b
atomicModifyIORef IORef RW
ref RW -> (RW, a)
f)

modifyRW_ :: (RW -> RW) -> REPL ()
modifyRW_ :: (RW -> RW) -> REPL ()
modifyRW_ f :: RW -> RW
f = (IORef RW -> IO ()) -> REPL ()
forall a. (IORef RW -> IO a) -> REPL a
REPL (\ ref :: IORef RW
ref -> IORef RW -> (RW -> RW) -> IO ()
forall a. IORef a -> (a -> a) -> IO ()
modifyIORef IORef RW
ref RW -> RW
f)

-- | Construct the prompt for the current environment.
getPrompt :: REPL String
getPrompt :: REPL FilePath
getPrompt  = RW -> FilePath
mkPrompt (RW -> FilePath) -> REPL RW -> REPL FilePath
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
`fmap` REPL RW
getRW

clearLoadedMod :: REPL ()
clearLoadedMod :: REPL ()
clearLoadedMod = do (RW -> RW) -> REPL ()
modifyRW_ (\rw :: RW
rw -> RW
rw { eLoadedMod :: Maybe LoadedModule
eLoadedMod = LoadedModule -> LoadedModule
upd (LoadedModule -> LoadedModule)
-> Maybe LoadedModule -> Maybe LoadedModule
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> RW -> Maybe LoadedModule
eLoadedMod RW
rw })
                    REPL ()
updateREPLTitle
  where upd :: LoadedModule -> LoadedModule
upd x :: LoadedModule
x = LoadedModule
x { lName :: Maybe ModName
lName = Maybe ModName
forall a. Maybe a
Nothing }

-- | Set the name of the currently focused file, loaded via @:r@.
setLoadedMod :: LoadedModule -> REPL ()
setLoadedMod :: LoadedModule -> REPL ()
setLoadedMod n :: LoadedModule
n = do
  (RW -> RW) -> REPL ()
modifyRW_ (\ rw :: RW
rw -> RW
rw { eLoadedMod :: Maybe LoadedModule
eLoadedMod = LoadedModule -> Maybe LoadedModule
forall a. a -> Maybe a
Just LoadedModule
n })
  REPL ()
updateREPLTitle

getLoadedMod :: REPL (Maybe LoadedModule)
getLoadedMod :: REPL (Maybe LoadedModule)
getLoadedMod  = RW -> Maybe LoadedModule
eLoadedMod (RW -> Maybe LoadedModule) -> REPL RW -> REPL (Maybe LoadedModule)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
`fmap` REPL RW
getRW



-- | Set the path for the ':e' command.
-- Note that this does not change the focused module (i.e., what ":r" reloads)
setEditPath :: FilePath -> REPL ()
setEditPath :: FilePath -> REPL ()
setEditPath p :: FilePath
p = (RW -> RW) -> REPL ()
modifyRW_ ((RW -> RW) -> REPL ()) -> (RW -> RW) -> REPL ()
forall a b. (a -> b) -> a -> b
$ \rw :: RW
rw -> RW
rw { eEditFile :: Maybe FilePath
eEditFile = FilePath -> Maybe FilePath
forall a. a -> Maybe a
Just FilePath
p }

getEditPath :: REPL (Maybe FilePath)
getEditPath :: REPL (Maybe FilePath)
getEditPath = RW -> Maybe FilePath
eEditFile (RW -> Maybe FilePath) -> REPL RW -> REPL (Maybe FilePath)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> REPL RW
getRW

clearEditPath :: REPL ()
clearEditPath :: REPL ()
clearEditPath = (RW -> RW) -> REPL ()
modifyRW_ ((RW -> RW) -> REPL ()) -> (RW -> RW) -> REPL ()
forall a b. (a -> b) -> a -> b
$ \rw :: RW
rw -> RW
rw { eEditFile :: Maybe FilePath
eEditFile = Maybe FilePath
forall a. Maybe a
Nothing }

setSearchPath :: [FilePath] -> REPL ()
setSearchPath :: [FilePath] -> REPL ()
setSearchPath path :: [FilePath]
path = do
  ModuleEnv
me <- REPL ModuleEnv
getModuleEnv
  ModuleEnv -> REPL ()
setModuleEnv (ModuleEnv -> REPL ()) -> ModuleEnv -> REPL ()
forall a b. (a -> b) -> a -> b
$ ModuleEnv
me { meSearchPath :: [FilePath]
M.meSearchPath = [FilePath]
path }

prependSearchPath :: [FilePath] -> REPL ()
prependSearchPath :: [FilePath] -> REPL ()
prependSearchPath path :: [FilePath]
path = do
  ModuleEnv
me <- REPL ModuleEnv
getModuleEnv
  ModuleEnv -> REPL ()
setModuleEnv (ModuleEnv -> REPL ()) -> ModuleEnv -> REPL ()
forall a b. (a -> b) -> a -> b
$ ModuleEnv
me { meSearchPath :: [FilePath]
M.meSearchPath = [FilePath]
path [FilePath] -> [FilePath] -> [FilePath]
forall a. [a] -> [a] -> [a]
++ ModuleEnv -> [FilePath]
M.meSearchPath ModuleEnv
me }

shouldContinue :: REPL Bool
shouldContinue :: REPL Bool
shouldContinue  = RW -> Bool
eContinue (RW -> Bool) -> REPL RW -> REPL Bool
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
`fmap` REPL RW
getRW

stop :: REPL ()
stop :: REPL ()
stop  = (RW -> RW) -> REPL ()
modifyRW_ (\ rw :: RW
rw -> RW
rw { eContinue :: Bool
eContinue = Bool
False })

unlessBatch :: REPL () -> REPL ()
unlessBatch :: REPL () -> REPL ()
unlessBatch body :: REPL ()
body = do
  RW
rw <- REPL RW
getRW
  Bool -> REPL () -> REPL ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (RW -> Bool
eIsBatch RW
rw) REPL ()
body

-- | Run a computation in batch mode, restoring the previous isBatch
-- flag afterwards
asBatch :: REPL a -> REPL a
asBatch :: REPL a -> REPL a
asBatch body :: REPL a
body = do
  Bool
wasBatch <- RW -> Bool
eIsBatch (RW -> Bool) -> REPL RW -> REPL Bool
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
`fmap` REPL RW
getRW
  (RW -> RW) -> REPL ()
modifyRW_ ((RW -> RW) -> REPL ()) -> (RW -> RW) -> REPL ()
forall a b. (a -> b) -> a -> b
$ (\ rw :: RW
rw -> RW
rw { eIsBatch :: Bool
eIsBatch = Bool
True })
  a
a <- REPL a
body
  (RW -> RW) -> REPL ()
modifyRW_ ((RW -> RW) -> REPL ()) -> (RW -> RW) -> REPL ()
forall a b. (a -> b) -> a -> b
$ (\ rw :: RW
rw -> RW
rw { eIsBatch :: Bool
eIsBatch = Bool
wasBatch })
  a -> REPL a
forall (m :: * -> *) a. Monad m => a -> m a
return a
a

disableLet :: REPL ()
disableLet :: REPL ()
disableLet  = (RW -> RW) -> REPL ()
modifyRW_ (\ rw :: RW
rw -> RW
rw { eLetEnabled :: Bool
eLetEnabled = Bool
False })

enableLet :: REPL ()
enableLet :: REPL ()
enableLet  = (RW -> RW) -> REPL ()
modifyRW_ (\ rw :: RW
rw -> RW
rw { eLetEnabled :: Bool
eLetEnabled = Bool
True })

-- | Are let-bindings enabled in this REPL?
getLetEnabled :: REPL Bool
getLetEnabled :: REPL Bool
getLetEnabled = (RW -> Bool) -> REPL RW -> REPL Bool
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap RW -> Bool
eLetEnabled REPL RW
getRW

-- | Is evaluation enabled.  If the currently focused module is
-- parameterized, then we cannot evalute.
validEvalContext :: T.FreeVars a => a -> REPL ()
validEvalContext :: a -> REPL ()
validEvalContext a :: a
a =
  do ModuleEnv
me <- RW -> ModuleEnv
eModuleEnv (RW -> ModuleEnv) -> REPL RW -> REPL ModuleEnv
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> REPL RW
getRW
     let ds :: Deps
ds      = a -> Deps
forall e. FreeVars e => e -> Deps
T.freeVars a
a
         badVals :: Set Name
badVals = (Name -> Set Name -> Set Name) -> Set Name -> Set Name -> Set Name
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr Name -> Set Name -> Set Name
badName Set Name
forall a. Set a
Set.empty (Deps -> Set Name
T.valDeps Deps
ds)
         bad :: Set Name
bad     = (Name -> Set Name -> Set Name) -> Set Name -> Set Name -> Set Name
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr Name -> Set Name -> Set Name
badName Set Name
badVals (Deps -> Set Name
T.tyDeps Deps
ds)

         badName :: Name -> Set Name -> Set Name
badName nm :: Name
nm bs :: Set Name
bs =
           case Name -> NameInfo
M.nameInfo Name
nm of
             M.Declared m :: ModName
m _
               | ModName -> LoadedModules -> Bool
M.isLoadedParamMod ModName
m (ModuleEnv -> LoadedModules
M.meLoadedModules ModuleEnv
me) -> Name -> Set Name -> Set Name
forall a. Ord a => a -> Set a -> Set a
Set.insert Name
nm Set Name
bs
             _ -> Set Name
bs

     Bool -> REPL () -> REPL ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (Set Name -> Bool
forall a. Set a -> Bool
Set.null Set Name
bad) (REPL () -> REPL ()) -> REPL () -> REPL ()
forall a b. (a -> b) -> a -> b
$
       REPLException -> REPL ()
forall a. REPLException -> REPL a
raise ([Name] -> REPLException
EvalInParamModule (Set Name -> [Name]
forall a. Set a -> [a]
Set.toList Set Name
bad))



-- | Update the title
updateREPLTitle :: REPL ()
updateREPLTitle :: REPL ()
updateREPLTitle  = REPL () -> REPL ()
unlessBatch (REPL () -> REPL ()) -> REPL () -> REPL ()
forall a b. (a -> b) -> a -> b
$ do
  RW
rw <- REPL RW
getRW
  RW -> REPL ()
eUpdateTitle RW
rw

-- | Set the function that will be called when updating the title
setUpdateREPLTitle :: REPL () -> REPL ()
setUpdateREPLTitle :: REPL () -> REPL ()
setUpdateREPLTitle m :: REPL ()
m = (RW -> RW) -> REPL ()
modifyRW_ (\rw :: RW
rw -> RW
rw { eUpdateTitle :: REPL ()
eUpdateTitle = REPL ()
m })

-- | Set the REPL's string-printer
setPutStr :: (String -> IO ()) -> REPL ()
setPutStr :: (FilePath -> IO ()) -> REPL ()
setPutStr fn :: FilePath -> IO ()
fn = (RW -> RW) -> REPL ()
modifyRW_ ((RW -> RW) -> REPL ()) -> (RW -> RW) -> REPL ()
forall a b. (a -> b) -> a -> b
$ \rw :: RW
rw -> RW
rw { eLogger :: Logger
eLogger = (FilePath -> IO ()) -> Logger
funLogger FilePath -> IO ()
fn }

-- | Get the REPL's string-printer
getPutStr :: REPL (String -> IO ())
getPutStr :: REPL (FilePath -> IO ())
getPutStr =
  do RW
rw <- REPL RW
getRW
     (FilePath -> IO ()) -> REPL (FilePath -> IO ())
forall (m :: * -> *) a. Monad m => a -> m a
return (Logger -> FilePath -> IO ()
logPutStr (RW -> Logger
eLogger RW
rw))

getLogger :: REPL Logger
getLogger :: REPL Logger
getLogger = RW -> Logger
eLogger (RW -> Logger) -> REPL RW -> REPL Logger
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> REPL RW
getRW


-- | Use the configured output action to print a string
rPutStr :: String -> REPL ()
rPutStr :: FilePath -> REPL ()
rPutStr str :: FilePath
str = do
  FilePath -> IO ()
f <- REPL (FilePath -> IO ())
getPutStr
  IO () -> REPL ()
forall a. IO a -> REPL a
io (FilePath -> IO ()
f FilePath
str)

-- | Use the configured output action to print a string with a trailing newline
rPutStrLn :: String -> REPL ()
rPutStrLn :: FilePath -> REPL ()
rPutStrLn str :: FilePath
str = FilePath -> REPL ()
rPutStr (FilePath -> REPL ()) -> FilePath -> REPL ()
forall a b. (a -> b) -> a -> b
$ FilePath
str FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ "\n"

-- | Use the configured output action to print something using its Show instance
rPrint :: Show a => a -> REPL ()
rPrint :: a -> REPL ()
rPrint x :: a
x = FilePath -> REPL ()
rPutStrLn (a -> FilePath
forall a. Show a => a -> FilePath
show a
x)

getFocusedEnv :: REPL (M.IfaceParams,M.IfaceDecls,M.NamingEnv,NameDisp)
getFocusedEnv :: REPL (IfaceParams, IfaceDecls, NamingEnv, NameDisp)
getFocusedEnv  = do
  ModuleEnv
me <- REPL ModuleEnv
getModuleEnv
  -- dyNames is a NameEnv that removes the #Uniq prefix from interactively-bound
  -- variables.
  let (dyDecls :: IfaceDecls
dyDecls,dyNames :: NamingEnv
dyNames,dyDisp :: NameDisp
dyDisp) = ModuleEnv -> (IfaceDecls, NamingEnv, NameDisp)
M.dynamicEnv ModuleEnv
me
  let (fParams :: IfaceParams
fParams,fDecls :: IfaceDecls
fDecls,fNames :: NamingEnv
fNames,fDisp :: NameDisp
fDisp) = ModuleEnv -> (IfaceParams, IfaceDecls, NamingEnv, NameDisp)
M.focusedEnv ModuleEnv
me
  (IfaceParams, IfaceDecls, NamingEnv, NameDisp)
-> REPL (IfaceParams, IfaceDecls, NamingEnv, NameDisp)
forall (m :: * -> *) a. Monad m => a -> m a
return ( IfaceParams
fParams
         , IfaceDecls
dyDecls IfaceDecls -> IfaceDecls -> IfaceDecls
forall a. Monoid a => a -> a -> a
`mappend` IfaceDecls
fDecls
         , NamingEnv
dyNames NamingEnv -> NamingEnv -> NamingEnv
`M.shadowing` NamingEnv
fNames
         , NameDisp
dyDisp NameDisp -> NameDisp -> NameDisp
forall a. Monoid a => a -> a -> a
`mappend` NameDisp
fDisp)

  -- -- the subtle part here is removing the #Uniq prefix from
  -- -- interactively-bound variables, and also excluding any that are
  -- -- shadowed and thus can no longer be referenced
  -- let (fDecls,fNames,fDisp) = M.focusedEnv me
  --     edecls = M.ifDecls dyDecls
  --     -- is this QName something the user might actually type?
  --     isShadowed (qn@(P.QName (Just (P.unModName -> ['#':_])) name), _) =
  --         case Map.lookup localName neExprs of
  --           Nothing -> False
  --           Just uniqueNames -> isNamed uniqueNames
  --       where localName = P.QName Nothing name
  --             isNamed us = any (== qn) (map M.qname us)
  --             neExprs = M.neExprs (M.deNames (M.meDynEnv me))
  --     isShadowed _ = False
  --     unqual ((P.QName _ name), ifds) = (P.QName Nothing name, ifds)
  --     edecls' = Map.fromList
  --             . map unqual
  --             . filter isShadowed
  --             $ Map.toList edecls
  -- return (decls `mappend` mempty { M.ifDecls = edecls' }, names `mappend` dyNames)

getVars :: REPL (Map.Map M.Name M.IfaceDecl)
getVars :: REPL (Map Name IfaceDecl)
getVars  = do
  (_,decls :: IfaceDecls
decls,_,_) <- REPL (IfaceParams, IfaceDecls, NamingEnv, NameDisp)
getFocusedEnv
  Map Name IfaceDecl -> REPL (Map Name IfaceDecl)
forall (m :: * -> *) a. Monad m => a -> m a
return (IfaceDecls -> Map Name IfaceDecl
M.ifDecls IfaceDecls
decls)

getTSyns :: REPL (Map.Map M.Name T.TySyn)
getTSyns :: REPL (Map Name TySyn)
getTSyns  = do
  (_,decls :: IfaceDecls
decls,_,_) <- REPL (IfaceParams, IfaceDecls, NamingEnv, NameDisp)
getFocusedEnv
  Map Name TySyn -> REPL (Map Name TySyn)
forall (m :: * -> *) a. Monad m => a -> m a
return (IfaceDecls -> Map Name TySyn
M.ifTySyns IfaceDecls
decls)

getNewtypes :: REPL (Map.Map M.Name T.Newtype)
getNewtypes :: REPL (Map Name Newtype)
getNewtypes = do
  (_,decls :: IfaceDecls
decls,_,_) <- REPL (IfaceParams, IfaceDecls, NamingEnv, NameDisp)
getFocusedEnv
  Map Name Newtype -> REPL (Map Name Newtype)
forall (m :: * -> *) a. Monad m => a -> m a
return (IfaceDecls -> Map Name Newtype
M.ifNewtypes IfaceDecls
decls)

-- | Get visible variable names.
getExprNames :: REPL [String]
getExprNames :: REPL [FilePath]
getExprNames =
  do (_,_, fNames :: NamingEnv
fNames, _) <- REPL (IfaceParams, IfaceDecls, NamingEnv, NameDisp)
getFocusedEnv
     [FilePath] -> REPL [FilePath]
forall (m :: * -> *) a. Monad m => a -> m a
return ((PName -> FilePath) -> [PName] -> [FilePath]
forall a b. (a -> b) -> [a] -> [b]
map (Doc -> FilePath
forall a. Show a => a -> FilePath
show (Doc -> FilePath) -> (PName -> Doc) -> PName -> FilePath
forall b c a. (b -> c) -> (a -> b) -> a -> c
. PName -> Doc
forall a. PP a => a -> Doc
pp) (Map PName [Name] -> [PName]
forall k a. Map k a -> [k]
Map.keys (NamingEnv -> Map PName [Name]
M.neExprs NamingEnv
fNames)))

-- | Get visible type signature names.
getTypeNames :: REPL [String]
getTypeNames :: REPL [FilePath]
getTypeNames  =
  do (_,_, fNames :: NamingEnv
fNames, _) <- REPL (IfaceParams, IfaceDecls, NamingEnv, NameDisp)
getFocusedEnv
     [FilePath] -> REPL [FilePath]
forall (m :: * -> *) a. Monad m => a -> m a
return ((PName -> FilePath) -> [PName] -> [FilePath]
forall a b. (a -> b) -> [a] -> [b]
map (Doc -> FilePath
forall a. Show a => a -> FilePath
show (Doc -> FilePath) -> (PName -> Doc) -> PName -> FilePath
forall b c a. (b -> c) -> (a -> b) -> a -> c
. PName -> Doc
forall a. PP a => a -> Doc
pp) (Map PName [Name] -> [PName]
forall k a. Map k a -> [k]
Map.keys (NamingEnv -> Map PName [Name]
M.neTypes NamingEnv
fNames)))

-- | Return a list of property names, sorted by position in the file.
getPropertyNames :: REPL ([M.Name],NameDisp)
getPropertyNames :: REPL ([Name], NameDisp)
getPropertyNames =
  do (_,decls :: IfaceDecls
decls,_,names :: NameDisp
names) <- REPL (IfaceParams, IfaceDecls, NamingEnv, NameDisp)
getFocusedEnv
     let xs :: Map Name IfaceDecl
xs = IfaceDecls -> Map Name IfaceDecl
M.ifDecls IfaceDecls
decls
         ps :: [Name]
ps = (Name -> Name -> Ordering) -> [Name] -> [Name]
forall a. (a -> a -> Ordering) -> [a] -> [a]
sortBy ((Name -> Position) -> Name -> Name -> Ordering
forall a b. Ord a => (b -> a) -> b -> b -> Ordering
comparing (Range -> Position
from (Range -> Position) -> (Name -> Range) -> Name -> Position
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Name -> Range
M.nameLoc))
            ([Name] -> [Name]) -> [Name] -> [Name]
forall a b. (a -> b) -> a -> b
$ [ Name
x | (x :: Name
x,d :: IfaceDecl
d) <- Map Name IfaceDecl -> [(Name, IfaceDecl)]
forall k a. Map k a -> [(k, a)]
Map.toList Map Name IfaceDecl
xs, Pragma
T.PragmaProperty Pragma -> [Pragma] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` IfaceDecl -> [Pragma]
M.ifDeclPragmas IfaceDecl
d ]

     ([Name], NameDisp) -> REPL ([Name], NameDisp)
forall (m :: * -> *) a. Monad m => a -> m a
return ([Name]
ps, NameDisp
names)

getModNames :: REPL [I.ModName]
getModNames :: REPL [ModName]
getModNames =
  do ModuleEnv
me <- REPL ModuleEnv
getModuleEnv
     [ModName] -> REPL [ModName]
forall (m :: * -> *) a. Monad m => a -> m a
return ((Module -> ModName) -> [Module] -> [ModName]
forall a b. (a -> b) -> [a] -> [b]
map Module -> ModName
T.mName (ModuleEnv -> [Module]
M.loadedModules ModuleEnv
me))

getModuleEnv :: REPL M.ModuleEnv
getModuleEnv :: REPL ModuleEnv
getModuleEnv  = RW -> ModuleEnv
eModuleEnv (RW -> ModuleEnv) -> REPL RW -> REPL ModuleEnv
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
`fmap` REPL RW
getRW

setModuleEnv :: M.ModuleEnv -> REPL ()
setModuleEnv :: ModuleEnv -> REPL ()
setModuleEnv me :: ModuleEnv
me = (RW -> RW) -> REPL ()
modifyRW_ (\rw :: RW
rw -> RW
rw { eModuleEnv :: ModuleEnv
eModuleEnv = ModuleEnv
me })

getDynEnv :: REPL M.DynamicEnv
getDynEnv :: REPL DynamicEnv
getDynEnv  = (ModuleEnv -> DynamicEnv
M.meDynEnv (ModuleEnv -> DynamicEnv) -> (RW -> ModuleEnv) -> RW -> DynamicEnv
forall b c a. (b -> c) -> (a -> b) -> a -> c
. RW -> ModuleEnv
eModuleEnv) (RW -> DynamicEnv) -> REPL RW -> REPL DynamicEnv
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
`fmap` REPL RW
getRW

setDynEnv :: M.DynamicEnv -> REPL ()
setDynEnv :: DynamicEnv -> REPL ()
setDynEnv denv :: DynamicEnv
denv = do
  ModuleEnv
me <- REPL ModuleEnv
getModuleEnv
  ModuleEnv -> REPL ()
setModuleEnv (ModuleEnv
me { meDynEnv :: DynamicEnv
M.meDynEnv = DynamicEnv
denv })


-- | Given an existing qualified name, prefix it with a
-- relatively-unique string. We make it unique by prefixing with a
-- character @#@ that is not lexically valid in a module name.
uniqify :: M.Name -> REPL M.Name

uniqify :: Name -> REPL Name
uniqify name :: Name
name =
  case Name -> NameInfo
M.nameInfo Name
name of
    M.Declared ns :: ModName
ns s :: NameSource
s ->
      (Supply -> (Name, Supply)) -> REPL Name
forall (m :: * -> *) a. FreshM m => (Supply -> (a, Supply)) -> m a
M.liftSupply (ModName
-> NameSource
-> Ident
-> Maybe Fixity
-> Range
-> Supply
-> (Name, Supply)
M.mkDeclared ModName
ns NameSource
s (Name -> Ident
M.nameIdent Name
name) (Name -> Maybe Fixity
M.nameFixity Name
name) (Name -> Range
M.nameLoc Name
name))

    M.Parameter ->
      FilePath -> [FilePath] -> REPL Name
forall a. HasCallStack => FilePath -> [FilePath] -> a
panic "[REPL] uniqify" ["tried to uniqify a parameter: " FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ Name -> FilePath
forall a. PP a => a -> FilePath
pretty Name
name]


-- uniqify (P.QName Nothing name) = do
--   i <- eNameSupply `fmap` getRW
--   modifyRW_ (\rw -> rw { eNameSupply = i+1 })
--   let modname' = P.mkModName [ '#' : ("Uniq_" ++ show i) ]
--   return (P.QName (Just modname') name)

-- uniqify qn =
--   panic "[REPL] uniqify" ["tried to uniqify a qualified name: " ++ pretty qn]


-- | Generate a fresh name using the given index. The name will reside within
-- the "<interactive>" namespace.
freshName :: I.Ident -> M.NameSource -> REPL M.Name
freshName :: Ident -> NameSource -> REPL Name
freshName i :: Ident
i sys :: NameSource
sys =
  (Supply -> (Name, Supply)) -> REPL Name
forall (m :: * -> *) a. FreshM m => (Supply -> (a, Supply)) -> m a
M.liftSupply (ModName
-> NameSource
-> Ident
-> Maybe Fixity
-> Range
-> Supply
-> (Name, Supply)
M.mkDeclared ModName
I.interactiveName NameSource
sys Ident
i Maybe Fixity
forall a. Maybe a
Nothing Range
emptyRange)


-- User Environment Interaction ------------------------------------------------

-- | User modifiable environment, for things like numeric base.
type UserEnv = Map.Map String EnvVal

data EnvVal
  = EnvString String
  | EnvProg   String [String]
  | EnvNum    !Int
  | EnvBool   Bool
    deriving (Int -> EnvVal -> FilePath -> FilePath
[EnvVal] -> FilePath -> FilePath
EnvVal -> FilePath
(Int -> EnvVal -> FilePath -> FilePath)
-> (EnvVal -> FilePath)
-> ([EnvVal] -> FilePath -> FilePath)
-> Show EnvVal
forall a.
(Int -> a -> FilePath -> FilePath)
-> (a -> FilePath) -> ([a] -> FilePath -> FilePath) -> Show a
showList :: [EnvVal] -> FilePath -> FilePath
$cshowList :: [EnvVal] -> FilePath -> FilePath
show :: EnvVal -> FilePath
$cshow :: EnvVal -> FilePath
showsPrec :: Int -> EnvVal -> FilePath -> FilePath
$cshowsPrec :: Int -> EnvVal -> FilePath -> FilePath
Show)

-- | Generate a UserEnv from a description of the options map.
mkUserEnv :: OptionMap -> UserEnv
mkUserEnv :: OptionMap -> UserEnv
mkUserEnv opts :: OptionMap
opts = [(FilePath, EnvVal)] -> UserEnv
forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList ([(FilePath, EnvVal)] -> UserEnv)
-> [(FilePath, EnvVal)] -> UserEnv
forall a b. (a -> b) -> a -> b
$ do
  OptionDescr
opt <- OptionMap -> [OptionDescr]
forall a. Trie a -> [a]
leaves OptionMap
opts
  (FilePath, EnvVal) -> [(FilePath, EnvVal)]
forall (m :: * -> *) a. Monad m => a -> m a
return (OptionDescr -> FilePath
optName OptionDescr
opt, OptionDescr -> EnvVal
optDefault OptionDescr
opt)

-- | Set a user option.
setUser :: String -> String -> REPL ()
setUser :: FilePath -> FilePath -> REPL ()
setUser name :: FilePath
name val :: FilePath
val = case FilePath -> OptionMap -> [OptionDescr]
forall a. FilePath -> Trie a -> [a]
lookupTrieExact FilePath
name OptionMap
userOptions of

  [opt :: OptionDescr
opt] -> OptionDescr -> REPL ()
setUserOpt OptionDescr
opt
  []    -> FilePath -> REPL ()
rPutStrLn ("Unknown env value `" FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ FilePath
name FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ "`")
  _     -> FilePath -> REPL ()
rPutStrLn ("Ambiguous env value `" FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ FilePath
name FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ "`")

  where
  setUserOpt :: OptionDescr -> REPL ()
setUserOpt opt :: OptionDescr
opt = case OptionDescr -> EnvVal
optDefault OptionDescr
opt of
    EnvString _ -> EnvVal -> REPL ()
doCheck (FilePath -> EnvVal
EnvString FilePath
val)

    EnvProg _ _ ->
      case FilePath -> [FilePath]
splitOptArgs FilePath
val of
        prog :: FilePath
prog:args :: [FilePath]
args -> EnvVal -> REPL ()
doCheck (FilePath -> [FilePath] -> EnvVal
EnvProg FilePath
prog [FilePath]
args)
        [] -> FilePath -> REPL ()
rPutStrLn ("Failed to parse command for field, `" FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ FilePath
name FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ "`")

    EnvNum _ -> case ReadS Int
forall a. Read a => ReadS a
reads FilePath
val of
      [(x :: Int
x,_)] -> EnvVal -> REPL ()
doCheck (Int -> EnvVal
EnvNum Int
x)
      _ -> FilePath -> REPL ()
rPutStrLn ("Failed to parse number for field, `" FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ FilePath
name FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ "`")

    EnvBool _
      | (FilePath -> Bool) -> [FilePath] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (FilePath -> FilePath -> Bool
forall a. Eq a => [a] -> [a] -> Bool
`isPrefixOf` FilePath
val) ["enable", "on", "yes", "true"] ->
        EnvVal -> REPL ()
writeEnv (Bool -> EnvVal
EnvBool Bool
True)
      | (FilePath -> Bool) -> [FilePath] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (FilePath -> FilePath -> Bool
forall a. Eq a => [a] -> [a] -> Bool
`isPrefixOf` FilePath
val) ["disable", "off", "no", "false"] ->
        EnvVal -> REPL ()
writeEnv (Bool -> EnvVal
EnvBool Bool
False)
      | Bool
otherwise ->
        FilePath -> REPL ()
rPutStrLn ("Failed to parse boolean for field, `" FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ FilePath
name FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ "`")
    where
    doCheck :: EnvVal -> REPL ()
doCheck v :: EnvVal
v = do (r :: Maybe FilePath
r,ws :: [FilePath]
ws) <- IO (Maybe FilePath, [FilePath])
-> REPL (Maybe FilePath, [FilePath])
forall a. IO a -> REPL a
io (OptionDescr -> Checker
optCheck OptionDescr
opt EnvVal
v)
                   case Maybe FilePath
r of
                     Just err :: FilePath
err -> FilePath -> REPL ()
rPutStrLn FilePath
err
                     Nothing  -> do (FilePath -> REPL ()) -> [FilePath] -> REPL ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ FilePath -> REPL ()
rPutStrLn [FilePath]
ws
                                    EnvVal -> REPL ()
writeEnv EnvVal
v
    writeEnv :: EnvVal -> REPL ()
writeEnv ev :: EnvVal
ev =
      do OptionDescr -> EnvVal -> REPL ()
optEff OptionDescr
opt EnvVal
ev
         (RW -> RW) -> REPL ()
modifyRW_ (\rw :: RW
rw -> RW
rw { eUserEnv :: UserEnv
eUserEnv = FilePath -> EnvVal -> UserEnv -> UserEnv
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert (OptionDescr -> FilePath
optName OptionDescr
opt) EnvVal
ev (RW -> UserEnv
eUserEnv RW
rw) })

splitOptArgs :: String -> [String]
splitOptArgs :: FilePath -> [FilePath]
splitOptArgs  = (FilePath -> Maybe (FilePath, FilePath)) -> FilePath -> [FilePath]
forall b a. (b -> Maybe (a, b)) -> b -> [a]
unfoldr (FilePath -> FilePath -> Maybe (FilePath, FilePath)
parse "")
  where

  parse :: FilePath -> FilePath -> Maybe (FilePath, FilePath)
parse acc :: FilePath
acc (c :: Char
c:cs :: FilePath
cs) | Char -> Bool
isQuote Char
c       = FilePath -> FilePath -> Maybe (FilePath, FilePath)
quoted (Char
cChar -> FilePath -> FilePath
forall a. a -> [a] -> [a]
:FilePath
acc) FilePath
cs
                   | Bool -> Bool
not (Char -> Bool
isSpace Char
c) = FilePath -> FilePath -> Maybe (FilePath, FilePath)
parse (Char
cChar -> FilePath -> FilePath
forall a. a -> [a] -> [a]
:FilePath
acc) FilePath
cs
                   | Bool
otherwise       = FilePath -> FilePath -> Maybe (FilePath, FilePath)
result FilePath
acc FilePath
cs
  parse acc :: FilePath
acc []                       = FilePath -> FilePath -> Maybe (FilePath, FilePath)
result FilePath
acc []

  quoted :: FilePath -> FilePath -> Maybe (FilePath, FilePath)
quoted acc :: FilePath
acc (c :: Char
c:cs :: FilePath
cs) | Char -> Bool
isQuote Char
c      = FilePath -> FilePath -> Maybe (FilePath, FilePath)
parse  (Char
cChar -> FilePath -> FilePath
forall a. a -> [a] -> [a]
:FilePath
acc) FilePath
cs
                    | Bool
otherwise      = FilePath -> FilePath -> Maybe (FilePath, FilePath)
quoted (Char
cChar -> FilePath -> FilePath
forall a. a -> [a] -> [a]
:FilePath
acc) FilePath
cs
  quoted acc :: FilePath
acc []                      = FilePath -> FilePath -> Maybe (FilePath, FilePath)
result FilePath
acc []

  result :: FilePath -> FilePath -> Maybe (FilePath, FilePath)
result []  [] = Maybe (FilePath, FilePath)
forall a. Maybe a
Nothing
  result []  cs :: FilePath
cs = FilePath -> FilePath -> Maybe (FilePath, FilePath)
parse [] ((Char -> Bool) -> FilePath -> FilePath
forall a. (a -> Bool) -> [a] -> [a]
dropWhile Char -> Bool
isSpace FilePath
cs)
  result acc :: FilePath
acc cs :: FilePath
cs = (FilePath, FilePath) -> Maybe (FilePath, FilePath)
forall a. a -> Maybe a
Just (FilePath -> FilePath
forall a. [a] -> [a]
reverse FilePath
acc, (Char -> Bool) -> FilePath -> FilePath
forall a. (a -> Bool) -> [a] -> [a]
dropWhile Char -> Bool
isSpace FilePath
cs)

  isQuote :: Char -> Bool
  isQuote :: Char -> Bool
isQuote c :: Char
c = Char
c Char -> FilePath -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` ("'\"" :: String)


-- | Get a user option, using Maybe for failure.
tryGetUser :: String -> REPL (Maybe EnvVal)
tryGetUser :: FilePath -> REPL (Maybe EnvVal)
tryGetUser name :: FilePath
name = do
  RW
rw <- REPL RW
getRW
  Maybe EnvVal -> REPL (Maybe EnvVal)
forall (m :: * -> *) a. Monad m => a -> m a
return (FilePath -> UserEnv -> Maybe EnvVal
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup FilePath
name (RW -> UserEnv
eUserEnv RW
rw))

-- | Get a user option, when it's known to exist.  Fail with panic when it
-- doesn't.
getUser :: String -> REPL EnvVal
getUser :: FilePath -> REPL EnvVal
getUser name :: FilePath
name = do
  Maybe EnvVal
mb <- FilePath -> REPL (Maybe EnvVal)
tryGetUser FilePath
name
  case Maybe EnvVal
mb of
    Just ev :: EnvVal
ev -> EnvVal -> REPL EnvVal
forall (m :: * -> *) a. Monad m => a -> m a
return EnvVal
ev
    Nothing -> FilePath -> [FilePath] -> REPL EnvVal
forall a. HasCallStack => FilePath -> [FilePath] -> a
panic "[REPL] getUser" ["option `" FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ FilePath
name FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ "` does not exist"]

getKnownUser :: IsEnvVal a => String -> REPL a
getKnownUser :: FilePath -> REPL a
getKnownUser x :: FilePath
x = EnvVal -> a
forall a. IsEnvVal a => EnvVal -> a
fromEnvVal (EnvVal -> a) -> REPL EnvVal -> REPL a
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> FilePath -> REPL EnvVal
getUser FilePath
x

class IsEnvVal a where
  fromEnvVal :: EnvVal -> a

instance IsEnvVal Bool where
  fromEnvVal :: EnvVal -> Bool
fromEnvVal x :: EnvVal
x = case EnvVal
x of
                   EnvBool b :: Bool
b -> Bool
b
                   _         -> FilePath -> Bool
forall a. FilePath -> a
badIsEnv "Bool"

instance IsEnvVal Int where
  fromEnvVal :: EnvVal -> Int
fromEnvVal x :: EnvVal
x = case EnvVal
x of
                   EnvNum b :: Int
b -> Int
b
                   _         -> FilePath -> Int
forall a. FilePath -> a
badIsEnv "Num"

instance IsEnvVal (String,[String]) where
  fromEnvVal :: EnvVal -> (FilePath, [FilePath])
fromEnvVal x :: EnvVal
x = case EnvVal
x of
                   EnvProg b :: FilePath
b bs :: [FilePath]
bs -> (FilePath
b,[FilePath]
bs)
                   _            -> FilePath -> (FilePath, [FilePath])
forall a. FilePath -> a
badIsEnv "Prog"

instance IsEnvVal String where
  fromEnvVal :: EnvVal -> FilePath
fromEnvVal x :: EnvVal
x = case EnvVal
x of
                   EnvString b :: FilePath
b -> FilePath
b
                   _           -> FilePath -> FilePath
forall a. FilePath -> a
badIsEnv "String"

badIsEnv :: String -> a
badIsEnv :: FilePath -> a
badIsEnv x :: FilePath
x = FilePath -> [FilePath] -> a
forall a. HasCallStack => FilePath -> [FilePath] -> a
panic "fromEnvVal" [ "[REPL] Expected a `" FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ FilePath
x FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ "` value." ]


getUserShowProverStats :: REPL Bool
getUserShowProverStats :: REPL Bool
getUserShowProverStats = FilePath -> REPL Bool
forall a. IsEnvVal a => FilePath -> REPL a
getKnownUser "prover-stats"

getUserProverValidate :: REPL Bool
getUserProverValidate :: REPL Bool
getUserProverValidate = FilePath -> REPL Bool
forall a. IsEnvVal a => FilePath -> REPL a
getKnownUser "prover-validate"

-- Environment Options ---------------------------------------------------------

type OptionMap = Trie OptionDescr

mkOptionMap :: [OptionDescr] -> OptionMap
mkOptionMap :: [OptionDescr] -> OptionMap
mkOptionMap  = (OptionMap -> OptionDescr -> OptionMap)
-> OptionMap -> [OptionDescr] -> OptionMap
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl OptionMap -> OptionDescr -> OptionMap
insert OptionMap
forall a. Trie a
emptyTrie
  where
  insert :: OptionMap -> OptionDescr -> OptionMap
insert m :: OptionMap
m d :: OptionDescr
d = FilePath -> OptionDescr -> OptionMap -> OptionMap
forall a. FilePath -> a -> Trie a -> Trie a
insertTrie (OptionDescr -> FilePath
optName OptionDescr
d) OptionDescr
d OptionMap
m

-- | Returns maybe an error, and some warnings
type Checker = EnvVal -> IO (Maybe String, [String])

noCheck :: Checker
noCheck :: Checker
noCheck _ = (Maybe FilePath, [FilePath]) -> IO (Maybe FilePath, [FilePath])
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe FilePath
forall a. Maybe a
Nothing, [])

noWarns :: Maybe String -> IO (Maybe String, [String])
noWarns :: Maybe FilePath -> IO (Maybe FilePath, [FilePath])
noWarns mb :: Maybe FilePath
mb = (Maybe FilePath, [FilePath]) -> IO (Maybe FilePath, [FilePath])
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe FilePath
mb, [])

data OptionDescr = OptionDescr
  { OptionDescr -> FilePath
optName    :: String
  , OptionDescr -> EnvVal
optDefault :: EnvVal
  , OptionDescr -> Checker
optCheck   :: Checker
  , OptionDescr -> FilePath
optHelp    :: String
  , OptionDescr -> EnvVal -> REPL ()
optEff     :: EnvVal -> REPL ()
  }

simpleOpt :: String -> EnvVal -> Checker -> String -> OptionDescr
simpleOpt :: FilePath -> EnvVal -> Checker -> FilePath -> OptionDescr
simpleOpt optName :: FilePath
optName optDefault :: EnvVal
optDefault optCheck :: Checker
optCheck optHelp :: FilePath
optHelp =
  OptionDescr :: FilePath
-> EnvVal
-> Checker
-> FilePath
-> (EnvVal -> REPL ())
-> OptionDescr
OptionDescr { optEff :: EnvVal -> REPL ()
optEff = \ _ -> () -> REPL ()
forall (m :: * -> *) a. Monad m => a -> m a
return (), .. }

userOptions :: OptionMap
userOptions :: OptionMap
userOptions  = [OptionDescr] -> OptionMap
mkOptionMap
  [ FilePath -> EnvVal -> Checker -> FilePath -> OptionDescr
simpleOpt "base" (Int -> EnvVal
EnvNum 16) Checker
checkBase
    "The base to display words at (2, 8, 10, or 16)."
  , FilePath -> EnvVal -> Checker -> FilePath -> OptionDescr
simpleOpt "debug" (Bool -> EnvVal
EnvBool Bool
False) Checker
noCheck
    "Enable debugging output."
  , FilePath -> EnvVal -> Checker -> FilePath -> OptionDescr
simpleOpt "ascii" (Bool -> EnvVal
EnvBool Bool
False) Checker
noCheck
    "Whether to display 7- or 8-bit words using ASCII notation."
  , FilePath -> EnvVal -> Checker -> FilePath -> OptionDescr
simpleOpt "infLength" (Int -> EnvVal
EnvNum 5) Checker
checkInfLength
    "The number of elements to display for infinite sequences."
  , FilePath -> EnvVal -> Checker -> FilePath -> OptionDescr
simpleOpt "tests" (Int -> EnvVal
EnvNum 100) Checker
noCheck
    "The number of random tests to try with ':check'."
  , FilePath -> EnvVal -> Checker -> FilePath -> OptionDescr
simpleOpt "satNum" (FilePath -> EnvVal
EnvString "1") Checker
checkSatNum
    "The maximum number of :sat solutions to display (\"all\" for no limit)."
  , FilePath -> EnvVal -> Checker -> FilePath -> OptionDescr
simpleOpt "prover" (FilePath -> EnvVal
EnvString "z3") Checker
checkProver (FilePath -> OptionDescr) -> FilePath -> OptionDescr
forall a b. (a -> b) -> a -> b
$
    "The external SMT solver for ':prove' and ':sat'\n(" FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ FilePath
proverListString FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ ")."
  , FilePath -> EnvVal -> Checker -> FilePath -> OptionDescr
simpleOpt "warnDefaulting" (Bool -> EnvVal
EnvBool Bool
True) Checker
noCheck
    "Choose whether to display warnings when defaulting."
  , FilePath -> EnvVal -> Checker -> FilePath -> OptionDescr
simpleOpt "warnShadowing" (Bool -> EnvVal
EnvBool Bool
True) Checker
noCheck
    "Choose whether to display warnings when shadowing symbols."
  , FilePath -> EnvVal -> Checker -> FilePath -> OptionDescr
simpleOpt "smtfile" (FilePath -> EnvVal
EnvString "-") Checker
noCheck
    "The file to use for SMT-Lib scripts (for debugging or offline proving).\nUse \"-\" for stdout."
  , FilePath
-> EnvVal
-> Checker
-> FilePath
-> (EnvVal -> REPL ())
-> OptionDescr
OptionDescr "mono-binds" (Bool -> EnvVal
EnvBool Bool
True) Checker
noCheck
    "Whether or not to generalize bindings in a 'where' clause." ((EnvVal -> REPL ()) -> OptionDescr)
-> (EnvVal -> REPL ()) -> OptionDescr
forall a b. (a -> b) -> a -> b
$
    \case EnvBool b :: Bool
b -> do ModuleEnv
me <- REPL ModuleEnv
getModuleEnv
                          ModuleEnv -> REPL ()
setModuleEnv ModuleEnv
me { meMonoBinds :: Bool
M.meMonoBinds = Bool
b }
          _         -> () -> REPL ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()

  , FilePath
-> EnvVal
-> Checker
-> FilePath
-> (EnvVal -> REPL ())
-> OptionDescr
OptionDescr "tc-solver" (FilePath -> [FilePath] -> EnvVal
EnvProg "z3" [ "-smt2", "-in" ])
    Checker
noCheck  -- TODO: check for the program in the path
    "The solver that will be used by the type checker." ((EnvVal -> REPL ()) -> OptionDescr)
-> (EnvVal -> REPL ()) -> OptionDescr
forall a b. (a -> b) -> a -> b
$
    \case EnvProg prog :: FilePath
prog args :: [FilePath]
args -> do ModuleEnv
me <- REPL ModuleEnv
getModuleEnv
                                  let cfg :: SolverConfig
cfg = ModuleEnv -> SolverConfig
M.meSolverConfig ModuleEnv
me
                                  ModuleEnv -> REPL ()
setModuleEnv ModuleEnv
me { meSolverConfig :: SolverConfig
M.meSolverConfig =
                                                      SolverConfig
cfg { solverPath :: FilePath
T.solverPath = FilePath
prog
                                                          , solverArgs :: [FilePath]
T.solverArgs = [FilePath]
args } }
          _                 -> () -> REPL ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()

  , FilePath
-> EnvVal
-> Checker
-> FilePath
-> (EnvVal -> REPL ())
-> OptionDescr
OptionDescr "tc-debug" (Int -> EnvVal
EnvNum 0)
    Checker
noCheck
    "Enable type-checker debugging output." ((EnvVal -> REPL ()) -> OptionDescr)
-> (EnvVal -> REPL ()) -> OptionDescr
forall a b. (a -> b) -> a -> b
$
    \case EnvNum n :: Int
n -> do ModuleEnv
me <- REPL ModuleEnv
getModuleEnv
                         let cfg :: SolverConfig
cfg = ModuleEnv -> SolverConfig
M.meSolverConfig ModuleEnv
me
                         ModuleEnv -> REPL ()
setModuleEnv ModuleEnv
me { meSolverConfig :: SolverConfig
M.meSolverConfig = SolverConfig
cfg{ solverVerbose :: Int
T.solverVerbose = Int
n } }
          _        -> () -> REPL ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
  , FilePath
-> EnvVal
-> Checker
-> FilePath
-> (EnvVal -> REPL ())
-> OptionDescr
OptionDescr "core-lint" (Bool -> EnvVal
EnvBool Bool
False)
    Checker
noCheck
    "Enable sanity checking of type-checker." ((EnvVal -> REPL ()) -> OptionDescr)
-> (EnvVal -> REPL ()) -> OptionDescr
forall a b. (a -> b) -> a -> b
$
      let setIt :: CoreLint -> REPL ()
setIt x :: CoreLint
x = do ModuleEnv
me <- REPL ModuleEnv
getModuleEnv
                       ModuleEnv -> REPL ()
setModuleEnv ModuleEnv
me { meCoreLint :: CoreLint
M.meCoreLint = CoreLint
x }
      in \case EnvBool True  -> CoreLint -> REPL ()
setIt CoreLint
M.CoreLint
               EnvBool False -> CoreLint -> REPL ()
setIt CoreLint
M.NoCoreLint
               _             -> () -> REPL ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()

  , FilePath -> EnvVal -> Checker -> FilePath -> OptionDescr
simpleOpt "prover-stats" (Bool -> EnvVal
EnvBool Bool
True) Checker
noCheck
    "Enable prover timing statistics."

  , FilePath -> EnvVal -> Checker -> FilePath -> OptionDescr
simpleOpt "prover-validate" (Bool -> EnvVal
EnvBool Bool
False) Checker
noCheck
    "Validate :sat examples and :prove counter-examples for correctness."

  , FilePath -> EnvVal -> Checker -> FilePath -> OptionDescr
simpleOpt "show-examples" (Bool -> EnvVal
EnvBool Bool
True) Checker
noCheck
    "Print the (counter) example after :sat or :prove"
  ]


-- | Check the value to the `base` option.
checkBase :: Checker
checkBase :: Checker
checkBase val :: EnvVal
val = case EnvVal
val of
  EnvNum n :: Int
n
    | Int
n Int -> [Int] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [2,8,10,16] -> Maybe FilePath -> IO (Maybe FilePath, [FilePath])
noWarns Maybe FilePath
forall a. Maybe a
Nothing
    | Bool
otherwise            -> Maybe FilePath -> IO (Maybe FilePath, [FilePath])
noWarns (Maybe FilePath -> IO (Maybe FilePath, [FilePath]))
-> Maybe FilePath -> IO (Maybe FilePath, [FilePath])
forall a b. (a -> b) -> a -> b
$ FilePath -> Maybe FilePath
forall a. a -> Maybe a
Just "base must be 2, 8, 10, or 16"
  _                     -> Maybe FilePath -> IO (Maybe FilePath, [FilePath])
noWarns (Maybe FilePath -> IO (Maybe FilePath, [FilePath]))
-> Maybe FilePath -> IO (Maybe FilePath, [FilePath])
forall a b. (a -> b) -> a -> b
$ FilePath -> Maybe FilePath
forall a. a -> Maybe a
Just "unable to parse a value for base"

checkInfLength :: Checker
checkInfLength :: Checker
checkInfLength val :: EnvVal
val = case EnvVal
val of
  EnvNum n :: Int
n
    | Int
n Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>= 0    -> Maybe FilePath -> IO (Maybe FilePath, [FilePath])
noWarns Maybe FilePath
forall a. Maybe a
Nothing
    | Bool
otherwise -> Maybe FilePath -> IO (Maybe FilePath, [FilePath])
noWarns (Maybe FilePath -> IO (Maybe FilePath, [FilePath]))
-> Maybe FilePath -> IO (Maybe FilePath, [FilePath])
forall a b. (a -> b) -> a -> b
$ FilePath -> Maybe FilePath
forall a. a -> Maybe a
Just "the number of elements should be positive"
  _ -> Maybe FilePath -> IO (Maybe FilePath, [FilePath])
noWarns (Maybe FilePath -> IO (Maybe FilePath, [FilePath]))
-> Maybe FilePath -> IO (Maybe FilePath, [FilePath])
forall a b. (a -> b) -> a -> b
$ FilePath -> Maybe FilePath
forall a. a -> Maybe a
Just "unable to parse a value for infLength"

checkProver :: Checker
checkProver :: Checker
checkProver val :: EnvVal
val = case EnvVal
val of
  EnvString s :: FilePath
s
    | FilePath
s FilePath -> [FilePath] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`notElem` [FilePath]
proverNames ->
      Maybe FilePath -> IO (Maybe FilePath, [FilePath])
noWarns (Maybe FilePath -> IO (Maybe FilePath, [FilePath]))
-> Maybe FilePath -> IO (Maybe FilePath, [FilePath])
forall a b. (a -> b) -> a -> b
$ FilePath -> Maybe FilePath
forall a. a -> Maybe a
Just (FilePath -> Maybe FilePath) -> FilePath -> Maybe FilePath
forall a b. (a -> b) -> a -> b
$ "Prover must be " FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ FilePath
proverListString
    | FilePath
s FilePath -> [FilePath] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` ["offline", "any"] -> Maybe FilePath -> IO (Maybe FilePath, [FilePath])
noWarns Maybe FilePath
forall a. Maybe a
Nothing
    | Bool
otherwise ->
      do let prover :: SMTConfig
prover = FilePath -> SMTConfig
lookupProver FilePath
s
         Bool
available <- SMTConfig -> IO Bool
sbvCheckSolverInstallation SMTConfig
prover
         let ws :: [FilePath]
ws = if Bool
available
                     then []
                     else ["Warning: " FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ FilePath
s FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ " installation not found"]
         (Maybe FilePath, [FilePath]) -> IO (Maybe FilePath, [FilePath])
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe FilePath
forall a. Maybe a
Nothing, [FilePath]
ws)

  _ -> Maybe FilePath -> IO (Maybe FilePath, [FilePath])
noWarns (Maybe FilePath -> IO (Maybe FilePath, [FilePath]))
-> Maybe FilePath -> IO (Maybe FilePath, [FilePath])
forall a b. (a -> b) -> a -> b
$ FilePath -> Maybe FilePath
forall a. a -> Maybe a
Just "unable to parse a value for prover"

proverListString :: String
proverListString :: FilePath
proverListString = (FilePath -> FilePath) -> [FilePath] -> FilePath
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ ", ") ([FilePath] -> [FilePath]
forall a. [a] -> [a]
init [FilePath]
proverNames) FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ "or " FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ [FilePath] -> FilePath
forall a. [a] -> a
last [FilePath]
proverNames

checkSatNum :: Checker
checkSatNum :: Checker
checkSatNum val :: EnvVal
val = case EnvVal
val of
  EnvString "all" -> Maybe FilePath -> IO (Maybe FilePath, [FilePath])
noWarns Maybe FilePath
forall a. Maybe a
Nothing
  EnvString s :: FilePath
s ->
    case FilePath -> Maybe Int
forall a. Read a => FilePath -> Maybe a
readMaybe FilePath
s :: Maybe Int of
      Just n :: Int
n | Int
n Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>= 1 -> Maybe FilePath -> IO (Maybe FilePath, [FilePath])
noWarns Maybe FilePath
forall a. Maybe a
Nothing
      _               -> Maybe FilePath -> IO (Maybe FilePath, [FilePath])
noWarns (Maybe FilePath -> IO (Maybe FilePath, [FilePath]))
-> Maybe FilePath -> IO (Maybe FilePath, [FilePath])
forall a b. (a -> b) -> a -> b
$ FilePath -> Maybe FilePath
forall a. a -> Maybe a
Just "must be an integer > 0 or \"all\""
  _ -> Maybe FilePath -> IO (Maybe FilePath, [FilePath])
noWarns (Maybe FilePath -> IO (Maybe FilePath, [FilePath]))
-> Maybe FilePath -> IO (Maybe FilePath, [FilePath])
forall a b. (a -> b) -> a -> b
$ FilePath -> Maybe FilePath
forall a. a -> Maybe a
Just "unable to parse a value for satNum"

getUserSatNum :: REPL SatNum
getUserSatNum :: REPL SatNum
getUserSatNum = do
  FilePath
s <- FilePath -> REPL FilePath
forall a. IsEnvVal a => FilePath -> REPL a
getKnownUser "satNum"
  case FilePath
s of
    "all"                     -> SatNum -> REPL SatNum
forall (m :: * -> *) a. Monad m => a -> m a
return SatNum
AllSat
    _ | Just n :: Int
n <- FilePath -> Maybe Int
forall a. Read a => FilePath -> Maybe a
readMaybe FilePath
s -> SatNum -> REPL SatNum
forall (m :: * -> *) a. Monad m => a -> m a
return (Int -> SatNum
SomeSat Int
n)
    _                         -> FilePath -> [FilePath] -> REPL SatNum
forall a. HasCallStack => FilePath -> [FilePath] -> a
panic "REPL.Monad.getUserSatNum"
                                   [ "invalid satNum option" ]

-- Environment Utilities -------------------------------------------------------

whenDebug :: REPL () -> REPL ()
whenDebug :: REPL () -> REPL ()
whenDebug m :: REPL ()
m = do
  Bool
b <- FilePath -> REPL Bool
forall a. IsEnvVal a => FilePath -> REPL a
getKnownUser "debug"
  Bool -> REPL () -> REPL ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when Bool
b REPL ()
m

-- Smoke Testing ---------------------------------------------------------------

smokeTest :: REPL [Smoke]
smokeTest :: REPL [Smoke]
smokeTest = [Maybe Smoke] -> [Smoke]
forall a. [Maybe a] -> [a]
catMaybes ([Maybe Smoke] -> [Smoke]) -> REPL [Maybe Smoke] -> REPL [Smoke]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [REPL (Maybe Smoke)] -> REPL [Maybe Smoke]
forall (t :: * -> *) (m :: * -> *) a.
(Traversable t, Monad m) =>
t (m a) -> m (t a)
sequence [REPL (Maybe Smoke)]
tests
  where
    tests :: [REPL (Maybe Smoke)]
tests = [ REPL (Maybe Smoke)
z3exists ]

type SmokeTest = REPL (Maybe Smoke)

data Smoke
  = Z3NotFound
  deriving (Int -> Smoke -> FilePath -> FilePath
[Smoke] -> FilePath -> FilePath
Smoke -> FilePath
(Int -> Smoke -> FilePath -> FilePath)
-> (Smoke -> FilePath)
-> ([Smoke] -> FilePath -> FilePath)
-> Show Smoke
forall a.
(Int -> a -> FilePath -> FilePath)
-> (a -> FilePath) -> ([a] -> FilePath -> FilePath) -> Show a
showList :: [Smoke] -> FilePath -> FilePath
$cshowList :: [Smoke] -> FilePath -> FilePath
show :: Smoke -> FilePath
$cshow :: Smoke -> FilePath
showsPrec :: Int -> Smoke -> FilePath -> FilePath
$cshowsPrec :: Int -> Smoke -> FilePath -> FilePath
Show, Smoke -> Smoke -> Bool
(Smoke -> Smoke -> Bool) -> (Smoke -> Smoke -> Bool) -> Eq Smoke
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Smoke -> Smoke -> Bool
$c/= :: Smoke -> Smoke -> Bool
== :: Smoke -> Smoke -> Bool
$c== :: Smoke -> Smoke -> Bool
Eq)

instance PP Smoke where
  ppPrec :: Int -> Smoke -> Doc
ppPrec _ smoke :: Smoke
smoke =
    case Smoke
smoke of
      Z3NotFound -> FilePath -> Doc
text (FilePath -> Doc) -> ([FilePath] -> FilePath) -> [FilePath] -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. FilePath -> [FilePath] -> FilePath
forall a. [a] -> [[a]] -> [a]
intercalate " " ([FilePath] -> Doc) -> [FilePath] -> Doc
forall a b. (a -> b) -> a -> b
$ [
          "[error] z3 is required to run Cryptol, but was not found in the"
        , "system path. See the Cryptol README for more on how to install z3."
        ]

z3exists :: SmokeTest
z3exists :: REPL (Maybe Smoke)
z3exists = do
  Maybe FilePath
mPath <- IO (Maybe FilePath) -> REPL (Maybe FilePath)
forall a. IO a -> REPL a
io (IO (Maybe FilePath) -> REPL (Maybe FilePath))
-> IO (Maybe FilePath) -> REPL (Maybe FilePath)
forall a b. (a -> b) -> a -> b
$ FilePath -> IO (Maybe FilePath)
findExecutable "z3"
  case Maybe FilePath
mPath of
    Nothing -> Maybe Smoke -> REPL (Maybe Smoke)
forall (m :: * -> *) a. Monad m => a -> m a
return (Smoke -> Maybe Smoke
forall a. a -> Maybe a
Just Smoke
Z3NotFound)
    Just _  -> Maybe Smoke -> REPL (Maybe Smoke)
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe Smoke
forall a. Maybe a
Nothing