Merge pull request #1767 from GaloisInc/1766-interface-docstrings

Allow doc comments on interface modules
GaloisInc · Nov 26, 2024 · 4485d70 · 4485d70
2 parents 56a93da + e032c78
commit 4485d70
Show file tree

Hide file tree

Showing 5 changed files with 20 additions and 5 deletions.
diff --git a/src/Cryptol/Parser.y b/src/Cryptol/Parser.y
@@ -173,8 +173,8 @@ import Paths_cryptol
 top_module :: { [Module PName] }
   : mbDoc 'module' module_def {% mkTopMods $1 $3 }
   | 'v{' vmod_body 'v}'       {% mkAnonymousModule $2 }
-  | 'interface' 'module' modName 'where' 'v{' sig_body 'v}'
-                              { mkTopSig $3 $6 }
+  | mbDoc 'interface' 'module' modName 'where' 'v{' sig_body 'v}'
+                              { mkTopSig $1 $4 $7 }
 
 module_def :: { Module PName }
 

diff --git a/src/Cryptol/Parser/ParserUtils.hs b/src/Cryptol/Parser/ParserUtils.hs
@@ -1364,12 +1364,12 @@ mkTopMods doc m =
  do (m', ms) <- desugarMod m { mDocTop = doc }
     pure (ms ++ [m'])
 
-mkTopSig :: Located ModName -> Signature PName -> [Module PName]
-mkTopSig nm sig =
+mkTopSig :: Maybe (Located Text) -> Located ModName -> Signature PName -> [Module PName]
+mkTopSig doc nm sig =
   [ Module { mName    = nm
            , mDef     = InterfaceModule sig
            , mInScope = mempty
-           , mDocTop  = Nothing
+           , mDocTop  = doc
            }
   ]
 

diff --git a/tests/docstrings/T12.cry b/tests/docstrings/T12.cry
@@ -0,0 +1,9 @@
+/** Doc strings on interfaces apply to the interface context.
+ *
+ * ```repl
+ * :check \x y z -> add x (add y z) == add (add x y) z
+ * ```
+ */
+interface module I where
+
+add : [8] -> [8] -> [8]
diff --git a/tests/docstrings/T12.icry b/tests/docstrings/T12.icry
@@ -0,0 +1,2 @@
+:m T12
+:check-docstrings
diff --git a/tests/docstrings/T12.icry.stdout b/tests/docstrings/T12.icry.stdout
@@ -0,0 +1,4 @@
+Loading module Cryptol
+Loading module Cryptol
+Loading interface module I
+Skipping docstrings on interface module