Initial implementation of :check-docstrings

CHANGES.md

@@ -14,6 +14,16 @@
 * 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.
+
+* New REPL command :check-docstrings extracts code-blocks from docstring
+  comments from a module. Code blocks can be delimited with three-or-more
+  backticks. "repl" and unlabeled code blocks are evaluated in a local
+  REPL context and checked to pass.
+
 # 3.1.0 -- 2024-02-05
 
 ## Language changes

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

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

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''

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."

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)

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

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

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