Merge pull request #1010 from GaloisInc/interactive-batch

Interactive batch

cryptol/CheckExercises.hs

@@ -217,11 +217,11 @@ processLine s = do
           -- be checked for errors but that the result can be discarded.
           addReplData
           nextLine
-      | Just (InlineReplin, cmd, rst) <- inlineRepl s_nocomment -> do
+      | Just (InlineReplin, cmd, rst) <- inlineRepl s -> do
           -- Ingest an inline replin command.
           addReplin cmd
           processLine rst
-      | Just (InlineReplout, cmd, rst) <- inlineRepl s_nocomment -> do
+      | Just (InlineReplout, cmd, rst) <- inlineRepl s -> do
           -- Ingest an inline replout command, switching to replout mode.
           modify' $ \st -> st { pMode = AwaitingReploutMode }
           addReplout cmd
@@ -253,14 +253,14 @@ processLine s = do
           addReplData
           modify' $ \st -> st { pMode = ReplinMode }
           nextLine
-      | Just (InlineReplin, cmd, rst) <- inlineRepl s_nocomment -> do
+      | Just (InlineReplin, cmd, rst) <- inlineRepl s -> do
           -- Ingest an inline replin command, switching to replin mode and
           -- committing the current repl data.
           addReplData
           modify' $ \st -> st { pMode = AwaitingReplinMode }
           addReplin cmd
           processLine rst
-      | Just (InlineReplout, cmd, rst) <- inlineRepl s_nocomment -> do
+      | Just (InlineReplout, cmd, rst) <- inlineRepl s -> do
           -- Ingest an replout command.
           addReplout cmd
           processLine rst
@@ -299,7 +299,7 @@ main = do
     let exe = fromMaybe "./cry run" (cryptolExe opts)
 
     if Seq.null (rdReplout rd)
-      then do let cryCmd = (P.shell (exe ++ " -b " ++ inFile ++ " -e"))
+      then do let cryCmd = (P.shell (exe ++ " --interactive-batch " ++ inFile ++ " -e"))
               (cryEC, cryOut, _) <- P.readCreateProcessWithExitCode cryCmd ""
 
 
@@ -318,7 +318,7 @@ main = do
                     fmap (trim . lineText) $ toList $ rdReplout rd
                   outExpectedFileNameTemplate = "out-expected.icry"
                   outFileNameTemplate = "out.icry"
-                  cryCmd = (P.shell (exe ++ " -b " ++ inFile))
+                  cryCmd = (P.shell (exe ++ " --interactive-batch " ++ inFile))
               outExpectedFile <- writeTempFile dir outExpectedFileNameTemplate outExpectedText
               outFile <- emptyTempFile dir outFileNameTemplate
 
@@ -349,7 +349,7 @@ main = do
                   putStrLn $ "  (replin lines " ++
                     show lnReplinStart ++ "-" ++ show lnReplinEnd ++
                     ", replout lines " ++ show lnReploutStart ++ "-" ++
-                    show lnReploutEnd
+                    show lnReploutEnd ++ ")."
                   putStrLn $ "Diff output:"
                   putStr diffOut
 

cryptol/Main.hs

@@ -26,7 +26,6 @@ import Cryptol.Utils.PP
 import Cryptol.Version (displayVersion)
 
 import Control.Monad (when)
-import Data.Maybe (isJust)
 import GHC.IO.Encoding (setLocaleEncoding, utf8)
 import System.Console.GetOpt
     (OptDescr(..),ArgOrder(..),ArgDescr(..),getOpt,usageInfo)
