-- | -- 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 Cryptol.REPL.Help 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, PrefixAssocChanged)) import qualified Cryptol.Utils.Ident as M import qualified Cryptol.ModuleSystem.Env as M import Cryptol.ModuleSystem.Fingerprint(fingerprintHexString) import Cryptol.Backend.FloatHelpers as FP 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 Cryptol.Eval.FFI import Cryptol.Eval.FFI.GenHeader 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) import qualified Cryptol.Utils.Benchmark as Bench 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 Text.Read (readMaybe) import Control.Applicative ((<|>)) import qualified Data.Set as Set 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) import qualified Data.Map as Map 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 System.IO (Handle,hFlush,stdout,openTempFile,hClose,openFile ,IOMode(..),hGetContents,hSeek,SeekMode(..)) import qualified System.Random.TF as TF import qualified System.Random.TF.Instances as TFI 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." "" , CommandDescr [ ":time" ] ["EXPR"] (ExprArg timeCmd) "Measure the time it takes to evaluate the given expression." (unlines [ "The expression will be evaluated many times to get accurate results." , "Note that the first evaluation of a binding may take longer due to" , " laziness, and this may affect the reported time. If this is not" , " desired then make sure to evaluate the expression once first before" , " running :time." , "The amount of time to spend collecting measurements can be changed" , " with the timeMeasurementPeriod option." , "Reports the average wall clock time, CPU time, and cycles." , " (Cycles are in unspecified units that may be CPU cycles.)" , "Binds the result to" , " it : { avgTime : Float64" , " , avgCpuTime : Float64" , " , avgCycles : Integer }" ]) , CommandDescr [ ":set-seed" ] ["SEED"] (OptionArg seedCmd) "Seed the random number generator for operations using randomness" (unlines [ "A seed takes the form of either a single integer or a 4-tuple" , "of unsigned 64-bit integers. Examples of commands using randomness" , "are dumpTests and check." ]) , CommandDescr [ ":new-seed"] [] (NoArg newSeedCmd) "Randomly generate and set a new seed for the random number generator" "" ] 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." ]) "" , CommandDescr [ ":generate-foreign-header" ] ["FILE"] (FilenameArg genHeaderCmd) "Generate a C header file from foreign declarations in a Cryptol file." (unlines [ "Converts all foreign declarations in the given Cryptol file into C" , "function declarations, and writes them to a file with the same name" , "but with a .h extension." ]) , CommandDescr [ ":file-deps" ] [ "FILE" ] (FilenameArg (moduleInfoCmd True)) "Show information about the dependencies of a file" "" , CommandDescr [ ":module-deps" ] [ "MODULE" ] (ModNameArg (moduleInfoCmd False)) "Show information about the dependencies of a module" "" ] 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 -- NB: Use a precedence of 1 here, as `vs` will be pretty-printed as -- arguments to the function in `exprDoc`. This ensures that arguments -- are parenthesized as needed. docs <- mapM (rEval . E.ppValuePrec Concrete ppOpts 1) 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 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 <- withRandomGen (\g -> 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 >>= \mb_res -> case mb_res of Just res -> pure res -- If instance is not found, doesn't necessarily mean that there is no instance. -- And due to nondeterminism in result from the solver (for finding solution to -- numeric type constraints), `:check` can get to this exception sometimes, but -- successfully find an instance and test with it other times. Nothing -> raise (InstantiationsNotFound schema) testNum <- (toInteger :: Int -> Integer) <$> getKnownUser "tests" tenv <- E.envTypes . M.deEnv <$> getDynEnv let tyv = E.evalValType tenv ty -- tv has already had polymorphism instantiated 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 (res,num) <- withRandomGen (randomTests' (\n -> ppProgress percentRef testsRef n testNum) testNum val gens) `Ex.catch` (\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 >>= \mb_res -> case mb_res of Just (fn, _) -> pure fn Nothing -> raise (EvalPolyError 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) timeCmd :: String -> (Int, Int) -> Maybe FilePath -> REPL () timeCmd str pos fnm = do period <- getKnownUser "timeMeasurementPeriod" :: REPL Int quiet <- getKnownUser "timeQuiet" unless quiet $ rPutStrLn $ "Measuring for " ++ show period ++ " seconds" pExpr <- replParseExpr str pos fnm (_, def, sig) <- replCheckExpr pExpr replPrepareCheckedExpr def sig >>= \case Nothing -> raise (EvalPolyError sig) Just (_, expr) -> do Bench.BenchmarkStats {..} <- liftModuleCmd (rethrowEvalError . M.benchmarkExpr (fromIntegral period) expr) unless quiet $ rPutStrLn $ "Avg time: " ++ Bench.secs benchAvgTime ++ " Avg CPU time: " ++ Bench.secs benchAvgCpuTime ++ " Avg cycles: " ++ show benchAvgCycles let mkStatsRec time cpuTime cycles = recordFromFields [("avgTime", time), ("avgCpuTime", cpuTime), ("avgCycles", cycles)] itType = E.TVRec $ mkStatsRec E.tvFloat64 E.tvFloat64 E.TVInteger itVal = E.VRecord $ mkStatsRec (pure $ E.VFloat $ FP.floatFromDouble benchAvgTime) (pure $ E.VFloat $ FP.floatFromDouble benchAvgCpuTime) (pure $ E.VInteger $ toInteger benchAvgCycles) bindItVariableVal itType itVal 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 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 -> 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.TCTopEntity) -> REPL () loadHelper how = do clearLoadedMod (path,ent) <- liftModuleCmd how whenDebug (rPutStrLn (dump ent)) setLoadedMod LoadedModule { lName = Just (T.tcTopEntitytName ent) , 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 genHeaderCmd :: FilePath -> REPL () genHeaderCmd path | null path = pure () | otherwise = do (mPath, m) <- liftModuleCmd $ M.checkModuleByPath path let decls = case m of T.TCTopModule mo -> findForeignDecls mo T.TCTopSignature {} -> [] if null decls then rPutStrLn $ "No foreign declarations in " ++ pretty mPath else do let header = generateForeignHeader decls case mPath of M.InFile p -> do let hPath = p -<.> "h" rPutStrLn $ "Writing header to " ++ hPath replWriteFileString hPath header (rPutStrLn . show) M.InMem _ _ -> rPutStrLn header 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 -> helpForNamed qname Nothing -> rPutStrLn ("Unable to parse name: " ++ cmd) where 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) -- TODO: add filter for my exhaustie prop guards warning here moduleCmdResult :: M.ModuleRes a -> REPL a moduleCmdResult (res,ws0) = do warnDefaulting <- getKnownUser "warnDefaulting" warnShadowing <- getKnownUser "warnShadowing" warnPrefixAssoc <- getKnownUser "warnPrefixAssoc" warnNonExhConGrds <- getKnownUser "warnNonExhaustiveConstraintGuards" -- XXX: let's generalize this pattern let isShadowWarn (M.SymbolShadowed {}) = True isShadowWarn _ = False isPrefixAssocWarn (M.PrefixAssocChanged {}) = True isPrefixAssocWarn _ = False filterRenamer True _ w = Just w filterRenamer _ check (M.RenamerWarnings xs) = case filter (not . check) xs of [] -> Nothing ys -> Just (M.RenamerWarnings ys) filterRenamer _ _ w = Just w -- ignore certain warnings during typechecking filterTypecheck :: M.ModuleWarning -> Maybe M.ModuleWarning filterTypecheck (M.TypeCheckWarnings nameMap xs) = case filter (allow . snd) xs of [] -> Nothing ys -> Just (M.TypeCheckWarnings nameMap ys) where allow :: T.Warning -> Bool allow = \case T.DefaultingTo _ _ | not warnDefaulting -> False T.NonExhaustivePropGuards _ | not warnNonExhConGrds -> False _ -> True filterTypecheck w = Just w let ws = mapMaybe (filterRenamer warnShadowing isShadowWarn) . mapMaybe (filterRenamer warnPrefixAssoc isPrefixAssocWarn) . mapMaybe filterTypecheck $ 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 >>= \case Just res -> pure res Nothing -> raise (EvalPolyError sig) replEvalCheckedExpr :: T.Expr -> T.Schema -> REPL (Maybe (Concrete.Value, T.Type)) replEvalCheckedExpr def sig = replPrepareCheckedExpr def sig >>= traverse \(tys, def1) -> do let su = T.listParamSubst tys let ty = 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) -- | Check that we are in a valid evaluation context and apply defaulting. replPrepareCheckedExpr :: T.Expr -> T.Schema -> REPL (Maybe ([(T.TParam, T.Type)], T.Expr)) replPrepareCheckedExpr def sig = do validEvalContext def validEvalContext sig s <- getTCSolver mbDef <- io (defaultReplExpr s def sig) case mbDef of Nothing -> pure Nothing Just (tys, def1) -> do warnDefaults tys pure $ Just (tys, def1) 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 = replWriteFileWith BS.writeFile replWriteFileString :: FilePath -> String -> (X.SomeException -> REPL ()) -> REPL () replWriteFileString = replWriteFileWith writeFile replWriteFileWith :: (FilePath -> a -> IO ()) -> FilePath -> a -> (X.SomeException -> REPL ()) -> REPL () replWriteFileWith write fp contents handler = do x <- io $ X.catch (write fp contents >> 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.singletonNS M.NSValue (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 newSeedCmd :: REPL () newSeedCmd = do seed <- createAndSetSeed rPutStrLn "Seed initialized to:" rPutStrLn (show seed) where createAndSetSeed = withRandomGen $ \g0 -> let (s1, g1) = TFI.random g0 (s2, g2) = TFI.random g1 (s3, g3) = TFI.random g2 (s4, _) = TFI.random g3 seed = (s1, s2, s3, s4) in pure (seed, TF.seedTFGen seed) seedCmd :: String -> REPL () seedCmd s = case mbGen of Nothing -> rPutStrLn "Could not parse seed argument - expecting an integer or 4-tuple of integers." Just gen -> setRandomGen gen where mbGen = (TF.mkTFGen <$> readMaybe s) <|> (TF.seedTFGen <$> readMaybe s) -- 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) moduleInfoCmd :: Bool -> String -> REPL () moduleInfoCmd isFile name | isFile = showInfo =<< liftModuleCmd (M.getFileDependencies name) | otherwise = case parseModName name of Just m -> showInfo =<< liftModuleCmd (M.getModuleDependencies m) Nothing -> rPutStrLn "Invalid module name." where showInfo (p,fi) = do rPutStr "{ \"source\": " case p of M.InFile f -> rPutStrLn (show f) M.InMem l _ -> rPutStrLn ("{ \"internal\": " ++ show l ++ " }") rPutStrLn (", \"fingerprint\": \"0x" ++ fingerprintHexString (M.fiFingerprint fi) ++ "\"") let depList f x ys = do rPutStr (", " ++ show (x :: String) ++ ":") case ys of [] -> rPutStrLn " []" i : is -> do rPutStrLn "" rPutStrLn (" [ " ++ f i) mapM_ (\j -> rPutStrLn (" , " ++ f j)) is rPutStrLn " ]" depList show "includes" (Set.toList (M.fiIncludeDeps fi)) depList (show . show . pp) "imports" (Set.toList (M.fiImportDeps fi)) depList show "foreign" (Map.toList (M.fiForeignDeps fi)) rPutStrLn "}"