cryptol-3.4.0: src/Cryptol/REPL/Command.hs
-- |
-- 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 OverloadedStrings #-}
{-# LANGUAGE PatternGuards #-}
{-# LANGUAGE RecordWildCards #-}
{-# LANGUAGE ScopedTypeVariables #-}
-- 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(..), CommandResult(..)
, parseCommand
, runCommand
, splitCommand
, findCommand
, findCommandExact
, findNbCommand
, commandList
, emptyCommandResult
, moduleCmd, loadCmd, loadPrelude, setOptionCmd
-- Parsing
, interactiveConfig
, replParseExpr
-- Evaluation and Typechecking
, replEvalExpr
, replCheckExpr
-- Check, SAT, and prove
, TestReport(..)
, qcExpr, qcCmd, QCMode(..)
, satCmd
, proveCmd
, onlineProveSat
, offlineProveSat
-- Check docstrings
, checkDocStrings
, updateDocstringCache
, SubcommandResult(..)
, DocstringResult(..)
-- Misc utilities
, handleCtrlC
, sanitize
, withRWTempFile
, printModuleWarnings
-- To support Notebook interface (might need to refactor)
, replParse
, liftModuleCmd
, moduleCmdResult
, loadProjectREPL
) 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.Interface as M
import qualified Cryptol.ModuleSystem.Monad 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.Logger as Logger
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.Backend.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,parseImpName)
import Cryptol.Parser.Position (replPosition,startOfLine,Range(..),HasLoc(..))
import qualified Cryptol.TypeCheck.AST as T
import qualified Cryptol.TypeCheck.Docstrings 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, emptyNameMap, ppWithNames)
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.Project as Proj
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 qualified Data.Map.Strict as Map
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 Data.Maybe (fromMaybe,mapMaybe,isNothing)
import Data.Foldable (traverse_)
import System.Environment (lookupEnv)
import System.Exit (ExitCode(ExitSuccess))
import System.Process (shell,createProcess,waitForProcess,spawnProcess)
import qualified System.Process as Process(runCommand)
import System.FilePath((</>), (-<.>), isPathSeparator)
import System.Directory(getHomeDirectory,setCurrentDirectory,doesDirectoryExist
,getTemporaryDirectory,setPermissions,removeFile
,emptyPermissions,setOwnerReadable,doesFileExist)
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)
import Data.Foldable (foldl')
import qualified Cryptol.Project.Cache as Proj
import Cryptol.Project.Monad (LoadProjectMode)
-- Commands --------------------------------------------------------------------
-- | Commands.
data Command
= Command (Int -> Maybe FilePath -> REPL CommandResult) -- ^ 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 CommandResult)
| FileExprArg (FilePath -> String -> (Int,Int) -> Maybe FilePath -> REPL CommandResult)
| DeclsArg (String -> REPL CommandResult)
| ExprTypeArg (String -> REPL CommandResult)
| ModNameArg (String -> REPL CommandResult)
| FilenameArg (FilePath -> REPL CommandResult)
| OptionArg (String -> REPL CommandResult)
| ShellArg (String -> REPL CommandResult)
| HelpArg (String -> REPL CommandResult)
| NoArg (REPL CommandResult)
data CommandResult = CommandResult
{ crType :: Maybe String -- ^ type output for relevant commands
, crValue :: Maybe String -- ^ value output for relevant commands
, crSuccess :: Bool -- ^ indicator that command successfully performed its task
}
deriving (Show)
emptyCommandResult :: CommandResult
emptyCommandResult = CommandResult
{ crType = Nothing
, crValue = Nothing
, crSuccess = True
}
-- | 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 extractCoqCmd)
"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"
""
, CommandDescr [ ":check-docstrings" ] [] (ModNameArg checkDocStringsCmd)
"Run the REPL code blocks in the module's docstring comments"
""
, CommandDescr [ ":print-docstrings" ] [] (ModNameArg printDocStringsCmd)
"Print the REPL code blocks in the module's docstring comments"
""
, CommandDescr [ ":saw" ] [] (FilenameArg sawCmd)
"Load a given SAW file."
(unlines
[ "The path to SAW is determined from the environment variable"
, "CRYPTOL_SAW. The user option sawFlags contains flags that will be"
, "added to all calls to SAW."
])
]
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 [ ":f", ":focus" ] ["[ MODULE ]"] (ModNameArg focusCmd)
"Focus name scope inside a loaded module."
""
, 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."
, "Use filename \"-\" to write tests to stdout."
])
""
, 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 CommandResult
runCommand lineNum mbBatch c = case c of
Command cmd -> cmd lineNum mbBatch `Cryptol.REPL.Monad.catch` handler
where
handler re = do
rPutStrLn ""
rPrint (pp re)
return emptyCommandResult { crSuccess = False }
Unknown cmd -> do
rPutStrLn ("Unknown command: " ++ cmd)
return emptyCommandResult { crSuccess = False }
Ambiguous cmd cmds -> do
rPutStrLn (cmd ++ " is ambiguous, it could mean one of:")
rPutStrLn ("\t" ++ intercalate ", " cmds)
return emptyCommandResult { crSuccess = False }
evalCmd :: String -> Int -> Maybe FilePath -> REPL CommandResult
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
let value = show valDoc
rPutStrLn value
pure emptyCommandResult { crValue = Just value }
P.LetInput ds -> do
-- explicitly make this a top-level declaration, so that it will
-- be generalized if mono-binds is enabled
replEvalDecls ds
pure emptyCommandResult
P.EmptyInput ->
-- comment or empty input does nothing
pure emptyCommandResult
-- parsing and evaluating expressions can fail in many different ways
`catch` \e -> do
rPutStrLn ""
rPrint (pp e)
pure emptyCommandResult { crSuccess = False }
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 CommandResult
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)
outs <- 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")
let out = concat outs
writeResult <- io (X.try (if outFile == "-" then putStr out else writeFile outFile out))
case writeResult of
Right{} -> pure emptyCommandResult
Left e ->
do rPutStrLn (X.displayException (e :: X.SomeException))
pure emptyCommandResult { crSuccess = False }
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 CommandResult
qcCmd qcMode "" _pos _fnm =
do (xs,disp) <- getPropertyNames
let nameStr x = show (fixNameDisp disp (pp x))
if null xs
then do
rPutStrLn "There are no properties in this module."
pure emptyCommandResult { crSuccess = False }
else do
let evalProp result (x,d) =
do let str = nameStr x
rPutStr $ "property " ++ str ++ " "
let texpr = T.EVar x
let schema = T.dSignature d
nd <- M.mctxNameDisp <$> getFocusedEnv
let doc = fixNameDisp nd (pp texpr)
testReport <- qcExpr qcMode doc texpr schema
pure $! result && isPass (reportResult testReport)
success <- foldM evalProp True xs
pure emptyCommandResult { crSuccess = success }
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
testReport <- qcExpr qcMode doc texpr schema
pure emptyCommandResult { crSuccess = isPass (reportResult testReport) }
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 CommandResult
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 CommandResult
--- Throw error when no argument is passed to a command expecting one
safeCmd "" _pos _fnm =
do rPutStrLn $ invalidCommandArgument ":safe"
return emptyCommandResult {crSuccess = False}
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
do success <- offlineProveSat proverName SafetyQuery texpr schema mfile
pure emptyCommandResult { crSuccess = success }
else
do (firstProver,result,stats) <- rethrowErrorCall (onlineProveSat proverName SafetyQuery texpr schema mfile)
cmdResult <- case result of
EmptyResult ->
panic "REPL.Command" [ "got EmptyResult for online prover query" ]
ProverError msg ->
do rPrintDoc msg
pure emptyCommandResult { crSuccess = False }
ThmResult _ts ->
do rPutStrLn "Safe"
pure emptyCommandResult
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
pure emptyCommandResult { crSuccess = False }
AllSatResult _ -> do
panic "REPL.Command" ["Unexpected AllSAtResult for ':safe' call"]
seeStats <- getUserShowProverStats
when seeStats (showProverStats firstProver stats)
pure cmdResult
-- | 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 CommandResult
cmdProveSat isSat "" _pos _fnm =
do (xs,disp) <- getPropertyNames
let nameStr x = show (fixNameDisp disp (pp x))
if null xs
then do
rPutStrLn "There are no properties in this module."
pure emptyCommandResult { crSuccess = False }
else do
let check acc (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 = T.dSignature d
nd <- M.mctxNameDisp <$> getFocusedEnv
let doc = fixNameDisp nd (pp texpr)
success <- proveSatExpr isSat (M.nameLoc x) doc texpr schema
pure $! acc && success
success <- foldM check True xs
pure emptyCommandResult { crSuccess = success }
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)
success <- proveSatExpr isSat rng doc texpr schema
pure emptyCommandResult { crSuccess = success }
proveSatExpr ::
Bool ->
Range ->
Doc ->
T.Expr ->
T.Schema ->
REPL Bool
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)
success <- case result of
EmptyResult ->
panic "REPL.Command" [ "got EmptyResult for online prover query" ]
ProverError msg -> False <$ rPrintDoc 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
pure (not isSat)
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
pure False
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
pure True
seeStats <- getUserShowProverStats
when seeStats (showProverStats firstProver stats)
pure success
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"
~(EnvNum timeoutSec) <- getUser "proverTimeout"
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 timeoutSec cmd
Right w4Cfg ->
do ~(EnvBool hashConsing) <- getUser "hashConsing"
~(EnvBool warnUninterp) <- getUser "warnUninterp"
liftModuleCmd $ W4.satProve w4Cfg hashConsing warnUninterp timeoutSec cmd
stas <- io (readIORef timing)
return (firstProver,res,stas)
offlineProveSat :: String -> QueryType -> T.Expr -> T.Schema -> Maybe FilePath -> REPL Bool
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 -> False <$ rPrintDoc msg
Right smtlib -> do
io $ displayMsg
case mfile of
Just path -> io $ writeFile path smtlib
Nothing -> rPutStr smtlib
pure True
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 -> rPrintDoc msg
Nothing -> return ()
pure True
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 CommandResult
--- Throw error when no argument is passed to a command expecting one
specializeCmd "" _pos _fnm =
do rPutStrLn $ invalidCommandArgument ":debug_specialize"
return emptyCommandResult {crSuccess = False}
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:"
let value = dump spexpr
rPutStrLn value
pure emptyCommandResult { crValue = Just value }
refEvalCmd :: String -> (Int,Int) -> Maybe FilePath -> REPL CommandResult
--- Throw error when no argument is passed to a command expecting one
refEvalCmd "" _pos _fnm =
do rPutStrLn $ invalidCommandArgument ":eval"
return emptyCommandResult {crSuccess = False}
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
let value = show (R.ppEValue opts val)
rPutStrLn value
pure emptyCommandResult { crValue = Just value }
astOfCmd :: String -> (Int,Int) -> Maybe FilePath -> REPL CommandResult
--- Throw error when no argument is passed to a command expecting one
astOfCmd "" _pos _fnm =
do rPutStrLn $ invalidCommandArgument ":ast"
return emptyCommandResult {crSuccess = False}
astOfCmd str pos fnm = do
expr <- replParseExpr str pos fnm
(re,_,_) <- replCheckExpr (P.noPos expr)
rPrint (fmap M.nameUnique re)
pure emptyCommandResult
extractCoqCmd :: REPL CommandResult
extractCoqCmd = do
me <- getModuleEnv
rPrint $ T.showParseable $ concatMap T.mDecls $ M.loadedModules me
pure emptyCommandResult
typeOfCmd :: String -> (Int,Int) -> Maybe FilePath -> REPL CommandResult
--- Throw error when no argument is passed to a command expecting one
typeOfCmd "" _pos _fnm =
do rPutStrLn $ invalidCommandArgument ":type"
return emptyCommandResult {crSuccess = False}
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))
--- Get module context parameters
modCtxtParams <- M.mctxParams <$> getFocusedEnv
--- Get the map that maps variable names to module type parameters
let modParamMap = T.mpnTypes (M.modContextParamNames modCtxtParams)
--- Get a list of type parameters from all module type parameterss in the Map
modTParams = map T.mtpParam (Map.elems modParamMap)
cfg = defaultPPCfg
--- Load module type param into a new empty NameMap
ns = T.addTNames cfg modTParams emptyNameMap
--- Create a pretty printed string
ppAll = ppWithNames ns sig
fDisp <- M.mctxNameDisp <$> getFocusedEnv
-- type annotation ':' has precedence 2
let output = show $ runDoc fDisp $ group $ hang
(ppPrec 2 expr <+> text ":") 2 ppAll
rPutStrLn output
pure emptyCommandResult { crType = Just output }
timeCmd :: String -> (Int, Int) -> Maybe FilePath -> REPL CommandResult
--- Throw error when no argument is passed to a command expecting one
timeCmd "" _pos _fnm =
do rPutStrLn $ invalidCommandArgument ":time"
return emptyCommandResult {crSuccess = False}
timeCmd str pos fnm = do
period <- getKnownUser "timeMeasurementPeriod" :: REPL Int
quiet <- getKnownUser "timeQuiet"
pExpr <- replParseExpr str pos fnm
unless quiet $
rPutStrLn $ "Measuring for " ++ show period ++ " seconds"
(_, 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
pure emptyCommandResult -- TODO: gather timing outputs
readFileCmd :: FilePath -> REPL CommandResult
readFileCmd fp = do
bytes <- replReadFile fp (\err -> rPutStrLn (show err) >> return Nothing)
case bytes of
Nothing -> return emptyCommandResult { crSuccess = False }
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
pure emptyCommandResult
-- | 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 CommandResult
writeFileCmd file str pos fnm = do
expr <- replParseExpr str pos fnm
(val,ty) <- replEvalExpr expr
if not (tIsByteSeq ty)
then do
rPrint $ "Cannot write expression of types other than [n][8]."
<+> "Type was: " <+> pp ty
pure emptyCommandResult { crSuccess = False }
else do
bytes <- serializeValue val
replWriteFile file bytes
where
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 CommandResult
reloadCmd = do
mb <- getLoadedMod
case mb of
Just lm ->
case lPath lm of
M.InFile f -> loadCmd f
_ -> return emptyCommandResult
Nothing -> return emptyCommandResult
editCmd :: String -> REPL CommandResult
editCmd path =
do mbE <- getEditPath
mbL <- getLoadedMod
if not (null path)
then do when (isNothing mbL)
$ setLoadedMod LoadedModule { lFocus = Nothing
, lPath = M.InFile path }
doEdit path
else case msum [ M.InFile <$> mbE, lPath <$> mbL ] of
Nothing ->
do rPutStrLn "No filed to edit."
pure emptyCommandResult { crSuccess = False }
Just p ->
case p of
M.InFile f -> doEdit f
M.InMem l bs -> do
_ <- withROTempFile l bs replEdit
pure emptyCommandResult
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 CommandResult
moduleCmd modString
| null modString = return emptyCommandResult
| 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 { lFocus = Just (P.ImpTop m), lPath = mpath }
loadHelper (M.loadModuleByPath file)
M.InMem {} -> loadHelper (M.loadModuleByName m)
Nothing ->
do rPutStrLn "Invalid module name."
pure emptyCommandResult { crSuccess = False }
focusCmd :: String -> REPL CommandResult
focusCmd modString
| null modString =
do mb <- getLoadedMod
case mb of
Nothing -> pure ()
Just lm ->
case lName lm of
Nothing -> pure ()
Just name -> do
let top = P.ImpTop name
liftModuleCmd (`M.runModuleM` M.setFocusedModule top)
setLoadedMod lm { lFocus = Just top }
pure emptyCommandResult
| otherwise =
case parseImpName modString of
Nothing ->
do rPutStrLn "Invalid module name."
pure emptyCommandResult { crSuccess = False }
Just pimpName -> do
impName <- liftModuleCmd (setFocusedModuleCmd pimpName)
mb <- getLoadedMod
case mb of
Nothing -> pure ()
Just lm -> setLoadedMod lm { lFocus = Just impName }
pure emptyCommandResult
setFocusedModuleCmd :: P.ImpName P.PName -> M.ModuleCmd (P.ImpName T.Name)
setFocusedModuleCmd pimpName i = M.runModuleM i $
do impName <- M.renameImpNameInCurrentEnv pimpName
M.setFocusedModule impName
pure impName
loadPrelude :: REPL ()
loadPrelude = void $ moduleCmd $ show $ pp M.preludeName
loadCmd :: FilePath -> REPL CommandResult
loadCmd path
| null path = return emptyCommandResult
-- when `:load`, the edit and focused paths become the parameter
| otherwise = do setEditPath path
setLoadedMod LoadedModule { lFocus = Nothing
, lPath = M.InFile path
}
loadHelper (M.loadModuleByPath path)
loadHelper :: M.ModuleCmd (M.ModulePath,T.TCTopEntity) -> REPL CommandResult
loadHelper how =
do clearLoadedMod
(path,ent) <- liftModuleCmd how
whenDebug (rPutStrLn (dump ent))
setLoadedMod LoadedModule
{ lFocus = Just (P.ImpTop (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
pure emptyCommandResult
genHeaderCmd :: FilePath -> REPL CommandResult
genHeaderCmd path
| null path = pure emptyCommandResult
| otherwise = do
(mPath, m) <- liftModuleCmd $ M.checkModuleByPath path
let decls = case m of
T.TCTopModule mo -> findForeignDecls mo
T.TCTopSignature {} -> []
if null decls
then do
rPutStrLn $ "No foreign declarations in " ++ pretty mPath
pure emptyCommandResult { crSuccess = False }
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
M.InMem _ _ ->
do rPutStrLn header
pure emptyCommandResult
versionCmd :: REPL CommandResult
versionCmd = do
displayVersion rPutStrLn
pure emptyCommandResult
quitCmd :: REPL CommandResult
quitCmd = do
stop
pure emptyCommandResult
browseCmd :: String -> REPL CommandResult
browseCmd input
| null input =
do fe <- getFocusedEnv
rPrint (browseModContext BrowseInScope fe)
pure emptyCommandResult
| otherwise =
case parseImpName input of
Nothing -> do
rPutStrLn "Invalid module name"
pure emptyCommandResult { crSuccess = False }
Just (P.ImpTop mn) | M.modNameToText mn == "Main" -> do
mainContexts <- M.mainContexts <$> getModuleEnv
mapM_ (rPrint . browseModContext BrowseExported) mainContexts
pure emptyCommandResult
Just pimpName -> do
impName <- liftModuleCmd (`M.runModuleM` M.renameImpNameInCurrentEnv pimpName)
mb <- M.modContextOf impName <$> getModuleEnv
case mb of
Nothing -> do
rPutStrLn ("Module " ++ show input ++ " is not loaded")
pure emptyCommandResult { crSuccess = False }
Just fe -> do
rPrint (browseModContext BrowseExported fe)
pure emptyCommandResult
setOptionCmd :: String -> REPL CommandResult
setOptionCmd str
| Just value <- mbValue = setUser key value >>= \success -> pure emptyCommandResult { crSuccess = success }
| null key = mapM_ (describe . optName) (leaves userOptions) >> pure emptyCommandResult
| 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 -> do rPutStrLn (k ++ " = " ++ showEnvVal v)
pure emptyCommandResult
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 ++ "`?")
pure emptyCommandResult { crSuccess = False }
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 CommandResult
helpCmd cmd
| null cmd = emptyCommandResult <$ mapM_ rPutStrLn (genHelp commandList)
| cmd0 : args <- words cmd, ":" `isPrefixOf` cmd0 =
case findCommandExact cmd0 of
[] -> runCommand 1 Nothing (Unknown cmd0)
[c] -> showCmdHelp c args
cs -> runCommand 1 Nothing (Ambiguous cmd0 (concatMap cNames cs))
| otherwise =
wrapResult <$>
case parseHelpName cmd of
Just qname -> True <$ helpForNamed qname
Nothing -> False <$ rPutStrLn ("Unable to parse name: " ++ cmd)
where
wrapResult success = emptyCommandResult { crSuccess = success }
showCmdHelp c [arg] | ":set" `elem` cNames c = wrapResult <$> showOptionHelp arg
showCmdHelp c _args =
do rPutStrLn ("\n " ++ intercalate ", " (cNames c) ++ " " ++ intercalate " " (cArgs c))
rPutStrLn ""
rPutStrLn (cHelp c)
rPutStrLn ""
unless (null (cLongHelp c)) $ do
rPutStrLn (cLongHelp c)
rPutStrLn ""
pure emptyCommandResult
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 ""
pure True
[] -> False <$ rPutStrLn ("Unknown setting name `" ++ arg ++ "`")
_ -> False <$ rPutStrLn ("Ambiguous setting name `" ++ arg ++ "`")
runShellCmd :: String -> REPL CommandResult
runShellCmd cmd
= io $ do h <- Process.runCommand cmd
e <- waitForProcess h
pure emptyCommandResult { crSuccess = e == ExitSuccess }
cdCmd :: FilePath -> REPL CommandResult
cdCmd f | null f = do rPutStrLn $ "[error] :cd requires a path argument"
pure emptyCommandResult { crSuccess = False }
| otherwise = do
exists <- io $ doesDirectoryExist f
if exists
then emptyCommandResult <$ 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 = startOfLine lineNum }
Just f -> defaultConfig
{ cfgSource = f
, cfgStart = startOfLine lineNum
}
replParseExpr :: String -> (Int,Int) -> Maybe FilePath -> REPL (P.Expr P.PName)
replParseExpr str p fnm = replParse (parseExprWith cfg. T.pack) str
where
pos = replPosition p
cfg = case fnm of
Nothing -> interactiveConfig{ cfgStart = pos }
Just f -> defaultConfig
{ cfgSource = f
, cfgStart = pos
}
mkInteractiveRange :: (Int,Int) -> Maybe FilePath -> Range
mkInteractiveRange p mb = Range pos pos src
where
pos = replPosition p
src = case mb of
Nothing -> "<interactive>"
Just b -> b
interactiveConfig :: Config
interactiveConfig = defaultConfig { cfgSource = "<interactive>" }
getPrimMap :: REPL M.PrimMap
getPrimMap = liftModuleCmd M.getPrimMap
liftModuleCmd :: M.ModuleCmd a -> REPL a
liftModuleCmd cmd = moduleCmdResult =<< io . cmd =<< getModuleInput
-- TODO: add filter for my exhaustive prop guards warning here
printModuleWarnings :: [M.ModuleWarning] -> REPL ()
printModuleWarnings 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
moduleCmdResult :: M.ModuleRes a -> REPL a
moduleCmdResult (res,ws) = do
printModuleWarnings 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
names <- M.mctxNameDisp <$> getFocusedEnv
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 -> REPL CommandResult
replWriteFile = replWriteFileWith BS.writeFile
replWriteFileString :: FilePath -> String -> REPL CommandResult
replWriteFileString = replWriteFileWith writeFile
replWriteFileWith :: (FilePath -> a -> IO ()) -> FilePath -> a -> REPL CommandResult
replWriteFileWith write fp contents =
do x <- io (X.try (write fp contents))
case x of
Left e ->
do rPutStrLn (show (e :: X.SomeException))
pure emptyCommandResult { crSuccess = False }
Right _ ->
pure emptyCommandResult
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 CommandResult
newSeedCmd =
do seed <- createAndSetSeed
rPutStrLn "Seed initialized to:"
let value = show seed
rPutStrLn value
pure emptyCommandResult { crValue = Just value }
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 CommandResult
seedCmd s =
do success <- case mbGen of
Nothing -> False <$ rPutStrLn "Could not parse seed argument - expecting an integer or 4-tuple of integers."
Just gen -> True <$ setRandomGen gen
pure emptyCommandResult { crSuccess = success }
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
-- | Construct a helpful error message for commad parse errors where
-- a cryptol command is not given expression arg when its expecting one.
invalidCommandArgument :: String -> String
invalidCommandArgument cmd = concat ["ERROR: Command `", cmd
, "` needs an EXPR argument. See `:help "
, cmd, "` for more details."]
-- | 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 CommandResult
moduleInfoCmd isFile name
| isFile = showInfo =<< liftModuleCmd (M.getFileDependencies name)
| otherwise =
case parseModName name of
Just m -> showInfo =<< liftModuleCmd (M.getModuleDependencies m)
Nothing -> do rPutStrLn "Invalid module name."
pure emptyCommandResult { crSuccess = False }
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" (Map.keys (M.fiIncludeDeps fi))
depList (show . show . pp) "imports" (Set.toList (M.fiImportDeps fi))
depList show "foreign" (Map.toList (M.fiForeignDeps fi))
rPutStrLn "}"
pure emptyCommandResult
data SubcommandResult = SubcommandResult
{ srInput :: T.Text
, srResult :: CommandResult
, srLog :: String
}
printBlock :: [T.Text] -> REPL ()
printBlock block =
mapM_ printLine (continuedLines block)
printLine :: T.Text -> REPL ()
printLine line
| T.all isSpace line = pure ()
| otherwise =
case parseCommand (findNbCommand True) (T.unpack line) of
Nothing -> rPutStrLn "Failed to parse command"
Just Ambiguous{} -> rPutStrLn "Ambiguous command"
Just Unknown{} -> rPutStrLn "Unknown command"
Just (Command _) -> rPutStrLn (T.unpack line)
-- | Check a single code block from inside a docstring.
--
-- The result will contain the results of processing the commands up to
-- the first failure.
--
-- Execution of the commands is run in an isolated REPL environment.
checkBlock ::
[T.Text] {- ^ lines of the code block -} ->
REPL [SubcommandResult]
checkBlock = isolated . go . continuedLines
where
go [] = pure []
go (line:block)
| T.all isSpace line = go block
| otherwise =
do let tab n = replicate n ' '
rPutStrLn (tab 4 ++ T.unpack line)
let doErr msg =
do rPutStrLn (tab 6 ++ msg)
pure [SubcommandResult
{ srInput = line
, srLog = msg
, srResult = emptyCommandResult { crSuccess = False }
}]
case parseCommand (findNbCommand True) (T.unpack line) of
Nothing -> doErr "Failed to parse command"
Just Ambiguous{} -> doErr "Ambiguous command"
Just Unknown{} -> doErr "Unknown command"
Just (Command cmd) -> do
(logtxt, eresult) <- captureLog (Cryptol.REPL.Monad.try (cmd 0 Nothing))
case eresult of
Left e -> do
let result = SubcommandResult
{ srInput = line
, srLog = logtxt ++ show (pp e) ++ "\n"
, srResult = emptyCommandResult { crSuccess = False }
}
pure [result]
Right result -> do
let subresult = SubcommandResult
{ srInput = line
, srLog = logtxt
, srResult = result
}
subresults <- checkBlock block
pure (subresult : subresults)
-- | Combine lines ending in a backslash with the next line.
continuedLines :: [T.Text] -> [T.Text]
continuedLines xs =
case span ("\\" `T.isSuffixOf`) xs of
([], []) -> []
(a, []) -> [concat' (map T.init a)] -- permissive
(a, b:bs) -> concat' (map T.init a ++ [b]) : continuedLines bs
where
-- concat that eats leading whitespace between elements
concat' [] = T.empty
concat' (y:ys) = T.concat (y : map (T.dropWhile isSpace) ys)
captureLog :: REPL a -> REPL (String, a)
captureLog m = do
previousLogger <- getLogger
outputsRef <- io (newIORef [])
setPutStr $ \str ->
unless (null str) $
do lns <- readIORef outputsRef
let msg = preTab lns (postTab str)
Logger.logPutStr previousLogger msg
writeIORef outputsRef (str:lns)
result <- m `finally` setLogger previousLogger
outputs <- io (readIORef outputsRef)
let output = interpretControls (concat (reverse outputs))
pure (output, result)
where
tab = replicate 6 ' '
preTab prevLns msg =
case prevLns of
l : _
| last l /= '\n' -> msg
_ -> tab ++ msg
postTab cs =
case cs of
[] -> ""
['\n'] -> "\n"
'\n' : more -> '\n' : tab ++ postTab more
c : more -> c : postTab more
-- | Apply control character semantics to the result of the logger
interpretControls :: String -> String
interpretControls = f []
where
f [] ('\b':ys) = f [] ys -- skips unmatched \b
f (_:xs) ('\b':ys) = f xs ys
f xs (y :ys) = f (y:xs) ys
f xs [] = reverse xs
-- | The result of running a docstring as attached to a definition
data DocstringResult = DocstringResult
{ drName :: T.DocFor -- ^ The associated definition of the docstring
, drFences :: [[SubcommandResult]] -- ^ list of fences in this definition's docstring
}
-- | Check all the code blocks in a given docstring.
checkDocItem :: T.DocItem -> REPL DocstringResult
checkDocItem item =
do rPrint (" Docstrings on" <+> pp (T.docFor item))
xs <- case traverse T.extractCodeBlocks (T.docText item) of
[] -> pure [] -- optimization
bs ->
Ex.bracket
(liftModuleCmd (`M.runModuleM` (M.getFocusedModule <* M.setFocusedModule (T.docModContext item))))
(\mb -> liftModuleCmd (`M.runModuleM` M.setMaybeFocusedModule mb))
(\_ -> traverse checkBlock (concat bs))
pure DocstringResult
{ drName = T.docFor item
, drFences = xs
}
printDocItem :: T.DocItem -> REPL ()
printDocItem item = do
let bs = traverse T.extractCodeBlocks (T.docText item)
traverse_ printBlock (concat bs)
printDocStrings :: M.LoadedModule -> REPL ()
printDocStrings m = do
let dat = M.lmdModule (M.lmData m)
let ds = T.gatherModuleDocstrings (M.ifaceNameToModuleMap (M.lmInterface m)) dat
traverse_ printDocItem ds
-- | Check all of the docstrings in the given module.
--
-- The outer list elements correspond to the code blocks from the
-- docstrings in file order. Each inner list corresponds to the
-- REPL commands inside each of the docstrings.
checkDocStrings :: M.LoadedModule -> Maybe Proj.CacheId -> REPL ([DocstringResult], Proj.CacheId)
checkDocStrings m expectCache = do
let dat = M.lmdModule (M.lmData m)
rPrint ("Checking module" <+> pp (T.mName dat))
let ds = T.gatherModuleDocstrings (M.ifaceNameToModuleMap (M.lmInterface m)) dat
results <- traverse checkDocItem ds
cid <- updateDocstringCache m results expectCache
pure (results,cid)
checkDocstringResult :: DocstringResult -> Bool
checkDocstringResult r = all (all (crSuccess . srResult)) (drFences r)
updateDocstringCache :: M.LoadedModule -> [DocstringResult] -> Maybe Proj.CacheId -> REPL Proj.CacheId
updateDocstringCache m result expectCache =
do (cache,cacheId) <- io Proj.loadLoadCache
case expectCache of
Just c | c /= cacheId -> pure cacheId
_ ->
case M.lmFilePath m of
M.InMem{} -> pure cacheId
M.InFile fp ->
case Map.lookup (Proj.CacheInFile fp) (Proj.cacheModules cache) of
Nothing -> pure cacheId
Just entry ->
if Proj.moduleFingerprint (Proj.cacheFingerprint entry) /= M.fiFingerprint (M.lmFileInfo m)
then pure cacheId
else
do let entry' = entry { Proj.cacheDocstringResult = Just (all checkDocstringResult result) }
let cache' = cache { Proj.cacheModules = Map.insert (Proj.CacheInFile fp) entry' (Proj.cacheModules cache) }
io (Proj.saveLoadCache cache')
withModule :: String -> (P.ModName -> REPL CommandResult) -> REPL CommandResult
withModule input f
| null input = do
mb <- getLoadedMod
case lName =<< mb of
Nothing -> do
rPutStrLn "No current module"
pure emptyCommandResult { crSuccess = False }
Just mn -> f mn
| otherwise =
case parseModName input of
Nothing -> do
rPutStrLn "Invalid module name"
pure emptyCommandResult { crSuccess = False }
Just mn -> f mn
printDocStringsCmd ::
String {- ^ module name -} ->
REPL CommandResult
printDocStringsCmd input = withModule input checkModNameForPrint
-- | Evaluate all the docstrings in the specified module.
--
-- This command succeeds when:
-- * the module can be found
-- * the docstrings can be parsed for code blocks
-- * all of the commands in the docstrings succeed
checkDocStringsCmd ::
String {- ^ module name -} ->
REPL CommandResult
checkDocStringsCmd input = withModule input (checkModName 0)
countOutcomes :: [[SubcommandResult]] -> (Int, Int, Int)
countOutcomes = foldl' countOutcomes1 (0, 0, 0)
where
countOutcomes1 (successes, nofences, failures) []
= (successes, nofences + 1, failures)
countOutcomes1 acc result = foldl' countOutcomes2 acc result
countOutcomes2 (successes, nofences, failures) result
| crSuccess (srResult result) = (successes + 1, nofences, failures)
| otherwise = (successes, nofences, failures + 1)
withValidModule :: P.ModName -> String -> (M.LoadedModule -> REPL CommandResult) -> REPL CommandResult
withValidModule mn tab f =
do env <- getModuleEnv
case M.lookupModule mn env of
Nothing ->
case M.lookupSignature mn env of
Nothing ->
do rPutStrLn (tab ++ "Module " ++ show mn ++ " is not loaded")
pure emptyCommandResult { crSuccess = False }
Just{} ->
do rPutStrLn (tab ++ "Skipping docstrings on interface module")
pure emptyCommandResult
Just fe
| T.isParametrizedModule (M.lmdModule (M.lmData fe)) -> do
rPutStrLn (tab ++ "Skipping docstrings on parameterized module")
pure emptyCommandResult
| otherwise -> f fe
checkModName :: Int -> P.ModName -> REPL CommandResult
checkModName ind mn =
withValidModule mn tab (\m -> do
(results,_) <- checkDocStrings m Nothing
let (successes, nofences, failures) = countOutcomes [concat (drFences r) | r <- results]
rPutStrLn ("Successes: " ++ show successes ++
", No fences: " ++ show nofences ++
", Failures: " ++ show failures)
pure emptyCommandResult { crSuccess = failures == 0 })
where tab = replicate ind ' '
checkModNameForPrint :: P.ModName -> REPL CommandResult
checkModNameForPrint mn =
withValidModule mn "" (\m -> do
printDocStrings m
pure emptyCommandResult { crSuccess = True })
-- | Load a project.
-- Note that this does not update the Cryptol environment, it only updates
-- the project cache.
loadProjectREPL :: LoadProjectMode -> Proj.Config -> REPL CommandResult
loadProjectREPL mode cfg =
do minp <- getModuleInput
(res, warnings) <- io $ M.runModuleM minp $ Proj.loadProject mode cfg
printModuleWarnings warnings
case res of
Left err ->
do names <- M.mctxNameDisp <$> getFocusedEnv
rPrint (pp (ModuleSystemError names err))
pure emptyCommandResult { crSuccess = False }
Right ((fps, mp, docstringResults),env) ->
do setModuleEnv env
let cache0 = fmap (\fp -> Proj.CacheEntry { cacheDocstringResult = Nothing, cacheFingerprint = fp }) fps
(cache, success) <-
foldM (\(fpAcc_, success_) (k, v) ->
case k of
M.InMem{} -> pure (fpAcc_, success_)
M.InFile path ->
case v of
Proj.Invalid e ->
do rPrint ("Failed to process module:" <+> (text path <> ":") $$
indent 2 (ppInvalidStatus e))
pure (fpAcc_, False) -- report failure
Proj.Scanned Proj.Unchanged _ ms ->
foldM f (fpAcc_, success_) ms
where
f (fpAcc, success) (m, _) =
do let name = P.thing (P.mName m)
case join (Map.lookup (Proj.CacheInFile path) docstringResults) of
Just True ->
do rPrint ("Checking module" <+> hcat [pp name, ": PASS (cached)"])
let fpAcc' = Map.adjust (\e -> e{ Proj.cacheDocstringResult = Just True }) (Proj.CacheInFile path) fpAcc
pure (fpAcc', success) -- preserve success
Just False ->
do rPrint ("Checking module" <+> hcat [pp name, ": FAIL (cached)"])
let fpAcc' = Map.adjust (\e -> e{ Proj.cacheDocstringResult = Just False }) (Proj.CacheInFile path) fpAcc
pure (fpAcc', False) -- preserve failure
Nothing ->
do checkRes <- checkModName 2 name
let success1 = crSuccess checkRes
let fpAcc' = Map.adjust (\e -> e{ Proj.cacheDocstringResult = Just success1 }) (Proj.CacheInFile path) fpAcc
pure (fpAcc', success && success1)
Proj.Scanned Proj.Changed _ ms ->
foldM f (fpAcc_, success_) ms
where
f (fpAcc, success) (m, _) =
do let name = P.thing (P.mName m)
checkRes <- checkModName 2 name
let fpAcc' = Map.adjust (\fp -> fp { Proj.cacheDocstringResult = Just (crSuccess checkRes) }) (Proj.CacheInFile path) fpAcc
pure (fpAcc', success && crSuccess checkRes)
) (cache0, True) (Map.assocs mp)
let (passing, failing, missing) =
foldl
(\(a,b,c) x ->
case Proj.cacheDocstringResult x of
Nothing -> (a,b,c+1)
Just True -> (a+1,b,c)
Just False -> (a,b+1,c))
(0::Int,0::Int,0::Int) (Map.elems cache)
rPutStrLn ("Passing: " ++ show passing ++ ", Failing: " ++ show failing ++ ", Missing: " ++ show missing)
_cacheId <- io (Proj.saveLoadCache (Proj.LoadCache cache))
pure emptyCommandResult { crSuccess = success }
-- | Get the path to the SAW command.
-- Search options, in order:
-- environment variable CRYPTOL_SAW=/path/to/saw
-- whatever's in $PATH
getSAW :: REPL (String, [String])
getSAW = do
io (lookupEnv "CRYPTOL_SAW") >>= \case
Just s -> do
let saw = lexFlags s
case saw of
cmd : args -> pure (cmd, args)
[] -> pure ("", [])
Nothing -> pure ("saw", [])
-- | Run SAW on a file.
--
-- This command succeeds when:
-- * SAW can be found
-- * the file can be found
-- * SAW processes the file successfully
sawCmd ::
FilePath {- ^ SAW filename -} ->
REPL CommandResult
sawCmd input = do
present <- io $ doesFileExist input
if present then do
(cmd, args) <- getSAW
flags <- getKnownUser "sawFlags"
if cmd == "" then do
rPutStrLn $ "SAW `" ++ cmd ++ "' was empty."
pure emptyCommandResult { crSuccess = False }
else do
hdl <- io $ spawnProcess cmd (args ++ lexFlags flags ++ [input])
exitCode <- io $ waitForProcess hdl
pure emptyCommandResult { crSuccess = exitCode == ExitSuccess }
else do
rPutStrLn $ "File `" ++ input ++ "' does not exist."
pure emptyCommandResult { crSuccess = False }
ppInvalidStatus :: Proj.InvalidStatus -> Doc
ppInvalidStatus = \case
Proj.InvalidModule modErr -> pp modErr
Proj.InvalidDep d _ -> "Error in dependency: " <> pp d
lexFlags :: String -> [String]
lexFlags cs =
case dropWhile isSpace cs of
[] -> []
ds@(c : _)
| c == '"', [(str,rest)] <- lex ds -> read str : lexFlags rest
| otherwise ->
let (as,rest) = break isSpace ds
in as : lexFlags rest