Functor docstrings (#1726)

* Fix docstring behaviors around functors

- Don't duplicate docstrings onto modules generated by the desugarer
- Combine docstrings when instantiating a functor to preserve both the instance and the instantiated documentation

* Suppress :check-docstring output for definitions without fences

src/Cryptol/ModuleSystem/Interface.hs

@@ -77,7 +77,7 @@ data IfaceNames name = IfaceNames
   , ifsNested   :: Set Name   -- ^ Things nested in this module
   , ifsDefines  :: Set Name   -- ^ Things defined in this module
   , ifsPublic   :: Set Name   -- ^ Subset of `ifsDefines` that is public
-  , ifsDoc      :: !(Maybe Text) -- ^ Documentation
+  , ifsDoc      :: ![Text]    -- ^ Documentation: more specific to least specific
   } deriving (Show, Generic, NFData, Functor)
 
 -- | Is this interface for a functor.
@@ -90,7 +90,7 @@ emptyIface nm = Iface
                            , ifsDefines = mempty
                            , ifsPublic  = mempty
                            , ifsNested  = mempty
-                           , ifsDoc     = Nothing
+                           , ifsDoc     = mempty
                            }
   , ifParams  = mempty
   , ifDefines = mempty

src/Cryptol/Parser.y

@@ -296,8 +296,8 @@ vtop_decl               :: { [TopDecl PName] }
   | private_decls          { $1                                               }
   | mbDoc 'interface' 'constraint' type {% mkInterfaceConstraint $1 $4 }
   | parameter_decls        { [ $1 ]                                       }
-  | mbDoc 'submodule'
-    module_def             {% ((:[]) . exportModule $1) `fmap` mkNested $3 }
+  | mbDoc 'submodule' module_def
+                           {% ((:[]) . exportModule $1) `fmap` mkNested $3 }
 
   | mbDoc sig_def          { [mkSigDecl $1 $2]  }
   | mod_param_decl         { [DModParam $1] }

src/Cryptol/Parser/AST.hs

@@ -169,7 +169,8 @@ data ModuleG mname name = Module
     --   Also, for the 'FunctorInstance' case this is not the final result of
     --   the names in scope. The typechecker adds in the names in scope in the
     --   functor, so this will just contain the names in the enclosing scope.
-  , mDoc      :: Maybe (Located Text)
+  , mDocTop   :: Maybe (Located Text)
+  -- ^ only used for top-level modules
   } deriving (Show, Generic, NFData)
 
 
@@ -1455,7 +1456,7 @@ instance NoPos (ModuleG mname name) where
   noPos m = Module { mName      = mName m
                    , mDef       = noPos (mDef m)
                    , mInScope   = mInScope m
-                   , mDoc       = noPos (mDoc m)
+                   , mDocTop    = noPos (mDocTop m)
                    }
 
 instance NoPos (ModuleDefinition name) where

src/Cryptol/Parser/ParserUtils.hs

@@ -1117,7 +1117,7 @@ mkModule :: Located ModName -> [TopDecl PName] -> Module PName
 mkModule nm ds = Module { mName = nm
                         , mDef = NormalModule ds
                         , mInScope = mempty
-                        , mDoc = Nothing
+                        , mDocTop = Nothing
                         }
 
 mkNested :: Module PName -> ParseM (NestedModule PName)
@@ -1139,7 +1139,7 @@ mkSigDecl doc (nm,sig) =
                         Module { mName    = nm
                                , mDef     = InterfaceModule sig
                                , mInScope = mempty
-                               , mDoc     = Nothing
+                               , mDocTop  = Nothing
                                }
            }
 
@@ -1217,7 +1217,7 @@ mkModuleInstanceAnon nm fun ds =
   Module { mName    = nm
          , mDef     = FunctorInstance fun (DefaultInstAnonArg ds) mempty
          , mInScope = mempty
-         , mDoc     = Nothing
+         , mDocTop  = Nothing
          }
 
 mkModuleInstance ::
@@ -1229,7 +1229,7 @@ mkModuleInstance m f as =
   Module { mName    = m
          , mDef     = FunctorInstance f as emptyModuleInstance
          , mInScope = mempty
-         , mDoc     = Nothing
+         , mDocTop  = Nothing
          }
 
 
@@ -1360,14 +1360,16 @@ mkImport loc impName optInst mbAs mbImportSpec optImportWhere doc =
 
 
 mkTopMods :: Maybe (Located Text) -> Module PName -> ParseM [Module PName]
