Gracefully skip checking docstrings on interface modules (#1734)

GaloisInc · Aug 20, 2024 · 688e478 · 688e478
1 parent cc3b3fb
commit 688e478
Show file tree

Hide file tree

Showing 5 changed files with 58 additions and 34 deletions.
diff --git a/cryptol-remote-api/src/CryptolServer/CheckDocstrings.hs b/cryptol-remote-api/src/CryptolServer/CheckDocstrings.hs
@@ -43,34 +43,36 @@ checkDocstrings CheckDocstringsParams = do
   ln <- case M.meFocusedModule env of
           Just (ImpTop n) -> pure n
           _ -> raise noModule
-  m <- case M.lookupModule ln env of
-         Nothing -> raise (moduleNotLoaded ln)
-         Just m -> pure m
-
-  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
+  case M.lookupModule ln env of
+    Nothing ->
+      case M.lookupSignature ln env of
+        Nothing -> raise (moduleNotLoaded ln)
+        Just{} -> pure (CheckDocstringsResult []) -- can't be checked directly
+    Just m ->
+      if T.isParametrizedModule (M.lmdModule (M.lmData m)) then
+        pure (CheckDocstringsResult []) -- can't be checked directly
+      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
@@ -2192,12 +2192,17 @@ checkDocStringsCmd input
 
 
     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 }
+    checkModName mn =
+     do env <- getModuleEnv
+        case M.lookupModule mn env of
+          Nothing ->
+            case M.lookupSignature mn env of
+              Nothing ->
+               do rPutStrLn ("Module " ++ show input ++ " is not loaded")
+                  pure emptyCommandResult { crSuccess = False }
+              Just{} ->
+               do rPutStrLn "Skipping docstrings on interface module"
+                  pure emptyCommandResult
 
           Just fe
             | T.isParametrizedModule (M.lmdModule (M.lmData fe)) -> do

diff --git a/tests/docstrings/T11.cry b/tests/docstrings/T11.cry
@@ -0,0 +1,11 @@
+interface module I where
+
+/** Interfaces don't contain definitions. We'll need to wait to check
+ * them when they are paired up with a module in the context of a
+ * functor instantiation.
+ *
+ * ```repl
+ * :check \x y z -> add x (add y z) == add (add x y) z
+ * ```
+ */
+add : [8] -> [8] -> [8]
diff --git a/tests/docstrings/T11.icry b/tests/docstrings/T11.icry
@@ -0,0 +1,2 @@
+:m T11
+:check-docstrings
diff --git a/tests/docstrings/T11.icry.stdout b/tests/docstrings/T11.icry.stdout
@@ -0,0 +1,4 @@
+Loading module Cryptol
+Loading module Cryptol
+Loading interface module I
+Skipping docstrings on interface module