-- | -- Module : Cryptol.REPL.Command -- Copyright : (c) 2013-2016 Galois, Inc. -- License : BSD3 -- Maintainer : cryptol@galois.com -- Stability : provisional -- Portability : portable {-# LANGUAGE BangPatterns #-} {-# LANGUAGE BlockArguments #-} {-# LANGUAGE FlexibleContexts #-} {-# LANGUAGE LambdaCase #-} {-# LANGUAGE MultiWayIf #-} {-# LANGUAGE OverloadedStrings #-} {-# LANGUAGE PatternGuards #-} {-# LANGUAGE RecordWildCards #-} -- See Note [-Wincomplete-uni-patterns and irrefutable patterns] in Cryptol.TypeCheck.TypePat {-# OPTIONS_GHC -Wno-incomplete-uni-patterns #-} module Cryptol.REPL.Command ( -- * Commands Command(..), CommandDescr(..), CommandBody(..), CommandExitCode(..) , parseCommand , runCommand , splitCommand , findCommand , findCommandExact , findNbCommand , commandList , moduleCmd, loadCmd, loadPrelude, setOptionCmd -- Parsing , interactiveConfig , replParseExpr -- Evaluation and Typechecking , replEvalExpr , replCheckExpr -- Check, SAT, and prove , TestReport(..) , qcExpr, qcCmd, QCMode(..) , satCmd , proveCmd , onlineProveSat , offlineProveSat -- Misc utilities , handleCtrlC , sanitize , withRWTempFile -- To support Notebook interface (might need to refactor) , replParse , liftModuleCmd , moduleCmdResult ) where import Cryptol.REPL.Monad import Cryptol.REPL.Trie import Cryptol.REPL.Browse 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.ModuleSystem.Env as M import qualified Cryptol.Backend.Monad as E import qualified Cryptol.Backend.SeqMap as E import Cryptol.Eval.Concrete( Concrete(..) ) import qualified Cryptol.Eval.Concrete as Concrete import qualified Cryptol.Eval.Env as E import qualified Cryptol.Eval.Type as E import qualified Cryptol.Eval.Value as E import qualified Cryptol.Eval.Reference as R import Cryptol.Testing.Random import qualified Cryptol.Testing.Random as TestR import Cryptol.Parser (parseExprWith,parseReplWith,ParseError(),Config(..),defaultConfig ,parseModName,parseHelpName) import Cryptol.Parser.Position (Position(..),Range(..),HasLoc(..)) import qualified Cryptol.TypeCheck.AST as T import qualified Cryptol.TypeCheck.Error as T import qualified Cryptol.TypeCheck.Parseable as T import qualified Cryptol.TypeCheck.Subst as T import Cryptol.TypeCheck.Solve(defaultReplExpr) import Cryptol.TypeCheck.PP (dump,ppWithNames,emptyNameMap) import Cryptol.Utils.PP hiding (()) import Cryptol.Utils.Panic(panic) import Cryptol.Utils.RecordMap import qualified Cryptol.Parser.AST as P import qualified Cryptol.Transform.Specialize as S import Cryptol.Symbolic ( ProverCommand(..), QueryType(..) , ProverStats,ProverResult(..),CounterExampleType(..) ) import qualified Cryptol.Symbolic.SBV as SBV import qualified Cryptol.Symbolic.What4 as W4 import Cryptol.Version (displayVersion) import qualified Control.Exception as X import Control.Monad hiding (mapM, mapM) import qualified Control.Monad.Catch as Ex import Control.Monad.IO.Class(liftIO) import Data.ByteString (ByteString) import qualified Data.ByteString as BS import qualified Data.ByteString.Char8 as BS8 import Data.Bits (shiftL, (.&.), (.|.)) import Data.Char (isSpace,isPunctuation,isSymbol,isAlphaNum,isAscii) import Data.Function (on) import Data.List (intercalate, nub, isPrefixOf,intersperse) import Data.Maybe (fromMaybe,mapMaybe,isNothing) 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 ,getTemporaryDirectory,setPermissions,removeFile ,emptyPermissions,setOwnerReadable) import qualified Data.Map as Map import qualified Data.Set as Set import System.IO (Handle,hFlush,stdout,openTempFile,hClose,openFile ,IOMode(..),hGetContents,hSeek,SeekMode(..)) import System.Random.TF(newTFGen) import Numeric (showFFloat) import qualified Data.Text as T import Data.IORef(newIORef,readIORef,writeIORef) import GHC.Float (log1p, expm1) import Prelude () import Prelude.Compat import qualified Data.SBV.Internals as SBV (showTDiff) -- Commands -------------------------------------------------------------------- -- | Commands. data Command = Command (Int -> Maybe FilePath -> REPL ()) -- ^ Successfully parsed command | Ambiguous String [String] -- ^ Ambiguous command, list of conflicting -- commands | Unknown String -- ^ The unknown command -- | Command builder. data CommandDescr = CommandDescr { cNames :: [String] , cArgs :: [String] , cBody :: CommandBody , cHelp :: String , cLongHelp :: 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 -> (Int,Int) -> Maybe FilePath -> REPL ()) | FileExprArg (FilePath -> String -> (Int,Int) -> Maybe FilePath -> REPL ()) | DeclsArg (String -> REPL ()) | ExprTypeArg (String -> REPL ()) | ModNameArg (String -> REPL ()) | FilenameArg (FilePath -> REPL ()) | OptionArg (String -> REPL ()) | ShellArg (String -> REPL ()) | HelpArg (String -> REPL ()) | NoArg (REPL ()) data CommandExitCode = CommandOk | CommandError -- XXX: More? -- | REPL command parsing. 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 -- | Notebook command parsing. 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 -- | A subset of commands safe for Notebook execution nbCommandList :: [CommandDescr] nbCommandList = [ CommandDescr [ ":t", ":type" ] ["EXPR"] (ExprArg typeOfCmd) "Check the type of an expression." "" , CommandDescr [ ":b", ":browse" ] ["[ MODULE ]"] (ModNameArg browseCmd) "Display information about loaded modules." (unlines [ "With no arguent, :browse shows information about the names in scope." , "With an argument M, shows information about the names exported from M" ] ) , CommandDescr [ ":version"] [] (NoArg versionCmd) "Display the version of this Cryptol executable" "" , CommandDescr [ ":?", ":help" ] ["[ TOPIC ]"] (HelpArg helpCmd) "Display a brief description of a function, type, or command. (e.g. :help :help)" (unlines [ "TOPIC can be any of:" , " * Specific REPL colon-commands (e.g. :help :prove)" , " * Functions (e.g. :help join)" , " * Infix operators (e.g. :help +)" , " * Type constructors (e.g. :help Z)" , " * Type constraints (e.g. :help fin)" , " * :set-able options (e.g. :help :set base)" ]) , CommandDescr [ ":s", ":set" ] ["[ OPTION [ = VALUE ] ]"] (OptionArg setOptionCmd) "Set an environmental option (:set on its own displays current values)." "" , CommandDescr [ ":check" ] ["[ EXPR ]"] (ExprArg (qcCmd QCRandom)) "Use random testing to check that the argument always returns true.\n(If no argument, check all properties.)" "" , CommandDescr [ ":exhaust" ] ["[ EXPR ]"] (ExprArg (qcCmd QCExhaust)) "Use exhaustive testing to prove that the argument always returns\ntrue. (If no argument, check all properties.)" "" , CommandDescr [ ":prove" ] ["[ EXPR ]"] (ExprArg proveCmd) "Use an external solver to prove that the argument always returns\ntrue. (If no argument, check all properties.)" "" , CommandDescr [ ":sat" ] ["[ EXPR ]"] (ExprArg satCmd) "Use a solver to find a satisfying assignment for which the argument\nreturns true. (If no argument, find an assignment for all properties.)" "" , CommandDescr [ ":safe" ] ["[ EXPR ]"] (ExprArg safeCmd) "Use an external solver to prove that an expression is safe\n(does not encounter run-time errors) for all inputs." "" , CommandDescr [ ":debug_specialize" ] ["EXPR"](ExprArg specializeCmd) "Do type specialization on a closed expression." "" , CommandDescr [ ":eval" ] ["EXPR"] (ExprArg refEvalCmd) "Evaluate an expression with the reference evaluator." "" , CommandDescr [ ":ast" ] ["EXPR"] (ExprArg astOfCmd) "Print out the pre-typechecked AST of a given term." "" , CommandDescr [ ":extract-coq" ] [] (NoArg allTerms) "Print out the post-typechecked AST of all currently defined terms,\nin a Coq-parseable format." "" ] commandList :: [CommandDescr] commandList = nbCommandList ++ [ CommandDescr [ ":q", ":quit" ] [] (NoArg quitCmd) "Exit the REPL." "" , CommandDescr [ ":l", ":load" ] ["FILE"] (FilenameArg loadCmd) "Load a module by filename." "" , CommandDescr [ ":r", ":reload" ] [] (NoArg reloadCmd) "Reload the currently loaded module." "" , CommandDescr [ ":e", ":edit" ] ["[ FILE ]"] (FilenameArg editCmd) "Edit FILE or the currently loaded module." "" , CommandDescr [ ":!" ] ["COMMAND"] (ShellArg runShellCmd) "Execute a command in the shell." "" , CommandDescr [ ":cd" ] ["DIR"] (FilenameArg cdCmd) "Set the current working directory." "" , CommandDescr [ ":m", ":module" ] ["[ MODULE ]"] (FilenameArg moduleCmd) "Load a module by its name." "" , CommandDescr [ ":w", ":writeByteArray" ] ["FILE", "EXPR"] (FileExprArg writeFileCmd) "Write data of type 'fin n => [n][8]' to a file." "" , CommandDescr [ ":readByteArray" ] ["FILE"] (FilenameArg readFileCmd) "Read data from a file as type 'fin n => [n][8]', binding\nthe value to variable 'it'." "" , CommandDescr [ ":dumptests" ] ["FILE", "EXPR"] (FileExprArg dumpTestsCmd) (unlines [ "Dump a tab-separated collection of tests for the given" , "expression into a file. The first column in each line is" , "the expected output, and the remainder are the inputs. The" , "number of tests is determined by the \"tests\" option." ]) "" ] genHelp :: [CommandDescr] -> [String] genHelp cs = map cmdHelp cs where cmdHelp cmd = concat $ [ " ", cmdNames cmd, pad (cmdNames cmd), intercalate ("\n " ++ pad []) (lines (cHelp cmd)) ] cmdNames cmd = intercalate ", " (cNames cmd) padding = 2 + maximum (map (length . cmdNames) cs) pad n = replicate (max 0 (padding - length n)) ' ' -- Command Evaluation ---------------------------------------------------------- -- | Run a command. runCommand :: Int -> Maybe FilePath -> Command -> REPL CommandExitCode runCommand lineNum mbBatch c = case c of Command cmd -> (cmd lineNum mbBatch >> return CommandOk) `Cryptol.REPL.Monad.catch` handler where handler re = rPutStrLn "" >> rPrint (pp re) >> return CommandError Unknown cmd -> do rPutStrLn ("Unknown command: " ++ cmd) return CommandError Ambiguous cmd cmds -> do rPutStrLn (cmd ++ " is ambiguous, it could mean one of:") rPutStrLn ("\t" ++ intercalate ", " cmds) return CommandError evalCmd :: String -> Int -> Maybe FilePath -> REPL () evalCmd str lineNum mbBatch = do ri <- replParseInput str lineNum mbBatch case ri of P.ExprInput expr -> do (val,_ty) <- replEvalExpr expr ppOpts <- getPPValOpts valDoc <- rEvalRethrow (E.ppValue Concrete ppOpts val) -- This is the point where the value gets forced. We deepseq the -- pretty-printed representation of it, rather than the value -- itself, leaving it up to the pretty-printer to determine how -- much of the value to force --out <- io $ rethrowEvalError -- $ return $!! show $ pp $ E.WithBase ppOpts val rPutStrLn (show valDoc) P.LetInput ds -> do -- explicitly make this a top-level declaration, so that it will -- be generalized if mono-binds is enabled replEvalDecls ds P.EmptyInput -> -- comment or empty input does nothing pure () printCounterexample :: CounterExampleType -> Doc -> [Concrete.Value] -> REPL () printCounterexample cexTy exprDoc vs = do ppOpts <- getPPValOpts docs <- mapM (rEval . E.ppValue Concrete ppOpts) vs let cexRes = case cexTy of SafetyViolation -> [text "~> ERROR"] PredicateFalsified -> [text "= False"] rPrint $ nest 2 (sep ([exprDoc] ++ docs ++ cexRes)) printSatisfyingModel :: Doc -> [Concrete.Value] -> REPL () printSatisfyingModel exprDoc vs = do ppOpts <- getPPValOpts docs <- mapM (rEval . E.ppValue Concrete ppOpts) vs rPrint $ nest 2 (sep ([exprDoc] ++ docs ++ [text "= True"])) dumpTestsCmd :: FilePath -> String -> (Int,Int) -> Maybe FilePath -> REPL () dumpTestsCmd outFile str pos fnm = do expr <- replParseExpr str pos fnm (val, ty) <- replEvalExpr expr ppopts <- getPPValOpts testNum <- getKnownUser "tests" :: REPL Int g <- io newTFGen tenv <- E.envTypes . M.deEnv <$> getDynEnv let tyv = E.evalValType tenv ty gens <- case TestR.dumpableType tyv of Nothing -> raise (TypeNotTestable ty) Just gens -> return gens tests <- io $ TestR.returnTests g gens val testNum out <- forM tests $ \(args, x) -> do argOut <- mapM (rEval . E.ppValue Concrete ppopts) args resOut <- rEval (E.ppValue Concrete ppopts x) return (renderOneLine resOut ++ "\t" ++ intercalate "\t" (map renderOneLine argOut) ++ "\n") io $ writeFile outFile (concat out) `X.catch` handler where handler :: X.SomeException -> IO () handler e = putStrLn (X.displayException e) data QCMode = QCRandom | QCExhaust deriving (Eq, Show) -- | Randomly test a property, or exhaustively check it if the number -- of values in the type under test is smaller than the @tests@ -- environment variable, or we specify exhaustive testing. qcCmd :: QCMode -> String -> (Int,Int) -> Maybe FilePath -> REPL () qcCmd qcMode "" _pos _fnm = 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,d) -> do let str = nameStr x rPutStr $ "property " ++ str ++ " " let texpr = T.EVar x let schema = M.ifDeclSig d nd <- M.mctxNameDisp <$> getFocusedEnv let doc = fixNameDisp nd (pp texpr) void (qcExpr qcMode doc texpr schema) qcCmd qcMode str pos fnm = do expr <- replParseExpr str pos fnm (_,texpr,schema) <- replCheckExpr expr nd <- M.mctxNameDisp <$> getFocusedEnv let doc = fixNameDisp nd (ppPrec 3 expr) -- function application has precedence 3 void (qcExpr qcMode doc texpr schema) data TestReport = TestReport { reportExpr :: Doc , reportResult :: TestResult , reportTestsRun :: Integer , reportTestsPossible :: Maybe Integer } qcExpr :: QCMode -> Doc -> T.Expr -> T.Schema -> REPL TestReport qcExpr qcMode exprDoc texpr schema = do (val,ty) <- replEvalCheckedExpr texpr schema testNum <- (toInteger :: Int -> Integer) <$> getKnownUser "tests" tenv <- E.envTypes . M.deEnv <$> getDynEnv let tyv = E.evalValType tenv ty percentRef <- io $ newIORef Nothing testsRef <- io $ newIORef 0 case testableType tyv of Just (Just sz,tys,vss,_gens) | qcMode == QCExhaust || sz <= testNum -> do rPutStrLn "Using exhaustive testing." prt testingMsg (res,num) <- Ex.catch (exhaustiveTests (\n -> ppProgress percentRef testsRef n sz) val vss) (\ex -> do rPutStrLn "\nTest interrupted..." num <- io $ readIORef testsRef let report = TestReport exprDoc Pass num (Just sz) ppReport tys False report rPutStrLn $ interruptedExhaust num sz Ex.throwM (ex :: Ex.SomeException)) let report = TestReport exprDoc res num (Just sz) delProgress delTesting ppReport tys True report return report Just (sz,tys,_,gens) | qcMode == QCRandom -> do rPutStrLn "Using random testing." prt testingMsg g <- io newTFGen (res,num) <- Ex.catch (randomTests (\n -> ppProgress percentRef testsRef n testNum) testNum val gens g) (\ex -> do rPutStrLn "\nTest interrupted..." num <- io $ readIORef testsRef let report = TestReport exprDoc Pass num sz ppReport tys False report case sz of Just n -> rPutStrLn $ coverageString num n _ -> return () Ex.throwM (ex :: Ex.SomeException)) let report = TestReport exprDoc res num sz delProgress delTesting ppReport tys False report case sz of Just n | isPass res -> rPutStrLn $ coverageString testNum n _ -> return () return report _ -> raise (TypeNotTestable ty) where testingMsg = "Testing... " interruptedExhaust testNum sz = let percent = (100.0 :: Double) * (fromInteger testNum) / fromInteger sz showValNum | sz > 2 ^ (20::Integer) = "2^^" ++ show (lg2 sz) | otherwise = show sz in "Test coverage: " ++ showFFloat (Just 2) percent "% (" ++ show testNum ++ " of " ++ showValNum ++ " values)" coverageString testNum sz = let (percent, expectedUnique) = expectedCoverage testNum sz showValNum | sz > 2 ^ (20::Integer) = "2^^" ++ show (lg2 sz) | otherwise = show sz in "Expected test coverage: " ++ showFFloat (Just 2) percent "% (" ++ showFFloat (Just 0) expectedUnique " of " ++ showValNum ++ " values)" totProgressWidth = 4 -- 100% lg2 :: Integer -> Integer lg2 x | x >= 2^(1024::Int) = 1024 + lg2 (x `div` 2^(1024::Int)) | x == 0 = 0 | otherwise = let valNumD = fromInteger x :: Double in round $ logBase 2 valNumD :: Integer prt msg = rPutStr msg >> io (hFlush stdout) ppProgress percentRef testsRef this tot = do io $ writeIORef testsRef this let percent = show (div (100 * this) tot) ++ "%" width = length percent pad = replicate (totProgressWidth - width) ' ' unlessBatch $ do oldPercent <- io $ readIORef percentRef case oldPercent of Nothing -> do io $ writeIORef percentRef (Just percent) prt (pad ++ percent) Just p | p /= percent -> do io $ writeIORef percentRef (Just percent) delProgress prt (pad ++ percent) _ -> return () del n = unlessBatch $ prt (replicate n '\BS' ++ replicate n ' ' ++ replicate n '\BS') delTesting = del (length testingMsg) delProgress = del totProgressWidth ppReport :: [E.TValue] -> Bool -> TestReport -> REPL () ppReport _tys isExhaustive (TestReport _exprDoc Pass testNum _testPossible) = do rPutStrLn ("Passed " ++ show testNum ++ " tests.") when isExhaustive (rPutStrLn "Q.E.D.") ppReport tys _ (TestReport exprDoc failure _testNum _testPossible) = do ppFailure tys exprDoc failure ppFailure :: [E.TValue] -> Doc -> TestResult -> REPL () ppFailure tys exprDoc failure = do ~(EnvBool showEx) <- getUser "showExamples" vs <- case failure of FailFalse vs -> do rPutStrLn "Counterexample" when showEx (printCounterexample PredicateFalsified exprDoc vs) pure vs FailError err vs | null vs || not showEx -> do rPutStrLn "ERROR" rPrint (pp err) pure vs | otherwise -> do rPutStrLn "ERROR for the following inputs:" printCounterexample SafetyViolation exprDoc vs rPrint (pp err) pure vs Pass -> panic "Cryptol.REPL.Command" ["unexpected Test.Pass"] -- bind the 'it' variable case (tys,vs) of ([t],[v]) -> bindItVariableVal t v _ -> let fs = [ M.packIdent ("arg" ++ show (i::Int)) | i <- [ 1 .. ] ] t = E.TVRec (recordFromFields (zip fs tys)) v = E.VRecord (recordFromFields (zip fs (map return vs))) in bindItVariableVal t v -- | This function computes the expected coverage percentage and -- expected number of unique test vectors when using random testing. -- -- The expected test coverage proportion is: -- @1 - ((n-1)/n)^k@ -- -- This formula takes into account the fact that test vectors are chosen -- uniformly at random _with replacement_, and thus the same vectors -- may be generated multiple times. If the test vectors were chosen -- randomly without replacement, the proportion would instead be @k/n@. -- -- We compute raising to the @k@ power in the log domain to improve -- numerical precision. The equivalant comptutation is: -- @-expm1( k * log1p (-1/n) )@ -- -- Where @expm1(x) = exp(x) - 1@ and @log1p(x) = log(1 + x)@. -- -- However, if @sz@ is large enough, even carefully preserving -- precision may not be enough to get sensible results. In such -- situations, we expect the naive approximation @k/n@ to be very -- close to accurate and the expected number of unique values is -- essentially equal to the number of tests. expectedCoverage :: Integer -> Integer -> (Double, Double) expectedCoverage testNum sz = -- If the Double computation has enough precision, use the -- "with replacement" formula. if testNum > 0 && proportion > 0 then (100.0 * proportion, szD * proportion) else (100.0 * naiveProportion, numD) where szD :: Double szD = fromInteger sz numD :: Double numD = fromIntegral testNum naiveProportion = numD / szD proportion = negate (expm1 (numD * log1p (negate (recip szD)))) satCmd, proveCmd :: String -> (Int,Int) -> Maybe FilePath -> REPL () satCmd = cmdProveSat True proveCmd = cmdProveSat False showProverStats :: Maybe String -> ProverStats -> REPL () showProverStats mprover stat = rPutStrLn msg where msg = "(Total Elapsed Time: " ++ SBV.showTDiff stat ++ maybe "" (\p -> ", using " ++ show p) mprover ++ ")" rethrowErrorCall :: REPL a -> REPL a rethrowErrorCall m = REPL (\r -> unREPL m r `X.catches` hs) where hs = [ X.Handler $ \ (X.ErrorCallWithLocation s _) -> X.throwIO (SBVError s) , X.Handler $ \ e -> X.throwIO (SBVException e) , X.Handler $ \ e -> X.throwIO (SBVPortfolioException e) , X.Handler $ \ e -> X.throwIO (W4Exception e) ] -- | Attempts to prove the given term is safe for all inputs safeCmd :: String -> (Int,Int) -> Maybe FilePath -> REPL () safeCmd str pos fnm = do proverName <- getKnownUser "prover" fileName <- getKnownUser "smtFile" let mfile = if fileName == "-" then Nothing else Just fileName pexpr <- replParseExpr str pos fnm nd <- M.mctxNameDisp <$> getFocusedEnv let exprDoc = fixNameDisp nd (ppPrec 3 pexpr) -- function application has precedence 3 let rng = fromMaybe (mkInteractiveRange pos fnm) (getLoc pexpr) (_,texpr,schema) <- replCheckExpr pexpr if proverName `elem` ["offline","sbv-offline","w4-offline"] then offlineProveSat proverName SafetyQuery texpr schema mfile else do (firstProver,result,stats) <- rethrowErrorCall (onlineProveSat proverName SafetyQuery texpr schema mfile) case result of EmptyResult -> panic "REPL.Command" [ "got EmptyResult for online prover query" ] ProverError msg -> rPutStrLn msg ThmResult _ts -> rPutStrLn "Safe" CounterExample cexType tevs -> do rPutStrLn "Counterexample" let tes = map ( \(t,e,_) -> (t,e)) tevs vs = map ( \(_,_,v) -> v) tevs (t,e) <- mkSolverResult "counterexample" rng False (Right tes) ~(EnvBool yes) <- getUser "showExamples" when yes $ printCounterexample cexType exprDoc vs when yes $ printSafetyViolation texpr schema vs void $ bindItVariable t e AllSatResult _ -> do panic "REPL.Command" ["Unexpected AllSAtResult for ':safe' call"] seeStats <- getUserShowProverStats when seeStats (showProverStats firstProver stats) -- | Console-specific version of 'proveSat'. Prints output to the -- console, and binds the @it@ variable to a record whose form depends -- on the expression given. See ticket #66 for a discussion of this -- design. cmdProveSat :: Bool -> String -> (Int,Int) -> Maybe FilePath -> REPL () cmdProveSat isSat "" _pos _fnm = 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,d) -> do let str = nameStr x if isSat then rPutStr $ ":sat " ++ str ++ "\n\t" else rPutStr $ ":prove " ++ str ++ "\n\t" let texpr = T.EVar x let schema = M.ifDeclSig d nd <- M.mctxNameDisp <$> getFocusedEnv let doc = fixNameDisp nd (pp texpr) proveSatExpr isSat (M.nameLoc x) doc texpr schema cmdProveSat isSat str pos fnm = do pexpr <- replParseExpr str pos fnm nd <- M.mctxNameDisp <$> getFocusedEnv let doc = fixNameDisp nd (ppPrec 3 pexpr) -- function application has precedence 3 (_,texpr,schema) <- replCheckExpr pexpr let rng = fromMaybe (mkInteractiveRange pos fnm) (getLoc pexpr) proveSatExpr isSat rng doc texpr schema proveSatExpr :: Bool -> Range -> Doc -> T.Expr -> T.Schema -> REPL () proveSatExpr isSat rng exprDoc texpr schema = do let cexStr | isSat = "satisfying assignment" | otherwise = "counterexample" qtype <- if isSat then SatQuery <$> getUserSatNum else pure ProveQuery proverName <- getKnownUser "prover" fileName <- getKnownUser "smtFile" let mfile = if fileName == "-" then Nothing else Just fileName if proverName `elem` ["offline","sbv-offline","w4-offline"] then offlineProveSat proverName qtype texpr schema mfile else do (firstProver,result,stats) <- rethrowErrorCall (onlineProveSat proverName qtype texpr schema mfile) case result of EmptyResult -> panic "REPL.Command" [ "got EmptyResult for online prover query" ] ProverError msg -> rPutStrLn msg ThmResult ts -> do rPutStrLn (if isSat then "Unsatisfiable" else "Q.E.D.") (t, e) <- mkSolverResult cexStr rng (not isSat) (Left ts) void $ bindItVariable t e CounterExample cexType tevs -> do rPutStrLn "Counterexample" let tes = map ( \(t,e,_) -> (t,e)) tevs vs = map ( \(_,_,v) -> v) tevs (t,e) <- mkSolverResult cexStr rng isSat (Right tes) ~(EnvBool yes) <- getUser "showExamples" when yes $ printCounterexample cexType exprDoc vs -- if there's a safety violation, evalute the counterexample to -- find and print the actual concrete error case cexType of SafetyViolation -> when yes $ printSafetyViolation texpr schema vs _ -> return () void $ bindItVariable t e AllSatResult tevss -> do rPutStrLn "Satisfiable" let tess = map (map $ \(t,e,_) -> (t,e)) tevss vss = map (map $ \(_,_,v) -> v) tevss resultRecs <- mapM (mkSolverResult cexStr rng 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 mkSolverResult" ] [(t, e)] -> (t, [e]) _ -> collectTes resultRecs ~(EnvBool yes) <- getUser "showExamples" when yes $ forM_ vss (printSatisfyingModel exprDoc) let numModels = length tevss when (numModels > 1) (rPutStrLn ("Models found: " ++ show numModels)) case exprs of [e] -> void $ bindItVariable ty e _ -> bindItVariables ty exprs seeStats <- getUserShowProverStats when seeStats (showProverStats firstProver stats) printSafetyViolation :: T.Expr -> T.Schema -> [E.GenValue Concrete] -> REPL () printSafetyViolation texpr schema vs = catch (do (fn,_) <- replEvalCheckedExpr texpr schema rEval (E.forceValue =<< foldM (\f v -> E.fromVFun Concrete f (pure v)) fn vs)) (\case EvalError eex -> rPutStrLn (show (pp eex)) ex -> raise ex) onlineProveSat :: String -> QueryType -> T.Expr -> T.Schema -> Maybe FilePath -> REPL (Maybe String,ProverResult,ProverStats) onlineProveSat proverName qtype expr schema mfile = do verbose <- getKnownUser "debug" modelValidate <- getUserProverValidate validEvalContext expr validEvalContext schema decls <- fmap M.deDecls getDynEnv timing <- io (newIORef 0) ~(EnvBool ignoreSafety) <- getUser "ignoreSafety" let cmd = ProverCommand { pcQueryType = qtype , pcProverName = proverName , pcVerbose = verbose , pcValidate = modelValidate , pcProverStats = timing , pcExtraDecls = decls , pcSmtFile = mfile , pcExpr = expr , pcSchema = schema , pcIgnoreSafety = ignoreSafety } (firstProver, res) <- getProverConfig >>= \case Left sbvCfg -> liftModuleCmd $ SBV.satProve sbvCfg cmd Right w4Cfg -> do ~(EnvBool hashConsing) <- getUser "hashConsing" ~(EnvBool warnUninterp) <- getUser "warnUninterp" liftModuleCmd $ W4.satProve w4Cfg hashConsing warnUninterp cmd stas <- io (readIORef timing) return (firstProver,res,stas) offlineProveSat :: String -> QueryType -> T.Expr -> T.Schema -> Maybe FilePath -> REPL () offlineProveSat proverName qtype expr schema mfile = do verbose <- getKnownUser "debug" modelValidate <- getUserProverValidate decls <- fmap M.deDecls getDynEnv timing <- io (newIORef 0) ~(EnvBool ignoreSafety) <- getUser "ignoreSafety" let cmd = ProverCommand { pcQueryType = qtype , pcProverName = proverName , pcVerbose = verbose , pcValidate = modelValidate , pcProverStats = timing , pcExtraDecls = decls , pcSmtFile = mfile , pcExpr = expr , pcSchema = schema , pcIgnoreSafety = ignoreSafety } put <- getPutStr let putLn x = put (x ++ "\n") let displayMsg = do let filename = fromMaybe "standard output" mfile let satWord = case qtype of SatQuery _ -> "satisfiability" ProveQuery -> "validity" SafetyQuery -> "safety" putLn $ "Writing to SMT-Lib file " ++ filename ++ "..." putLn $ "To determine the " ++ satWord ++ " of the expression, use an external SMT solver." getProverConfig >>= \case Left sbvCfg -> do result <- liftModuleCmd $ SBV.satProveOffline sbvCfg cmd case result of Left msg -> rPutStrLn msg Right smtlib -> do io $ displayMsg case mfile of Just path -> io $ writeFile path smtlib Nothing -> rPutStr smtlib Right _w4Cfg -> do ~(EnvBool hashConsing) <- getUser "hashConsing" ~(EnvBool warnUninterp) <- getUser "warnUninterp" result <- liftModuleCmd $ W4.satProveOffline hashConsing warnUninterp cmd $ \f -> do displayMsg case mfile of Just path -> X.bracket (openFile path WriteMode) hClose f Nothing -> withRWTempFile "smtOutput.tmp" $ \h -> do f h hSeek h AbsoluteSeek 0 hGetContents h >>= put case result of Just msg -> rPutStrLn msg Nothing -> return () rIdent :: M.Ident rIdent = M.packIdent "result" -- | Make a type/expression pair that is suitable for binding to @it@ -- after running @:sat@ or @:prove@ mkSolverResult :: String -> Range -> Bool -> Either [E.TValue] [(E.TValue, T.Expr)] -> REPL (E.TValue, T.Expr) mkSolverResult thing rng result earg = do prims <- getPrimMap let addError t = (t, T.ELocated rng (T.eError prims (E.tValTy t) ("no " ++ thing ++ " available"))) argF = case earg of Left ts -> mkArgs (map addError ts) Right tes -> mkArgs tes eTrue = T.ePrim prims (M.prelPrim "True") eFalse = T.ePrim prims (M.prelPrim "False") resultE = if result then eTrue else eFalse rty = E.TVRec (recordFromFields $ [(rIdent, E.TVBit)] ++ map fst argF) re = T.ERec (recordFromFields $ [(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 -> (Int,Int) -> Maybe FilePath -> REPL () specializeCmd str pos fnm = do parseExpr <- replParseExpr str pos fnm (_, 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 refEvalCmd :: String -> (Int,Int) -> Maybe FilePath -> REPL () refEvalCmd str pos fnm = do parseExpr <- replParseExpr str pos fnm (_, expr, schema) <- replCheckExpr parseExpr validEvalContext expr validEvalContext schema val <- liftModuleCmd (rethrowEvalError . R.evaluate expr) opts <- getPPValOpts rPrint $ R.ppEValue opts val astOfCmd :: String -> (Int,Int) -> Maybe FilePath -> REPL () astOfCmd str pos fnm = do expr <- replParseExpr str pos fnm (re,_,_) <- replCheckExpr (P.noPos expr) rPrint (fmap M.nameUnique re) allTerms :: REPL () allTerms = do me <- getModuleEnv rPrint $ T.showParseable $ concatMap T.mDecls $ M.loadedModules me typeOfCmd :: String -> (Int,Int) -> Maybe FilePath -> REPL () typeOfCmd str pos fnm = do expr <- replParseExpr str pos fnm (_re,def,sig) <- replCheckExpr expr -- XXX need more warnings from the module system whenDebug (rPutStrLn (dump def)) fDisp <- M.mctxNameDisp <$> getFocusedEnv -- type annotation ':' has precedence 2 rPrint $ runDoc fDisp $ group $ hang (ppPrec 2 expr <+> text ":") 2 (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 val = byteStringToInteger bs let len = BS.length bs let split = T.ePrim pm (M.prelPrim "split") let number = T.ePrim pm (M.prelPrim "number") let f = T.EProofApp (foldl T.ETApp split [T.tNum len, T.tNum (8::Integer), T.tBit]) let t = T.tWord (T.tNum (toInteger len * 8)) let x = T.EProofApp (T.ETApp (T.ETApp number (T.tNum val)) t) let expr = T.EApp f x void $ bindItVariable (E.TVSeq (toInteger len) (E.TVSeq 8 E.TVBit)) expr -- | Convert a 'ByteString' (big-endian) of length @n@ to an 'Integer' -- with @8*n@ bits. This function uses a balanced binary fold to -- achieve /O(n log n)/ total memory allocation and run-time, in -- contrast to the /O(n^2)/ that would be required by a naive -- left-fold. byteStringToInteger :: BS.ByteString -> Integer -- byteStringToInteger = BS.foldl' (\a b -> a `shiftL` 8 .|. toInteger b) 0 byteStringToInteger bs | l == 0 = 0 | l == 1 = toInteger (BS.head bs) | otherwise = x1 `shiftL` (l2 * 8) .|. x2 where l = BS.length bs l1 = l `div` 2 l2 = l - l1 (bs1, bs2) = BS.splitAt l1 bs x1 = byteStringToInteger bs1 x2 = byteStringToInteger bs2 writeFileCmd :: FilePath -> String -> (Int,Int) -> Maybe FilePath -> REPL () writeFileCmd file str pos fnm = do expr <- replParseExpr str pos fnm (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 n vs) = do ws <- rEval (mapM (>>= E.fromVWord Concrete "serializeValue") $ E.enumerateSeqMap n vs) return $ BS.pack $ map serializeByte ws serializeValue _ = panic "Cryptol.REPL.Command.writeFileCmd" ["Impossible: Non-VSeq value of type [n][8]."] serializeByte (Concrete.BV _ v) = fromIntegral (v .&. 0xFF) rEval :: E.Eval a -> REPL a rEval m = io (E.runEval mempty m) rEvalRethrow :: E.Eval a -> REPL a rEvalRethrow m = io $ rethrowEvalError $ E.runEval mempty m reloadCmd :: REPL () reloadCmd = do mb <- getLoadedMod case mb of Just lm -> case lName lm of Just m | M.isParamInstModName m -> loadHelper (M.loadModuleByName m) _ -> case lPath lm of M.InFile f -> loadCmd f _ -> return () Nothing -> return () editCmd :: String -> REPL () editCmd path = do mbE <- getEditPath mbL <- getLoadedMod if not (null path) then do when (isNothing mbL) $ setLoadedMod LoadedModule { lName = Nothing , lPath = M.InFile path } doEdit path else case msum [ M.InFile <$> mbE, lPath <$> mbL ] of Nothing -> rPutStrLn "No filed to edit." Just p -> case p of M.InFile f -> doEdit f M.InMem l bs -> withROTempFile l bs replEdit >> pure () where doEdit p = do setEditPath p _ <- replEdit p reloadCmd withRWTempFile :: String -> (Handle -> IO a) -> IO a withRWTempFile name k = X.bracket (do tmp <- getTemporaryDirectory let esc c = if isAscii c && isAlphaNum c then c else '_' openTempFile tmp (map esc name)) (\(nm,h) -> hClose h >> removeFile nm) (k . snd) withROTempFile :: String -> ByteString -> (FilePath -> REPL a) -> REPL a withROTempFile name cnt k = do (path,h) <- mkTmp do mkFile path h k path `finally` liftIO (do hClose h removeFile path) where mkTmp = liftIO $ do tmp <- getTemporaryDirectory let esc c = if isAscii c && isAlphaNum c then c else '_' openTempFile tmp (map esc name ++ ".cry") mkFile path h = liftIO $ do BS8.hPutStrLn h cnt hFlush h setPermissions path (setOwnerReadable True emptyPermissions) moduleCmd :: String -> REPL () moduleCmd modString | null modString = return () | otherwise = do case parseModName modString of Just m | M.isParamInstModName m -> loadHelper (M.loadModuleByName m) | otherwise -> do mpath <- liftModuleCmd (M.findModule m) case mpath of M.InFile file -> do setEditPath file setLoadedMod LoadedModule { lName = Just m, lPath = mpath } loadHelper (M.loadModuleByPath file) M.InMem {} -> loadHelper (M.loadModuleByName m) Nothing -> rPutStrLn "Invalid module name." loadPrelude :: REPL () loadPrelude = moduleCmd $ show $ pp M.preludeName loadCmd :: FilePath -> REPL () loadCmd path | null path = return () -- when `:load`, the edit and focused paths become the parameter | otherwise = do setEditPath path setLoadedMod LoadedModule { lName = Nothing , lPath = M.InFile path } loadHelper (M.loadModuleByPath path) loadHelper :: M.ModuleCmd (M.ModulePath,T.Module) -> REPL () loadHelper how = do clearLoadedMod (path,m) <- liftModuleCmd how whenDebug (rPutStrLn (dump m)) setLoadedMod LoadedModule { lName = Just (T.mName m) , lPath = path } -- after a successful load, the current module becomes the edit target case path of M.InFile f -> setEditPath f M.InMem {} -> clearEditPath setDynEnv mempty versionCmd :: REPL () versionCmd = displayVersion rPutStrLn quitCmd :: REPL () quitCmd = stop browseCmd :: String -> REPL () browseCmd input | null input = do fe <- getFocusedEnv rPrint (browseModContext BrowseInScope fe) | otherwise = case parseModName input of Nothing -> rPutStrLn "Invalid module name" Just m -> do mb <- M.modContextOf m <$> getModuleEnv case mb of Nothing -> rPutStrLn ("Module " ++ show input ++ " is not loaded") Just fe -> rPrint (browseModContext BrowseExported fe) 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 v -> rPutStrLn (k ++ " = " ++ showEnvVal v) 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 ++ "`?") showEnvVal :: EnvVal -> String showEnvVal ev = case ev of EnvString s -> s EnvProg p as -> intercalate " " (p:as) EnvNum n -> show n EnvBool True -> "on" EnvBool False -> "off" -- XXX at the moment, this can only look at declarations. helpCmd :: String -> REPL () helpCmd cmd | null cmd = mapM_ rPutStrLn (genHelp commandList) | cmd0 : args <- words cmd, ":" `isPrefixOf` cmd0 = case findCommandExact cmd0 of [] -> void $ runCommand 1 Nothing (Unknown cmd0) [c] -> showCmdHelp c args cs -> void $ runCommand 1 Nothing (Ambiguous cmd0 (concatMap cNames cs)) | otherwise = case parseHelpName cmd of Just qname -> do fe <- getFocusedEnv let params = M.mctxParams fe env = M.mctxDecls fe rnEnv = M.mctxNames fe disp = M.mctxNameDisp fe vNames = M.lookupValNames qname rnEnv tNames = M.lookupTypeNames qname rnEnv mNames = M.lookupNS M.NSModule qname rnEnv let helps = map (showTypeHelp params env disp) tNames ++ map (showValHelp params env disp qname) vNames ++ map (showModHelp env disp) mNames separ = rPutStrLn " ---------" sequence_ (intersperse separ helps) when (null (vNames ++ tNames ++ mNames)) $ rPrint $ "Undefined name:" <+> pp qname Nothing -> rPutStrLn ("Unable to parse name: " ++ cmd) where noInfo nameEnv name = case M.nameInfo name of M.Declared m _ -> rPrint $ runDoc nameEnv ("Name defined in module" <+> pp m) M.Parameter -> rPutStrLn "// No documentation is available." showModHelp _env disp x = rPrint $ runDoc disp $ vcat [ "`" <> pp x <> "` is a module." ] -- XXX: show doc. if any showTypeHelp params env nameEnv name = fromMaybe (noInfo nameEnv name) $ msum [ fromTySyn, fromPrimType, fromNewtype, fromTyParam ] where fromTySyn = do ts <- Map.lookup name (M.ifTySyns env) return (doShowTyHelp nameEnv (pp ts) (T.tsDoc ts)) fromNewtype = do nt <- Map.lookup name (M.ifNewtypes env) let decl = pp nt $$ (pp name <+> text ":" <+> pp (T.newtypeConType nt)) return $ doShowTyHelp nameEnv decl (T.ntDoc nt) fromPrimType = do a <- Map.lookup name (M.ifAbstractTypes env) pure $ do rPutStrLn "" rPrint $ runDoc nameEnv $ nest 4 $ "primitive type" <+> pp (T.atName a) <+> ":" <+> pp (T.atKind a) let (vs,cs) = T.atCtrs a unless (null cs) $ do let example = T.TCon (T.abstractTypeTC a) (map (T.TVar . T.tpVar) vs) ns = T.addTNames vs emptyNameMap rs = [ "•" <+> ppWithNames ns c | c <- cs ] rPutStrLn "" rPrint $ runDoc nameEnv $ indent 4 $ backticks (ppWithNames ns example) <+> "requires:" $$ indent 2 (vcat rs) doShowFix (T.atFixitiy a) doShowDocString (T.atDoc a) fromTyParam = do p <- Map.lookup name (M.ifParamTypes params) let uses c = T.TVBound (T.mtpParam p) `Set.member` T.fvs c ctrs = filter uses (map P.thing (M.ifParamConstraints params)) ctrDoc = case ctrs of [] -> [] [x] -> [pp x] xs -> [parens $ commaSep $ map pp xs] decl = vcat $ [ text "parameter" <+> pp name <+> text ":" <+> pp (T.mtpKind p) ] ++ ctrDoc return $ doShowTyHelp nameEnv decl (T.mtpDoc p) doShowTyHelp nameEnv decl doc = do rPutStrLn "" rPrint (runDoc nameEnv (nest 4 decl)) doShowDocString doc doShowFix fx = case fx of Just f -> let msg = "Precedence " ++ show (P.fLevel f) ++ ", " ++ (case P.fAssoc f of P.LeftAssoc -> "associates to the left." P.RightAssoc -> "associates to the right." P.NonAssoc -> "does not associate.") in rPutStrLn ('\n' : msg) Nothing -> return () showValHelp params env nameEnv qname name = fromMaybe (noInfo nameEnv name) (msum [ fromDecl, fromNewtype, fromParameter ]) where fromDecl = do M.IfaceDecl { .. } <- Map.lookup name (M.ifDecls env) return $ do rPutStrLn "" let property | P.PragmaProperty `elem` ifDeclPragmas = [text "property"] | otherwise = [] rPrint $ runDoc nameEnv $ indent 4 $ hsep $ property ++ [pp qname, colon, pp (ifDeclSig)] doShowFix $ ifDeclFixity `mplus` (guard ifDeclInfix >> return P.defaultFixity) doShowDocString ifDeclDoc fromNewtype = do _ <- Map.lookup name (M.ifNewtypes env) return $ return () fromParameter = do p <- Map.lookup name (M.ifParamFuns params) return $ do rPutStrLn "" rPrint $ runDoc nameEnv $ indent 4 $ text "parameter" <+> pp qname <+> colon <+> pp (T.mvpType p) doShowFix (T.mvpFixity p) doShowDocString (T.mvpDoc p) doShowDocString doc = case doc of Nothing -> pure () Just d -> rPutStrLn ('\n' : T.unpack d) showCmdHelp c [arg] | ":set" `elem` cNames c = showOptionHelp arg showCmdHelp c _args = do rPutStrLn ("\n " ++ intercalate ", " (cNames c) ++ " " ++ intercalate " " (cArgs c)) rPutStrLn "" rPutStrLn (cHelp c) rPutStrLn "" when (not (null (cLongHelp c))) $ do rPutStrLn (cLongHelp c) rPutStrLn "" showOptionHelp arg = case lookupTrieExact arg userOptions of [opt] -> do let k = optName opt ev <- tryGetUser k rPutStrLn $ "\n " ++ k ++ " = " ++ maybe "???" showEnvVal ev rPutStrLn "" rPutStrLn ("Default value: " ++ showEnvVal (optDefault opt)) rPutStrLn "" rPutStrLn (optHelp opt) rPutStrLn "" [] -> rPutStrLn ("Unknown setting name `" ++ arg ++ "`") _ -> rPutStrLn ("Ambiguous setting name `" ++ arg ++ "`") 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 -- C-c Handlings --------------------------------------------------------------- -- XXX this should probably do something a bit more specific. handleCtrlC :: a -> REPL a handleCtrlC a = do rPutStrLn "Ctrl-C" resetTCSolver return a -- Utilities ------------------------------------------------------------------- -- | Lift a parsing action into the REPL monad. 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 -> Int -> Maybe FilePath -> REPL (P.ReplInput P.PName) replParseInput str lineNum fnm = replParse (parseReplWith cfg . T.pack) str where cfg = case fnm of Nothing -> interactiveConfig{ cfgStart = Position lineNum 1 } Just f -> defaultConfig { cfgSource = f , cfgStart = Position lineNum 1 } replParseExpr :: String -> (Int,Int) -> Maybe FilePath -> REPL (P.Expr P.PName) replParseExpr str (l,c) fnm = replParse (parseExprWith cfg. T.pack) str where cfg = case fnm of Nothing -> interactiveConfig{ cfgStart = Position l c } Just f -> defaultConfig { cfgSource = f , cfgStart = Position l c } mkInteractiveRange :: (Int,Int) -> Maybe FilePath -> Range mkInteractiveRange (l,c) mb = Range p p src where p = Position l c src = case mb of Nothing -> "" Just b -> b interactiveConfig :: Config interactiveConfig = defaultConfig { cfgSource = "" } getPrimMap :: REPL M.PrimMap getPrimMap = liftModuleCmd M.getPrimMap liftModuleCmd :: M.ModuleCmd a -> REPL a liftModuleCmd cmd = do evo <- getEvalOptsAction env <- getModuleEnv callStacks <- getCallStacks tcSolver <- getTCSolver let minp = M.ModuleInput { minpCallStacks = callStacks , minpEvalOpts = evo , minpByteReader = BS.readFile , minpModuleEnv = env , minpTCSolver = tcSolver } moduleCmdResult =<< io (cmd minp) moduleCmdResult :: M.ModuleRes a -> REPL a moduleCmdResult (res,ws0) = do warnDefaulting <- getKnownUser "warnDefaulting" warnShadowing <- getKnownUser "warnShadowing" -- XXX: let's generalize this pattern let isDefaultWarn (T.DefaultingTo _ _) = True isDefaultWarn _ = False filterDefaults w | warnDefaulting = Just w filterDefaults (M.TypeCheckWarnings nameMap xs) = case filter (not . isDefaultWarn . snd) xs of [] -> Nothing ys -> Just (M.TypeCheckWarnings nameMap ys) filterDefaults w = Just w isShadowWarn (M.SymbolShadowed {}) = True isShadowWarn _ = False 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 <- M.mctxNameDisp <$> getFocusedEnv mapM_ (rPrint . runDoc names . pp) ws case res of Right (a,me') -> setModuleEnv me' >> return a Left err -> do e <- case err of M.ErrorInFile (M.InFile file) e -> -- on error, the file with the error becomes the edit -- target. Note, however, that the focused module is not -- changed. do setEditPath file return e _ -> return err raise (ModuleSystemError names e) replCheckExpr :: P.Expr P.PName -> REPL (P.Expr M.Name,T.Expr,T.Schema) replCheckExpr e = liftModuleCmd $ M.checkExpr e -- | Check declarations as though they were defined at the top-level. replCheckDecls :: [P.Decl P.PName] -> REPL [T.DeclGroup] replCheckDecls ds = do -- check the decls npds <- liftModuleCmd (M.noPat ds) let mkTop d = P.Decl P.TopLevel { P.tlExport = P.Public , P.tlDoc = Nothing , P.tlValue = d } (names,ds',tyMap) <- liftModuleCmd (M.checkDecls (map mkTop npds)) -- extend the naming env and type synonym maps denv <- getDynEnv setDynEnv denv { M.deNames = names `M.shadowing` M.deNames denv , M.deTySyns = tyMap <> M.deTySyns denv } return ds' replSpecExpr :: T.Expr -> REPL T.Expr replSpecExpr e = liftModuleCmd $ S.specialize e replEvalExpr :: P.Expr P.PName -> REPL (Concrete.Value, T.Type) replEvalExpr expr = do (_,def,sig) <- replCheckExpr expr replEvalCheckedExpr def sig replEvalCheckedExpr :: T.Expr -> T.Schema -> REPL (Concrete.Value, T.Type) replEvalCheckedExpr def sig = do validEvalContext def validEvalContext sig s <- getTCSolver mbDef <- io (defaultReplExpr s def sig) (def1,ty) <- case mbDef of Nothing -> raise (EvalPolyError sig) Just (tys,def1) -> do warnDefaults tys let su = T.listParamSubst tys return (def1, T.apSubst su (T.sType sig)) whenDebug (rPutStrLn (dump def1)) tenv <- E.envTypes . M.deEnv <$> getDynEnv let tyv = E.evalValType tenv ty -- add "it" to the namespace via a new declaration itVar <- bindItVariable tyv def1 let itExpr = case getLoc def of Nothing -> T.EVar itVar Just rng -> T.ELocated rng (T.EVar itVar) -- evaluate the it variable val <- liftModuleCmd (rethrowEvalError . M.evalExpr itExpr) return (val,ty) where warnDefaults ts = case ts of [] -> return () _ -> do rPutStrLn "Showing a specific instance of polymorphic result:" mapM_ warnDefault ts warnDefault (x,t) = rPrint (" *" <+> nest 2 ("Using" <+> quotes (pp t) <+> "for" <+> pp (T.tvarDesc (T.tpInfo x)))) 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 -- | Creates a fresh binding of "it" to the expression given, and adds -- it to the current dynamic environment. The fresh name generated -- is returned. bindItVariable :: E.TValue -> T.Expr -> REPL T.Name bindItVariable ty expr = do freshIt <- freshName itIdent M.UserName let schema = T.Forall { T.sVars = [] , T.sProps = [] , T.sType = E.tValTy 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' } return freshIt -- | Extend the dynamic environment with a fresh binding for "it", -- as defined by the given value. If we cannot determine the definition -- of the value, then we don't bind `it`. bindItVariableVal :: E.TValue -> Concrete.Value -> REPL () bindItVariableVal ty val = do prims <- getPrimMap mb <- rEval (Concrete.toExpr prims ty val) case mb of Nothing -> return () Just expr -> void $ bindItVariable ty expr -- | Creates a fresh binding of "it" to a finite sequence of -- expressions of the same type, and adds that sequence to the current -- dynamic environment bindItVariables :: E.TValue -> [T.Expr] -> REPL () bindItVariables ty exprs = void $ bindItVariable seqTy seqExpr where len = length exprs seqTy = E.TVSeq (toInteger len) ty seqExpr = T.EList exprs (E.tValTy ty) replEvalDecls :: [P.Decl P.PName] -> REPL () replEvalDecls ds = do dgs <- replCheckDecls ds validEvalContext dgs 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 -- Command Parsing ------------------------------------------------------------- -- | Strip leading space. sanitize :: String -> String sanitize = dropWhile isSpace -- | Strip trailing space. sanitizeEnd :: String -> String sanitizeEnd = reverse . sanitize . reverse trim :: String -> String trim = sanitizeEnd . sanitize -- | Split at the first word boundary. splitCommand :: String -> Maybe (Int,String,String) splitCommand = go 0 where go !len (c : more) | isSpace c = go (len+1) more go !len (':': more) | (as,bs) <- span (\x -> isPunctuation x || isSymbol x) more , (ws,cs) <- span isSpace bs , not (null as) = Just (len+1+length as+length ws, ':' : as, cs) | (as,bs) <- break isSpace more , (ws,cs) <- span isSpace bs , not (null as) = Just (len+1+length as+length ws, ':' : as, cs) | otherwise = Nothing go !len expr | null expr = Nothing | otherwise = Just (len+length expr, expr, []) -- | Uncons a list. uncons :: [a] -> Maybe (a,[a]) uncons as = case as of a:rest -> Just (a,rest) _ -> Nothing -- | Lookup a string in the command list. findCommand :: String -> [CommandDescr] findCommand str = lookupTrie str commands -- | Lookup a string in the command list, returning an exact match -- even if it's the prefix of another command. findCommandExact :: String -> [CommandDescr] findCommandExact str = lookupTrieExact str commands -- | Lookup a string in the notebook-safe command list. findNbCommand :: Bool -> String -> [CommandDescr] findNbCommand True str = lookupTrieExact str nbCommands findNbCommand False str = lookupTrie str nbCommands -- | Parse a line as a command. parseCommand :: (String -> [CommandDescr]) -> String -> Maybe Command parseCommand findCmd line = do (cmdLen,cmd,args) <- splitCommand line let args' = sanitizeEnd args case findCmd cmd of [c] -> case cBody c of ExprArg body -> Just (Command \l fp -> (body args' (l,cmdLen+1) fp)) DeclsArg body -> Just (Command \_ _ -> (body args')) ExprTypeArg body -> Just (Command \_ _ -> (body args')) ModNameArg body -> Just (Command \_ _ -> (body args')) FilenameArg body -> Just (Command \_ _ -> (body =<< expandHome args')) OptionArg body -> Just (Command \_ _ -> (body args')) ShellArg body -> Just (Command \_ _ -> (body args')) HelpArg body -> Just (Command \_ _ -> (body args')) NoArg body -> Just (Command \_ _ -> body) FileExprArg body -> do (fpLen,fp,expr) <- extractFilePath args' Just (Command \l fp' -> do let col = cmdLen + fpLen + 1 hm <- expandHome fp body hm expr (l,col) fp') [] -> 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) -> (length a + 2, a, drop 1 b)) . break (== q) in case ipt of "" -> Nothing '\'':rest -> Just $ quoted '\'' rest '"':rest -> Just $ quoted '"' rest _ -> let (a,b) = break isSpace ipt in if null a then Nothing else Just (length a, a, b)