From e032c7856e0c8d5b253e5b51af462250aece039c Mon Sep 17 00:00:00 2001
From: David Holland <dholland@galois.com>
Date: Thu, 14 Nov 2024 15:10:26 -0500
Subject: [PATCH] Allow doc comments on interface modules.

For the record, this change was rebased across the CI fixes from #1768.
---
 src/Cryptol/Parser.y              | 4 ++--
 src/Cryptol/Parser/ParserUtils.hs | 6 +++---
 tests/docstrings/T12.cry          | 9 +++++++++
 tests/docstrings/T12.icry         | 2 ++
 tests/docstrings/T12.icry.stdout  | 4 ++++
 5 files changed, 20 insertions(+), 5 deletions(-)
 create mode 100644 tests/docstrings/T12.cry
 create mode 100644 tests/docstrings/T12.icry
 create mode 100644 tests/docstrings/T12.icry.stdout

diff --git a/src/Cryptol/Parser.y b/src/Cryptol/Parser.y
index 8543b0a8c..f31d6b7ea 100644
--- 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
index de989e330..b5d92f81f 100644
--- 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
new file mode 100644
index 000000000..b730eba4d
--- /dev/null
+++ 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
new file mode 100644
index 000000000..321186601
--- /dev/null
+++ 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
new file mode 100644
index 000000000..9ffab7d08
--- /dev/null
+++ 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