module Cryptol.REPL.Command (
Command(..), CommandDescr(..), CommandBody(..)
, parseCommand
, runCommand
, splitCommand
, findCommand
, findCommandExact
, findNbCommand
, moduleCmd, loadCmd, loadPrelude
, handleCtrlC
, sanitize
, replParse
, liftModuleCmd
, moduleCmdResult
) where
import Cryptol.REPL.Monad
import Cryptol.REPL.Trie
import qualified Cryptol.ModuleSystem as M
import qualified Cryptol.ModuleSystem.Base as M (preludeName)
import qualified Cryptol.ModuleSystem.NamingEnv as M
import qualified Cryptol.ModuleSystem.Renamer as M (RenamerWarning(SymbolShadowed))
import qualified Cryptol.Eval.Value as E
import qualified Cryptol.Testing.Eval as Test
import qualified Cryptol.Testing.Random as TestR
import qualified Cryptol.Testing.Exhaust as TestX
import Cryptol.Parser
(parseExprWith,parseReplWith,ParseError(),Config(..),defaultConfig,parseModName)
import Cryptol.Parser.Position (emptyRange,getLoc)
import qualified Cryptol.TypeCheck.AST as T
import qualified Cryptol.TypeCheck.Subst as T
import qualified Cryptol.TypeCheck.InferTypes as T
import Cryptol.TypeCheck.PP (dump,ppWithNames)
import Cryptol.TypeCheck.Defaulting(defaultExpr)
import Cryptol.Utils.PP
import Cryptol.Utils.Panic(panic)
import qualified Cryptol.Parser.AST as P
import Cryptol.Prims.Doc(helpDoc)
import qualified Cryptol.Transform.Specialize as S
import qualified Cryptol.Symbolic as Symbolic
import Control.Applicative ((<$>))
import Control.DeepSeq
import qualified Control.Exception as X
import Control.Monad (guard,unless,forM_,when)
import Data.Char (isSpace,isPunctuation,isSymbol)
import Data.Function (on)
import Data.List (intercalate,isPrefixOf,nub)
import Data.Maybe (fromMaybe,mapMaybe)
import Data.Monoid (mempty)
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.IntMap as IntMap
import System.IO(hFlush,stdout)
import System.Random.TF(newTFGen)
import Numeric (showFFloat)
#if __GLASGOW_HASKELL__ < 706
import Control.Monad (liftM)
import qualified Text.ParserCombinators.ReadP as P
import Text.Read hiding (step)
import System.Environment (getEnvironment)
lookupEnv :: String -> IO (Maybe String)
lookupEnv key = lookup key `liftM` getEnvironment
readEither :: Read a => String -> Either String a
readEither s =
case [ x | (x,"") <- readPrec_to_S read' minPrec s ] of
[x] -> Right x
[] -> Left "Prelude.read: no parse"
_ -> Left "Prelude.read: ambiguous parse"
where
read' =
do x <- readPrec
lift P.skipSpaces
return x
readMaybe :: Read a => String -> Maybe a
readMaybe s = case readEither s of
Left _ -> Nothing
Right a -> Just a
#else
import System.Environment (lookupEnv)
#endif
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 ())
| 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 built-in operator"
, CommandDescr [ ":s", ":set" ] (OptionArg setOptionCmd)
"set an environmental option (:set on its own displays current values)"
, CommandDescr [ ":check" ] (ExprArg (qcCmd QCRandom))
"use random testing to check that the argument always returns true (if no argument, check all properties)"
, CommandDescr [ ":exhaust" ] (ExprArg (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"
]
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 ()
qcCmd qcMode "" =
do xs <- getPropertyNames
if null xs
then rPutStrLn "There are no properties in scope."
else forM_ xs $ \x ->
do rPutStr $ "property " ++ x ++ " "
qcCmd qcMode x
qcCmd qcMode str =
do expr <- replParseExpr str
(val,ty) <- replEvalExpr expr
EnvNum testNum <- getUser "tests"
case TestX.testableType ty of
Just (sz,vss) | qcMode == QCExhaust || sz <= toInteger testNum ->
do rPutStrLn "Using exhaustive testing."
let doTest _ [] = panic "We've unexpectedly run out of test cases"
[]
doTest _ (vs : vss1) = do
result <- TestX.runOneTest val vs
return (result, vss1)
ok <- go doTest sz 0 vss
when ok $ rPutStrLn "Q.E.D."
n -> case TestR.testableType ty of
Nothing -> raise (TypeNotTestable ty)
Just gens ->
do rPutStrLn "Using random testing."
prt testingMsg
g <- io newTFGen
ok <- go (TestR.runOneTest val gens) testNum 0 g
when ok $
case n of
Just (valNum,_) ->
do let valNumD = fromIntegral valNum :: Double
percent = fromIntegral (testNum * 100)
/ valNumD
showValNum
| valNum > 2 ^ (20::Integer) =
"2^^" ++ show (round $ logBase 2 valNumD :: Integer)
| otherwise = show valNum
rPutStrLn $ "Coverage: "
++ showFFloat (Just 2) percent "% ("
++ show testNum ++ " of "
++ showValNum ++ " values)"
Nothing -> return ()
where
testingMsg = "testing..."
totProgressWidth = 4
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
go _ totNum testNum _
| testNum >= totNum =
do delTesting
prtLn $ "passed " ++ show totNum ++ " tests."
return True
go doTest totNum testNum st =
do ppProgress testNum totNum
res <- io $ doTest (div (100 * (1 + testNum)) totNum) st
opts <- getPPValOpts
delProgress
case res of
(Test.Pass, st1) -> do delProgress
go doTest totNum (testNum + 1) st1
(failure, _g1) -> do
delTesting
case failure of
Test.FailFalse [] -> do
prtLn "FAILED"
Test.FailFalse vs -> do
prtLn "FAILED for the following inputs:"
mapM_ (rPrint . pp . E.WithBase opts) vs
Test.FailError err [] -> do
prtLn "ERROR"
rPrint (pp err)
Test.FailError err vs -> do
prtLn "ERROR for the following inputs:"
mapM_ (rPrint . pp . E.WithBase opts) vs
rPrint (pp err)
Test.Pass -> panic "Cryptol.REPL.Command" ["unexpected Test.Pass"]
return False
satCmd, proveCmd :: String -> REPL ()
satCmd = cmdProveSat True
proveCmd = cmdProveSat False
cmdProveSat :: Bool -> String -> REPL ()
cmdProveSat isSat "" =
do xs <- getPropertyNames
if null xs
then rPutStrLn "There are no properties in scope."
else forM_ xs $ \x ->
do if isSat
then rPutStr $ ":sat " ++ x ++ "\n\t"
else rPutStr $ ":prove " ++ x ++ "\n\t"
cmdProveSat isSat x
cmdProveSat isSat str = do
EnvString proverName <- getUser "prover"
EnvString fileName <- getUser "smtfile"
let mfile = if fileName == "-" then Nothing else Just fileName
case proverName of
"offline" -> offlineProveSat isSat str mfile
_ -> onlineProveSat isSat str proverName mfile
onlineProveSat :: Bool
-> String -> String -> Maybe FilePath -> REPL ()
onlineProveSat isSat str proverName mfile = do
EnvBool iteSolver <- getUser "iteSolver"
EnvBool verbose <- getUser "debug"
mSatNum <- getUserSatNum
let cexStr | isSat = "satisfying assignment"
| otherwise = "counterexample"
parseExpr <- replParseExpr str
(expr, schema) <- replCheckExpr parseExpr
denv <- getDynEnv
result <- liftModuleCmd $
Symbolic.satProve
isSat
mSatNum
(proverName, iteSolver, verbose)
(M.deDecls denv)
mfile
(expr, schema)
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.")
let (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
let docs = map (pp . E.WithBase ppOpts) vs
doc = ppPrec 3 parseExpr
rPrint $ hsep (doc : docs) <+>
text (if isSat then "= True" else "= False")
resultRecs = map (mkSolverResult cexStr isSat . Right) tess
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
offlineProveSat :: Bool -> String -> Maybe FilePath -> REPL ()
offlineProveSat isSat str mfile = do
EnvBool useIte <- getUser "iteSolver"
EnvBool vrb <- getUser "debug"
parseExpr <- replParseExpr str
exsch <- replCheckExpr parseExpr
decls <- fmap M.deDecls getDynEnv
result <- liftModuleCmd $
Symbolic.satProveOffline isSat useIte vrb decls mfile exsch
case result of
Symbolic.ProverError msg -> rPutStrLn msg
Symbolic.EmptyResult -> return ()
_ -> panic "REPL.Command" [ "unexpected prover result for offline prover" ]
mkSolverResult :: String
-> Bool
-> Either [T.Type] [(T.Type, T.Expr)]
-> (T.Type, T.Expr)
mkSolverResult thing result earg = (rty, re)
where
rName = T.Name "result"
rty = T.TRec $ [(rName, T.tBit )] ++ map fst argF
re = T.ERec $ [(rName, resultE)] ++ map snd argF
resultE = if result then T.eTrue else T.eFalse
mkArgs tes = reverse (go tes [] (1 :: Int))
where
go [] fs _ = fs
go ((t, e):tes') fs n = go tes' (((argName, t), (argName, e)):fs) (n+1)
where argName = T.Name ("arg" ++ show n)
argF = case earg of
Left ts -> mkArgs $ (map addError) ts
where addError t = (t, T.eError t ("no " ++ thing ++ " available"))
Right tes -> mkArgs tes
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
(def,sig) <- replCheckExpr expr
whenDebug (rPutStrLn (dump def))
rPrint $ pp expr <+> text ":" <+> pp sig
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
browseTSyns pfx
browseNewtypes pfx
browseVars pfx
browseTSyns :: String -> REPL ()
browseTSyns pfx = do
tsyns <- getTSyns
let tsyns' = Map.filterWithKey (\k _ -> pfx `isNamePrefix` k) tsyns
unless (Map.null tsyns') $ do
rPutStrLn "Type Synonyms"
rPutStrLn "============="
let ppSyn (qn,T.TySyn _ ps cs ty) = pp (T.TySyn qn ps cs ty)
rPrint (nest 4 (vcat (map ppSyn (Map.toList tsyns'))))
rPutStrLn ""
browseNewtypes :: String -> REPL ()
browseNewtypes pfx = do
nts <- getNewtypes
let nts' = Map.filterWithKey (\k _ -> pfx `isNamePrefix` k) nts
unless (Map.null nts') $ do
rPutStrLn "Newtypes"
rPutStrLn "========"
let ppNT (qn,nt) = T.ppNewtypeShort (nt { T.ntName = qn })
rPrint (nest 4 (vcat (map ppNT (Map.toList nts'))))
rPutStrLn ""
browseVars :: String -> REPL ()
browseVars pfx = do
vars <- getVars
let allNames = vars
vars' = Map.filterWithKey (\k _ -> pfx `isNamePrefix` k) allNames
isProp p = T.PragmaProperty `elem` (M.ifDeclPragmas p)
(props,syms) = Map.partition isProp vars'
ppBlock "Properties" props
ppBlock "Symbols" syms
where
ppBlock name xs =
unless (Map.null xs) $ do
rPutStrLn name
rPutStrLn (replicate (length name) '=')
let step k d acc =
pp k <+> char ':' <+> pp (M.ifDeclSig d) : acc
rPrint (nest 4 (vcat (Map.foldrWithKey step [] 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 (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)
| Just (ec,_) <- lookup cmd builtIns =
rPrint $ helpDoc ec
| otherwise = do rPutStrLn $ "// No documentation is available."
typeOfCmd 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 -> P.QName -> Bool
isNamePrefix pfx n = case n of
P.QName _ (P.Name _) -> pfx `isPrefixOf` pretty n
_ -> 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
replParseInput = replParse $ parseReplWith interactiveConfig
replParseExpr :: String -> REPL P.Expr
replParseExpr = replParse $ parseExprWith interactiveConfig
interactiveConfig :: Config
interactiveConfig = defaultConfig { cfgSource = "<interactive>" }
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
mapM_ (rPrint . pp) ws
case res of
Right (a,me') -> setModuleEnv me' >> return a
Left err -> raise (ModuleSystemError err)
replCheckExpr :: P.Expr -> REPL (T.Expr,T.Schema)
replCheckExpr e = liftModuleCmd $ M.checkExpr e
replCheckDecls :: [P.Decl] -> REPL [T.DeclGroup]
replCheckDecls ds = do
npds <- liftModuleCmd $ M.noPat ds
denv <- getDynEnv
let dnames = M.namingEnv npds
ne' <- M.travNamingEnv uniqify dnames
let denv' = denv { M.deNames = ne' `M.shadowing` M.deNames denv }
undo exn = do
setDynEnv denv
raise exn
setDynEnv denv'
let topDecls = [ P.Decl (P.TopLevel P.Public d) | d <- npds ]
catch (liftModuleCmd $ M.checkDecls topDecls) undo
replSpecExpr :: T.Expr -> REPL T.Expr
replSpecExpr e = liftModuleCmd $ S.specialize e
replEvalExpr :: P.Expr -> REPL (E.Value, T.Type)
replEvalExpr expr =
do (def,sig) <- replCheckExpr expr
let range = fromMaybe emptyRange (getLoc expr)
(def1,ty) <-
case defaultExpr range def sig 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
bindItVariable :: T.Type -> T.Expr -> REPL ()
bindItVariable ty expr = do
let it = T.QName Nothing (P.Name "it")
freshIt <- uniqify it
let dg = T.NonRecursive decl
schema = T.Forall { T.sVars = []
, T.sProps = []
, T.sType = ty
}
decl = T.Decl { T.dName = freshIt
, T.dSignature = schema
, T.dDefinition = expr
, T.dPragmas = []
}
liftModuleCmd (M.evalDecls [dg])
denv <- getDynEnv
let en = M.EFromBind (P.Located emptyRange freshIt)
nenv' = M.singletonE it en `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 -> 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)
[] -> 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