module Cryptol.REPL.Command (
Command(..), CommandDescr(..), CommandBody(..)
, parseCommand
, runCommand
, splitCommand
, findCommand
, findCommandExact
, findNbCommand
, moduleCmd, loadCmd, loadPrelude, setOptionCmd
, interactiveConfig
, replParseExpr
, replEvalExpr
, replCheckExpr
, qcCmd, QCMode(..)
, satCmd
, proveCmd
, onlineProveSat
, offlineProveSat
, handleCtrlC
, sanitize
, replParse
, liftModuleCmd
, moduleCmdResult
) where
import Cryptol.REPL.Monad
import Cryptol.REPL.Trie
import qualified Cryptol.ModuleSystem as M
import qualified Cryptol.ModuleSystem.Name as M
import qualified Cryptol.ModuleSystem.NamingEnv as M
import qualified Cryptol.ModuleSystem.Renamer as M (RenamerWarning(SymbolShadowed))
import qualified Cryptol.Utils.Ident as M
import qualified Cryptol.Eval.Value as E
import Cryptol.Testing.Concrete
import qualified Cryptol.Testing.Random as TestR
import Cryptol.Parser
(parseExprWith,parseReplWith,ParseError(),Config(..),defaultConfig
,parseModName,parseHelpName)
import qualified Cryptol.TypeCheck.AST as T
import qualified Cryptol.TypeCheck.Subst as T
import qualified Cryptol.TypeCheck.InferTypes as T
import Cryptol.TypeCheck.Solve(defaultReplExpr)
import qualified Cryptol.TypeCheck.Solver.CrySAT as CrySAT
import Cryptol.TypeCheck.PP (dump,ppWithNames)
import Cryptol.Utils.PP
import Cryptol.Utils.Panic(panic)
import qualified Cryptol.Parser.AST as P
import qualified Cryptol.Transform.Specialize as S
import Cryptol.Symbolic (ProverCommand(..), QueryType(..), SatNum(..))
import qualified Cryptol.Symbolic as Symbolic
import Control.DeepSeq
import qualified Control.Exception as X
import Control.Monad hiding (mapM, mapM_)
import qualified Data.ByteString as BS
import Data.Bits ((.&.))
import Data.Char (isSpace,isPunctuation,isSymbol)
import Data.Function (on)
import Data.List (intercalate,nub,sortBy,partition)
import Data.Maybe (fromMaybe,mapMaybe)
import System.Environment (lookupEnv)
import System.Exit (ExitCode(ExitSuccess))
import System.Process (shell,createProcess,waitForProcess)
import qualified System.Process as Process(runCommand)
import System.FilePath((</>), isPathSeparator)
import System.Directory(getHomeDirectory,setCurrentDirectory,doesDirectoryExist)
import qualified Data.Map as Map
import qualified Data.Set as Set
import qualified Data.IntMap as IntMap
import System.IO(hFlush,stdout)
import System.Random.TF(newTFGen)
import Numeric (showFFloat)
import qualified Data.Text as ST
import qualified Data.Text.Lazy as T
import Prelude ()
import Prelude.Compat
data Command
= Command (REPL ())
| Ambiguous String [String]
| Unknown String
data CommandDescr = CommandDescr
{ cNames :: [String]
, cBody :: CommandBody
, cHelp :: String
}
instance Show CommandDescr where
show = show . cNames
instance Eq CommandDescr where
(==) = (==) `on` cNames
instance Ord CommandDescr where
compare = compare `on` cNames
data CommandBody
= ExprArg (String -> REPL ())
| FileExprArg (FilePath -> String -> REPL ())
| DeclsArg (String -> REPL ())
| ExprTypeArg (String -> REPL ())
| FilenameArg (FilePath -> REPL ())
| OptionArg (String -> REPL ())
| ShellArg (String -> REPL ())
| NoArg (REPL ())
commands :: CommandMap
commands = foldl insert emptyTrie commandList
where
insert m d = foldl (insertOne d) m (cNames d)
insertOne d m name = insertTrie name d m
nbCommands :: CommandMap
nbCommands = foldl insert emptyTrie nbCommandList
where
insert m d = foldl (insertOne d) m (cNames d)
insertOne d m name = insertTrie name d m
nbCommandList :: [CommandDescr]
nbCommandList =
[ CommandDescr [ ":t", ":type" ] (ExprArg typeOfCmd)
"check the type of an expression"
, CommandDescr [ ":b", ":browse" ] (ExprTypeArg browseCmd)
"display the current environment"
, CommandDescr [ ":?", ":help" ] (ExprArg helpCmd)
"display a brief description about a function"
, CommandDescr [ ":s", ":set" ] (OptionArg setOptionCmd)
"set an environmental option (:set on its own displays current values)"
, CommandDescr [ ":check" ] (ExprArg (void . qcCmd QCRandom))
"use random testing to check that the argument always returns true (if no argument, check all properties)"
, CommandDescr [ ":exhaust" ] (ExprArg (void . qcCmd QCExhaust))
"use exhaustive testing to prove that the argument always returns true (if no argument, check all properties)"
, CommandDescr [ ":prove" ] (ExprArg proveCmd)
"use an external solver to prove that the argument always returns true (if no argument, check all properties)"
, CommandDescr [ ":sat" ] (ExprArg satCmd)
"use a solver to find a satisfying assignment for which the argument returns true (if no argument, find an assignment for all properties)"
, CommandDescr [ ":debug_specialize" ] (ExprArg specializeCmd)
"do type specialization on a closed expression"
]
commandList :: [CommandDescr]
commandList =
nbCommandList ++
[ CommandDescr [ ":q", ":quit" ] (NoArg quitCmd)
"exit the REPL"
, CommandDescr [ ":l", ":load" ] (FilenameArg loadCmd)
"load a module"
, CommandDescr [ ":r", ":reload" ] (NoArg reloadCmd)
"reload the currently loaded module"
, CommandDescr [ ":e", ":edit" ] (FilenameArg editCmd)
"edit the currently loaded module"
, CommandDescr [ ":!" ] (ShellArg runShellCmd)
"execute a command in the shell"
, CommandDescr [ ":cd" ] (FilenameArg cdCmd)
"set the current working directory"
, CommandDescr [ ":m", ":module" ] (FilenameArg moduleCmd)
"load a module"
, CommandDescr [ ":w", ":writeByteArray" ] (FileExprArg writeFileCmd)
"write data of type `fin n => [n][8]` to a file"
, CommandDescr [ ":readByteArray" ] (FilenameArg readFileCmd)
"read data from a file as type `fin n => [n][8]`, binding the value to variable `it`"
]
genHelp :: [CommandDescr] -> [String]
genHelp cs = map cmdHelp cs
where
cmdHelp cmd = concat [ " ", cmdNames cmd, pad (cmdNames cmd), cHelp cmd ]
cmdNames cmd = intercalate ", " (cNames cmd)
padding = 2 + maximum (map (length . cmdNames) cs)
pad n = replicate (max 0 (padding length n)) ' '
runCommand :: Command -> REPL ()
runCommand c = case c of
Command cmd -> cmd `Cryptol.REPL.Monad.catch` handler
where
handler re = rPutStrLn "" >> rPrint (pp re)
Unknown cmd -> rPutStrLn ("Unknown command: " ++ cmd)
Ambiguous cmd cmds -> do
rPutStrLn (cmd ++ " is ambiguous, it could mean one of:")
rPutStrLn ("\t" ++ intercalate ", " cmds)
getPPValOpts :: REPL E.PPOpts
getPPValOpts =
do EnvNum base <- getUser "base"
EnvBool ascii <- getUser "ascii"
EnvNum infLength <- getUser "infLength"
return E.PPOpts { E.useBase = base
, E.useAscii = ascii
, E.useInfLength = infLength
}
evalCmd :: String -> REPL ()
evalCmd str = do
letEnabled <- getLetEnabled
ri <- if letEnabled
then replParseInput str
else P.ExprInput <$> replParseExpr str
case ri of
P.ExprInput expr -> do
(val,_ty) <- replEvalExpr expr
ppOpts <- getPPValOpts
out <- io $ rethrowEvalError
$ return $!! show $ pp $ E.WithBase ppOpts val
rPutStrLn out
P.LetInput decl -> do
replEvalDecl decl
data QCMode = QCRandom | QCExhaust deriving (Eq, Show)
qcCmd :: QCMode -> String -> REPL [TestReport]
qcCmd qcMode "" =
do (xs,disp) <- getPropertyNames
let nameStr x = show (fixNameDisp disp (pp x))
if null xs
then rPutStrLn "There are no properties in scope." *> return []
else concat <$> (forM xs $ \x ->
do let str = nameStr x
rPutStr $ "property " ++ str ++ " "
qcCmd qcMode str)
qcCmd qcMode str =
do expr <- replParseExpr str
(val,ty) <- replEvalExpr expr
EnvNum testNum <- getUser "tests"
case testableType ty of
Just (sz,vss) | qcMode == QCExhaust || sz <= toInteger testNum -> do
rPutStrLn "Using exhaustive testing."
let f _ [] = panic "Cryptol.REPL.Command"
["Exhaustive testing ran out of test cases"]
f _ (vs : vss1) = do
result <- io $ runOneTest val vs
return (result, vss1)
testSpec = TestSpec {
testFn = f
, testProp = str
, testTotal = sz
, testPossible = sz
, testRptProgress = ppProgress
, testClrProgress = delProgress
, testRptFailure = ppFailure
, testRptSuccess = do
delTesting
prtLn $ "passed " ++ show sz ++ " tests."
rPutStrLn "Q.E.D."
}
prt testingMsg
report <- runTests testSpec vss
return [report]
Just (sz,_) -> case TestR.testableType ty of
Nothing -> raise (TypeNotTestable ty)
Just gens -> do
rPutStrLn "Using random testing."
let testSpec = TestSpec {
testFn = \sz' g -> io $ TestR.runOneTest val gens sz' g
, testProp = str
, testTotal = toInteger testNum
, testPossible = sz
, testRptProgress = ppProgress
, testClrProgress = delProgress
, testRptFailure = ppFailure
, testRptSuccess = do
delTesting
prtLn $ "passed " ++ show testNum ++ " tests."
}
prt testingMsg
g <- io newTFGen
report <- runTests testSpec g
when (isPass (reportResult report)) $ do
let szD = fromIntegral sz :: Double
percent = fromIntegral (testNum * 100) / szD
showValNum
| sz > 2 ^ (20::Integer) =
"2^^" ++ show (lg2 sz)
| otherwise = show sz
rPutStrLn $ "Coverage: "
++ showFFloat (Just 2) percent "% ("
++ show testNum ++ " of "
++ showValNum ++ " values)"
return [report]
Nothing -> return []
where
testingMsg = "testing..."
totProgressWidth = 4
lg2 :: Integer -> Integer
lg2 x | x >= 2^(1024::Int) = 1024 + lg2 (x `div` 2^(1024::Int))
| x == 0 = 0
| otherwise = let valNumD = fromIntegral x :: Double
in round $ logBase 2 valNumD :: Integer
prt msg = rPutStr msg >> io (hFlush stdout)
prtLn msg = rPutStrLn msg >> io (hFlush stdout)
ppProgress this tot = unlessBatch $
let percent = show (div (100 * this) tot) ++ "%"
width = length percent
pad = replicate (totProgressWidth width) ' '
in prt (pad ++ percent)
del n = unlessBatch $ prt (replicate n '\BS')
delTesting = del (length testingMsg)
delProgress = del totProgressWidth
ppFailure failure = do
delTesting
opts <- getPPValOpts
case failure of
FailFalse [] -> do
prtLn "FAILED"
FailFalse vs -> do
prtLn "FAILED for the following inputs:"
mapM_ (rPrint . pp . E.WithBase opts) vs
FailError err [] -> do
prtLn "ERROR"
rPrint (pp err)
FailError err vs -> do
prtLn "ERROR for the following inputs:"
mapM_ (rPrint . pp . E.WithBase opts) vs
rPrint (pp err)
Pass -> panic "Cryptol.REPL.Command" ["unexpected Test.Pass"]
satCmd, proveCmd :: String -> REPL ()
satCmd = cmdProveSat True
proveCmd = cmdProveSat False
cmdProveSat :: Bool -> String -> REPL ()
cmdProveSat isSat "" =
do (xs,disp) <- getPropertyNames
let nameStr x = show (fixNameDisp disp (pp x))
if null xs
then rPutStrLn "There are no properties in scope."
else forM_ xs $ \x ->
do let str = nameStr x
if isSat
then rPutStr $ ":sat " ++ str ++ "\n\t"
else rPutStr $ ":prove " ++ str ++ "\n\t"
cmdProveSat isSat str
cmdProveSat isSat str = do
let cexStr | isSat = "satisfying assignment"
| otherwise = "counterexample"
EnvString proverName <- getUser "prover"
EnvString fileName <- getUser "smtfile"
let mfile = if fileName == "-" then Nothing else Just fileName
case proverName of
"offline" -> do
result <- offlineProveSat isSat str mfile
case result of
Left msg -> rPutStrLn msg
Right smtlib -> do
let filename = fromMaybe "standard output" mfile
let satWord | isSat = "satisfiability"
| otherwise = "validity"
rPutStrLn $
"Writing to SMT-Lib file " ++ filename ++ "..."
rPutStrLn $
"To determine the " ++ satWord ++
" of the expression, use an external SMT solver."
case mfile of
Just path -> io $ writeFile path smtlib
Nothing -> rPutStr smtlib
_ -> do
result <- onlineProveSat isSat str mfile
ppOpts <- getPPValOpts
case result of
Symbolic.EmptyResult ->
panic "REPL.Command" [ "got EmptyResult for online prover query" ]
Symbolic.ProverError msg -> rPutStrLn msg
Symbolic.ThmResult ts -> do
rPutStrLn (if isSat then "Unsatisfiable" else "Q.E.D.")
(t, e) <- mkSolverResult cexStr (not isSat) (Left ts)
bindItVariable t e
Symbolic.AllSatResult tevss -> do
let tess = map (map $ \(t,e,_) -> (t,e)) tevss
vss = map (map $ \(_,_,v) -> v) tevss
ppvs vs = do
parseExpr <- replParseExpr str
let docs = map (pp . E.WithBase ppOpts) vs
doc = ppPrec 3 parseExpr
rPrint $ hang doc 2 (sep docs) <+>
text (if isSat then "= True" else "= False")
resultRecs <- mapM (mkSolverResult cexStr isSat . Right) tess
let collectTes tes = (t, es)
where
(ts, es) = unzip tes
t = case nub ts of
[t'] -> t'
_ -> panic "REPL.Command.onlineProveSat"
[ "satisfying assignments with different types" ]
(ty, exprs) =
case resultRecs of
[] -> panic "REPL.Command.onlineProveSat"
[ "no satisfying assignments after mkSovlerResult" ]
[(t, e)] -> (t, [e])
_ -> collectTes resultRecs
forM_ vss ppvs
case (ty, exprs) of
(t, [e]) -> bindItVariable t e
(t, es ) -> bindItVariables t es
onlineProveSat :: Bool
-> String -> Maybe FilePath -> REPL Symbolic.ProverResult
onlineProveSat isSat str mfile = do
EnvString proverName <- getUser "prover"
EnvBool verbose <- getUser "debug"
satNum <- getUserSatNum
parseExpr <- replParseExpr str
(_, expr, schema) <- replCheckExpr parseExpr
decls <- fmap M.deDecls getDynEnv
let cmd = Symbolic.ProverCommand {
pcQueryType = if isSat then SatQuery satNum else ProveQuery
, pcProverName = proverName
, pcVerbose = verbose
, pcExtraDecls = decls
, pcSmtFile = mfile
, pcExpr = expr
, pcSchema = schema
}
liftModuleCmd $ Symbolic.satProve cmd
offlineProveSat :: Bool -> String -> Maybe FilePath -> REPL (Either String String)
offlineProveSat isSat str mfile = do
EnvBool verbose <- getUser "debug"
parseExpr <- replParseExpr str
(_, expr, schema) <- replCheckExpr parseExpr
decls <- fmap M.deDecls getDynEnv
let cmd = Symbolic.ProverCommand {
pcQueryType = if isSat then SatQuery (SomeSat 0) else ProveQuery
, pcProverName = "offline"
, pcVerbose = verbose
, pcExtraDecls = decls
, pcSmtFile = mfile
, pcExpr = expr
, pcSchema = schema
}
liftModuleCmd $ Symbolic.satProveOffline cmd
rIdent :: M.Ident
rIdent = M.packIdent "result"
mkSolverResult :: String
-> Bool
-> Either [T.Type] [(T.Type, T.Expr)]
-> REPL (T.Type, T.Expr)
mkSolverResult thing result earg =
do prims <- getPrimMap
let addError t = (t, T.eError prims t ("no " ++ thing ++ " available"))
argF = case earg of
Left ts -> mkArgs (map addError ts)
Right tes -> mkArgs tes
eTrue = T.ePrim prims (M.packIdent "True")
eFalse = T.ePrim prims (M.packIdent "False")
resultE = if result then eTrue else eFalse
rty = T.TRec $ [(rIdent, T.tBit )] ++ map fst argF
re = T.ERec $ [(rIdent, resultE)] ++ map snd argF
return (rty, re)
where
mkArgs tes = zipWith mkArg [1 :: Int ..] tes
where
mkArg n (t,e) =
let argName = M.packIdent ("arg" ++ show n)
in ((argName,t),(argName,e))
specializeCmd :: String -> REPL ()
specializeCmd str = do
parseExpr <- replParseExpr str
(_, expr, schema) <- replCheckExpr parseExpr
spexpr <- replSpecExpr expr
rPutStrLn "Expression type:"
rPrint $ pp schema
rPutStrLn "Original expression:"
rPutStrLn $ dump expr
rPutStrLn "Specialized expression:"
rPutStrLn $ dump spexpr
typeOfCmd :: String -> REPL ()
typeOfCmd str = do
expr <- replParseExpr str
(_re,def,sig) <- replCheckExpr expr
whenDebug (rPutStrLn (dump def))
(_,_,names) <- getFocusedEnv
rPrint $ runDoc names $ ppPrec 2 expr <+> text ":" <+> pp sig
readFileCmd :: FilePath -> REPL ()
readFileCmd fp = do
bytes <- replReadFile fp (\err -> rPutStrLn (show err) >> return Nothing)
case bytes of
Nothing -> return ()
Just bs ->
do pm <- getPrimMap
let expr = T.eString pm (map (toEnum . fromIntegral) (BS.unpack bs))
ty = T.tString (BS.length bs)
bindItVariable ty expr
writeFileCmd :: FilePath -> String -> REPL ()
writeFileCmd file str = do
expr <- replParseExpr str
(val,ty) <- replEvalExpr expr
if not (tIsByteSeq ty)
then rPrint $ "Cannot write expression of types other than [n][8]."
<+> "Type was: " <+> pp ty
else wf file =<< serializeValue val
where
wf fp bytes = replWriteFile fp bytes (rPutStrLn . show)
tIsByteSeq x = maybe False
(tIsByte . snd)
(T.tIsSeq x)
tIsByte x = maybe False
(\(n,b) -> T.tIsBit b && T.tIsNum n == Just 8)
(T.tIsSeq x)
serializeValue (E.VSeq _ vs) =
return $ BS.pack $ map (serializeByte . E.fromVWord) vs
serializeValue _ =
panic "Cryptol.REPL.Command.writeFileCmd"
["Impossible: Non-VSeq value of type [n][8]."]
serializeByte (E.BV _ v) = fromIntegral (v .&. 0xFF)
reloadCmd :: REPL ()
reloadCmd = do
mb <- getLoadedMod
case mb of
Just m -> loadCmd (lPath m)
Nothing -> return ()
editCmd :: String -> REPL ()
editCmd path
| null path = do
mb <- getLoadedMod
case mb of
Just m -> do
success <- replEdit (lPath m)
if success
then loadCmd (lPath m)
else return ()
Nothing -> do
rPutStrLn "No files to edit."
return ()
| otherwise = do
_ <- replEdit path
mb <- getLoadedMod
case mb of
Nothing -> loadCmd path
Just _ -> return ()
moduleCmd :: String -> REPL ()
moduleCmd modString
| null modString = return ()
| otherwise = do
case parseModName modString of
Just m -> loadCmd =<< liftModuleCmd (M.findModule m)
Nothing -> rPutStrLn "Invalid module name."
loadPrelude :: REPL ()
loadPrelude = moduleCmd $ show $ pp M.preludeName
loadCmd :: FilePath -> REPL ()
loadCmd path
| null path = return ()
| otherwise = do
setLoadedMod LoadedModule
{ lName = Nothing
, lPath = path
}
m <- liftModuleCmd (M.loadModuleByPath path)
whenDebug (rPutStrLn (dump m))
setLoadedMod LoadedModule
{ lName = Just (T.mName m)
, lPath = path
}
setDynEnv mempty
quitCmd :: REPL ()
quitCmd = stop
browseCmd :: String -> REPL ()
browseCmd pfx = do
(iface,names,disp) <- getFocusedEnv
let (visibleTypes,visibleDecls) = M.visibleNames names
(visibleType,visibleDecl)
| null pfx =
((`Set.member` visibleTypes)
,(`Set.member` visibleDecls))
| otherwise =
(\n -> n `Set.member` visibleTypes && pfx `isNamePrefix` n
,\n -> n `Set.member` visibleDecls && pfx `isNamePrefix` n)
browseTSyns visibleType iface disp
browseNewtypes visibleType iface disp
browseVars visibleDecl iface disp
browseTSyns :: (M.Name -> Bool) -> M.IfaceDecls -> NameDisp -> REPL ()
browseTSyns isVisible M.IfaceDecls { .. } names = do
let tsyns = sortBy (M.cmpNameDisplay names `on` T.tsName)
[ ts | ts <- Map.elems ifTySyns, isVisible (T.tsName ts) ]
unless (null tsyns) $ do
rPutStrLn "Type Synonyms"
rPutStrLn "============="
rPrint (runDoc names (nest 4 (vcat (map pp tsyns))))
rPutStrLn ""
browseNewtypes :: (M.Name -> Bool) -> M.IfaceDecls -> NameDisp -> REPL ()
browseNewtypes isVisible M.IfaceDecls { .. } names = do
let nts = sortBy (M.cmpNameDisplay names `on` T.ntName)
[ nt | nt <- Map.elems ifNewtypes, isVisible (T.ntName nt) ]
unless (null nts) $ do
rPutStrLn "Newtypes"
rPutStrLn "========"
rPrint (runDoc names (nest 4 (vcat (map T.ppNewtypeShort nts))))
rPutStrLn ""
browseVars :: (M.Name -> Bool) -> M.IfaceDecls -> NameDisp -> REPL ()
browseVars isVisible M.IfaceDecls { .. } names = do
let vars = sortBy (M.cmpNameDisplay names `on` M.ifDeclName)
[ d | d <- Map.elems ifDecls, isVisible (M.ifDeclName d) ]
let isProp p = T.PragmaProperty `elem` (M.ifDeclPragmas p)
(props,syms) = partition isProp vars
ppBlock "Properties" props
ppBlock "Symbols" syms
where
ppBlock name xs = unless (null xs) $
do rPutStrLn name
rPutStrLn (replicate (length name) '=')
let ppVar M.IfaceDecl { .. } = pp ifDeclName <+> char ':' <+> pp ifDeclSig
rPrint (runDoc names (nest 4 (vcat (map ppVar xs))))
rPutStrLn ""
setOptionCmd :: String -> REPL ()
setOptionCmd str
| Just value <- mbValue = setUser key value
| null key = mapM_ (describe . optName) (leaves userOptions)
| otherwise = describe key
where
(before,after) = break (== '=') str
key = trim before
mbValue = case after of
_ : stuff -> Just (trim stuff)
_ -> Nothing
describe k = do
ev <- tryGetUser k
case ev of
Just (EnvString s) -> rPutStrLn (k ++ " = " ++ s)
Just (EnvProg p as) -> rPutStrLn (k ++ " = " ++ intercalate " " (p:as))
Just (EnvNum n) -> rPutStrLn (k ++ " = " ++ show n)
Just (EnvBool True) -> rPutStrLn (k ++ " = on")
Just (EnvBool False) -> rPutStrLn (k ++ " = off")
Nothing -> do rPutStrLn ("Unknown user option: `" ++ k ++ "`")
when (any isSpace k) $ do
let (k1, k2) = break isSpace k
rPutStrLn ("Did you mean: `:set " ++ k1 ++ " =" ++ k2 ++ "`?")
helpCmd :: String -> REPL ()
helpCmd cmd
| null cmd = mapM_ rPutStrLn (genHelp commandList)
| otherwise =
case parseHelpName cmd of
Just qname ->
do (env,rnEnv,nameEnv) <- getFocusedEnv
name <- liftModuleCmd (M.renameVar rnEnv qname)
case Map.lookup name (M.ifDecls env) of
Just M.IfaceDecl { .. } ->
do rPutStrLn ""
let property
| P.PragmaProperty `elem` ifDeclPragmas = text "property"
| otherwise = empty
rPrint $ runDoc nameEnv
$ nest 4
$ property
<+> pp qname
<+> colon
<+> pp (ifDeclSig)
case ifDeclDoc of
Just str -> rPutStrLn ('\n' : str)
Nothing -> return ()
Nothing -> rPutStrLn "// No documentation is available."
Nothing ->
rPutStrLn ("Unable to parse name: " ++ cmd)
runShellCmd :: String -> REPL ()
runShellCmd cmd
= io $ do h <- Process.runCommand cmd
_ <- waitForProcess h
return ()
cdCmd :: FilePath -> REPL ()
cdCmd f | null f = rPutStrLn $ "[error] :cd requires a path argument"
| otherwise = do
exists <- io $ doesDirectoryExist f
if exists
then io $ setCurrentDirectory f
else raise $ DirectoryNotFound f
handleCtrlC :: REPL ()
handleCtrlC = rPutStrLn "Ctrl-C"
isNamePrefix :: String -> M.Name -> Bool
isNamePrefix pfx =
let pfx' = ST.pack pfx
in \n -> case M.nameInfo n of
M.Declared _ -> pfx' `ST.isPrefixOf` M.identText (M.nameIdent n)
M.Parameter -> False
replParse :: (String -> Either ParseError a) -> String -> REPL a
replParse parse str = case parse str of
Right a -> return a
Left e -> raise (ParseError e)
replParseInput :: String -> REPL (P.ReplInput P.PName)
replParseInput = replParse (parseReplWith interactiveConfig . T.pack)
replParseExpr :: String -> REPL (P.Expr P.PName)
replParseExpr = replParse (parseExprWith interactiveConfig . T.pack)
interactiveConfig :: Config
interactiveConfig = defaultConfig { cfgSource = "<interactive>" }
getPrimMap :: REPL M.PrimMap
getPrimMap = liftModuleCmd M.getPrimMap
liftModuleCmd :: M.ModuleCmd a -> REPL a
liftModuleCmd cmd = moduleCmdResult =<< io . cmd =<< getModuleEnv
moduleCmdResult :: M.ModuleRes a -> REPL a
moduleCmdResult (res,ws0) = do
EnvBool warnDefaulting <- getUser "warnDefaulting"
EnvBool warnShadowing <- getUser "warnShadowing"
let isDefaultWarn (T.DefaultingTo _ _) = True
isDefaultWarn _ = False
filterDefaults w | warnDefaulting = Just w
filterDefaults (M.TypeCheckWarnings xs) =
case filter (not . isDefaultWarn . snd) xs of
[] -> Nothing
ys -> Just (M.TypeCheckWarnings ys)
filterDefaults w = Just w
isShadowWarn (M.SymbolShadowed {}) = True
filterShadowing w | warnShadowing = Just w
filterShadowing (M.RenamerWarnings xs) =
case filter (not . isShadowWarn) xs of
[] -> Nothing
ys -> Just (M.RenamerWarnings ys)
filterShadowing w = Just w
let ws = mapMaybe filterDefaults . mapMaybe filterShadowing $ ws0
(_,_,names) <- getFocusedEnv
mapM_ (rPrint . runDoc names . pp) ws
case res of
Right (a,me') -> setModuleEnv me' >> return a
Left err -> raise (ModuleSystemError names err)
replCheckExpr :: P.Expr P.PName -> REPL (P.Expr M.Name,T.Expr,T.Schema)
replCheckExpr e = liftModuleCmd $ M.checkExpr e
replCheckDecls :: [P.Decl P.PName] -> REPL [T.DeclGroup]
replCheckDecls ds = do
npds <- liftModuleCmd (M.noPat ds)
let mkTop d = P.Decl P.TopLevel { P.tlExport = P.Public
, P.tlDoc = Nothing
, P.tlValue = d }
(names,ds') <- liftModuleCmd (M.checkDecls (map mkTop npds))
denv <- getDynEnv
setDynEnv denv { M.deNames = names `M.shadowing` M.deNames denv }
return ds'
replSpecExpr :: T.Expr -> REPL T.Expr
replSpecExpr e = liftModuleCmd $ S.specialize e
replEvalExpr :: P.Expr P.PName -> REPL (E.Value, T.Type)
replEvalExpr expr =
do (_,def,sig) <- replCheckExpr expr
me <- getModuleEnv
let cfg = M.meSolverConfig me
mbDef <- io $ CrySAT.withSolver cfg (\s -> defaultReplExpr s def sig)
(def1,ty) <-
case mbDef of
Nothing -> raise (EvalPolyError sig)
Just (tys,def1) ->
do let nms = T.addTNames (T.sVars sig) IntMap.empty
mapM_ (warnDefault nms) tys
let su = T.listSubst [ (T.tpVar a, t) | (a,t) <- tys ]
return (def1, T.apSubst su (T.sType sig))
val <- liftModuleCmd (M.evalExpr def1)
_ <- io $ rethrowEvalError $ X.evaluate val
whenDebug (rPutStrLn (dump def1))
bindItVariable ty def1
return (val,ty)
where
warnDefault ns (x,t) =
rPrint $ text "Assuming" <+> ppWithNames ns x <+> text "=" <+> pp t
itIdent :: M.Ident
itIdent = M.packIdent "it"
replWriteFile :: FilePath -> BS.ByteString -> (X.SomeException -> REPL ()) -> REPL ()
replWriteFile fp bytes handler =
do x <- io $ X.catch (BS.writeFile fp bytes >> return Nothing) (return . Just)
maybe (return ()) handler x
replReadFile :: FilePath -> (X.SomeException -> REPL (Maybe BS.ByteString)) -> REPL (Maybe BS.ByteString)
replReadFile fp handler =
do x <- io $ X.catch (Right `fmap` BS.readFile fp) (\e -> return $ Left e)
either handler (return . Just) x
bindItVariable :: T.Type -> T.Expr -> REPL ()
bindItVariable ty expr = do
freshIt <- freshName itIdent
let schema = T.Forall { T.sVars = []
, T.sProps = []
, T.sType = ty
}
decl = T.Decl { T.dName = freshIt
, T.dSignature = schema
, T.dDefinition = T.DExpr expr
, T.dPragmas = []
, T.dInfix = False
, T.dFixity = Nothing
, T.dDoc = Nothing
}
liftModuleCmd (M.evalDecls [T.NonRecursive decl])
denv <- getDynEnv
let nenv' = M.singletonE (P.UnQual itIdent) freshIt
`M.shadowing` M.deNames denv
setDynEnv $ denv { M.deNames = nenv' }
bindItVariables :: T.Type -> [T.Expr] -> REPL ()
bindItVariables ty exprs = bindItVariable seqTy seqExpr
where
len = length exprs
seqTy = T.tSeq (T.tNum len) ty
seqExpr = T.EList exprs ty
replEvalDecl :: P.Decl P.PName -> REPL ()
replEvalDecl decl = do
dgs <- replCheckDecls [decl]
whenDebug (mapM_ (\dg -> (rPutStrLn (dump dg))) dgs)
liftModuleCmd (M.evalDecls dgs)
replEdit :: String -> REPL Bool
replEdit file = do
mb <- io (lookupEnv "EDITOR")
let editor = fromMaybe "vim" mb
io $ do
(_,_,_,ph) <- createProcess (shell (unwords [editor, file]))
exit <- waitForProcess ph
return (exit == ExitSuccess)
type CommandMap = Trie CommandDescr
sanitize :: String -> String
sanitize = dropWhile isSpace
sanitizeEnd :: String -> String
sanitizeEnd = reverse . sanitize . reverse
trim :: String -> String
trim = sanitizeEnd . sanitize
splitCommand :: String -> Maybe (String,String)
splitCommand txt =
case sanitize txt of
':' : more
| (as,bs) <- span (\x -> isPunctuation x || isSymbol x) more
, not (null as) -> Just (':' : as, sanitize bs)
| (as,bs) <- break isSpace more
, not (null as) -> Just (':' : as, sanitize bs)
| otherwise -> Nothing
expr -> guard (not (null expr)) >> return (expr,[])
uncons :: [a] -> Maybe (a,[a])
uncons as = case as of
a:rest -> Just (a,rest)
_ -> Nothing
findCommand :: String -> [CommandDescr]
findCommand str = lookupTrie str commands
findCommandExact :: String -> [CommandDescr]
findCommandExact str = lookupTrieExact str commands
findNbCommand :: Bool -> String -> [CommandDescr]
findNbCommand True str = lookupTrieExact str nbCommands
findNbCommand False str = lookupTrie str nbCommands
parseCommand :: (String -> [CommandDescr]) -> String -> Maybe Command
parseCommand findCmd line = do
(cmd,args) <- splitCommand line
let args' = sanitizeEnd args
case findCmd cmd of
[c] -> case cBody c of
ExprArg body -> Just (Command (body args'))
DeclsArg body -> Just (Command (body args'))
ExprTypeArg body -> Just (Command (body args'))
FilenameArg body -> Just (Command (body =<< expandHome args'))
OptionArg body -> Just (Command (body args'))
ShellArg body -> Just (Command (body args'))
NoArg body -> Just (Command body)
FileExprArg body ->
case extractFilePath args' of
Just (fp,expr) -> Just (Command (expandHome fp >>= flip body expr))
Nothing -> Nothing
[] -> case uncons cmd of
Just (':',_) -> Just (Unknown cmd)
Just _ -> Just (Command (evalCmd line))
_ -> Nothing
cs -> Just (Ambiguous cmd (concatMap cNames cs))
where
expandHome path =
case path of
'~' : c : more | isPathSeparator c -> do dir <- io getHomeDirectory
return (dir </> more)
_ -> return path
extractFilePath ipt =
let quoted q = (\(a,b) -> (a, drop 1 b)) . break (== q)
in case ipt of
"" -> Nothing
'\'':rest -> Just $ quoted '\'' rest
'"':rest -> Just $ quoted '"' rest
_ -> Just $ break isSpace ipt