@@ -47,7 +46,7 @@ data Options = Options
   { optLoad            :: [FilePath]
   , optVersion         :: Bool
   , optHelp            :: Bool
-  , optBatch           :: Maybe FilePath
+  , optBatch           :: ReplMode
   , optCallStacks      :: Bool
   , optCommands        :: [String]
   , optColorMode       :: ColorMode
@@ -62,7 +61,7 @@ defaultOptions  = Options
   { optLoad            = []
   , optVersion         = False
   , optHelp            = False
-  , optBatch           = Nothing
+  , optBatch           = InteractiveRepl
   , optCallStacks      = True
   , optCommands        = []
   , optColorMode       = AutoColor
@@ -77,6 +76,9 @@ options  =
   [ Option "b" ["batch"] (ReqArg setBatchScript "FILE")
     "run the script provided and exit"
 
+  , Option "" ["interactive-batch"] (ReqArg setInteractiveBatchScript "FILE")
+    "run the script provided and exit, but behave as if running an interactive session"
+
   , Option "e" ["stop-on-error"] (NoArg setStopOnError)
     "stop script execution as soon as an error occurs."
 
@@ -129,7 +131,11 @@ setStopOnError = modify $ \opts -> opts { optStopOnError = True }
 
 -- | Set a batch script to be run.
 setBatchScript :: String -> OptParser Options
-setBatchScript path = modify $ \ opts -> opts { optBatch = Just path }
+setBatchScript path = modify $ \ opts -> opts { optBatch = Batch path }
+
+-- | Set an interactive batch script
+setInteractiveBatchScript :: String -> OptParser Options
+setInteractiveBatchScript path = modify $ \ opts -> opts { optBatch = InteractiveBatch path }
 
 -- | Set the color mode of the terminal output.
 setColorMode :: String -> OptParser Options
@@ -235,9 +241,9 @@ setupCmdScript opts =
       (path, h) <- openTempFile tmpdir "cmds.icry"
       hPutStr h (unlines cmds)
       hClose h
-      when (isJust (optBatch opts)) $
+      when (optBatch opts /= InteractiveRepl) $
         putStrLn "[warning] --command argument specified; ignoring batch file"
-      return (opts { optBatch = Just path }, Just path)
+      return (opts { optBatch = InteractiveBatch path }, Just path)
 
 setupREPL :: Options -> REPL ()
 setupREPL opts = do
@@ -271,9 +277,10 @@ setupREPL opts = do
   setUpdateREPLTitle (shouldSetREPLTitle >>= \b -> when b setREPLTitle)
   updateREPLTitle
   case optBatch opts of
-    Nothing -> return ()
     -- add the directory containing the batch file to the module search path
-    Just file -> prependSearchPath [ takeDirectory file ]
+    Batch file -> prependSearchPath [ takeDirectory file ]
+    _ -> return ()
+
   case optLoad opts of
     []  -> loadPrelude `REPL.catch` \x -> io $ print $ pp x
     [l] -> loadCmd l `REPL.catch` \x -> do

cryptol/REPL/Haskeline.hs

@@ -29,7 +29,6 @@ import           Control.Monad.Trans.Control
 import           Data.Char (isAlphaNum, isSpace)
 import           Data.Function (on)
 import           Data.List (isPrefixOf,nub,sortBy,sort)
-import           Data.Maybe(isJust)
 import qualified Data.Set as Set
 import qualified Data.Text as T (unpack)
 import           System.Console.ANSI (setTitle, hSupportsANSI)
@@ -44,16 +43,25 @@ import           Prelude ()
 import           Prelude.Compat
 
 
+data ReplMode
+  = InteractiveRepl -- ^ Interactive terminal session
+  | Batch FilePath  -- ^ Execute from a batch file
+  | InteractiveBatch FilePath
+     -- ^ Execute from a batch file, but behave as though
+     --   lines are entered in an interactive session.
+ deriving (Show, Eq)
+
 -- | One REPL invocation, either from a file or from the terminal.
-crySession :: Maybe FilePath -> Bool -> REPL CommandExitCode
-crySession mbBatch stopOnError =
+crySession :: ReplMode -> Bool -> REPL CommandExitCode
+crySession replMode stopOnError =
   do settings <- io (setHistoryFile (replSettings isBatch))
      let act = runInputTBehavior behavior settings (withInterrupt (loop 1))
      if isBatch then asBatch act else act
   where
-  (isBatch,behavior) = case mbBatch of
-    Nothing   -> (False,defaultBehavior)
-    Just path -> (True,useFile path)
+  (isBatch,behavior) = case replMode of
+    InteractiveRepl       -> (False, defaultBehavior)
+    Batch path            -> (True,  useFile path)
+    InteractiveBatch path -> (False, useFile path)
 
   loop :: Int -> InputT REPL CommandExitCode
   loop lineNum =
@@ -67,12 +75,18 @@ crySession mbBatch stopOnError =
            | all (all isSpace) ls -> loop (lineNum + length ls)
            | otherwise            -> doCommand lineNum ls
 
+  run lineNum cmd =
+    case replMode of
+      InteractiveRepl    -> runCommand lineNum Nothing cmd
+      InteractiveBatch _ -> runCommand lineNum Nothing cmd
+      Batch path         -> runCommand lineNum (Just path) cmd
+
   doCommand lineNum txt =
     case parseCommand findCommandExact (unlines txt) of
       Nothing | isBatch && stopOnError -> return CommandError
               | otherwise -> loop (lineNum + length txt)  -- say somtething?
       Just cmd -> join $ MTL.lift $
-        do status <- handleInterrupt (handleCtrlC CommandError) (runCommand lineNum mbBatch cmd)
+        do status <- handleInterrupt (handleCtrlC CommandError) (run lineNum cmd)
            case status of
              CommandError | isBatch && stopOnError -> return (return status)
              _ -> do goOn <- shouldContinue
@@ -106,25 +120,32 @@ loadCryRC cryrc =
        let file = dir </> ".cryptolrc"
        present <- io (doesFileExist file)
        if present
-         then crySession (Just file) True
+         then crySession (Batch file) True
          else check others
 
   loadMany []       = return CommandOk
-  loadMany (f : fs) = do status <- crySession (Just f) True
+  loadMany (f : fs) = do status <- crySession (Batch f) True
                          case status of
                            CommandOk -> loadMany fs
                            _         -> return status
 
 -- | Haskeline-specific repl implementation.
-repl :: Cryptolrc -> Maybe FilePath -> Bool -> Bool -> REPL () -> IO CommandExitCode
-repl cryrc mbBatch callStacks stopOnError begin =
-  runREPL (isJust mbBatch) callStacks stdoutLogger $
-  do status <- loadCryRC cryrc
-     case status of
-       CommandOk -> begin >> crySession mbBatch stopOnError
-       _         -> return status
-
-
+repl :: Cryptolrc -> ReplMode -> Bool -> Bool -> REPL () -> IO CommandExitCode
+repl cryrc replMode callStacks stopOnError begin =
+  runREPL isBatch callStacks stdoutLogger replAction
+
+ where
+  -- this flag is used to suppress the logo and prompts
+  isBatch = case replMode of
+              InteractiveRepl -> False
+              Batch _ -> True
+              InteractiveBatch _ -> True
+
+  replAction =
+    do status <- loadCryRC cryrc
+       case status of
+         CommandOk -> begin >> crySession replMode stopOnError
+         _         -> return status
 
 -- | Try to set the history file.
 setHistoryFile :: Settings REPL -> IO (Settings REPL)

docs/ProgrammingCryptol/crashCourse/CrashCourse.tex

@@ -97,7 +97,7 @@ \section{Basic data types}
 \begin{small}
 \begin{reploutVerb}
   True
-  [error] at <interactive>:1:1--1:6 Value not in scope: false
+  [error] at <interactive>:2:1--2:6 Value not in scope: false
   False
   0x4
   True
@@ -301,13 +301,17 @@ \section{Basic data types}
   5
   1
   division by 0
+  -- Backtrace --
+  Cryptol::recip called at <interactive>:4:1--4:6
   division by 0
-  [error] at <interactive>:1:1--1:20:
+  -- Backtrace --
+  Cryptol::recip called at <interactive>:5:1--5:6
+  [error] at <interactive>:6:1--6:20:
   • Unsolvable constraint:
       prime 8
       arising from
       use of expression recip
-      at <interactive>:1:2--1:7
+      at <interactive>:6:2--6:7
 \end{reploutVerb}
 \end{Answer}
 
@@ -532,7 +536,7 @@ \section{Floating Point Numbers}
       Expected type: Bit
       Inferred type: [1]
       When checking type of sequence member
-  [error] at <interactive>:1:13--1:19:
+  [error] at <interactive>:2:13--2:19:
     Type mismatch:
       Expected type: 3
       Inferred type: 2
@@ -763,15 +767,22 @@ \subsection{Appending and indexing}
   0
   5
   invalid sequence index: 10
+  -- Backtrace --
+  (Cryptol::@) called at <interactive>:6:1--6:22
   [3, 4]
   []
   invalid sequence index: 12
+   -- Backtrace --
+  (Cryptol::@) called at Cryptol:806:14--806:20
+  (Cryptol::@@) called at <interactive>:9:1--9:28
   [9, 8, 7, 6, 5, 4, 3, 2, 1, 0]
   9
   6
   [6, 3]
   [9, 8, 7, 6, 5, 4, 3, 2, 1, 0]
   invalid sequence index: 12
+  -- Backtrace --
+  (Cryptol::!) called at <interactive>:15:1--15:22
 \end{reploutVerb}
 \end{Answer}
 
@@ -1507,9 +1518,16 @@ \section{Characters and strings}
 \end{Exercise}
 \begin{Answer}\ansref{ex:arith:4}
   \hidereplout|division by 0|
+  \hidereplout|-- Backtrace --|
+  \hidereplout|(Cryptol::/) called at <interactive>:1:1--1:16|
   \hidereplout|division by 0|
+  \hidereplout|-- Backtrace --|
+  \hidereplout|(Cryptol::%) called at <interactive>:2:1--2:16|
   \hidereplout|15|
   \hidereplout|division by 0|
+  \hidereplout|-- Backtrace --|
+  \hidereplout|(Cryptol::/) called at <interactive>:4:41--4:44|
+  \hidereplout|(Cryptol::+) called at <interactive>:4:1--4:45|
   \hidereplout|Showing a specific instance of polymorphic result:|
   \hidereplout|* Using '5' for type argument 'n' of 'Cryptol::lg2'|
   \hidereplout|0x03|

docs/README.md

@@ -54,3 +54,10 @@ following commands:
   `\replout` command. When we don't record any expected output, the
   actual REPL output is not checked, but is instead simply issued to
   the REPL to ensure no errors are raised.
+
+Other notes:
+
+* I tried to do reasonable things with % comments, but I can't guarantee it will
+  work as expected in all cases (particularly with the inline commands). It's
+  probably best to avoid using LaTeX comments that are on the same line as any
+  of the above commands.