Gracefully skip docstrings on top-level functors (#1730)

GaloisInc · Aug 13, 2024 · 2fb70e6 · 2fb70e6
1 parent 1f15ca6
commit 2fb70e6
Show file tree

Hide file tree

Showing 5 changed files with 60 additions and 39 deletions.
diff --git a/cryptol-remote-api/src/CryptolServer/CheckDocstrings.hs b/cryptol-remote-api/src/CryptolServer/CheckDocstrings.hs
@@ -24,6 +24,7 @@ import CryptolServer.Exceptions (noModule, moduleNotLoaded)
 import qualified Cryptol.REPL.Monad as REPL
 import Cryptol.Utils.Logger (quietLogger)
 import Cryptol.Parser.AST (ImpName(..))
+import qualified Cryptol.TypeCheck.AST as T
 import qualified System.Random.TF as TF
 import qualified Cryptol.Symbolic.SBV as SBV
 import Cryptol.REPL.Monad (mkUserEnv, userOptions)
@@ -45,27 +46,31 @@ checkDocstrings CheckDocstringsParams = do
   m <- case M.lookupModule ln env of
          Nothing -> raise (moduleNotLoaded ln)
          Just m -> pure m
-  solver <- getTCSolver
-  cfg <- getTCSolverConfig
-  liftIO $
-   do rng <- TF.newTFGen
-      rwRef <- newIORef REPL.RW
-        { REPL.eLoadedMod        = Nothing
-        , REPL.eEditFile         = Nothing
-        , REPL.eContinue         = True
-        , REPL.eIsBatch          = False
-        , REPL.eModuleEnv        = env
-        , REPL.eUserEnv          = mkUserEnv userOptions
-        , REPL.eLogger           = quietLogger
-        , REPL.eCallStacks       = False
-        , REPL.eUpdateTitle      = return ()
-        , REPL.eProverConfig     = Left SBV.defaultProver
-        , REPL.eTCConfig         = cfg
-        , REPL.eTCSolver         = Just solver
-        , REPL.eTCSolverRestarts = 0
-        , REPL.eRandomGen        = rng
-        }
-      REPL.unREPL (CheckDocstringsResult <$> checkDocStrings m) rwRef
+
+  if T.isParametrizedModule (M.lmdModule (M.lmData m)) then
+    pure (CheckDocstringsResult [])
+  else do
+    solver <- getTCSolver
+    cfg <- getTCSolverConfig
+    liftIO $
+     do rng <- TF.newTFGen
+        rwRef <- newIORef REPL.RW
+          { REPL.eLoadedMod        = Nothing
+          , REPL.eEditFile         = Nothing
+          , REPL.eContinue         = True
+          , REPL.eIsBatch          = False
+          , REPL.eModuleEnv        = env
+          , REPL.eUserEnv          = mkUserEnv userOptions
+          , REPL.eLogger           = quietLogger
+          , REPL.eCallStacks       = False
+          , REPL.eUpdateTitle      = return ()
+          , REPL.eProverConfig     = Left SBV.defaultProver
+          , REPL.eTCConfig         = cfg
+          , REPL.eTCSolver         = Just solver
+          , REPL.eTCSolverRestarts = 0
+          , REPL.eRandomGen        = rng
+          }
+        REPL.unREPL (CheckDocstringsResult <$> checkDocStrings m) rwRef
 
 newtype CheckDocstringsResult = CheckDocstringsResult [DocstringResult]
 

diff --git a/src/Cryptol/REPL/Command.hs b/src/Cryptol/REPL/Command.hs
@@ -2199,21 +2199,26 @@ checkDocStringsCmd input
             rPutStrLn ("Module " ++ show input ++ " is not loaded")
             pure emptyCommandResult { crSuccess = False }
 
-          Just fe -> do
-            results <- checkDocStrings fe
-            let (successes, nofences, failures) = countOutcomes [concat (drFences r) | r <- results]
-
-            forM_ results $ \dr ->
-              unless (null (drFences dr)) $
-               do rPutStrLn ""
-                  rPutStrLn ("\nChecking " ++ show (pp (drName dr)))
-                  forM_ (drFences dr) $ \fence ->
-                    forM_ fence $ \line -> do
-                      rPutStrLn ""
-                      rPutStrLn (T.unpack (srInput line))
-                      rPutStr (srLog line)
-
-            rPutStrLn ""
-            rPutStrLn ("Successes: " ++ show successes ++ ", No fences: " ++ show nofences ++ ", Failures: " ++ show failures)
-
-            pure emptyCommandResult { crSuccess = failures == 0 }
+          Just fe
+            | T.isParametrizedModule (M.lmdModule (M.lmData fe)) -> do
+              rPutStrLn "Skipping docstrings on parameterized module"
+              pure emptyCommandResult
+
+            | otherwise -> do
+              results <- checkDocStrings fe
+              let (successes, nofences, failures) = countOutcomes [concat (drFences r) | r <- results]
+
+              forM_ results $ \dr ->
+                unless (null (drFences dr)) $
+                 do rPutStrLn ""
+                    rPutStrLn ("\nChecking " ++ show (pp (drName dr)))
+                    forM_ (drFences dr) $ \fence ->
+                      forM_ fence $ \line -> do
+                        rPutStrLn ""
+                        rPutStrLn (T.unpack (srInput line))
+                        rPutStr (srLog line)
+
+              rPutStrLn ""
+              rPutStrLn ("Successes: " ++ show successes ++ ", No fences: " ++ show nofences ++ ", Failures: " ++ show failures)
+
+              pure emptyCommandResult { crSuccess = failures == 0 }
diff --git a/tests/docstrings/T09.cry b/tests/docstrings/T09.cry
@@ -0,0 +1,4 @@
+module T09 where
+
+parameter
+  type n : #
diff --git a/tests/docstrings/T09.icry b/tests/docstrings/T09.icry
@@ -0,0 +1,2 @@
+:m T09
+:check-docstrings
diff --git a/tests/docstrings/T09.icry.stdout b/tests/docstrings/T09.icry.stdout
@@ -0,0 +1,5 @@
+Loading module Cryptol
+Loading module Cryptol
+Loading interface module `parameter` interface of T09
+Loading module T09
+Skipping docstrings on parameterized module