Correctly detect top-level parameterized modules in modules() API call (

#1758) Fixes #1756
GaloisInc · Sep 30, 2024 · 1369ce3 · 1369ce3
1 parent 8cd51e8
commit 1369ce3
Show file tree

Hide file tree

Showing 2 changed files with 15 additions and 7 deletions.
diff --git a/cryptol-remote-api/python/tests/cryptol/test_modules.py b/cryptol-remote-api/python/tests/cryptol/test_modules.py
@@ -6,8 +6,8 @@
 class TestModules(unittest.TestCase):
     def test_modules(self):
         connect(verify=False)
-        load_file(str(Path('tests','cryptol','test-files', 'Modules.cry')))
 
+        load_file(str(Path('tests','cryptol','test-files', 'Modules.cry')))
         expected = [
             {'module': 'Cryptol', 'parameterized': False},
             {'module': 'Modules', 'parameterized': False, 'documentation': ['A top-level\ndocstring\n']},
@@ -17,10 +17,17 @@ def test_modules(self):
             {'module': 'Modules::F', 'parameterized': True, 'documentation': ['A functor docstring\n']},
             {'module': 'Modules::F::Q', 'parameterized': True, 'documentation': ['A submodule in a functor docstring\n']},
         ]
-
         names_to_check = modules()
-
         self.assertCountEqual(expected, names_to_check)
+
+        load_file(str(Path('tests','cryptol','test-files', 'Param.cry')))
+        expected = [
+            {'module': 'Param', 'parameterized': True},
+            {'module': 'Cryptol', 'parameterized': False},
+        ]
+        names_to_check = modules()
+        self.assertCountEqual(expected, names_to_check)
+
 
 if __name__ == "__main__":
     unittest.main()
diff --git a/cryptol-remote-api/src/CryptolServer/Modules.hs b/cryptol-remote-api/src/CryptolServer/Modules.hs
@@ -47,11 +47,12 @@ visibleModulesDescr =
   Doc.Paragraph [Doc.Text "List the currently visible (i.e., in scope) module names."]
 
 visibleModules :: VisibleModulesParams -> CryptolCommand [VisibleModuleInfo]
-visibleModules _ = concatMap (moduleToInfos False) . loadedModules <$> getModuleEnv
+visibleModules _ = concatMap moduleToInfos . loadedModules <$> getModuleEnv
 
 
-moduleToInfos :: PP a => Bool -> T.ModuleG a -> [VisibleModuleInfo]
-moduleToInfos p m =
+moduleToInfos :: PP a => T.ModuleG a -> [VisibleModuleInfo]
+moduleToInfos m =
+  let p = isParametrizedModule m in
   ModuleInfo
   { name = show (pp (T.mName m))
   , parameterized = p
@@ -66,7 +67,7 @@ moduleToInfos p m =
   ] ++
   [ x
     | v <- Map.elems (T.mFunctors m)
-    , x <- moduleToInfos True v
+    , x <- moduleToInfos v
   ]
 
 data VisibleModuleInfo =