Initial implementation of :check-docstrings (#1682)

* Update all commands to track their results * Implement REPL :check-docstrings command This command checks that all of the unlabeled and "repl" labeled codeblocks in docstrings can successfully evaluate as REPL commands. Cryptol will now indicate exit failure if any of REPL commands fail, making it possible to use in automated testing. :check-docstrings internal implementation is set up to track results of subcommands in support for integration into a remote server API endpoint. * Implement :focus * Add some :check-docstring test cases * Update changelog * Update CrashCourse.tex now that more commands are checked * Require repl and convert \r\n to \n in lexer
GaloisInc · Jul 18, 2024 · 4ca0629 · 4ca0629
1 parent f5fa503
commit 4ca0629
Show file tree

Hide file tree

Showing 35 changed files with 942 additions and 275 deletions.
diff --git a/CHANGES.md b/CHANGES.md
@@ -5,7 +5,6 @@
 * Add implicit imports for non-anonymous modules defined by functor
   instantiation.   For details, see #1691.
 
-
 ## Bug fixes
 
 * Fix #1685, which caused Cryptol to panic when given a local definition without
@@ -14,6 +13,31 @@
 * Fix #1593 and #1693, two related bugs that would cause Cryptol to panic when
   checking ill-typed constraint guards for exhaustivity.
 
+## New features
+
+* New REPL command :focus enables specifying a submodule scope for evaluating
+  expressions.
+
+  ```repl
+  :focus submodule M
+  :browse
+  ```
+
+* New REPL command :check-docstrings extracts code-blocks from docstring
+  comments from a module. Code blocks can be delimited with three-or-more
+  backticks using the language "repl". Code blocks are evaluated in a local
+  REPL context and checked to pass.
+
+  ````cryptol
+  /**
+   * ```repl
+   * :exhaust f
+   * ```
+   */
+  f : [8] -> Bool
+  f x = x + 1 - 1 == x
+  ````
+
 # 3.1.0 -- 2024-02-05
 
 ## Language changes

diff --git a/bench/Main.hs b/bench/Main.hs
@@ -138,7 +138,7 @@ ceval cd name path expr =
         menv <- M.initialModuleEnv
         (eres, _) <-  M.runModuleM (evOpts,menv) $ withLib $ do
           m <- M.loadModuleByPath path
-          M.setFocusedModule (T.mName m)
+          M.setFocusedModule (P.ImpTop (T.mName m))
           let Right pexpr = P.parseExpr expr
           (_, texpr, _) <- M.checkExpr pexpr
           return texpr
@@ -160,7 +160,7 @@ seval cd name path expr =
         menv <- M.initialModuleEnv
         (eres, _) <-  M.runModuleM (evOpts,menv) $ withLib $ do
           m <- M.loadModuleByPath path
-          M.setFocusedModule (T.mName m)
+          M.setFocusedModule (P.ImpTop (T.mName m))
           let Right pexpr = P.parseExpr expr
           (_, texpr, _) <- M.checkExpr pexpr
           return texpr

diff --git a/cry b/cry
@@ -4,7 +4,7 @@ set -e
 
 BIN=bin
 
-QUICKTESTS="tests/issues tests/modsys tests/mono-binds tests/parser tests/regression tests/renamer"
+QUICKTESTS="tests/docstrings tests/issues tests/modsys tests/mono-binds tests/parser tests/regression tests/renamer"
 
 function setup_external_tools() {
   [[ -x "$BIN/test-runner" || -x "$BIN/test-runner.exe" ]] && return

diff --git a/cryptol-remote-api/cryptol-eval-server/Main.hs b/cryptol-remote-api/cryptol-eval-server/Main.hs
@@ -26,7 +26,7 @@ import CryptolServer.Interrupt
     ( interruptServer, interruptServerDescr )
 import Cryptol.ModuleSystem (ModuleInput(..), loadModuleByPath, loadModuleByName)
 import Cryptol.ModuleSystem.Monad (runModuleM, setFocusedModule)
-import Cryptol.TypeCheck.AST (tcTopEntitytName)
+import Cryptol.TypeCheck.AST (tcTopEntitytName, ImpName(..))
 import Cryptol.Utils.Ident (ModName, modNameToText, textToModName, preludeName)
 import Cryptol.Utils.Logger (quietLogger)
 
@@ -77,7 +77,7 @@ main = customMain initMod initMod initMod initMod description buildApp
               case res of
                 Left err -> die err
                 Right (m, menv') ->
-                  do res' <- fst <$> runModuleM minp{ minpModuleEnv = menv' } (setFocusedModule (tcTopEntitytName (snd m)))
+                  do res' <- fst <$> runModuleM minp{ minpModuleEnv = menv' } (setFocusedModule (ImpTop (tcTopEntitytName (snd m))))
                      case res' of
                        Left err -> die err
                        Right (_, menv'') -> pure menv''

diff --git a/cryptol/Main.hs b/cryptol/Main.hs
@@ -13,7 +13,7 @@ module Main where
 
 import OptParser
 
-import Cryptol.REPL.Command (loadCmd,loadPrelude,CommandExitCode(..))
+import Cryptol.REPL.Command (loadCmd,loadPrelude,CommandResult(..))
 import Cryptol.REPL.Monad (REPL,updateREPLTitle,setUpdateREPLTitle,
                    io,prependSearchPath,setSearchPath,parseSearchPath)
 import qualified Cryptol.REPL.Monad as REPL
@@ -25,7 +25,7 @@ import REPL.Logo
 import Cryptol.Utils.PP
 import Cryptol.Version (displayVersion)
 
-import Control.Monad (when)
+import Control.Monad (when, void)
 import GHC.IO.Encoding (setLocaleEncoding, utf8)
 import System.Console.GetOpt
     (OptDescr(..),ArgOrder(..),ArgDescr(..),getOpt,usageInfo)
@@ -234,9 +234,9 @@ main  = do
             Nothing -> return ()
             Just cmdFile -> removeFile cmdFile
 
-          case status of
-            CommandError -> exitFailure
-            CommandOk    -> exitSuccess
+          if crSuccess status
+            then exitSuccess
+            else exitFailure
 
 setupCmdScript :: Options -> IO (Options, Maybe FilePath)
 setupCmdScript opts =
@@ -283,7 +283,7 @@ setupREPL opts = do
 
   case optLoad opts of
     []  -> loadPrelude `REPL.catch` \x -> io $ print $ pp x
-    [l] -> loadCmd l `REPL.catch` \x -> do
+    [l] -> void (loadCmd l) `REPL.catch` \x -> do
              io $ print $ pp x
              -- If the requested file fails to load, load the prelude instead...
              loadPrelude `REPL.catch` \y -> do
@@ -292,7 +292,7 @@ setupREPL opts = do
              -- we tried, instead of the Prelude
              REPL.setEditPath l
              REPL.setLoadedMod REPL.LoadedModule
-               { REPL.lName = Nothing
+               { REPL.lFocus = Nothing
                , REPL.lPath = InFile l
                }
     _   -> io $ putStrLn "Only one file may be loaded at the command line."
diff --git a/cryptol/REPL/Haskeline.hs b/cryptol/REPL/Haskeline.hs
@@ -9,6 +9,7 @@
 {-# LANGUAGE CPP #-}
 {-# LANGUAGE MultiWayIf #-}
 {-# LANGUAGE PatternGuards #-}
+{-# LANGUAGE BangPatterns #-}
 {-# OPTIONS_GHC -fno-warn-orphans #-}
 
 module REPL.Haskeline where
@@ -52,45 +53,45 @@ data ReplMode
  deriving (Show, Eq)
 
 -- | One REPL invocation, either from a file or from the terminal.
-crySession :: ReplMode -> Bool -> REPL CommandExitCode
+crySession :: ReplMode -> Bool -> REPL CommandResult
 crySession replMode stopOnError =
   do settings <- io (setHistoryFile (replSettings isBatch))
-     let act = runInputTBehavior behavior settings (withInterrupt (loop 1))
+     let act = runInputTBehavior behavior settings (withInterrupt (loop True 1))
      if isBatch then asBatch act else act
   where
   (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 =
+  loop :: Bool -> Int -> InputT REPL CommandResult
+  loop !success !lineNum =
     do ln <- getInputLines =<< MTL.lift getPrompt
        case ln of
-         NoMoreLines -> return CommandOk
+         NoMoreLines -> return emptyCommandResult { crSuccess = success }
          Interrupted
-           | isBatch && stopOnError -> return CommandError
-           | otherwise -> loop lineNum
+           | isBatch && stopOnError -> return emptyCommandResult { crSuccess = False }
+           | otherwise -> loop success lineNum
          NextLine ls
-           | all (all isSpace) ls -> loop (lineNum + length ls)
-           | otherwise            -> doCommand lineNum ls
+           | all (all isSpace) ls -> loop success (lineNum + length ls)
+           | otherwise            -> doCommand success 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 =
+  doCommand success lineNum txt =
     case parseCommand findCommandExact (unlines txt) of
-      Nothing | isBatch && stopOnError -> return CommandError
-              | otherwise -> loop (lineNum + length txt)  -- say somtething?
+      Nothing | isBatch && stopOnError -> return emptyCommandResult { crSuccess = False }
+              | otherwise -> loop False (lineNum + length txt)  -- say somtething?
       Just cmd -> join $ MTL.lift $
-        do status <- handleInterrupt (handleCtrlC CommandError) (run lineNum cmd)
-           case status of
-             CommandError | isBatch && stopOnError -> return (return status)
+        do status <- handleInterrupt (handleCtrlC emptyCommandResult { crSuccess = False }) (run lineNum cmd)
+           case crSuccess status of
+             False | isBatch && stopOnError -> return (return status)
              _ -> do goOn <- shouldContinue
-                     return (if goOn then loop (lineNum + length txt) else return status)
+                     return (if goOn then loop (crSuccess status && success) (lineNum + length txt) else return status)
 
 
 data NextLine = NextLine [String] | NoMoreLines | Interrupted
@@ -107,14 +108,14 @@ getInputLines = handleInterrupt (MTL.lift (handleCtrlC Interrupted)) . loop []
            | not (null l) && last l == '\\' -> loop (init l : ls) newPropmpt
            | otherwise -> return $ NextLine $ reverse $ l : ls
 
-loadCryRC :: Cryptolrc -> REPL CommandExitCode
+loadCryRC :: Cryptolrc -> REPL CommandResult
 loadCryRC cryrc =
   case cryrc of
-    CryrcDisabled   -> return CommandOk
+    CryrcDisabled   -> return emptyCommandResult
     CryrcDefault    -> check [ getCurrentDirectory, getHomeDirectory ]
     CryrcFiles opts -> loadMany opts
   where
-  check [] = return CommandOk
+  check [] = return emptyCommandResult
   check (place : others) =
     do dir <- io place
        let file = dir </> ".cryptolrc"
@@ -123,14 +124,14 @@ loadCryRC cryrc =
          then crySession (Batch file) True
          else check others
 
-  loadMany []       = return CommandOk
+  loadMany []       = return emptyCommandResult
   loadMany (f : fs) = do status <- crySession (Batch f) True
-                         case status of
-                           CommandOk -> loadMany fs
-                           _         -> return status
+                         if crSuccess status
+                           then loadMany fs
+                           else return status
 
 -- | Haskeline-specific repl implementation.
-repl :: Cryptolrc -> ReplMode -> Bool -> Bool -> REPL () -> IO CommandExitCode
+repl :: Cryptolrc -> ReplMode -> Bool -> Bool -> REPL () -> IO CommandResult
 repl cryrc replMode callStacks stopOnError begin =
   runREPL isBatch callStacks stdoutLogger replAction
 
@@ -143,9 +144,9 @@ repl cryrc replMode callStacks stopOnError begin =
 
   replAction =
     do status <- loadCryRC cryrc
-       case status of
-         CommandOk -> begin >> crySession replMode stopOnError
-         _         -> return status
+       if crSuccess status
+         then begin >> crySession replMode stopOnError
+         else return status
 
 -- | Try to set the history file.
 setHistoryFile :: Settings REPL -> IO (Settings REPL)

diff --git a/docs/ProgrammingCryptol/crashCourse/CrashCourse.tex b/docs/ProgrammingCryptol/crashCourse/CrashCourse.tex
@@ -1094,9 +1094,7 @@ \subsection{Manipulating sequences}
   comprehension fits the bill:\indComp
 \restartrepl
 \begin{replinVerb}
-  [ split level1 : [4][10][8]
-  | level1 <- split ([1 .. 120] : [120][8]) : [3][40][8]
-  ]
+  [ split level1 : [4][10][8] | level1 <- split ([1 .. 120] : [120][8]) : [3][40][8] ]
 \end{replinVerb}
 (Note again that you can enter the above in the command line all in
 one line, or by putting the line continuation character
@@ -2076,14 +2074,15 @@ \subsection{Polymorphic types}\indPolymorphism
 \texttt{a=[4]}. The third expression does not type-check. Cryptol
 tells us:
 \restartrepl
-\begin{replinVerb}
+\begin{replPrompt}
   Cryptol> split`{3} [1..10] : [3][2][8]
   [error] at <interactive>:1:11--1:18:
     Type mismatch:
       Expected type: 6
       Inferred type: 10
+      Context: [ERROR] _
       When checking type of function argument
-\end{replinVerb}
+\end{replPrompt}
 In this case, we are telling Cryptol that \texttt{parts = 3},
 \texttt{each = 2}, and \texttt{a = [8]} by providing the explicit type
 signature.\indSignature Using this information, Cryptol must ensure

diff --git a/src/Cryptol/ModuleSystem.hs b/src/Cryptol/ModuleSystem.hs
@@ -30,6 +30,9 @@ module Cryptol.ModuleSystem (
   , getPrimMap
   , renameVar
   , renameType
+  , setFocusedModule
+  , Base.renameImpNameInCurrentEnv
+  , impNameTopModule
 
     -- * Interfaces
   , Iface, IfaceG(..), IfaceDecls(..), T.genIface, IfaceDecl(..)
@@ -45,7 +48,7 @@ import qualified Cryptol.Eval.Concrete as Concrete
 import           Cryptol.ModuleSystem.Env
 import           Cryptol.ModuleSystem.Interface
 import           Cryptol.ModuleSystem.Monad
-import           Cryptol.ModuleSystem.Name (Name,PrimMap)
+import           Cryptol.ModuleSystem.Name (Name,PrimMap,nameTopModule)
 import qualified Cryptol.ModuleSystem.Renamer as R
 import qualified Cryptol.ModuleSystem.Base as Base
 import qualified Cryptol.Parser.AST        as P
@@ -76,7 +79,7 @@ loadModuleByPath path minp = do
   runModuleM minp{ minpModuleEnv = moduleEnv' } $ do
     unloadModule ((InFile path ==) . lmFilePath)
     m <- Base.loadModuleByPath True path
-    setFocusedModule (T.tcTopEntitytName m)
+    setFocusedModule (P.ImpTop (T.tcTopEntitytName m))
     return (InFile path,m)
 
 -- | Load the given parsed module.
@@ -86,7 +89,7 @@ loadModuleByName n minp = do
   runModuleM minp{ minpModuleEnv = moduleEnv' } $ do
     unloadModule ((n ==) . lmName)
     (path,m') <- Base.loadModuleFrom False (FromModule n)
-    setFocusedModule (T.tcTopEntitytName m')
+    setFocusedModule (P.ImpTop (T.tcTopEntitytName m'))
     return (path,m')
 
 -- | Parse and typecheck a module, but don't evaluate or change the environment.
@@ -155,3 +158,11 @@ getFileDependencies f env = runModuleM env (Base.findDepsOf (InFile f))
 getModuleDependencies :: M.ModName -> ModuleCmd (ModulePath, FileInfo)
 getModuleDependencies m env = runModuleM env (Base.findDepsOfModule m)
 
+--------------------------------------------------------------------------------
+-- ImpName utilities
+
+impNameTopModule :: P.ImpName Name -> M.ModName
+impNameTopModule impName =
+    case impName of
+      P.ImpTop m -> m
+      P.ImpNested n -> nameTopModule n
diff --git a/src/Cryptol/ModuleSystem/Base.hs b/src/Cryptol/ModuleSystem/Base.hs
@@ -28,6 +28,7 @@ import qualified Data.List.NonEmpty as NE
 import Data.List.NonEmpty (NonEmpty(..))
 import Data.Function(on)
 import Data.Monoid ((<>),Endo(..), Any(..))
+import qualified Data.Text as T
 import Data.Text.Encoding (decodeUtf8')
 import System.Directory (doesFileExist, canonicalizePath)
 import System.FilePath ( addExtension
@@ -81,7 +82,7 @@ import qualified Cryptol.Backend.FFI.Error as FFI
 
 import Cryptol.Utils.Ident ( preludeName, floatName, arrayName, suiteBName, primeECName
                            , preludeReferenceName, interactiveName, modNameChunks
-                           , modNameToNormalModName )
+                           , modNameToNormalModName, Namespace(NSModule) )
 import Cryptol.Utils.PP (pretty, pp, hang, vcat, ($$), (<+>), (<.>), colon)
 import Cryptol.Utils.Panic (panic)
 import Cryptol.Utils.Logger(logPutStrLn, logPrint)
@@ -118,6 +119,21 @@ rename modName env m = do
 renameModule :: P.Module PName -> ModuleM R.RenamedModule
 renameModule m = rename (thing (mName m)) mempty (R.renameModule m)
 
+renameImpNameInCurrentEnv :: P.ImpName PName -> ModuleM (P.ImpName Name)
+renameImpNameInCurrentEnv (P.ImpTop top) =
+ do ok <- isLoaded top
+    if ok then
+      pure (P.ImpTop top)
+    else
+      fail ("Top-level module not loaded: " ++ show (pp top))
+renameImpNameInCurrentEnv (P.ImpNested pname) =
+ do env <- getFocusedEnv
+    case R.lookupListNS NSModule pname (mctxNames env) of
+      [] -> do
+        fail ("Undefined submodule name: " ++ show (pp pname))
+      _:_:_ -> do
+        fail ("Ambiguous submodule name: " ++ show (pp pname))
+      [name] -> pure (P.ImpNested name)
 
 -- NoPat -----------------------------------------------------------------------
 
@@ -164,7 +180,7 @@ parseModule path = do
                        , "Exception: " ++ show exn ]
 
   txt <- case decodeUtf8' bytes of
-    Right txt -> return txt
+    Right txt -> return $! (T.replace "\r\n" "\n" txt)
     Left e    -> badUtf8 path e
 
   let cfg = P.defaultConfig