-mkTopMods doc m = desugarMod m { mDoc = doc }
+mkTopMods doc m =
+ do (m', ms) <- desugarMod m { mDocTop = doc }
+    pure (ms ++ [m'])
 
 mkTopSig :: Located ModName -> Signature PName -> [Module PName]
 mkTopSig nm sig =
   [ Module { mName    = nm
            , mDef     = InterfaceModule sig
            , mInScope = mempty
-           , mDoc     = Nothing
+           , mDocTop  = Nothing
            }
   ]
 
@@ -1392,8 +1394,9 @@ instance MkAnon PName where
                 . getIdent
   toImpName     = ImpNested
 
-
-desugarMod :: MkAnon name => ModuleG name PName -> ParseM [ModuleG name PName]
+-- | Desugar a module returning first the updated original module and a
+-- list of any new modules generated by desugaring.
+desugarMod :: MkAnon name => ModuleG name PName -> ParseM (ModuleG name PName, [ModuleG name PName])
 desugarMod mo =
   case mDef mo of
 
@@ -1411,16 +1414,20 @@ desugarMod mo =
          let i      = mkAnon AnonArg (thing (mName mo))
              nm     = Located { srcRange = srcRange (mName mo), thing = i }
              as'    = DefaultInstArg (ModuleArg . toImpName <$> nm)
-         pure [ Module
-                  { mName = nm, mDef  = NormalModule lds', mInScope = mempty, mDoc = mDoc mo }
-              , mo { mDef = FunctorInstance f as' mempty }
-              ]
+         pure ( mo { mDef = FunctorInstance f as' mempty }
+              , [ Module
+                    { mName = nm
+                    , mDef  = NormalModule lds'
+                    , mInScope = mempty
+                    , mDocTop = Nothing
+                    }]
+              )
 
     NormalModule ds ->
       do (newMs, newDs) <- desugarTopDs (mName mo) ds
-         pure (newMs ++ [ mo { mDef = NormalModule newDs } ])
+         pure (mo {mDef = NormalModule newDs }, newMs)
 
-    _ -> pure [mo]
+    _ -> pure (mo, [])
 
 
 desugarTopDs ::
@@ -1463,7 +1470,7 @@ desugarTopDs ownerName = go emptySig
              pure ( [ Module { mName = nm
                              , mDef = InterfaceModule sig
                              , mInScope = mempty
-                             , mDoc = Nothing
+                             , mDocTop = Nothing
                              }
                      ]
                   , [ DModParam
@@ -1498,8 +1505,14 @@ desugarTopDs ownerName = go emptySig
           DParamDecl _ ds' -> cont [] (jnSig ds' sig)
 
           DModule tl | NestedModule mo <- tlValue tl ->
-            do ms <- desugarMod mo
-               cont [ DModule tl { tlValue = NestedModule m } | m <- ms ] sig
+            do (mo', ms) <- desugarMod mo
+               cont ([ DModule TopLevel
+                          { tlExport = tlExport tl
+                          , tlValue = NestedModule m
+                          , tlDoc = Nothing -- generated modules have no docstrings
+                          }
+                      | m <- ms] ++ [DModule tl { tlValue = NestedModule mo' }])
+                    sig
 
           _ -> cont [d] sig
 
@@ -1508,14 +1521,14 @@ desugarInstImport ::
   ModuleInstanceArgs PName          {- ^ The insantiation -} ->
   ParseM [TopDecl PName]
 desugarInstImport i inst =
-  do ms <- desugarMod
+  do (m, ms) <- desugarMod
            Module { mName    = i { thing = iname }
                   , mDef     = FunctorInstance
                                  (iModule <$> i) inst emptyModuleInstance
                   , mInScope = mempty
-                  , mDoc     = Nothing
+                  , mDocTop  = Nothing
                   }
-     pure (DImport (newImp <$> i) : map modTop ms)
+     pure (DImport (newImp <$> i) : map modTop (ms ++ [m]))
 
   where
   imp = thing i

src/Cryptol/REPL/Command.hs

@@ -2123,14 +2123,14 @@ interpretControls [] = []
 
 -- | The result of running a docstring as attached to a definition
 data DocstringResult = DocstringResult
-  { drName :: P.ImpName T.Name -- ^ The associated definition of the docstring
+  { drName   :: T.DocFor -- ^ The associated definition of the docstring
   , drFences :: [[SubcommandResult]] -- ^ list of fences in this definition's docstring
   }
 
 -- | Check all the code blocks in a given docstring.
 checkDocItem :: T.DocItem -> REPL DocstringResult
 checkDocItem item =
- do xs <- case extractCodeBlocks (fromMaybe "" (T.docText item)) of
+ do xs <- case traverse extractCodeBlocks (T.docText item) of
             Left e -> do
               pure [[SubcommandResult
                 { srInput = T.empty
@@ -2142,7 +2142,7 @@ checkDocItem item =
               Ex.bracket
                 (liftModuleCmd (`M.runModuleM` (M.getFocusedModule <* M.setFocusedModule (T.docModContext item))))
                 (\mb -> liftModuleCmd (`M.runModuleM` M.setMaybeFocusedModule mb))
-                (\_ -> traverse checkBlock bs)
+                (\_ -> traverse checkBlock (concat bs))
     pure DocstringResult
       { drName = T.docFor item
       , drFences = xs
@@ -2210,14 +2210,15 @@ checkDocStringsCmd input
             let (successes, nofences, failures) = countOutcomes [concat (drFences r) | r <- results]
 
             forM_ results $ \dr ->
-             do rPutStrLn ""
-                rPutStrLn ("Checking " ++ show (pp (drName dr)))
-                forM_ (drFences dr) $ \fence ->
-                  forM_ fence $ \line -> do
-                    rPutStrLn ""
-                    rPutStrLn (T.unpack (srInput line))
-                    rPutStr (srLog line)
-
+              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)
 

src/Cryptol/REPL/Help.hs

@@ -8,8 +8,9 @@ import qualified Data.Text as Text
 import Data.Map (Map)
 import qualified Data.Map as Map
 import qualified Data.Set as Set
-import Data.Maybe(fromMaybe)
+import Data.Maybe(fromMaybe, maybeToList)
 import Data.List(intersperse)
+import Data.Foldable (for_)
 import Control.Monad(when,guard,unless,msum,mplus)
 
 import Cryptol.Utils.PP
@@ -93,7 +94,7 @@ ifaceSummary env info =
                       , addV <$> fromD
                       , addM <$> msum [ fromM, fromS, fromF ]
                       ]
-    where
+    where 
     addT (k,d) = ns { msTypes = T.ModTParam { T.mtpName = x
                                             , T.mtpKind = k
                                             , T.mtpDoc  = d
@@ -124,7 +125,7 @@ ifaceSummary env info =
                pure (M.AFunctor, M.ifsDoc (M.ifNames def))
 
     fromS = do def <- Map.lookup x (M.ifSignatures env)
-               pure (M.ASignature, T.mpnDoc def)
+               pure (M.ASignature, maybeToList (T.mpnDoc def))
 
 
 
@@ -144,7 +145,7 @@ showFunctorHelp _env _nameEnv name info =
 showSigHelp ::
   M.IfaceDecls -> NameDisp -> M.Name -> T.ModParamNames -> REPL ()
 showSigHelp _env _nameEnv name info =
-  showSummary M.ASignature name (T.mpnDoc info)
+  showSummary M.ASignature name (maybeToList (T.mpnDoc info))
     emptySummary
       { msTypes = Map.elems (T.mpnTypes info)
       , msVals  = Map.elems (T.mpnFuns info)
@@ -157,7 +158,7 @@ data ModSummary = ModSummary
   , msConstraints :: [T.Prop]
   , msTypes       :: [T.ModTParam]
   , msVals        :: [T.ModVParam]
-  , msMods        :: [ (M.Name, M.ModKind, Maybe Text) ]
+  , msMods        :: [ (M.Name, M.ModKind, [Text]) ]
   }
 
 emptySummary :: ModSummary
@@ -169,7 +170,7 @@ emptySummary = ModSummary
   , msMods        = []
   }
 
-showSummary :: M.ModKind -> M.Name -> Maybe Text -> ModSummary -> REPL ()
+showSummary :: M.ModKind -> M.Name -> [Text] -> ModSummary -> REPL ()
 showSummary k name doc info =
   do rPutStrLn ""
 
@@ -385,11 +386,10 @@ doShowParameterSource i =
     | otherwise       = "Provided by `parameters` declaration."
 
 
-doShowDocString :: Maybe Text -> REPL ()
+doShowDocString :: Foldable f => f Text -> REPL ()
 doShowDocString doc =
-  case doc of
-    Nothing -> pure ()
-    Just d  -> rPutStrLn ('\n' : Text.unpack d)
+  for_ doc $ \d ->
+    rPutStrLn ('\n' : Text.unpack d)
 
 ppFixity :: T.Fixity -> String
 ppFixity f = "Precedence " ++ show (P.fLevel f) ++ ", " ++