Merge pull request #162 from kiranandcode/kg-env-catalog

Expose `env.catalog` as `env_catalog` method on pantograph.Server

Author: lenianiva

pantograph/server.py

@@ -409,6 +409,25 @@ async def env_add_async(
 
     env_add = to_sync(env_add_async)
 
+    async def env_catalog_async(
+            self,
+            module_prefix: str | None = None,
+            invert_filter: bool = False
+    ) -> list[str]:
+        """
+        Print all symbols in environment.
+        """
+        with tempfile.NamedTemporaryFile('r') as tmp_file:
+            result = await self.run_async('env.catalog', {
+                'filename': tmp_file.name,
+                'modulePrefix': module_prefix,
+                'invertFilter': invert_filter,
+            })
+            if "error" in result:
+                raise ServerError(result["desc"])
+            return [line.strip() for line in tmp_file.readlines()]
+    env_catalog = to_sync(env_catalog_async)
+
     async def env_inspect_async(
             self,
             name: str,

pantograph/test_server.py

@@ -226,6 +226,15 @@ def test_env_add_inspect(self):
         inspect_result = server.env_inspect(name="mystery")
         self.assertEqual(inspect_result['type'], {'pp': 'Nat → Nat'})
 
+    def test_env_catalog(self):
+        server = Server()
+        server.load_definitions("def foo: Nat -> Nat | 0 => 1 | n + 1 => foo n")
+        definitions = server.env_catalog(module_prefix="Init", invert_filter=True)
+        self.assertEqual(
+            set(definitions),
+            {'dfoo._sunfold', 'dfoo._unsafe_rec', 'dfoo', 'dfoo.match_1'}
+        )
+
     def test_env_parse(self):
         server = Server()
         head, tail = server.env_parse("intro x; apply a", category="tactic")