module Cryptol.REPL.Monad (
REPL(..), runREPL
, io
, raise
, stop
, catch
, rPutStrLn
, rPutStr
, rPrint
, REPLException(..)
, rethrowEvalError
, getFocusedEnv
, getModuleEnv, setModuleEnv
, getDynEnv, setDynEnv
, uniqify, freshName
, getTSyns, getNewtypes, getVars
, whenDebug
, getExprNames
, getTypeNames
, getPropertyNames
, LoadedModule(..), getLoadedMod, setLoadedMod
, setSearchPath, prependSearchPath
, getPrompt
, shouldContinue
, unlessBatch
, asBatch
, disableLet
, enableLet
, getLetEnabled
, updateREPLTitle
, setUpdateREPLTitle
, EnvVal(..)
, OptionDescr(..)
, setUser, getUser, tryGetUser
, userOptions
, getUserSatNum
, getPutStr
, setPutStr
, 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.Utils.Ident as I
import Cryptol.Utils.PP
import Cryptol.Utils.Panic (panic)
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 Text.Read (readMaybe)
import Data.SBV.Dynamic (sbvCheckSolverInstallation)
import Prelude ()
import Prelude.Compat
data LoadedModule = LoadedModule
{ lName :: Maybe P.ModName
, lPath :: FilePath
}
data RW = RW
{ eLoadedMod :: Maybe LoadedModule
, eContinue :: Bool
, eIsBatch :: Bool
, eModuleEnv :: M.ModuleEnv
, eUserEnv :: UserEnv
, ePutStr :: String -> IO ()
, eLetEnabled :: Bool
, eUpdateTitle :: REPL ()
}
defaultRW :: Bool -> IO RW
defaultRW isBatch = do
env <- M.initialModuleEnv
return RW
{ eLoadedMod = Nothing
, eContinue = True
, eIsBatch = isBatch
, eModuleEnv = env
, eUserEnv = mkUserEnv userOptions
, ePutStr = putStr
, eLetEnabled = True
, eUpdateTitle = return ()
}
mkPrompt :: RW -> String
mkPrompt rw
| eIsBatch rw = ""
| otherwise = maybe "cryptol" pretty (lName =<< eLoadedMod rw) ++ "> "
newtype REPL a = REPL { unREPL :: IORef RW -> IO a }
runREPL :: Bool -> REPL a -> IO a
runREPL isBatch m = do
ref <- newIORef =<< defaultRW isBatch
unREPL m ref
instance Functor REPL where
fmap f m = REPL (\ ref -> fmap f (unREPL m ref))
instance Applicative REPL where
pure = return
(<*>) = ap
instance Monad REPL where
return x = REPL (\_ -> return x)
m >>= f = REPL $ \ref -> do
x <- unREPL m ref
unREPL (f x) ref
instance MonadIO REPL where
liftIO = io
instance MonadBase IO REPL where
liftBase = liftIO
instance MonadBaseControl IO REPL where
type StM REPL a = a
liftBaseWith f = REPL $ \ref ->
f $ \m -> unREPL m ref
restoreM x = return x
instance M.FreshM REPL where
liftSupply f = modifyRW $ \ RW { .. } ->
let (a,s') = f (M.meSupply eModuleEnv)
in (RW { eModuleEnv = eModuleEnv { M.meSupply = s' }, .. },a)
data REPLException
= ParseError ParseError
| FileNotFound FilePath
| DirectoryNotFound FilePath
| NoPatError [Error]
| NoIncludeError [IncludeError]
| EvalError EvalError
| ModuleSystemError NameDisp M.ModuleError
| EvalPolyError T.Schema
| TypeNotTestable T.Type
deriving (Show,Typeable)
instance X.Exception REPLException
instance PP REPLException where
ppPrec _ re = case re of
ParseError e -> ppError e
FileNotFound path -> sep [ text "File"
, text ("`" ++ path ++ "'")
, text"not found"
]
DirectoryNotFound path -> sep [ text "Directory"
, text ("`" ++ path ++ "'")
, text"not found or not a directory"
]
NoPatError es -> vcat (map pp es)
NoIncludeError es -> vcat (map ppIncludeError es)
ModuleSystemError ns me -> fixNameDisp ns (pp me)
EvalError e -> pp e
EvalPolyError s -> text "Cannot evaluate polymorphic value."
$$ text "Type:" <+> pp s
TypeNotTestable t -> text "The expression is not of a testable type."
$$ text "Type:" <+> pp t
raise :: REPLException -> REPL a
raise exn = io (X.throwIO exn)
catch :: REPL a -> (REPLException -> REPL a) -> REPL a
catch m k = REPL (\ ref -> unREPL m ref `X.catch` \ e -> unREPL (k e) ref)
rethrowEvalError :: IO a -> IO a
rethrowEvalError m = run `X.catch` rethrow
where
run = do
a <- m
return $! a
rethrow :: EvalError -> IO a
rethrow exn = X.throwIO (EvalError exn)
io :: IO a -> REPL a
io m = REPL (\ _ -> m)
getRW :: REPL RW
getRW = REPL readIORef
modifyRW :: (RW -> (RW,a)) -> REPL a
modifyRW f = REPL (\ ref -> atomicModifyIORef ref f)
modifyRW_ :: (RW -> RW) -> REPL ()
modifyRW_ f = REPL (\ ref -> modifyIORef ref f)
getPrompt :: REPL String
getPrompt = mkPrompt `fmap` getRW
setLoadedMod :: LoadedModule -> REPL ()
setLoadedMod n = do
modifyRW_ (\ rw -> rw { eLoadedMod = Just n })
updateREPLTitle
getLoadedMod :: REPL (Maybe LoadedModule)
getLoadedMod = eLoadedMod `fmap` getRW
setSearchPath :: [FilePath] -> REPL ()
setSearchPath path = do
me <- getModuleEnv
setModuleEnv $ me { M.meSearchPath = path }
prependSearchPath :: [FilePath] -> REPL ()
prependSearchPath path = do
me <- getModuleEnv
setModuleEnv $ me { M.meSearchPath = path ++ M.meSearchPath me }
shouldContinue :: REPL Bool
shouldContinue = eContinue `fmap` getRW
stop :: REPL ()
stop = modifyRW_ (\ rw -> rw { eContinue = False })
unlessBatch :: REPL () -> REPL ()
unlessBatch body = do
rw <- getRW
unless (eIsBatch rw) body
asBatch :: REPL () -> REPL ()
asBatch body = do
wasBatch <- eIsBatch `fmap` getRW
modifyRW_ $ (\ rw -> rw { eIsBatch = True })
body
modifyRW_ $ (\ rw -> rw { eIsBatch = wasBatch })
disableLet :: REPL ()
disableLet = modifyRW_ (\ rw -> rw { eLetEnabled = False })
enableLet :: REPL ()
enableLet = modifyRW_ (\ rw -> rw { eLetEnabled = True })
getLetEnabled :: REPL Bool
getLetEnabled = fmap eLetEnabled getRW
updateREPLTitle :: REPL ()
updateREPLTitle = unlessBatch $ do
rw <- getRW
eUpdateTitle rw
setUpdateREPLTitle :: REPL () -> REPL ()
setUpdateREPLTitle m = modifyRW_ (\rw -> rw { eUpdateTitle = m })
setPutStr :: (String -> IO ()) -> REPL ()
setPutStr fn = modifyRW_ (\rw -> rw { ePutStr = fn })
getPutStr :: REPL (String -> IO ())
getPutStr = fmap ePutStr getRW
rPutStr :: String -> REPL ()
rPutStr str = do
rw <- getRW
io $ ePutStr rw str
rPutStrLn :: String -> REPL ()
rPutStrLn str = rPutStr $ str ++ "\n"
rPrint :: Show a => a -> REPL ()
rPrint x = rPutStrLn (show x)
getFocusedEnv :: REPL (M.IfaceDecls,M.NamingEnv,NameDisp)
getFocusedEnv = do
me <- getModuleEnv
let (dyDecls,dyNames,dyDisp) = M.dynamicEnv me
let (fDecls,fNames,fDisp) = M.focusedEnv me
return ( dyDecls `mappend` fDecls
, dyNames `M.shadowing` fNames
, dyDisp `mappend` fDisp)
getVars :: REPL (Map.Map M.Name M.IfaceDecl)
getVars = do
(decls,_,_) <- getFocusedEnv
return (M.ifDecls decls)
getTSyns :: REPL (Map.Map M.Name T.TySyn)
getTSyns = do
(decls,_,_) <- getFocusedEnv
return (M.ifTySyns decls)
getNewtypes :: REPL (Map.Map M.Name T.Newtype)
getNewtypes = do
(decls,_,_) <- getFocusedEnv
return (M.ifNewtypes decls)
getExprNames :: REPL [String]
getExprNames =
do (_, fNames, _) <- getFocusedEnv
return (map (show . pp) (Map.keys (M.neExprs fNames)))
getTypeNames :: REPL [String]
getTypeNames =
do (_, fNames, _) <- getFocusedEnv
return (map (show . pp) (Map.keys (M.neTypes fNames)))
getPropertyNames :: REPL ([M.Name],NameDisp)
getPropertyNames =
do (decls,_,names) <- getFocusedEnv
let xs = M.ifDecls decls
ps = sortBy (comparing (from . M.nameLoc))
$ [ x | (x,d) <- Map.toList xs, T.PragmaProperty `elem` M.ifDeclPragmas d ]
return (ps, names)
getModuleEnv :: REPL M.ModuleEnv
getModuleEnv = eModuleEnv `fmap` getRW
setModuleEnv :: M.ModuleEnv -> REPL ()
setModuleEnv me = modifyRW_ (\rw -> rw { eModuleEnv = me })
getDynEnv :: REPL M.DynamicEnv
getDynEnv = (M.meDynEnv . eModuleEnv) `fmap` getRW
setDynEnv :: M.DynamicEnv -> REPL ()
setDynEnv denv = do
me <- getModuleEnv
setModuleEnv (me { M.meDynEnv = denv })
uniqify :: M.Name -> REPL M.Name
uniqify name =
case M.nameInfo name of
M.Declared ns ->
M.liftSupply (M.mkDeclared ns (M.nameIdent name) (M.nameFixity name) (M.nameLoc name))
M.Parameter ->
panic "[REPL] uniqify" ["tried to uniqify a parameter: " ++ pretty name]
freshName :: I.Ident -> REPL M.Name
freshName i = M.liftSupply (M.mkDeclared I.interactiveName i Nothing emptyRange)
type UserEnv = Map.Map String EnvVal
data EnvVal
= EnvString String
| EnvProg String [String]
| EnvNum !Int
| EnvBool Bool
deriving (Show)
mkUserEnv :: OptionMap -> UserEnv
mkUserEnv opts = Map.fromList $ do
opt <- leaves opts
return (optName opt, optDefault opt)
setUser :: String -> String -> REPL ()
setUser name val = case lookupTrie name userOptions of
[opt] -> setUserOpt opt
[] -> io (putStrLn ("Unknown env value `" ++ name ++ "`"))
_ -> io (putStrLn ("Ambiguous env value `" ++ name ++ "`"))
where
setUserOpt opt = case optDefault opt of
EnvString _ -> do r <- io (optCheck opt (EnvString val))
case r of
Just err -> io (putStrLn err)
Nothing -> writeEnv (EnvString val)
EnvProg _ _ ->
case splitOptArgs val of
prog:args -> do r <- io (optCheck opt (EnvProg prog args))
case r of
Just err -> io (putStrLn err)
Nothing -> writeEnv (EnvProg prog args)
[] -> io (putStrLn ("Failed to parse command for field, `" ++ name ++ "`"))
EnvNum _ -> case reads val of
[(x,_)] -> do r <- io (optCheck opt (EnvNum x))
case r of
Just err -> io (putStrLn err)
Nothing -> writeEnv (EnvNum x)
_ -> io (putStrLn ("Failed to parse number for field, `" ++ name ++ "`"))
EnvBool _
| any (`isPrefixOf` val) ["enable","on","yes"] ->
writeEnv (EnvBool True)
| any (`isPrefixOf` val) ["disable","off","no"] ->
writeEnv (EnvBool False)
| otherwise ->
io (putStrLn ("Failed to parse boolean for field, `" ++ name ++ "`"))
where
writeEnv ev =
do optEff opt ev
modifyRW_ (\rw -> rw { eUserEnv = Map.insert name ev (eUserEnv rw) })
splitOptArgs :: String -> [String]
splitOptArgs = unfoldr (parse "")
where
parse acc (c:cs) | isQuote c = quoted (c:acc) cs
| not (isSpace c) = parse (c:acc) cs
| otherwise = result acc cs
parse acc [] = result acc []
quoted acc (c:cs) | isQuote c = parse (c:acc) cs
| otherwise = quoted (c:acc) cs
quoted acc [] = result acc []
result [] [] = Nothing
result [] cs = parse [] (dropWhile isSpace cs)
result acc cs = Just (reverse acc, dropWhile isSpace cs)
isQuote :: Char -> Bool
isQuote c = c `elem` ("'\"" :: String)
tryGetUser :: String -> REPL (Maybe EnvVal)
tryGetUser name = do
rw <- getRW
return (Map.lookup name (eUserEnv rw))
getUser :: String -> REPL EnvVal
getUser name = do
mb <- tryGetUser name
case mb of
Just ev -> return ev
Nothing -> panic "[REPL] getUser" ["option `" ++ name ++ "` does not exist"]
type OptionMap = Trie OptionDescr
mkOptionMap :: [OptionDescr] -> OptionMap
mkOptionMap = foldl insert emptyTrie
where
insert m d = insertTrie (optName d) d m
data OptionDescr = OptionDescr
{ optName :: String
, optDefault :: EnvVal
, optCheck :: EnvVal -> IO (Maybe String)
, optHelp :: String
, optEff :: EnvVal -> REPL ()
}
simpleOpt :: String -> EnvVal -> (EnvVal -> IO (Maybe String)) -> String
-> OptionDescr
simpleOpt optName optDefault optCheck optHelp =
OptionDescr { optEff = \ _ -> return (), .. }
userOptions :: OptionMap
userOptions = mkOptionMap
[ simpleOpt "base" (EnvNum 16) checkBase
"the base to display words at"
, simpleOpt "debug" (EnvBool False) (const $ return Nothing)
"enable debugging output"
, simpleOpt "ascii" (EnvBool False) (const $ return Nothing)
"display 7- or 8-bit words using ASCII notation."
, simpleOpt "infLength" (EnvNum 5) checkInfLength
"The number of elements to display for infinite sequences."
, simpleOpt "tests" (EnvNum 100) (const $ return Nothing)
"The number of random tests to try."
, simpleOpt "satNum" (EnvString "1") checkSatNum
"The maximum number of :sat solutions to display (\"all\" for no limit)."
, simpleOpt "prover" (EnvString "z3") checkProver $
"The external SMT solver for :prove and :sat (" ++ proverListString ++ ")."
, simpleOpt "warnDefaulting" (EnvBool True) (const $ return Nothing)
"Choose if we should display warnings when defaulting."
, simpleOpt "warnShadowing" (EnvBool True) (const $ return Nothing)
"Choose if we should display warnings when shadowing symbols."
, simpleOpt "smtfile" (EnvString "-") (const $ return Nothing)
"The file to use for SMT-Lib scripts (for debugging or offline proving)"
, OptionDescr "mono-binds" (EnvBool True) (const $ return Nothing)
"Whether or not to generalize bindings in a where-clause" $
\case EnvBool b -> do me <- getModuleEnv
setModuleEnv me { M.meMonoBinds = b }
_ -> return ()
, OptionDescr "tc-solver" (EnvProg "z3" [ "-smt2", "-in" ])
(const (return Nothing))
"The solver that will be used by the type checker" $
\case EnvProg prog args -> do me <- getModuleEnv
let cfg = M.meSolverConfig me
setModuleEnv me { M.meSolverConfig =
cfg { T.solverPath = prog
, T.solverArgs = args } }
_ -> return ()
, OptionDescr "tc-debug" (EnvNum 0)
(const (return Nothing))
"Enable type-checker debugging output" $
\case EnvNum n -> do me <- getModuleEnv
let cfg = M.meSolverConfig me
setModuleEnv me { M.meSolverConfig = cfg{ T.solverVerbose = fromIntegral n } }
_ -> return ()
, OptionDescr "core-lint" (EnvBool False)
(const (return Nothing))
"Enable sanity checking of type-checker" $
let setIt x = do me <- getModuleEnv
setModuleEnv me { M.meCoreLint = x }
in \case EnvBool True -> setIt M.CoreLint
EnvBool False -> setIt M.NoCoreLint
_ -> return ()
]
checkBase :: EnvVal -> IO (Maybe String)
checkBase val = case val of
EnvNum n
| n >= 2 && n <= 36 -> return Nothing
| otherwise -> return $ Just "base must fall between 2 and 36"
_ -> return $ Just "unable to parse a value for base"
checkInfLength :: EnvVal -> IO (Maybe String)
checkInfLength val = case val of
EnvNum n
| n >= 0 -> return Nothing
| otherwise -> return $ Just "the number of elements should be positive"
_ -> return $ Just "unable to parse a value for infLength"
checkProver :: EnvVal -> IO (Maybe String)
checkProver val = case val of
EnvString s
| s `notElem` proverNames -> return $ Just $ "Prover must be " ++ proverListString
| s `elem` ["offline", "any"] -> return Nothing
| otherwise -> do let prover = lookupProver s
available <- sbvCheckSolverInstallation prover
unless available $
putStrLn $ "Warning: " ++ s ++ " installation not found"
return Nothing
_ -> return $ Just "unable to parse a value for prover"
proverListString :: String
proverListString = concatMap (++ ", ") (init proverNames) ++ "or " ++ last proverNames
checkSatNum :: EnvVal -> IO (Maybe String)
checkSatNum val = case val of
EnvString "all" -> return Nothing
EnvString s ->
case readMaybe s :: Maybe Int of
Just n | n >= 1 -> return Nothing
_ -> return $ Just "must be an integer > 0 or \"all\""
_ -> return $ Just "unable to parse a value for satNum"
getUserSatNum :: REPL SatNum
getUserSatNum = do
EnvString s <- getUser "satNum"
case s of
"all" -> return AllSat
_ | Just n <- readMaybe s -> return (SomeSat n)
_ -> panic "REPL.Monad.getUserSatNum"
[ "invalid satNum option" ]
whenDebug :: REPL () -> REPL ()
whenDebug m = do
EnvBool b <- getUser "debug"
when b m
smokeTest :: REPL [Smoke]
smokeTest = catMaybes <$> sequence tests
where
tests = [ z3exists ]
type SmokeTest = REPL (Maybe Smoke)
data Smoke
= Z3NotFound
deriving (Show, Eq)
instance PP Smoke where
ppPrec _ smoke =
case smoke of
Z3NotFound -> text . intercalate " " $ [
"[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 = do
mPath <- io $ findExecutable "z3"
case mPath of
Nothing -> return (Just Z3NotFound)
Just _ -> return Nothing