From ad5af8b4625097bceee50ca90a1c097b925d8429 Mon Sep 17 00:00:00 2001 From: Eric Mertens Date: Thu, 6 Jun 2024 10:57:53 -0700 Subject: [PATCH 01/12] Update all commands to track their results --- cryptol/Main.hs | 12 +- cryptol/REPL/Haskeline.hs | 38 ++-- src/Cryptol/REPL/Command.hs | 396 +++++++++++++++++++++++------------- src/Cryptol/REPL/Help.hs | 7 +- src/Cryptol/REPL/Monad.hs | 20 +- 5 files changed, 290 insertions(+), 183 deletions(-) diff --git a/cryptol/Main.hs b/cryptol/Main.hs index 253c84937..425cb06ba 100644 --- 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 diff --git a/cryptol/REPL/Haskeline.hs b/cryptol/REPL/Haskeline.hs index 0ad7b00a8..0a30b7e07 100644 --- a/cryptol/REPL/Haskeline.hs +++ b/cryptol/REPL/Haskeline.hs @@ -52,7 +52,7 @@ 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)) @@ -63,13 +63,13 @@ crySession replMode stopOnError = Batch path -> (True, useFile path) InteractiveBatch path -> (False, useFile path) - loop :: Int -> InputT REPL CommandExitCode + loop :: Int -> InputT REPL CommandResult loop lineNum = do ln <- getInputLines =<< MTL.lift getPrompt case ln of - NoMoreLines -> return CommandOk + NoMoreLines -> return emptyCommandResult Interrupted - | isBatch && stopOnError -> return CommandError + | isBatch && stopOnError -> return emptyCommandResult { crSuccess = False } | otherwise -> loop lineNum NextLine ls | all (all isSpace) ls -> loop (lineNum + length ls) @@ -83,12 +83,12 @@ crySession replMode stopOnError = doCommand lineNum txt = case parseCommand findCommandExact (unlines txt) of - Nothing | isBatch && stopOnError -> return CommandError + Nothing | isBatch && stopOnError -> return emptyCommandResult { crSuccess = False } | otherwise -> loop (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) @@ -107,14 +107,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 +123,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 +143,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/src/Cryptol/REPL/Command.hs b/src/Cryptol/REPL/Command.hs index f8489f635..17d713392 100644 --- a/src/Cryptol/REPL/Command.hs +++ b/src/Cryptol/REPL/Command.hs @@ -18,7 +18,7 @@ {-# OPTIONS_GHC -Wno-incomplete-uni-patterns #-} module Cryptol.REPL.Command ( -- * Commands - Command(..), CommandDescr(..), CommandBody(..), CommandExitCode(..) + Command(..), CommandDescr(..), CommandBody(..), CommandResult(..) , parseCommand , runCommand , splitCommand @@ -26,6 +26,7 @@ module Cryptol.REPL.Command ( , findCommandExact , findNbCommand , commandList + , emptyCommandResult , moduleCmd, loadCmd, loadPrelude, setOptionCmd @@ -153,7 +154,7 @@ import qualified Data.SBV.Internals as SBV (showTDiff) -- | Commands. data Command - = Command (Int -> Maybe FilePath -> REPL ()) -- ^ Successfully parsed command + = Command (Int -> Maybe FilePath -> REPL CommandResult) -- ^ Successfully parsed command | Ambiguous String [String] -- ^ Ambiguous command, list of conflicting -- commands | Unknown String -- ^ The unknown command @@ -177,21 +178,29 @@ instance Ord CommandDescr where compare = compare `on` cNames data CommandBody - = ExprArg (String -> (Int,Int) -> Maybe FilePath -> REPL ()) - | FileExprArg (FilePath -> String -> (Int,Int) -> Maybe FilePath -> REPL ()) - | DeclsArg (String -> REPL ()) - | ExprTypeArg (String -> REPL ()) - | ModNameArg (String -> REPL ()) - | FilenameArg (FilePath -> REPL ()) - | OptionArg (String -> REPL ()) - | ShellArg (String -> REPL ()) - | HelpArg (String -> REPL ()) - | NoArg (REPL ()) - - -data CommandExitCode = CommandOk - | CommandError -- XXX: More? + = 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 relevan commands + , crSuccess :: Bool -- ^ indicator that command successfully performed its task + } +emptyCommandResult :: CommandResult +emptyCommandResult = CommandResult + { crType = Nothing + , crValue = Nothing + , crSuccess = True + } -- | REPL command parsing. commands :: CommandMap @@ -260,7 +269,7 @@ nbCommandList = , CommandDescr [ ":ast" ] ["EXPR"] (ExprArg astOfCmd) "Print out the pre-typechecked AST of a given term." "" - , CommandDescr [ ":extract-coq" ] [] (NoArg allTerms) + , 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) @@ -361,23 +370,27 @@ genHelp cs = map cmdHelp cs -- Command Evaluation ---------------------------------------------------------- -- | Run a command. -runCommand :: Int -> Maybe FilePath -> Command -> REPL CommandExitCode +runCommand :: Int -> Maybe FilePath -> Command -> REPL CommandResult runCommand lineNum mbBatch c = case c of - Command cmd -> (cmd lineNum mbBatch >> return CommandOk) `Cryptol.REPL.Monad.catch` handler + Command cmd -> cmd lineNum mbBatch `Cryptol.REPL.Monad.catch` handler where - handler re = rPutStrLn "" >> rPrint (pp re) >> return CommandError + handler re = do + rPutStrLn "" + rPrint (pp re) + return emptyCommandResult { crSuccess = False } - Unknown cmd -> do rPutStrLn ("Unknown command: " ++ cmd) - return CommandError + 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 CommandError + return emptyCommandResult { crSuccess = False } -evalCmd :: String -> Int -> Maybe FilePath -> REPL () +evalCmd :: String -> Int -> Maybe FilePath -> REPL CommandResult evalCmd str lineNum mbBatch = do ri <- replParseInput str lineNum mbBatch case ri of @@ -393,14 +406,19 @@ evalCmd str lineNum mbBatch = do --out <- io $ rethrowEvalError -- $ return $!! show $ pp $ E.WithBase ppOpts val - rPutStrLn (show valDoc) + 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 () + pure emptyCommandResult printCounterexample :: CounterExampleType -> Doc -> [Concrete.Value] -> REPL () printCounterexample cexTy exprDoc vs = @@ -421,7 +439,7 @@ printSatisfyingModel exprDoc vs = rPrint $ nest 2 (sep ([exprDoc] ++ docs ++ [text "= True"])) -dumpTestsCmd :: FilePath -> String -> (Int,Int) -> Maybe FilePath -> REPL () +dumpTestsCmd :: FilePath -> String -> (Int,Int) -> Maybe FilePath -> REPL CommandResult dumpTestsCmd outFile str pos fnm = do expr <- replParseExpr str pos fnm (val, ty) <- replEvalExpr expr @@ -439,11 +457,12 @@ dumpTestsCmd outFile str pos fnm = 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") - io $ writeFile outFile (concat out) `X.catch` handler - where - handler :: X.SomeException -> IO () - handler e = putStrLn (X.displayException e) - + writeResult <- io $ X.try (writeFile outFile (concat 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) @@ -452,27 +471,34 @@ 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 () +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 rPutStrLn "There are no properties in scope." - else forM_ xs $ \(x,d) -> + then do + rPutStrLn "There are no properties in scope." + 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 = M.ifDeclSig d nd <- M.mctxNameDisp <$> getFocusedEnv let doc = fixNameDisp nd (pp texpr) - void (qcExpr qcMode doc texpr schema) + 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 - void (qcExpr qcMode doc texpr schema) + testReport <- qcExpr qcMode doc texpr schema + pure emptyCommandResult { crSuccess = isPass (reportResult testReport) } data TestReport = TestReport @@ -687,7 +713,7 @@ expectedCoverage testNum sz = proportion = negate (expm1 (numD * log1p (negate (recip szD)))) -satCmd, proveCmd :: String -> (Int,Int) -> Maybe FilePath -> REPL () +satCmd, proveCmd :: String -> (Int,Int) -> Maybe FilePath -> REPL CommandResult satCmd = cmdProveSat True proveCmd = cmdProveSat False @@ -709,7 +735,7 @@ rethrowErrorCall m = REPL (\r -> unREPL m r `X.catches` hs) ] -- | Attempts to prove the given term is safe for all inputs -safeCmd :: String -> (Int,Int) -> Maybe FilePath -> REPL () +safeCmd :: String -> (Int,Int) -> Maybe FilePath -> REPL CommandResult safeCmd str pos fnm = do proverName <- getKnownUser "prover" fileName <- getKnownUser "smtFile" @@ -722,16 +748,21 @@ safeCmd str pos fnm = do (_,texpr,schema) <- replCheckExpr pexpr if proverName `elem` ["offline","sbv-offline","w4-offline"] then - offlineProveSat proverName SafetyQuery texpr schema mfile + do success <- offlineProveSat proverName SafetyQuery texpr schema mfile + pure emptyCommandResult { crSuccess = success } else do (firstProver,result,stats) <- rethrowErrorCall (onlineProveSat proverName SafetyQuery texpr schema mfile) - case result of + cmdResult <- case result of EmptyResult -> panic "REPL.Command" [ "got EmptyResult for online prover query" ] - ProverError msg -> rPutStrLn msg + ProverError msg -> + do rPutStrLn msg + pure emptyCommandResult { crSuccess = False } - ThmResult _ts -> rPutStrLn "Safe" + ThmResult _ts -> + do rPutStrLn "Safe" + pure emptyCommandResult CounterExample cexType tevs -> do rPutStrLn "Counterexample" @@ -746,33 +777,43 @@ safeCmd str pos fnm = do 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 () +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 rPutStrLn "There are no properties in scope." - else forM_ xs $ \(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 = M.ifDeclSig d - nd <- M.mctxNameDisp <$> getFocusedEnv - let doc = fixNameDisp nd (pp texpr) - proveSatExpr isSat (M.nameLoc x) doc texpr schema + then do + rPutStrLn "There are no properties in scope." + 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 = M.ifDeclSig 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 @@ -780,7 +821,8 @@ cmdProveSat isSat str pos fnm = do let doc = fixNameDisp nd (ppPrec 3 pexpr) -- function application has precedence 3 (_,texpr,schema) <- replCheckExpr pexpr let rng = fromMaybe (mkInteractiveRange pos fnm) (getLoc pexpr) - proveSatExpr isSat rng doc texpr schema + success <- proveSatExpr isSat rng doc texpr schema + pure emptyCommandResult { crSuccess = success } proveSatExpr :: Bool -> @@ -788,7 +830,7 @@ proveSatExpr :: Doc -> T.Expr -> T.Schema -> - REPL () + REPL Bool proveSatExpr isSat rng exprDoc texpr schema = do let cexStr | isSat = "satisfying assignment" | otherwise = "counterexample" @@ -801,16 +843,17 @@ proveSatExpr isSat rng exprDoc texpr schema = do offlineProveSat proverName qtype texpr schema mfile else do (firstProver,result,stats) <- rethrowErrorCall (onlineProveSat proverName qtype texpr schema mfile) - case result of + success <- case result of EmptyResult -> panic "REPL.Command" [ "got EmptyResult for online prover query" ] - ProverError msg -> rPutStrLn msg + ProverError msg -> False <$ rPutStrLn msg - ThmResult ts -> do + 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" @@ -829,6 +872,7 @@ proveSatExpr isSat rng exprDoc texpr schema = do _ -> return () void $ bindItVariable t e + pure False AllSatResult tevss -> do rPutStrLn "Satisfiable" @@ -859,8 +903,11 @@ proveSatExpr isSat rng exprDoc texpr schema = do [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 () @@ -911,7 +958,7 @@ onlineProveSat proverName qtype expr schema mfile = do stas <- io (readIORef timing) return (firstProver,res,stas) -offlineProveSat :: String -> QueryType -> T.Expr -> T.Schema -> Maybe FilePath -> REPL () +offlineProveSat :: String -> QueryType -> T.Expr -> T.Schema -> Maybe FilePath -> REPL Bool offlineProveSat proverName qtype expr schema mfile = do verbose <- getKnownUser "debug" modelValidate <- getUserProverValidate @@ -950,12 +997,13 @@ offlineProveSat proverName qtype expr schema mfile = do Left sbvCfg -> do result <- liftModuleCmd $ SBV.satProveOffline sbvCfg cmd case result of - Left msg -> rPutStrLn msg + Left msg -> False <$ rPutStrLn 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" @@ -974,6 +1022,7 @@ offlineProveSat proverName qtype expr schema mfile = do case result of Just msg -> rPutStrLn msg Nothing -> return () + pure True rIdent :: M.Ident @@ -1010,7 +1059,7 @@ mkSolverResult thing rng result earg = let argName = M.packIdent ("arg" ++ show n) in ((argName,t),(argName,e)) -specializeCmd :: String -> (Int,Int) -> Maybe FilePath -> REPL () +specializeCmd :: String -> (Int,Int) -> Maybe FilePath -> REPL CommandResult specializeCmd str pos fnm = do parseExpr <- replParseExpr str pos fnm (_, expr, schema) <- replCheckExpr parseExpr @@ -1020,9 +1069,11 @@ specializeCmd str pos fnm = do rPutStrLn "Original expression:" rPutStrLn $ dump expr rPutStrLn "Specialized expression:" - rPutStrLn $ dump spexpr + let value = dump spexpr + rPutStrLn value + pure emptyCommandResult { crValue = Just value } -refEvalCmd :: String -> (Int,Int) -> Maybe FilePath -> REPL () +refEvalCmd :: String -> (Int,Int) -> Maybe FilePath -> REPL CommandResult refEvalCmd str pos fnm = do parseExpr <- replParseExpr str pos fnm (_, expr, schema) <- replCheckExpr parseExpr @@ -1030,20 +1081,24 @@ refEvalCmd str pos fnm = do validEvalContext schema val <- liftModuleCmd (rethrowEvalError . R.evaluate expr) opts <- getPPValOpts - rPrint $ R.ppEValue opts val + let value = show (R.ppEValue opts val) + rPutStrLn value + pure emptyCommandResult { crValue = Just value } -astOfCmd :: String -> (Int,Int) -> Maybe FilePath -> REPL () +astOfCmd :: String -> (Int,Int) -> Maybe FilePath -> REPL CommandResult astOfCmd str pos fnm = do expr <- replParseExpr str pos fnm (re,_,_) <- replCheckExpr (P.noPos expr) rPrint (fmap M.nameUnique re) + pure emptyCommandResult -allTerms :: REPL () -allTerms = do +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 () +typeOfCmd :: String -> (Int,Int) -> Maybe FilePath -> REPL CommandResult typeOfCmd str pos fnm = do expr <- replParseExpr str pos fnm @@ -1053,10 +1108,13 @@ typeOfCmd str pos fnm = do whenDebug (rPutStrLn (dump def)) fDisp <- M.mctxNameDisp <$> getFocusedEnv -- type annotation ':' has precedence 2 - rPrint $ runDoc fDisp $ group $ hang - (ppPrec 2 expr <+> text ":") 2 (pp sig) + let output = show $ runDoc fDisp $ group $ hang + (ppPrec 2 expr <+> text ":") 2 (pp sig) + + rPutStrLn output + pure emptyCommandResult { crType = Just output } -timeCmd :: String -> (Int, Int) -> Maybe FilePath -> REPL () +timeCmd :: String -> (Int, Int) -> Maybe FilePath -> REPL CommandResult timeCmd str pos fnm = do period <- getKnownUser "timeMeasurementPeriod" :: REPL Int quiet <- getKnownUser "timeQuiet" @@ -1081,12 +1139,13 @@ timeCmd str pos fnm = do (pure $ E.VFloat $ FP.floatFromDouble benchAvgCpuTime) (pure $ E.VInteger $ toInteger benchAvgCycles) bindItVariableVal itType itVal + pure emptyCommandResult -- TODO: gather timing outputs -readFileCmd :: FilePath -> REPL () +readFileCmd :: FilePath -> REPL CommandResult readFileCmd fp = do bytes <- replReadFile fp (\err -> rPutStrLn (show err) >> return Nothing) case bytes of - Nothing -> return () + Nothing -> return emptyCommandResult { crSuccess = False } Just bs -> do pm <- getPrimMap let val = byteStringToInteger bs @@ -1098,6 +1157,7 @@ readFileCmd fp = do 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 @@ -1118,16 +1178,19 @@ byteStringToInteger bs x1 = byteStringToInteger bs1 x2 = byteStringToInteger bs2 -writeFileCmd :: FilePath -> String -> (Int,Int) -> Maybe FilePath -> REPL () +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 rPrint $ "Cannot write expression of types other than [n][8]." + then do + rPrint $ "Cannot write expression of types other than [n][8]." <+> "Type was: " <+> pp ty - else wf file =<< serializeValue val + pure emptyCommandResult { crSuccess = False } + else do + bytes <- serializeValue val + replWriteFile file bytes where - wf fp bytes = replWriteFile fp bytes (rPutStrLn . show) tIsByteSeq x = maybe False (tIsByte . snd) (T.tIsSeq x) @@ -1150,18 +1213,18 @@ rEval m = io (E.runEval mempty m) rEvalRethrow :: E.Eval a -> REPL a rEvalRethrow m = io $ rethrowEvalError $ E.runEval mempty m -reloadCmd :: REPL () +reloadCmd :: REPL CommandResult reloadCmd = do mb <- getLoadedMod case mb of Just lm -> case lPath lm of M.InFile f -> loadCmd f - _ -> return () - Nothing -> return () + _ -> return emptyCommandResult + Nothing -> return emptyCommandResult -editCmd :: String -> REPL () +editCmd :: String -> REPL CommandResult editCmd path = do mbE <- getEditPath mbL <- getLoadedMod @@ -1171,11 +1234,15 @@ editCmd path = , lPath = M.InFile path } doEdit path else case msum [ M.InFile <$> mbE, lPath <$> mbL ] of - Nothing -> rPutStrLn "No filed to edit." + 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 -> withROTempFile l bs replEdit >> pure () + M.InMem l bs -> do + _ <- withROTempFile l bs replEdit + pure emptyCommandResult where doEdit p = do setEditPath p @@ -1213,9 +1280,9 @@ withROTempFile name cnt k = -moduleCmd :: String -> REPL () +moduleCmd :: String -> REPL CommandResult moduleCmd modString - | null modString = return () + | null modString = return emptyCommandResult | otherwise = do case parseModName modString of Just m -> @@ -1226,14 +1293,16 @@ moduleCmd modString setLoadedMod LoadedModule { lName = Just m, lPath = mpath } loadHelper (M.loadModuleByPath file) M.InMem {} -> loadHelper (M.loadModuleByName m) - Nothing -> rPutStrLn "Invalid module name." + Nothing -> + do rPutStrLn "Invalid module name." + pure emptyCommandResult { crSuccess = False } loadPrelude :: REPL () -loadPrelude = moduleCmd $ show $ pp M.preludeName +loadPrelude = void $ moduleCmd $ show $ pp M.preludeName -loadCmd :: FilePath -> REPL () +loadCmd :: FilePath -> REPL CommandResult loadCmd path - | null path = return () + | null path = return emptyCommandResult -- when `:load`, the edit and focused paths become the parameter | otherwise = do setEditPath path @@ -1242,7 +1311,7 @@ loadCmd path } loadHelper (M.loadModuleByPath path) -loadHelper :: M.ModuleCmd (M.ModulePath,T.TCTopEntity) -> REPL () +loadHelper :: M.ModuleCmd (M.ModulePath,T.TCTopEntity) -> REPL CommandResult loadHelper how = do clearLoadedMod (path,ent) <- liftModuleCmd how @@ -1257,51 +1326,67 @@ loadHelper how = M.InFile f -> setEditPath f M.InMem {} -> clearEditPath setDynEnv mempty + pure emptyCommandResult -genHeaderCmd :: FilePath -> REPL () +genHeaderCmd :: FilePath -> REPL CommandResult genHeaderCmd path - | null path = pure () + | 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 rPutStrLn $ "No foreign declarations in " ++ pretty mPath + 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 (rPutStrLn . show) - M.InMem _ _ -> rPutStrLn header - -versionCmd :: REPL () -versionCmd = displayVersion rPutStrLn - -quitCmd :: REPL () -quitCmd = stop - -browseCmd :: String -> REPL () + 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 parseModName input of - Nothing -> rPutStrLn "Invalid module name" - Just m -> - do mb <- M.modContextOf m <$> getModuleEnv - case mb of - Nothing -> rPutStrLn ("Module " ++ show input ++ " is not loaded") - Just fe -> rPrint (browseModContext BrowseExported fe) - - -setOptionCmd :: String -> REPL () + Nothing -> do + rPutStrLn "Invalid module name" + pure emptyCommandResult { crSuccess = False } + Just m -> do + mb <- M.modContextOf m <$> 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 - | null key = mapM_ (describe . optName) (leaves userOptions) + | 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 @@ -1313,11 +1398,13 @@ setOptionCmd str describe k = do ev <- tryGetUser k case ev of - Just v -> rPutStrLn (k ++ " = " ++ showEnvVal v) + 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 = @@ -1329,29 +1416,33 @@ showEnvVal ev = EnvBool False -> "off" -- XXX at the moment, this can only look at declarations. -helpCmd :: String -> REPL () +helpCmd :: String -> REPL CommandResult helpCmd cmd - | null cmd = mapM_ rPutStrLn (genHelp commandList) + | null cmd = emptyCommandResult <$ mapM_ rPutStrLn (genHelp commandList) | cmd0 : args <- words cmd, ":" `isPrefixOf` cmd0 = case findCommandExact cmd0 of - [] -> void $ runCommand 1 Nothing (Unknown cmd0) + [] -> runCommand 1 Nothing (Unknown cmd0) [c] -> showCmdHelp c args - cs -> void $ runCommand 1 Nothing (Ambiguous cmd0 (concatMap cNames cs)) + cs -> runCommand 1 Nothing (Ambiguous cmd0 (concatMap cNames cs)) | otherwise = + wrapResult <$> case parseHelpName cmd of - Just qname -> helpForNamed qname - Nothing -> rPutStrLn ("Unable to parse name: " ++ cmd) + Just qname -> True <$ helpForNamed qname + Nothing -> False <$ rPutStrLn ("Unable to parse name: " ++ cmd) where - showCmdHelp c [arg] | ":set" `elem` cNames c = showOptionHelp arg + 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 "" - when (not (null (cLongHelp c))) $ do + unless (null (cLongHelp c)) $ do rPutStrLn (cLongHelp c) rPutStrLn "" + pure emptyCommandResult showOptionHelp arg = case lookupTrieExact arg userOptions of @@ -1364,22 +1455,24 @@ helpCmd cmd rPutStrLn "" rPutStrLn (optHelp opt) rPutStrLn "" - [] -> rPutStrLn ("Unknown setting name `" ++ arg ++ "`") - _ -> rPutStrLn ("Ambiguous setting name `" ++ arg ++ "`") + pure True + [] -> False <$ rPutStrLn ("Unknown setting name `" ++ arg ++ "`") + _ -> False <$ rPutStrLn ("Ambiguous setting name `" ++ arg ++ "`") -runShellCmd :: String -> REPL () +runShellCmd :: String -> REPL CommandResult runShellCmd cmd = io $ do h <- Process.runCommand cmd _ <- waitForProcess h - return () + return emptyCommandResult -- This could check for exit code 0 -cdCmd :: FilePath -> REPL () -cdCmd f | null f = rPutStrLn $ "[error] :cd requires a path argument" +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 io $ setCurrentDirectory f + then emptyCommandResult <$ io (setCurrentDirectory f) else raise $ DirectoryNotFound f -- C-c Handlings --------------------------------------------------------------- @@ -1587,17 +1680,21 @@ replPrepareCheckedExpr def sig = do itIdent :: M.Ident itIdent = M.packIdent "it" -replWriteFile :: FilePath -> BS.ByteString -> (X.SomeException -> REPL ()) -> REPL () +replWriteFile :: FilePath -> BS.ByteString -> REPL CommandResult replWriteFile = replWriteFileWith BS.writeFile -replWriteFileString :: FilePath -> String -> (X.SomeException -> REPL ()) -> REPL () +replWriteFileString :: FilePath -> String -> REPL CommandResult replWriteFileString = replWriteFileWith writeFile -replWriteFileWith :: (FilePath -> a -> IO ()) -> FilePath -> a -> - (X.SomeException -> REPL ()) -> REPL () -replWriteFileWith write fp contents handler = - do x <- io $ X.catch (write fp contents >> return Nothing) (return . Just) - maybe (return ()) handler x +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 = @@ -1670,11 +1767,13 @@ replEdit file = do type CommandMap = Trie CommandDescr -newSeedCmd :: REPL () +newSeedCmd :: REPL CommandResult newSeedCmd = do seed <- createAndSetSeed rPutStrLn "Seed initialized to:" - rPutStrLn (show seed) + let value = show seed + rPutStrLn value + pure emptyCommandResult { crValue = Just value } where createAndSetSeed = withRandomGen $ \g0 -> @@ -1685,11 +1784,12 @@ newSeedCmd = seed = (s1, s2, s3, s4) in pure (seed, TF.seedTFGen seed) -seedCmd :: String -> REPL () +seedCmd :: String -> REPL CommandResult seedCmd s = - case mbGen of - Nothing -> rPutStrLn "Could not parse seed argument - expecting an integer or 4-tuple of integers." - Just gen -> setRandomGen gen + 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 = @@ -1797,13 +1897,14 @@ parseCommand findCmd line = do -moduleInfoCmd :: Bool -> String -> REPL () +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 -> rPutStrLn "Invalid module name." + Nothing -> do rPutStrLn "Invalid module name." + pure emptyCommandResult { crSuccess = False } where showInfo (p,fi) = @@ -1830,6 +1931,7 @@ moduleInfoCmd isFile name depList show "foreign" (Map.toList (M.fiForeignDeps fi)) rPutStrLn "}" + pure emptyCommandResult diff --git a/src/Cryptol/REPL/Help.hs b/src/Cryptol/REPL/Help.hs index b3cdcf91e..1c2654f21 100644 --- a/src/Cryptol/REPL/Help.hs +++ b/src/Cryptol/REPL/Help.hs @@ -26,7 +26,7 @@ import Cryptol.TypeCheck.PP(emptyNameMap,ppWithNames) import Cryptol.REPL.Monad -helpForNamed :: P.PName -> REPL () +helpForNamed :: P.PName -> REPL Bool helpForNamed qname = do fe <- getFocusedEnv let params = M.mctxParams fe @@ -47,8 +47,11 @@ helpForNamed qname = separ = rPutStrLn " ---------" sequence_ (intersperse separ helps) - when (null (vNames ++ cNames ++ tNames ++ mNames)) $ + let failure = null (vNames ++ cNames ++ tNames ++ mNames) + when failure $ rPrint $ "Undefined name:" <+> pp qname + + pure (not failure) noInfo :: NameDisp -> M.Name -> REPL () diff --git a/src/Cryptol/REPL/Monad.hs b/src/Cryptol/REPL/Monad.hs index b94938a6d..153d98d80 100644 --- a/src/Cryptol/REPL/Monad.hs +++ b/src/Cryptol/REPL/Monad.hs @@ -738,12 +738,13 @@ mkUserEnv opts = Map.fromList $ do return (optName opt, optDefault opt) -- | Set a user option. -setUser :: String -> String -> REPL () +-- Returns 'True' on success +setUser :: String -> String -> REPL Bool setUser name val = case lookupTrieExact name userOptionsWithAliases of [opt] -> setUserOpt opt - [] -> rPutStrLn ("Unknown env value `" ++ name ++ "`") - _ -> rPutStrLn ("Ambiguous env value `" ++ name ++ "`") + [] -> False <$ rPutStrLn ("Unknown env value `" ++ name ++ "`") + _ -> False <$ rPutStrLn ("Ambiguous env value `" ++ name ++ "`") where setUserOpt opt = case optDefault opt of @@ -752,25 +753,26 @@ setUser name val = case lookupTrieExact name userOptionsWithAliases of EnvProg _ _ -> case splitOptArgs val of prog:args -> doCheck (EnvProg prog args) - [] -> rPutStrLn ("Failed to parse command for field, `" ++ name ++ "`") + [] -> False <$ rPutStrLn ("Failed to parse command for field, `" ++ name ++ "`") EnvNum _ -> case reads val of [(x,_)] -> doCheck (EnvNum x) - _ -> rPutStrLn ("Failed to parse number for field, `" ++ name ++ "`") + _ -> False <$ rPutStrLn ("Failed to parse number for field, `" ++ name ++ "`") EnvBool _ | any (`isPrefixOf` val) ["enable", "on", "yes", "true"] -> - writeEnv (EnvBool True) + True <$ writeEnv (EnvBool True) | any (`isPrefixOf` val) ["disable", "off", "no", "false"] -> - writeEnv (EnvBool False) + True <$ writeEnv (EnvBool False) | otherwise -> - rPutStrLn ("Failed to parse boolean for field, `" ++ name ++ "`") + False <$ rPutStrLn ("Failed to parse boolean for field, `" ++ name ++ "`") where doCheck v = do (r,ws) <- optCheck opt v case r of - Just err -> rPutStrLn err + Just err -> False <$ rPutStrLn err Nothing -> do mapM_ rPutStrLn ws writeEnv v + pure True writeEnv ev = do optEff opt ev modifyRW_ (\rw -> rw { eUserEnv = Map.insert (optName opt) ev (eUserEnv rw) }) From b2ce8200cdf2b97522451b06b02b8b0a9a3588c4 Mon Sep 17 00:00:00 2001 From: Eric Mertens Date: Fri, 7 Jun 2024 12:05:55 -0700 Subject: [PATCH 02/12] 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. --- cryptol/REPL/Haskeline.hs | 21 ++-- src/Cryptol/REPL/Command.hs | 204 +++++++++++++++++++++++++++++++++-- src/Cryptol/REPL/Monad.hs | 9 ++ src/Cryptol/TypeCheck/AST.hs | 40 +++++-- 4 files changed, 248 insertions(+), 26 deletions(-) diff --git a/cryptol/REPL/Haskeline.hs b/cryptol/REPL/Haskeline.hs index 0a30b7e07..98e597f4f 100644 --- 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 @@ -55,7 +56,7 @@ data ReplMode 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 @@ -63,17 +64,17 @@ crySession replMode stopOnError = Batch path -> (True, useFile path) InteractiveBatch path -> (False, useFile path) - loop :: Int -> InputT REPL CommandResult - loop lineNum = + loop :: Bool -> Int -> InputT REPL CommandResult + loop !success !lineNum = do ln <- getInputLines =<< MTL.lift getPrompt case ln of - NoMoreLines -> return emptyCommandResult + NoMoreLines -> return emptyCommandResult { crSuccess = success } Interrupted | isBatch && stopOnError -> return emptyCommandResult { crSuccess = False } - | otherwise -> loop lineNum + | 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 @@ -81,16 +82,16 @@ crySession replMode stopOnError = 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 emptyCommandResult { crSuccess = False } - | otherwise -> loop (lineNum + length txt) -- say somtething? + | otherwise -> loop False (lineNum + length txt) -- say somtething? Just cmd -> join $ MTL.lift $ 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 diff --git a/src/Cryptol/REPL/Command.hs b/src/Cryptol/REPL/Command.hs index 17d713392..14dd01209 100644 --- a/src/Cryptol/REPL/Command.hs +++ b/src/Cryptol/REPL/Command.hs @@ -139,7 +139,7 @@ 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 Data.IORef(newIORef, readIORef, writeIORef, modifyIORef) import GHC.Float (log1p, expm1) @@ -147,6 +147,7 @@ import Prelude () import Prelude.Compat import qualified Data.SBV.Internals as SBV (showTDiff) +import Data.Foldable (foldl') @@ -191,9 +192,10 @@ data CommandBody data CommandResult = CommandResult { crType :: Maybe String -- ^ type output for relevant commands - , crValue :: Maybe String -- ^ value output for relevan commands + , crValue :: Maybe String -- ^ value output for relevant commands , crSuccess :: Bool -- ^ indicator that command successfully performed its task } + deriving (Show) emptyCommandResult :: CommandResult emptyCommandResult = CommandResult @@ -299,6 +301,9 @@ nbCommandList = , 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" + "" ] commandList :: [CommandDescr] @@ -420,6 +425,12 @@ evalCmd str lineNum mbBatch = do -- 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 @@ -518,14 +529,14 @@ 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 + -- 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 + -- tv has already had polymorphism instantiated percentRef <- io $ newIORef Nothing testsRef <- io $ newIORef 0 @@ -813,7 +824,7 @@ cmdProveSat isSat "" _pos _fnm = pure $! acc && success success <- foldM check True xs pure emptyCommandResult { crSuccess = success } - + cmdProveSat isSat str pos fnm = do pexpr <- replParseExpr str pos fnm @@ -913,7 +924,7 @@ proveSatExpr isSat rng exprDoc texpr schema = do 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 + (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)) @@ -1110,7 +1121,7 @@ typeOfCmd str pos fnm = do -- type annotation ':' has precedence 2 let output = show $ runDoc fDisp $ group $ hang (ppPrec 2 expr <+> text ":") 2 (pp sig) - + rPutStrLn output pure emptyCommandResult { crType = Just output } @@ -1565,12 +1576,12 @@ moduleCmdResult (res,ws0) = do -- ignore certain warnings during typechecking filterTypecheck :: M.ModuleWarning -> Maybe M.ModuleWarning - filterTypecheck (M.TypeCheckWarnings nameMap xs) = - case filter (allow . snd) xs of + filterTypecheck (M.TypeCheckWarnings nameMap xs) = + case filter (allow . snd) xs of [] -> Nothing ys -> Just (M.TypeCheckWarnings nameMap ys) where - allow :: T.Warning -> Bool + allow :: T.Warning -> Bool allow = \case T.DefaultingTo _ _ | not warnDefaulting -> False T.NonExhaustivePropGuards _ | not warnNonExhConGrds -> False @@ -1933,5 +1944,178 @@ moduleInfoCmd isFile name rPutStrLn "}" pure emptyCommandResult +-- | Extract the code blocks from the body of a docstring. +-- +-- A single code block starts with at least 3 backticks followed by an +-- optional language specifier of "cryptol". This allowed other kinds +-- of code blocks to be included (and ignored) in docstrings. Longer +-- backtick sequences can be used when a code block needs to be able to +-- contain backtick sequences. +-- +-- @ +-- /** +-- * A docstring example +-- * +-- * ```cryptol +-- * :check example +-- * ``` +-- */ +-- @ +extractCodeBlocks :: T.Text -> Either String [[T.Text]] +extractCodeBlocks raw = go [] (T.lines raw) + where + go finished [] = Right (reverse finished) + go finished (x:xs) + | (ticks, lang) <- T.span ('`' ==) x + , 3 <= T.length ticks + = if lang `elem` ["", "repl"] + then keep finished ticks [] xs + else skip finished ticks xs + | otherwise = go finished xs + + -- process a code block that we're keeping + keep _ _ _ [] = Left "Unclosed code block" + keep finished close acc (x:xs) + | close == x = go (reverse acc : finished) xs + | otherwise = keep finished close (x : acc) xs + + -- process a code block that we're skipping + skip _ _ [] = Left "Unclosed code block" + skip finished close (x:xs) + | close == x = go finished xs + | otherwise = skip finished close xs + +data SubcommandResult = SubcommandResult + { srInput :: T.Text + , srResult :: CommandResult + , srLog :: String + } + +-- | 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 + where + go [] = pure [] + go (line:block) = + case parseCommand (findNbCommand True) (T.unpack line) of + Nothing -> do + pure [SubcommandResult + { srInput = line + , srLog = "Failed to parse command" + , srResult = emptyCommandResult { crSuccess = False } + }] + Just Ambiguous{} -> do + pure [SubcommandResult + { srInput = line + , srLog = "Ambiguous command" + , srResult = emptyCommandResult { crSuccess = False } + }] + Just Unknown{} -> do + pure [SubcommandResult + { srInput = line + , srLog = "Unknown command" + , srResult = emptyCommandResult { crSuccess = False } + }] + Just (Command cmd) -> do + (logtxt, result) <- captureLog (cmd 0 Nothing) + results <- checkBlock block + let subresult = SubcommandResult + { srInput = line + , srLog = logtxt + , srResult = result + } + pure (subresult : results) + +captureLog :: REPL a -> REPL (String, a) +captureLog m = do + previousLogger <- getLogger + outputsRef <- io (newIORef []) + setPutStr (\str -> modifyIORef outputsRef (str:)) + result <- m `finally` setLogger previousLogger + outputs <- io (readIORef outputsRef) + let output = concat (reverse outputs) + pure (output, result) + +-- | Check all the code blocks in a given docstring. +checkDocString :: T.Text -> REPL [[SubcommandResult]] +checkDocString str = + case extractCodeBlocks str of + Left e -> do + pure [[SubcommandResult + { srInput = T.empty + , srResult = emptyCommandResult { crSuccess = False } + , srLog = e + }]] + Right bs -> do + traverse checkBlock bs + +-- | 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 -> REPL [[SubcommandResult]] +checkDocStrings m = do + let dat = M.lmdModule (M.lmData m) + let ds = T.gatherModuleDocstrings dat + concat <$> traverse checkDocString ds + +-- | 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 + | null input = do + mb <- getLoadedMod + case lName =<< mb of + Nothing -> do + rPutStrLn "No current module" + pure emptyCommandResult { crSuccess = False } + Just mn -> checkModName mn + | otherwise = + case parseModName input of + Nothing -> do + rPutStrLn "Invalid module name" + pure emptyCommandResult { crSuccess = False } + Just mn -> checkModName mn + + where + + countOutcomes :: [SubcommandResult] -> (Int, Int) + countOutcomes = foldl' countOutcomes' (0, 0) + where + countOutcomes' (successes, failures) result + | crSuccess (srResult result) = (successes + 1, failures) + | otherwise = (successes, failures + 1) + + checkModName :: P.ModName -> REPL CommandResult + checkModName mn = do + mb <- M.lookupModule mn <$> getModuleEnv + case mb of + Nothing -> do + rPutStrLn ("Module " ++ show input ++ " is not loaded") + pure emptyCommandResult { crSuccess = False } + + Just fe -> do + results <- checkDocStrings fe + let (successes, failures) = countOutcomes (concat results) + forM_ results $ \result -> + forM_ result $ \line -> do + rPutStrLn (T.unpack (srInput line)) + rPutStr (srLog line) + rPutStrLn ("Successes: " ++ show successes ++ " Failures: " ++ show failures) + pure emptyCommandResult { crSuccess = failures == 0 } diff --git a/src/Cryptol/REPL/Monad.hs b/src/Cryptol/REPL/Monad.hs index 153d98d80..342eade88 100644 --- a/src/Cryptol/REPL/Monad.hs +++ b/src/Cryptol/REPL/Monad.hs @@ -57,6 +57,7 @@ module Cryptol.REPL.Monad ( , asBatch , validEvalContext , updateREPLTitle + , isolated , setUpdateREPLTitle , withRandomGen , setRandomGen @@ -79,6 +80,7 @@ module Cryptol.REPL.Monad ( -- ** Configurable Output , getPutStr , getLogger + , setLogger , setPutStr -- ** Smoke Test @@ -560,6 +562,11 @@ asBatch body = do modifyRW_ $ (\ rw -> rw { eIsBatch = wasBatch }) return a +isolated :: REPL a -> REPL a +isolated body = do + rw <- getRW + body `finally` modifyRW_ (const rw) + -- | Is evaluation enabled? If the currently focused module is parameterized, -- then we cannot evaluate. validEvalContext :: T.FreeVars a => a -> REPL () @@ -592,6 +599,8 @@ getPutStr = getLogger :: REPL Logger getLogger = eLogger <$> getRW +setLogger :: Logger -> REPL () +setLogger logger = modifyRW_ $ \rw -> rw { eLogger = logger } -- | Use the configured output action to print a string rPutStr :: String -> REPL () diff --git a/src/Cryptol/TypeCheck/AST.hs b/src/Cryptol/TypeCheck/AST.hs index a8798c704..e6bcdf52f 100644 --- a/src/Cryptol/TypeCheck/AST.hs +++ b/src/Cryptol/TypeCheck/AST.hs @@ -30,11 +30,9 @@ module Cryptol.TypeCheck.AST , module Cryptol.TypeCheck.Type ) where -import Data.Maybe(mapMaybe) - import Cryptol.Utils.Panic(panic) import Cryptol.Utils.Ident (Ident,isInfixIdent,ModName,PrimIdent,prelPrim) -import Cryptol.Parser.Position(Located,Range,HasLoc(..)) +import Cryptol.Parser.Position(Located,Range,HasLoc(..), Position, start, from) import Cryptol.ModuleSystem.Name import Cryptol.ModuleSystem.NamingEnv.Types import Cryptol.ModuleSystem.Interface @@ -55,11 +53,14 @@ import GHC.Generics (Generic) import Control.DeepSeq -import Data.Set (Set) +import qualified Data.IntMap as IntMap +import Data.List (sortBy) import Data.Map (Map) import qualified Data.Map as Map -import qualified Data.IntMap as IntMap -import Data.Text (Text) +import Data.Maybe (mapMaybe) +import Data.Ord (comparing) +import Data.Set (Set) +import Data.Text (Text) data TCTopEntity = @@ -522,3 +523,30 @@ instance PP (WithNames TCTopEntity) where TCTopModule m -> ppWithNames nm m TCTopSignature n ps -> hang ("interface module" <+> pp n <+> "where") 2 (pp ps) + +gatherModuleDocstrings :: Module -> [Text] +gatherModuleDocstrings m = + map snd $ + sortBy (comparing fst) $ + gatherModuleDocstrings' m { mName = start } + +gatherModuleDocstrings' :: ModuleG Position -> [(Position, Text)] +gatherModuleDocstrings' m = + cat [(mName m, mDoc m)] ++ + cat [(mName m, mpnDoc (mpParameters param)) | (_, param) <- Map.assocs (mParams m)] ++ + cat [(pos n, mtpDoc param) | (n, param) <- Map.assocs (mParamTypes m)] ++ + cat [(pos n, mvpDoc param) | (n, param) <- Map.assocs (mParamFuns m)] ++ + cat [(pos n, tsDoc t) | (n, t) <- Map.assocs (mTySyns m)] ++ + cat [(pos n, ntDoc t) | (n, t) <- Map.assocs (mNominalTypes m)] ++ + cat [(pos (dName d), dDoc d) | g <- mDecls m, d <- groupDecls g] ++ + cat [(pos n, ifsDoc s) | (n, s) <- Map.assocs (mSubmodules m)] ++ + cat [(pos n, mpnDoc s) | (n, s) <- Map.assocs (mSignatures m)] ++ + [doc | m' <- Map.elems (mFunctors m), doc <- gatherModuleDocstrings' (mapModName pos m')] + -- functor parameters don't have a *name*, so we associate them with their module for now + where + pos = from . nameLoc + + mapModName f md = md { mName = f (mName md) } + + cat :: [(Position, Maybe Text)] -> [(Position, Text)] + cat entries = [(p, d) | (p, Just d) <- entries] From 72902bddf3c681aeb87066c8caa15f8e9556b1a7 Mon Sep 17 00:00:00 2001 From: Eric Mertens Date: Mon, 8 Jul 2024 17:41:06 -0700 Subject: [PATCH 03/12] Implement :focus --- bench/Main.hs | 4 +- .../cryptol-eval-server/Main.hs | 2 +- cryptol/Main.hs | 2 +- src/Cryptol/ModuleSystem.hs | 17 +++- src/Cryptol/ModuleSystem/Base.hs | 17 +++- src/Cryptol/ModuleSystem/Env.hs | 30 +++++-- src/Cryptol/ModuleSystem/Interface.hs | 30 ++++--- src/Cryptol/ModuleSystem/Monad.hs | 11 ++- src/Cryptol/ModuleSystem/Name.hs | 1 - src/Cryptol/Parser.y | 8 ++ src/Cryptol/REPL/Command.hs | 80 +++++++++++++++---- src/Cryptol/REPL/Monad.hs | 23 +++--- src/Cryptol/TypeCheck/AST.hs | 51 ++++++------ src/Cryptol/TypeCheck/Interface.hs | 5 +- src/Cryptol/TypeCheck/ModuleInstance.hs | 6 ++ src/Cryptol/TypeCheck/Monad.hs | 9 ++- 16 files changed, 214 insertions(+), 82 deletions(-) diff --git a/bench/Main.hs b/bench/Main.hs index 761c3c5c4..7457587c7 100644 --- 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/cryptol-remote-api/cryptol-eval-server/Main.hs b/cryptol-remote-api/cryptol-eval-server/Main.hs index aa1048b05..5016aff33 100644 --- a/cryptol-remote-api/cryptol-eval-server/Main.hs +++ b/cryptol-remote-api/cryptol-eval-server/Main.hs @@ -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 (P.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 index 425cb06ba..85beccf28 100644 --- a/cryptol/Main.hs +++ b/cryptol/Main.hs @@ -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/src/Cryptol/ModuleSystem.hs b/src/Cryptol/ModuleSystem.hs index 81f7cbae0..6845b51d2 100644 --- 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 index ae1461fe6..6f050d9b0 100644 --- a/src/Cryptol/ModuleSystem/Base.hs +++ b/src/Cryptol/ModuleSystem/Base.hs @@ -81,7 +81,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 +118,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 ----------------------------------------------------------------------- diff --git a/src/Cryptol/ModuleSystem/Env.hs b/src/Cryptol/ModuleSystem/Env.hs index 3f033babd..49a9899f5 100644 --- a/src/Cryptol/ModuleSystem/Env.hs +++ b/src/Cryptol/ModuleSystem/Env.hs @@ -25,7 +25,7 @@ import Cryptol.Eval (EvalEnv) import qualified Cryptol.IR.FreeVars as T import Cryptol.ModuleSystem.Fingerprint import Cryptol.ModuleSystem.Interface -import Cryptol.ModuleSystem.Name (Name,NameInfo(..),Supply,emptySupply,nameInfo) +import Cryptol.ModuleSystem.Name (Name,NameInfo(..),Supply,emptySupply,nameInfo,nameTopModuleMaybe) import qualified Cryptol.ModuleSystem.NamingEnv as R import Cryptol.Parser.AST import qualified Cryptol.TypeCheck as T @@ -58,6 +58,7 @@ import Prelude.Compat import Cryptol.Utils.Panic(panic) import Cryptol.Utils.PP(pp) +import Cryptol.TypeCheck.AST (Submodule(smIface)) -- Module Environment ---------------------------------------------------------- @@ -84,7 +85,7 @@ data ModuleEnv = ModuleEnv - , meFocusedModule :: Maybe ModName + , meFocusedModule :: Maybe (ImpName Name) -- ^ The "current" module. Used to decide how to print names, for example. , meSearchPath :: [FilePath] @@ -195,7 +196,7 @@ initialModuleEnv = do focusModule :: ModName -> ModuleEnv -> Maybe ModuleEnv focusModule n me = do guard (isLoaded n (meLoadedModules me)) - return me { meFocusedModule = Just n } + return me { meFocusedModule = Just (ImpTop n) } -- | Get a list of all the loaded modules. Each module in the -- resulting list depends only on other modules that precede it. @@ -273,9 +274,28 @@ instance Monoid ModContext where } +modContextOf :: ImpName Name -> ModuleEnv -> Maybe ModContext +modContextOf (ImpNested name) me = + do mname <- nameTopModuleMaybe name + lm <- lookupModule mname me + sm <- Map.lookup name (T.mSubmodules (lmModule lm)) -- TODO: support uninstantiated functors + let + localNames = T.smInScope sm -modContextOf :: ModName -> ModuleEnv -> Maybe ModContext -modContextOf mname me = + -- XXX: do we want only public ones here? + loadedDecls = map (ifDefines . lmInterface) + $ getLoadedModules (meLoadedModules me) + + pure ModContext + { mctxParams = NoParams + , mctxExported = ifsPublic (smIface sm) + , mctxDecls = mconcat (ifDefines (lmInterface lm) : loadedDecls) + , mctxNames = localNames + , mctxNameDisp = R.toNameDisp localNames + } + -- TODO: support focusing inside a submodule signature to support browsing? + +modContextOf (ImpTop mname) me = do lm <- lookupModule mname me let localIface = lmInterface lm localNames = lmNamingEnv lm diff --git a/src/Cryptol/ModuleSystem/Interface.hs b/src/Cryptol/ModuleSystem/Interface.hs index adc63513d..92b65a6f0 100644 --- a/src/Cryptol/ModuleSystem/Interface.hs +++ b/src/Cryptol/ModuleSystem/Interface.hs @@ -10,6 +10,7 @@ {-# LANGUAGE DeriveAnyClass #-} {-# LANGUAGE DeriveGeneric #-} {-# LANGUAGE RecordWildCards #-} +{-# LANGUAGE DeriveFunctor #-} {-# LANGUAGE Safe #-} module Cryptol.ModuleSystem.Interface ( Iface @@ -26,6 +27,7 @@ module Cryptol.ModuleSystem.Interface ( , filterIfaceDecls , ifaceDeclsNames , ifaceOrigNameMap + , ifaceNameToModuleMap ) where import Data.Set(Set) @@ -45,8 +47,9 @@ import Cryptol.ModuleSystem.Name import Cryptol.Utils.Ident (ModName, OrigName(..)) import Cryptol.Utils.Panic(panic) import Cryptol.Utils.Fixity(Fixity) -import Cryptol.Parser.AST(Pragma) +import Cryptol.Parser.AST(Pragma, ImpName(..)) import Cryptol.TypeCheck.Type +import Data.Maybe (maybeToList) type Iface = IfaceG ModName @@ -56,7 +59,7 @@ data IfaceG name = Iface , ifParams :: FunctorParams -- ^ Module parameters, if any , ifDefines :: IfaceDecls -- ^ All things defines in the module -- (includes nested definitions) - } deriving (Show, Generic, NFData) + } deriving (Show, Generic, NFData, Functor) -- | Remove the name of a module. This is useful for dealing with collections -- of modules, as in `Map (ImpName Name) (IfaceG ())`. @@ -75,7 +78,7 @@ data IfaceNames name = IfaceNames , ifsDefines :: Set Name -- ^ Things defined in this module , ifsPublic :: Set Name -- ^ Subset of `ifsDefines` that is public , ifsDoc :: !(Maybe Text) -- ^ Documentation - } deriving (Show, Generic, NFData) + } deriving (Show, Generic, NFData, Functor) -- | Is this interface for a functor. ifaceIsFunctor :: IfaceG name -> Bool @@ -232,9 +235,18 @@ ifaceOrigNameMap ifa = Map.unionsWith Map.union (here : nested) (concatMap conNames (Map.elems (ifNominalTypes decls))) where conNames = map fst . nominalTypeConTypes - - - - - - +-- | For every name in the interface compute the direct module that defines it. +-- This does not traverse into functors or interfaces. +ifaceNameToModuleMap :: Iface -> Map Name (ImpName Name) +ifaceNameToModuleMap iface = go (ImpTop <$> ifNames iface) + where + theModules = ifModules (ifDefines iface) + + go :: IfaceNames (ImpName Name) -> Map Name (ImpName Name) + go names = + Map.fromSet (\_ -> ifsName names) (ifsDefines names) <> + Map.unions + [ go (ImpNested <$> modu) + | childName <- Set.toList (ifsNested names) + , modu <- maybeToList (Map.lookup childName theModules) + ] diff --git a/src/Cryptol/ModuleSystem/Monad.hs b/src/Cryptol/ModuleSystem/Monad.hs index c4350e9f8..78d939d53 100644 --- a/src/Cryptol/ModuleSystem/Monad.hs +++ b/src/Cryptol/ModuleSystem/Monad.hs @@ -577,13 +577,16 @@ getEvalOpts = getNominalTypes :: ModuleM (Map T.Name T.NominalType) getNominalTypes = ModuleT (loadedNominalTypes <$> get) -getFocusedModule :: ModuleM (Maybe P.ModName) +getFocusedModule :: ModuleM (Maybe (P.ImpName T.Name)) getFocusedModule = ModuleT (meFocusedModule `fmap` get) -setFocusedModule :: P.ModName -> ModuleM () -setFocusedModule n = ModuleT $ do +setFocusedModule :: P.ImpName T.Name -> ModuleM () +setFocusedModule = setMaybeFocusedModule . Just + +setMaybeFocusedModule :: Maybe (P.ImpName T.Name) -> ModuleM () +setMaybeFocusedModule mb = ModuleT $ do me <- get - set $! me { meFocusedModule = Just n } + set $! me { meFocusedModule = mb } getSearchPath :: ModuleM [FilePath] getSearchPath = ModuleT (meSearchPath `fmap` get) diff --git a/src/Cryptol/ModuleSystem/Name.hs b/src/Cryptol/ModuleSystem/Name.hs index aff8e3468..fc865ad56 100644 --- a/src/Cryptol/ModuleSystem/Name.hs +++ b/src/Cryptol/ModuleSystem/Name.hs @@ -276,7 +276,6 @@ nameTopModuleMaybe = fmap topModuleFor . nameModPathMaybe nameTopModule :: Name -> ModName nameTopModule = topModuleFor . nameModPath - -- Name Supply ----------------------------------------------------------------- class Monad m => FreshM m where diff --git a/src/Cryptol/Parser.y b/src/Cryptol/Parser.y index d6a8f8344..03a2dfcdf 100644 --- a/src/Cryptol/Parser.y +++ b/src/Cryptol/Parser.y @@ -19,6 +19,7 @@ module Cryptol.Parser , parseRepl, parseReplWith , parseSchema, parseSchemaWith , parseModName, parseHelpName + , parseImpName , ParseError(..), ppError , Layout(..) , Config(..), defaultConfig @@ -155,6 +156,7 @@ import Paths_cryptol %name repl repl %name schema schema %name modName modName +%name impName impName %name helpName help_name %tokentype { Located Token } %monad { ParseM } @@ -945,6 +947,12 @@ parseModName txt = Right a -> Just (thing a) Left _ -> Nothing +parseImpName :: String -> Maybe (ImpName PName) +parseImpName txt = + case parseString defaultConfig { cfgModuleScope = False } impName txt of + Right a -> Just (thing a) + Left _ -> Nothing + parseHelpName :: String -> Maybe PName parseHelpName txt = case parseString defaultConfig { cfgModuleScope = False } helpName txt of diff --git a/src/Cryptol/REPL/Command.hs b/src/Cryptol/REPL/Command.hs index 14dd01209..77645bb94 100644 --- a/src/Cryptol/REPL/Command.hs +++ b/src/Cryptol/REPL/Command.hs @@ -63,6 +63,8 @@ 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 @@ -74,7 +76,7 @@ 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.Eval.Concrete( Concrete(..) ) +import Cryptol.Backend.Concrete ( Concrete(..) ) import qualified Cryptol.Eval.Concrete as Concrete import qualified Cryptol.Eval.Env as E import Cryptol.Eval.FFI @@ -86,7 +88,7 @@ import Cryptol.Testing.Random import qualified Cryptol.Testing.Random as TestR import Cryptol.Parser (parseExprWith,parseReplWith,ParseError(),Config(..),defaultConfig - ,parseModName,parseHelpName) + ,parseModName,parseHelpName,parseImpName) import Cryptol.Parser.Position (Position(..),Range(..),HasLoc(..)) import qualified Cryptol.TypeCheck.AST as T import qualified Cryptol.TypeCheck.Error as T @@ -330,6 +332,9 @@ commandList = , 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." "" @@ -1241,7 +1246,7 @@ editCmd path = mbL <- getLoadedMod if not (null path) then do when (isNothing mbL) - $ setLoadedMod LoadedModule { lName = Nothing + $ setLoadedMod LoadedModule { lFocus = Nothing , lPath = M.InFile path } doEdit path else case msum [ M.InFile <$> mbE, lPath <$> mbL ] of @@ -1301,13 +1306,49 @@ moduleCmd modString case mpath of M.InFile file -> do setEditPath file - setLoadedMod LoadedModule { lName = Just m, lPath = mpath } + 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 @@ -1317,7 +1358,7 @@ loadCmd path -- when `:load`, the edit and focused paths become the parameter | otherwise = do setEditPath path - setLoadedMod LoadedModule { lName = Nothing + setLoadedMod LoadedModule { lFocus = Nothing , lPath = M.InFile path } loadHelper (M.loadModuleByPath path) @@ -1329,7 +1370,7 @@ loadHelper how = whenDebug (rPutStrLn (dump ent)) setLoadedMod LoadedModule - { lName = Just (T.tcTopEntitytName ent) + { lFocus = Just (P.ImpTop (T.tcTopEntitytName ent)) , lPath = path } -- after a successful load, the current module becomes the edit target @@ -1379,12 +1420,13 @@ browseCmd input rPrint (browseModContext BrowseInScope fe) pure emptyCommandResult | otherwise = - case parseModName input of + case parseImpName input of Nothing -> do rPutStrLn "Invalid module name" pure emptyCommandResult { crSuccess = False } - Just m -> do - mb <- M.modContextOf m <$> getModuleEnv + 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") @@ -2044,8 +2086,8 @@ captureLog m = do pure (output, result) -- | Check all the code blocks in a given docstring. -checkDocString :: T.Text -> REPL [[SubcommandResult]] -checkDocString str = +checkDocString :: P.ImpName T.Name -> T.Text -> REPL [[SubcommandResult]] +checkDocString impName str = case extractCodeBlocks str of Left e -> do pure [[SubcommandResult @@ -2053,8 +2095,11 @@ checkDocString str = , srResult = emptyCommandResult { crSuccess = False } , srLog = e }]] - Right bs -> do - traverse checkBlock bs + Right bs -> + Ex.bracket + (liftModuleCmd (`M.runModuleM` (M.getFocusedModule <* M.setFocusedModule impName))) + (\mb -> liftModuleCmd (`M.runModuleM` M.setMaybeFocusedModule mb)) + (\_ -> traverse checkBlock bs) -- | Check all of the docstrings in the given module. -- @@ -2064,8 +2109,8 @@ checkDocString str = checkDocStrings :: M.LoadedModule -> REPL [[SubcommandResult]] checkDocStrings m = do let dat = M.lmdModule (M.lmData m) - let ds = T.gatherModuleDocstrings dat - concat <$> traverse checkDocString ds + let ds = T.gatherModuleDocstrings (M.ifaceNameToModuleMap (M.lmInterface m)) dat + concat <$> traverse (uncurry checkDocString) ds -- | Evaluate all the docstrings in the specified module. -- @@ -2114,8 +2159,11 @@ checkDocStringsCmd input forM_ results $ \result -> forM_ result $ \line -> do + rPutStrLn "" rPutStrLn (T.unpack (srInput line)) rPutStr (srLog line) - rPutStrLn ("Successes: " ++ show successes ++ " Failures: " ++ show failures) + + rPutStrLn "" + rPutStrLn ("Successes: " ++ show successes ++ ", Failures: " ++ show failures) pure emptyCommandResult { crSuccess = failures == 0 } diff --git a/src/Cryptol/REPL/Monad.hs b/src/Cryptol/REPL/Monad.hs index 342eade88..fefc91d6e 100644 --- a/src/Cryptol/REPL/Monad.hs +++ b/src/Cryptol/REPL/Monad.hs @@ -48,7 +48,7 @@ module Cryptol.REPL.Monad ( , getTypeNames , getPropertyNames , getModNames - , LoadedModule(..), getLoadedMod, setLoadedMod, clearLoadedMod + , LoadedModule(..), lName, getLoadedMod, setLoadedMod, clearLoadedMod , setEditPath, getEditPath, clearEditPath , setSearchPath, prependSearchPath , getPrompt @@ -147,10 +147,13 @@ import Prelude.Compat -- | This indicates what the user would like to work on. data LoadedModule = LoadedModule - { lName :: Maybe P.ModName -- ^ Working on this module. - , lPath :: M.ModulePath -- ^ Working on this file. + { lFocus :: Maybe (P.ImpName T.Name) -- ^ Working on this module. + , lPath :: M.ModulePath -- ^ Working on this file. } +lName :: LoadedModule -> Maybe P.ModName +lName lm = M.impNameTopModule <$> lFocus lm + -- | REPL RW Environment. data RW = RW { eLoadedMod :: Maybe LoadedModule @@ -234,14 +237,16 @@ mkPrompt rw detailedPrompt = id False modLn = - case lName =<< eLoadedMod rw of + case lFocus =<< eLoadedMod rw of Nothing -> show (pp I.preludeName) Just m - | M.isLoadedParamMod m loaded -> modName ++ "(parameterized)" - | M.isLoadedInterface m loaded -> modName ++ "(interface)" + | M.isLoadedParamMod top loaded -> modName ++ "(parameterized)" + | M.isLoadedInterface top loaded -> modName ++ "(interface)" | otherwise -> modName - where modName = pretty m - loaded = M.meLoadedModules (eModuleEnv rw) + where + top = M.impNameTopModule m + modName = pretty m + loaded = M.meLoadedModules (eModuleEnv rw) withFocus = case eLoadedMod rw of @@ -501,7 +506,7 @@ getEvalOptsAction = REPL $ \rwRef -> pure $ clearLoadedMod :: REPL () clearLoadedMod = do modifyRW_ (\rw -> rw { eLoadedMod = upd <$> eLoadedMod rw }) updateREPLTitle - where upd x = x { lName = Nothing } + where upd x = x { lFocus = Nothing } -- | Set the name of the currently focused file, loaded via @:r@. setLoadedMod :: LoadedModule -> REPL () diff --git a/src/Cryptol/TypeCheck/AST.hs b/src/Cryptol/TypeCheck/AST.hs index e6bcdf52f..5d1f79db5 100644 --- a/src/Cryptol/TypeCheck/AST.hs +++ b/src/Cryptol/TypeCheck/AST.hs @@ -110,7 +110,7 @@ data ModuleG mname = , mTySyns :: Map Name TySyn , mNominalTypes :: Map Name NominalType , mDecls :: [DeclGroup] - , mSubmodules :: Map Name (IfaceNames Name) + , mSubmodules :: Map Name Submodule , mSignatures :: !(Map Name ModParamNames) , mInScope :: NamingEnv @@ -118,6 +118,11 @@ data ModuleG mname = -- Submodule in-scope information is in 'mSubmodules'. } deriving (Show, Generic, NFData) +data Submodule = Submodule + { smIface :: IfaceNames Name + , smInScope :: NamingEnv + } deriving (Show, Generic, NFData) + emptyModule :: mname -> ModuleG mname emptyModule nm = Module @@ -524,29 +529,25 @@ instance PP (WithNames TCTopEntity) where TCTopSignature n ps -> hang ("interface module" <+> pp n <+> "where") 2 (pp ps) -gatherModuleDocstrings :: Module -> [Text] -gatherModuleDocstrings m = - map snd $ - sortBy (comparing fst) $ - gatherModuleDocstrings' m { mName = start } - -gatherModuleDocstrings' :: ModuleG Position -> [(Position, Text)] -gatherModuleDocstrings' m = - cat [(mName m, mDoc m)] ++ - cat [(mName m, mpnDoc (mpParameters param)) | (_, param) <- Map.assocs (mParams m)] ++ - cat [(pos n, mtpDoc param) | (n, param) <- Map.assocs (mParamTypes m)] ++ - cat [(pos n, mvpDoc param) | (n, param) <- Map.assocs (mParamFuns m)] ++ - cat [(pos n, tsDoc t) | (n, t) <- Map.assocs (mTySyns m)] ++ - cat [(pos n, ntDoc t) | (n, t) <- Map.assocs (mNominalTypes m)] ++ - cat [(pos (dName d), dDoc d) | g <- mDecls m, d <- groupDecls g] ++ - cat [(pos n, ifsDoc s) | (n, s) <- Map.assocs (mSubmodules m)] ++ - cat [(pos n, mpnDoc s) | (n, s) <- Map.assocs (mSignatures m)] ++ - [doc | m' <- Map.elems (mFunctors m), doc <- gatherModuleDocstrings' (mapModName pos m')] - -- functor parameters don't have a *name*, so we associate them with their module for now +gatherModuleDocstrings :: + Map Name (ImpName Name) -> + Module -> + [(ImpName Name, Text)] +gatherModuleDocstrings nameToModule m = + cat [(ImpTop (mName m), mDoc m)] ++ + -- mParams m + -- mParamTypes m + -- mParamFuns m + cat [(lookupModuleName n, tsDoc t) | (n, t) <- Map.assocs (mTySyns m)] ++ + cat [(lookupModuleName n, ntDoc t) | (n, t) <- Map.assocs (mNominalTypes m)] ++ + cat [(lookupModuleName (dName d), dDoc d) | g <- mDecls m, d <- groupDecls g] ++ + cat [(ImpNested n, ifsDoc (smIface s)) | (n, s) <- Map.assocs (mSubmodules m)] ++ + cat [(ImpTop (mName m), mpnDoc s) | s <- Map.elems (mSignatures m)] where - pos = from . nameLoc - - mapModName f md = md { mName = f (mName md) } - - cat :: [(Position, Maybe Text)] -> [(Position, Text)] + cat :: [(a, Maybe Text)] -> [(a, Text)] cat entries = [(p, d) | (p, Just d) <- entries] + + lookupModuleName n = + case Map.lookup n nameToModule of + Just x -> x + Nothing -> panic "gatherModuleDocstrings" ["No owning module for name:", show (pp n)] diff --git a/src/Cryptol/TypeCheck/Interface.hs b/src/Cryptol/TypeCheck/Interface.hs index 57588c4f7..6e8422496 100644 --- a/src/Cryptol/TypeCheck/Interface.hs +++ b/src/Cryptol/TypeCheck/Interface.hs @@ -51,7 +51,8 @@ genModDefines m = where nestedInSet = Set.unions . map inNested . Set.toList inNested x = case Map.lookup x (mSubmodules m) of - Just y -> ifsDefines y `Set.union` nestedInSet (ifsNested y) + Just y -> ifsDefines iface `Set.union` nestedInSet (ifsNested iface) + where iface = smIface y Nothing -> Set.empty -- must be signature or a functor genIface :: ModuleG name -> IfaceG name @@ -71,7 +72,7 @@ genIfaceWithNames names m = , d <- groupDecls dg , let qn = dName d ] - , ifModules = mSubmodules m + , ifModules = smIface <$> mSubmodules m , ifSignatures = mSignatures m , ifFunctors = genIface <$> mFunctors m } diff --git a/src/Cryptol/TypeCheck/ModuleInstance.hs b/src/Cryptol/TypeCheck/ModuleInstance.hs index f7524b4cf..3b2dfac51 100644 --- a/src/Cryptol/TypeCheck/ModuleInstance.hs +++ b/src/Cryptol/TypeCheck/ModuleInstance.hs @@ -63,6 +63,12 @@ instance ModuleInstance name => ModuleInstance (ImpName name) where ImpTop t -> ImpTop t ImpNested n -> ImpNested (moduleInstance n) +instance ModuleInstance Submodule where + moduleInstance x = Submodule + { smInScope = moduleInstance (smInScope x) + , smIface = moduleInstance (smIface x) + } + instance ModuleInstance (ModuleG name) where moduleInstance m = Module { mName = mName m diff --git a/src/Cryptol/TypeCheck/Monad.hs b/src/Cryptol/TypeCheck/Monad.hs index a30f060c9..84dd52b79 100644 --- a/src/Cryptol/TypeCheck/Monad.hs +++ b/src/Cryptol/TypeCheck/Monad.hs @@ -852,7 +852,7 @@ lookupModule iname = do localMods <- getScope mSubmodules case Map.lookup m localMods of Just names -> - do n <- genIfaceWithNames names <$> getCurDecls + do n <- genIfaceWithNames (smIface names) <$> getCurDecls pure (If.ifaceForgetName n) Nothing -> @@ -1057,7 +1057,10 @@ endSubmodule = , mSignatures = add mSignatures , mSubmodules = if isFun then mSubmodules y - else Map.insert m (genIfaceNames x1) + else let sm = Submodule + { smIface = genIfaceNames x1 + , smInScope = mInScope x } + in Map.insert m sm (mSubmodules x <> mSubmodules y) , mFunctors = if isFun then Map.insert m x1 (mFunctors y) @@ -1183,7 +1186,7 @@ addSignatures :: Map Name ModParamNames -> InferM () addSignatures mp = updScope \r -> r { mSignatures = Map.union mp (mSignatures r) } -addSubmodules :: Map Name (If.IfaceNames Name) -> InferM () +addSubmodules :: Map Name Submodule -> InferM () addSubmodules mp = updScope \r -> r { mSubmodules = Map.union mp (mSubmodules r) } From 5639fa9d554744f2772ce98ba0af92e2cace22a4 Mon Sep 17 00:00:00 2001 From: Eric Mertens Date: Tue, 16 Jul 2024 11:59:05 -0700 Subject: [PATCH 04/12] Add some :check-docstring test cases --- cry | 2 +- src/Cryptol/REPL/Command.hs | 4 +++- tests/docstrings/T01.cry | 17 +++++++++++++++++ tests/docstrings/T01.icry | 2 ++ tests/docstrings/T01.icry.stdout | 15 +++++++++++++++ tests/docstrings/T02.cry | 30 ++++++++++++++++++++++++++++++ tests/docstrings/T02.icry | 2 ++ tests/docstrings/T02.icry.stdout | 17 +++++++++++++++++ tests/docstrings/T03.cry | 20 ++++++++++++++++++++ tests/docstrings/T03.icry | 2 ++ tests/docstrings/T03.icry.stdout | 6 ++++++ 11 files changed, 115 insertions(+), 2 deletions(-) create mode 100644 tests/docstrings/T01.cry create mode 100644 tests/docstrings/T01.icry create mode 100644 tests/docstrings/T01.icry.stdout create mode 100644 tests/docstrings/T02.cry create mode 100644 tests/docstrings/T02.icry create mode 100644 tests/docstrings/T02.icry.stdout create mode 100644 tests/docstrings/T03.cry create mode 100644 tests/docstrings/T03.icry create mode 100644 tests/docstrings/T03.icry.stdout diff --git a/cry b/cry index 63964cbc4..e0f041adf 100755 --- 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/src/Cryptol/REPL/Command.hs b/src/Cryptol/REPL/Command.hs index 77645bb94..722ce2194 100644 --- a/src/Cryptol/REPL/Command.hs +++ b/src/Cryptol/REPL/Command.hs @@ -2004,8 +2004,10 @@ moduleInfoCmd isFile name -- */ -- @ extractCodeBlocks :: T.Text -> Either String [[T.Text]] -extractCodeBlocks raw = go [] (T.lines raw) +extractCodeBlocks raw = go [] cleanLines where + cleanLines = T.dropWhile isSpace <$> T.lines raw + go finished [] = Right (reverse finished) go finished (x:xs) | (ticks, lang) <- T.span ('`' ==) x diff --git a/tests/docstrings/T01.cry b/tests/docstrings/T01.cry new file mode 100644 index 000000000..442f3f614 --- /dev/null +++ b/tests/docstrings/T01.cry @@ -0,0 +1,17 @@ +module T01 where + +submodule Sub where + /** + * This verifies that pp shadows the outer definition + * ``` + * :check pp + * ``` + */ + pp = True + +/** + * ``` + * :check ~ pp + * ``` + */ +pp = False diff --git a/tests/docstrings/T01.icry b/tests/docstrings/T01.icry new file mode 100644 index 000000000..77ec0e253 --- /dev/null +++ b/tests/docstrings/T01.icry @@ -0,0 +1,2 @@ +:m T01 +:check-docstrings diff --git a/tests/docstrings/T01.icry.stdout b/tests/docstrings/T01.icry.stdout new file mode 100644 index 000000000..4e7facdf0 --- /dev/null +++ b/tests/docstrings/T01.icry.stdout @@ -0,0 +1,15 @@ +Loading module Cryptol +Loading module Cryptol +Loading module T01 + +:check pp +Using exhaustive testing. +Testing... Passed 1 tests. +Q.E.D. + +:check ~ pp +Using exhaustive testing. +Testing... Passed 1 tests. +Q.E.D. + +Successes: 2, Failures: 0 diff --git a/tests/docstrings/T02.cry b/tests/docstrings/T02.cry new file mode 100644 index 000000000..36c44360d --- /dev/null +++ b/tests/docstrings/T02.cry @@ -0,0 +1,30 @@ + +module T02 where + +submodule F where + parameter + type n : # + type constraint (fin n, n >= 2) + + private + c : Z n + c = 1 + + /** + * ``` + * :exhaust p + * ``` + */ + p x = c + x == x + c + +submodule F7 = submodule F where + type n = 7 + +/** + * ``` + * let y = 20 + * :check f 10 == 20 + * ``` + */ +f : Integer -> Integer +f x = x + x diff --git a/tests/docstrings/T02.icry b/tests/docstrings/T02.icry new file mode 100644 index 000000000..11cd27366 --- /dev/null +++ b/tests/docstrings/T02.icry @@ -0,0 +1,2 @@ +:m T02 +:check-docstrings diff --git a/tests/docstrings/T02.icry.stdout b/tests/docstrings/T02.icry.stdout new file mode 100644 index 000000000..bd32f9961 --- /dev/null +++ b/tests/docstrings/T02.icry.stdout @@ -0,0 +1,17 @@ +Loading module Cryptol +Loading module Cryptol +Loading module T02 + +:exhaust p +Using exhaustive testing. +Testing... Passed 7 tests. +Q.E.D. + +let y = 20 + +:check f 10 == 20 +Using exhaustive testing. +Testing... Passed 1 tests. +Q.E.D. + +Successes: 3, Failures: 0 diff --git a/tests/docstrings/T03.cry b/tests/docstrings/T03.cry new file mode 100644 index 000000000..9699f3f9e --- /dev/null +++ b/tests/docstrings/T03.cry @@ -0,0 +1,20 @@ +module T03 where + +/** + * + * Each code block is meant to be independent + * + * ```repl + * let x = 1 + * :check x == 1 + * ``` + * + * The x defined in the previous block shouldn't be in scope for this next test + * + * ```repl + * :check x == 1 + * ``` + * + */ +a : Bit +a = True diff --git a/tests/docstrings/T03.icry b/tests/docstrings/T03.icry new file mode 100644 index 000000000..167920abd --- /dev/null +++ b/tests/docstrings/T03.icry @@ -0,0 +1,2 @@ +:m T03 +:check-docstrings diff --git a/tests/docstrings/T03.icry.stdout b/tests/docstrings/T03.icry.stdout new file mode 100644 index 000000000..22f16b006 --- /dev/null +++ b/tests/docstrings/T03.icry.stdout @@ -0,0 +1,6 @@ +Loading module Cryptol +Loading module Cryptol +Loading module T03 + +[error] at :0:8--0:9 + Value not in scope: x From 87ca401476322cb2ae99a984aa56f0d11b5c3108 Mon Sep 17 00:00:00 2001 From: Eric Mertens Date: Tue, 16 Jul 2024 14:49:31 -0700 Subject: [PATCH 05/12] Update changelog --- CHANGES.md | 10 ++++++++++ 1 file changed, 10 insertions(+) diff --git a/CHANGES.md b/CHANGES.md index dc85a51e9..7b7013d26 100644 --- a/CHANGES.md +++ b/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 From 37fa28832afff99b59ed8b140bdfe60da48de953 Mon Sep 17 00:00:00 2001 From: Eric Mertens Date: Tue, 16 Jul 2024 15:14:15 -0700 Subject: [PATCH 06/12] Make cryptol-server build to with focused module change --- cryptol-remote-api/cryptol-eval-server/Main.hs | 4 ++-- cryptol-remote-api/src/CryptolServer/FocusedModule.hs | 6 +++++- tests/docstrings/T04.cry | 11 +++++++++++ tests/docstrings/T04.icry | 2 ++ tests/docstrings/T04.icry.stdout | 7 +++++++ 5 files changed, 27 insertions(+), 3 deletions(-) create mode 100644 tests/docstrings/T04.cry create mode 100644 tests/docstrings/T04.icry create mode 100644 tests/docstrings/T04.icry.stdout diff --git a/cryptol-remote-api/cryptol-eval-server/Main.hs b/cryptol-remote-api/cryptol-eval-server/Main.hs index 5016aff33..db38fe51e 100644 --- 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 (P.ImpTop (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-remote-api/src/CryptolServer/FocusedModule.hs b/cryptol-remote-api/src/CryptolServer/FocusedModule.hs index 4ea5a6c39..238a07704 100644 --- a/cryptol-remote-api/src/CryptolServer/FocusedModule.hs +++ b/cryptol-remote-api/src/CryptolServer/FocusedModule.hs @@ -11,6 +11,7 @@ import Data.Aeson as JSON import Cryptol.ModuleSystem (meFocusedModule, meLoadedModules) import Cryptol.ModuleSystem.Env (isLoadedParamMod) +import qualified Cryptol.TypeCheck.AST as T import Cryptol.Utils.PP import CryptolServer @@ -27,7 +28,10 @@ focusedModule _ = Nothing -> return $ JSON.object [ "module" .= JSON.Null ] Just name -> - do let parameterized = isLoadedParamMod name (meLoadedModules me) + do let parameterized = + case name of + T.ImpTop top -> isLoadedParamMod top (meLoadedModules me) + _ -> False return $ JSON.object [ "module" .= pretty name , "parameterized" .= parameterized ] diff --git a/tests/docstrings/T04.cry b/tests/docstrings/T04.cry new file mode 100644 index 000000000..81d1ada85 --- /dev/null +++ b/tests/docstrings/T04.cry @@ -0,0 +1,11 @@ +module T03 where + +/** + * Only a subset of REPL commands work in docstrings + * + * ```repl + * :load AFile.cry + * ``` + */ +a : Bit +a = True diff --git a/tests/docstrings/T04.icry b/tests/docstrings/T04.icry new file mode 100644 index 000000000..435ca0398 --- /dev/null +++ b/tests/docstrings/T04.icry @@ -0,0 +1,2 @@ +:m T04 +:check-docstrings diff --git a/tests/docstrings/T04.icry.stdout b/tests/docstrings/T04.icry.stdout new file mode 100644 index 000000000..f07a45361 --- /dev/null +++ b/tests/docstrings/T04.icry.stdout @@ -0,0 +1,7 @@ +Loading module Cryptol +Loading module Cryptol +Loading module T03 + +:load AFile.cry +Unknown command +Successes: 0, Failures: 1 From 17e8366d965163bfce0da53095a063cdf2dff7f2 Mon Sep 17 00:00:00 2001 From: Eric Mertens Date: Wed, 17 Jul 2024 08:40:10 -0700 Subject: [PATCH 07/12] Generalize isLoaded* to handle ImpName --- .../src/CryptolServer/FocusedModule.hs | 5 +- src/Cryptol/ModuleSystem/Env.hs | 51 +++++++++++++++---- src/Cryptol/ModuleSystem/Monad.hs | 2 +- src/Cryptol/REPL/Monad.hs | 5 +- src/Cryptol/Utils/Ident.hs | 2 +- 5 files changed, 45 insertions(+), 20 deletions(-) diff --git a/cryptol-remote-api/src/CryptolServer/FocusedModule.hs b/cryptol-remote-api/src/CryptolServer/FocusedModule.hs index 238a07704..52e38857c 100644 --- a/cryptol-remote-api/src/CryptolServer/FocusedModule.hs +++ b/cryptol-remote-api/src/CryptolServer/FocusedModule.hs @@ -28,10 +28,7 @@ focusedModule _ = Nothing -> return $ JSON.object [ "module" .= JSON.Null ] Just name -> - do let parameterized = - case name of - T.ImpTop top -> isLoadedParamMod top (meLoadedModules me) - _ -> False + do let parameterized = isLoadedParamMod name (meLoadedModules me) return $ JSON.object [ "module" .= pretty name , "parameterized" .= parameterized ] diff --git a/src/Cryptol/ModuleSystem/Env.hs b/src/Cryptol/ModuleSystem/Env.hs index 49a9899f5..f17e78411 100644 --- a/src/Cryptol/ModuleSystem/Env.hs +++ b/src/Cryptol/ModuleSystem/Env.hs @@ -195,7 +195,7 @@ initialModuleEnv = do -- | Try to focus a loaded module in the module environment. focusModule :: ModName -> ModuleEnv -> Maybe ModuleEnv focusModule n me = do - guard (isLoaded n (meLoadedModules me)) + guard (isLoaded (ImpTop n) (meLoadedModules me)) return me { meFocusedModule = Just (ImpTop n) } -- | Get a list of all the loaded modules. Each module in the @@ -489,16 +489,45 @@ type LoadedSignature = LoadedModuleG T.ModParamNames -- | Has this module been loaded already. -isLoaded :: ModName -> LoadedModules -> Bool -isLoaded mn lm = mn `Set.member` getLoadedNames lm +isLoaded :: ImpName Name -> LoadedModules -> Bool +isLoaded (ImpTop mn) lm = mn `Set.member` getLoadedNames lm +isLoaded (ImpNested nn) lm = any (check . lmModule) (getLoadedModules lm) + where + check :: T.ModuleG a -> Bool + check m = + Map.member nn (T.mSubmodules m) || + Map.member nn (T.mSignatures m) || + Map.member nn (T.mSubmodules m) || + any check (T.mFunctors m) -- | Is this a loaded parameterized module. -isLoadedParamMod :: ModName -> LoadedModules -> Bool -isLoadedParamMod mn ln = any ((mn ==) . lmName) (lmLoadedParamModules ln) +isLoadedParamMod :: ImpName Name -> LoadedModules -> Bool +isLoadedParamMod (ImpTop mn) lm = any ((mn ==) . lmName) (lmLoadedParamModules lm) +isLoadedParamMod (ImpNested n) lm = + any (check1 . lmModule) (lmLoadedModules lm) || + any (check2 . lmModule) (lmLoadedParamModules lm) + where + -- We haven't crossed into a parameterized functor yet + check1 m = Map.member n (T.mFunctors m) + || any check2 (T.mFunctors m) + + -- We're inside a parameterized module and are finished as soon as we have containment + check2 :: T.ModuleG a -> Bool + check2 m = + Map.member n (T.mSubmodules m) || + Map.member n (T.mSignatures m) || + Map.member n (T.mFunctors m) || + any check2 (T.mFunctors m) -- | Is this a loaded interface module. -isLoadedInterface :: ModName -> LoadedModules -> Bool -isLoadedInterface mn ln = any ((mn ==) . lmName) (lmLoadedSignatures ln) +isLoadedInterface :: ImpName Name -> LoadedModules -> Bool +isLoadedInterface (ImpTop mn) ln = any ((mn ==) . lmName) (lmLoadedSignatures ln) +isLoadedInterface (ImpNested nn) ln = any (check . lmModule) (getLoadedModules ln) + where + check :: T.ModuleG a -> Bool + check m = + Map.member nn (T.mSignatures m) || + any check (T.mFunctors m) -- | Return the set of type parameters (@'Set' 'T.TParam'@) and definitions -- (@'Set' 'Name'@) from the supplied 'LoadedModules' value that another @@ -520,8 +549,8 @@ loadedParamModDeps lm a = (badTs, bad) -- XXX: Changes if focusing on nested modules GlobalName _ I.OrigName { ogModule = I.TopModule m } - | isLoadedParamMod m lm -> Set.insert nm bs - | isLoadedInterface m lm -> Set.insert nm bs + | isLoadedParamMod (ImpTop m) lm -> Set.insert nm bs + | isLoadedInterface (ImpTop m) lm -> Set.insert nm bs _ -> bs @@ -551,7 +580,7 @@ addLoadedSignature :: ModName -> T.ModParamNames -> LoadedModules -> LoadedModules addLoadedSignature path ident fi nameEnv nm si lm - | isLoaded nm lm = lm + | isLoaded (ImpTop nm) lm = lm | otherwise = lm { lmLoadedSignatures = loaded : lmLoadedSignatures lm } where loaded = LoadedModule @@ -573,7 +602,7 @@ addLoadedModule :: Maybe ForeignSrc -> T.Module -> LoadedModules -> LoadedModules addLoadedModule path ident fi nameEnv fsrc tm lm - | isLoaded (T.mName tm) lm = lm + | isLoaded (ImpTop (T.mName tm)) lm = lm | T.isParametrizedModule tm = lm { lmLoadedParamModules = loaded : lmLoadedParamModules lm } | otherwise = lm { lmLoadedModules = diff --git a/src/Cryptol/ModuleSystem/Monad.hs b/src/Cryptol/ModuleSystem/Monad.hs index 78d939d53..90e1193dd 100644 --- a/src/Cryptol/ModuleSystem/Monad.hs +++ b/src/Cryptol/ModuleSystem/Monad.hs @@ -433,7 +433,7 @@ getLoadedMaybe mn = ModuleT $ isLoaded :: P.ModName -> ModuleM Bool isLoaded mn = do env <- ModuleT get - pure (MEnv.isLoaded mn (meLoadedModules env)) + pure (MEnv.isLoaded (T.ImpTop mn) (meLoadedModules env)) loadingImport :: Located P.Import -> ModuleM a -> ModuleM a loadingImport = loading . FromImport diff --git a/src/Cryptol/REPL/Monad.hs b/src/Cryptol/REPL/Monad.hs index fefc91d6e..7fa871b89 100644 --- a/src/Cryptol/REPL/Monad.hs +++ b/src/Cryptol/REPL/Monad.hs @@ -240,11 +240,10 @@ mkPrompt rw case lFocus =<< eLoadedMod rw of Nothing -> show (pp I.preludeName) Just m - | M.isLoadedParamMod top loaded -> modName ++ "(parameterized)" - | M.isLoadedInterface top loaded -> modName ++ "(interface)" + | M.isLoadedParamMod m loaded -> modName ++ "(parameterized)" + | M.isLoadedInterface m loaded -> modName ++ "(interface)" | otherwise -> modName where - top = M.impNameTopModule m modName = pretty m loaded = M.meLoadedModules (eModuleEnv rw) diff --git a/src/Cryptol/Utils/Ident.hs b/src/Cryptol/Utils/Ident.hs index be34f9fd4..c63423348 100644 --- a/src/Cryptol/Utils/Ident.hs +++ b/src/Cryptol/Utils/Ident.hs @@ -101,7 +101,7 @@ data Namespace = NSValue allNamespaces :: [Namespace] allNamespaces = [ minBound .. maxBound ] --- | Idnetifies a possibly nested module +-- | Identifies a possibly nested module data ModPath = TopModule ModName | Nested ModPath Ident deriving (Eq,Ord,Show,Generic,NFData) From 551219fabc8ca0067987606fc02ec3c474c9ca68 Mon Sep 17 00:00:00 2001 From: Eric Mertens Date: Wed, 17 Jul 2024 09:32:27 -0700 Subject: [PATCH 08/12] Update CrashCourse.tex now that more commands are checked --- docs/ProgrammingCryptol/crashCourse/CrashCourse.tex | 9 ++++----- 1 file changed, 4 insertions(+), 5 deletions(-) diff --git a/docs/ProgrammingCryptol/crashCourse/CrashCourse.tex b/docs/ProgrammingCryptol/crashCourse/CrashCourse.tex index 9669950cb..562e19d2e 100644 --- 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 :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 From 70fc3aff94fe7582dc7cebd192b5ee8f81faa649 Mon Sep 17 00:00:00 2001 From: Eric Mertens Date: Wed, 17 Jul 2024 10:50:08 -0700 Subject: [PATCH 09/12] Require repl and convert \r\n to \n in lexer --- cryptol-remote-api/src/CryptolServer/FocusedModule.hs | 1 - src/Cryptol/Parser/LexerUtils.hs | 5 ++++- src/Cryptol/REPL/Command.hs | 2 +- tests/docstrings/T01.cry | 4 ++-- tests/docstrings/T02.cry | 7 ++++--- tests/docstrings/T04.cry | 5 +++++ 6 files changed, 16 insertions(+), 8 deletions(-) diff --git a/cryptol-remote-api/src/CryptolServer/FocusedModule.hs b/cryptol-remote-api/src/CryptolServer/FocusedModule.hs index 52e38857c..4ea5a6c39 100644 --- a/cryptol-remote-api/src/CryptolServer/FocusedModule.hs +++ b/cryptol-remote-api/src/CryptolServer/FocusedModule.hs @@ -11,7 +11,6 @@ import Data.Aeson as JSON import Cryptol.ModuleSystem (meFocusedModule, meLoadedModules) import Cryptol.ModuleSystem.Env (isLoadedParamMod) -import qualified Cryptol.TypeCheck.AST as T import Cryptol.Utils.PP import CryptolServer diff --git a/src/Cryptol/Parser/LexerUtils.hs b/src/Cryptol/Parser/LexerUtils.hs index 41bb3ff0c..000ae8be6 100644 --- a/src/Cryptol/Parser/LexerUtils.hs +++ b/src/Cryptol/Parser/LexerUtils.hs @@ -342,7 +342,10 @@ alexGetByte i = do (c,rest) <- T.uncons (input i) let i' = i { alexPos = move (alexPos i) c, input = rest } b = byteForChar c - return (b,i') + -- treat \r\n as \n + case (b, alexGetByte i') of + (13, skip@(Just (10, _))) -> skip + _ -> pure (b, i') data Layout = Layout | NoLayout diff --git a/src/Cryptol/REPL/Command.hs b/src/Cryptol/REPL/Command.hs index 722ce2194..da2cc8c0f 100644 --- a/src/Cryptol/REPL/Command.hs +++ b/src/Cryptol/REPL/Command.hs @@ -2012,7 +2012,7 @@ extractCodeBlocks raw = go [] cleanLines go finished (x:xs) | (ticks, lang) <- T.span ('`' ==) x , 3 <= T.length ticks - = if lang `elem` ["", "repl"] + = if lang == "repl" then keep finished ticks [] xs else skip finished ticks xs | otherwise = go finished xs diff --git a/tests/docstrings/T01.cry b/tests/docstrings/T01.cry index 442f3f614..13fdefc00 100644 --- a/tests/docstrings/T01.cry +++ b/tests/docstrings/T01.cry @@ -3,14 +3,14 @@ module T01 where submodule Sub where /** * This verifies that pp shadows the outer definition - * ``` + * ```repl * :check pp * ``` */ pp = True /** - * ``` + * ```repl * :check ~ pp * ``` */ diff --git a/tests/docstrings/T02.cry b/tests/docstrings/T02.cry index 36c44360d..36e55fcb3 100644 --- a/tests/docstrings/T02.cry +++ b/tests/docstrings/T02.cry @@ -11,9 +11,10 @@ submodule F where c = 1 /** - * ``` + * Longer code block delimiters are supported + * ````repl * :exhaust p - * ``` + * ```` */ p x = c + x == x + c @@ -21,7 +22,7 @@ submodule F7 = submodule F where type n = 7 /** - * ``` + * ```repl * let y = 20 * :check f 10 == 20 * ``` diff --git a/tests/docstrings/T04.cry b/tests/docstrings/T04.cry index 81d1ada85..066d7bdb8 100644 --- a/tests/docstrings/T04.cry +++ b/tests/docstrings/T04.cry @@ -6,6 +6,11 @@ module T03 where * ```repl * :load AFile.cry * ``` + * + * Stuff not marked repl is ignored + * ``` + * garbage + * ``` */ a : Bit a = True From 77d00963933424f84780b6261096ef8dd99d456b Mon Sep 17 00:00:00 2001 From: Eric Mertens Date: Wed, 17 Jul 2024 11:13:32 -0700 Subject: [PATCH 10/12] replace \r\n earlier, alexGetByte is too late --- src/Cryptol/ModuleSystem/Base.hs | 3 ++- src/Cryptol/Parser/LexerUtils.hs | 5 +---- 2 files changed, 3 insertions(+), 5 deletions(-) diff --git a/src/Cryptol/ModuleSystem/Base.hs b/src/Cryptol/ModuleSystem/Base.hs index 6f050d9b0..63c91bb39 100644 --- 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 @@ -179,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 diff --git a/src/Cryptol/Parser/LexerUtils.hs b/src/Cryptol/Parser/LexerUtils.hs index 000ae8be6..aa426daa9 100644 --- a/src/Cryptol/Parser/LexerUtils.hs +++ b/src/Cryptol/Parser/LexerUtils.hs @@ -342,10 +342,7 @@ alexGetByte i = do (c,rest) <- T.uncons (input i) let i' = i { alexPos = move (alexPos i) c, input = rest } b = byteForChar c - -- treat \r\n as \n - case (b, alexGetByte i') of - (13, skip@(Just (10, _))) -> skip - _ -> pure (b, i') + pure (b, i') data Layout = Layout | NoLayout From 2c674ac87f38dae835d6778430a95d1bc3e4e1e2 Mon Sep 17 00:00:00 2001 From: Eric Mertens Date: Wed, 17 Jul 2024 13:11:50 -0700 Subject: [PATCH 11/12] Demonstrate that docstrings on submodules run in the correct context --- tests/docstrings/T01.cry | 7 +++++++ tests/docstrings/T01.icry.stdout | 7 ++++++- 2 files changed, 13 insertions(+), 1 deletion(-) diff --git a/tests/docstrings/T01.cry b/tests/docstrings/T01.cry index 13fdefc00..a24cada1b 100644 --- a/tests/docstrings/T01.cry +++ b/tests/docstrings/T01.cry @@ -1,5 +1,12 @@ module T01 where +/** + * docstrings on submodules get run inside the scope of the submodule + * + * ```repl + * :exhaust pp && pp + * ``` + */ submodule Sub where /** * This verifies that pp shadows the outer definition diff --git a/tests/docstrings/T01.icry.stdout b/tests/docstrings/T01.icry.stdout index 4e7facdf0..260566ab3 100644 --- a/tests/docstrings/T01.icry.stdout +++ b/tests/docstrings/T01.icry.stdout @@ -12,4 +12,9 @@ Using exhaustive testing. Testing... Passed 1 tests. Q.E.D. -Successes: 2, Failures: 0 +:exhaust pp && pp +Using exhaustive testing. +Testing... Passed 1 tests. +Q.E.D. + +Successes: 3, Failures: 0 From 05b7691792dbcdfbf37e864319fdf425ea165bdb Mon Sep 17 00:00:00 2001 From: Eric Mertens Date: Thu, 18 Jul 2024 13:08:05 -0700 Subject: [PATCH 12/12] Handle focusing on a functor submodule --- CHANGES.md | 18 ++++++++++++++++-- src/Cryptol/ModuleSystem/Env.hs | 21 ++++++++++++--------- 2 files changed, 28 insertions(+), 11 deletions(-) diff --git a/CHANGES.md b/CHANGES.md index 7b7013d26..ad2754afc 100644 --- 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 @@ -19,11 +18,26 @@ * 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. "repl" and unlabeled code blocks are evaluated in a local + 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/src/Cryptol/ModuleSystem/Env.hs b/src/Cryptol/ModuleSystem/Env.hs index f17e78411..e37785b62 100644 --- a/src/Cryptol/ModuleSystem/Env.hs +++ b/src/Cryptol/ModuleSystem/Env.hs @@ -58,7 +58,6 @@ import Prelude.Compat import Cryptol.Utils.Panic(panic) import Cryptol.Utils.PP(pp) -import Cryptol.TypeCheck.AST (Submodule(smIface)) -- Module Environment ---------------------------------------------------------- @@ -273,22 +272,26 @@ instance Monoid ModContext where , mctxNameDisp = R.toNameDisp mempty } +findEnv :: Name -> Iface -> T.ModuleG a -> Maybe (R.NamingEnv, Set Name) +findEnv n iface m + | Just sm <- Map.lookup n (T.mSubmodules m) = Just (T.smInScope sm, ifsPublic (T.smIface sm)) + | Just fn <- Map.lookup n (T.mFunctors m) = + case Map.lookup n (ifFunctors (ifDefines iface)) of + Nothing -> panic "findEnv" ["Submodule functor not present in interface"] + Just d -> Just (T.mInScope fn, ifsPublic (ifNames d)) + | otherwise = asum (fmap (findEnv n iface) (Map.elems (T.mFunctors m))) modContextOf :: ImpName Name -> ModuleEnv -> Maybe ModContext modContextOf (ImpNested name) me = do mname <- nameTopModuleMaybe name lm <- lookupModule mname me - sm <- Map.lookup name (T.mSubmodules (lmModule lm)) -- TODO: support uninstantiated functors - let - localNames = T.smInScope sm - - -- XXX: do we want only public ones here? + (localNames, exported) <- findEnv name (lmInterface lm) (lmModule lm) + let -- XXX: do we want only public ones here? loadedDecls = map (ifDefines . lmInterface) $ getLoadedModules (meLoadedModules me) - pure ModContext { mctxParams = NoParams - , mctxExported = ifsPublic (smIface sm) + , mctxExported = exported , mctxDecls = mconcat (ifDefines (lmInterface lm) : loadedDecls) , mctxNames = localNames , mctxNameDisp = R.toNameDisp localNames @@ -510,7 +513,7 @@ isLoadedParamMod (ImpNested n) lm = -- We haven't crossed into a parameterized functor yet check1 m = Map.member n (T.mFunctors m) || any check2 (T.mFunctors m) - + -- We're inside a parameterized module and are finished as soon as we have containment check2 :: T.ModuleG a -> Bool check2 m =