content: -- |
  -- 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
  