Merge remote-tracking branch 'origin/master' into anvacaru/vacuous-2

Author: anvacaru

deps/k_release

@@ -1 +1 @@
-6.0.48
+6.0.50

package/version

@@ -1 +1 @@
-0.1.409
+0.1.411

pyproject.toml

@@ -4,7 +4,7 @@ build-backend = "poetry.core.masonry.api"
 
 [tool.poetry]
 name = "pyk"
-version = "0.1.409"
+version = "0.1.411"
 description = ""
 authors = [
     "Runtime Verification, Inc. <[email protected]>",

src/pyk/__init__.py

@@ -6,4 +6,4 @@
     from typing import Final
 
 
-K_VERSION: Final = '6.0.48'
+K_VERSION: Final = '6.0.50'

src/pyk/kore/rpc.py

@@ -232,6 +232,8 @@ def request(self, method: str, **params: Any) -> dict[str, Any]:
 
         _LOGGER.debug(f'Sending request to {server_addr}: {req}')
         resp = self._transport.request(req)
+        if not resp:
+            raise RuntimeError('Empty response received')
         _LOGGER.debug(f'Received response from {server_addr}: {resp}')
 
         if self._bug_report:

src/pyk/ktool/kprint.py

@@ -19,6 +19,7 @@
 from ..kore.kompiled import KompiledKore
 from ..kore.parser import KoreParser
 from ..kore.syntax import App, SortApp
+from ..kore.tools import PrintOutput, kore_print
 from ..utils import run_process
 from .kompile import DefinitionInfo
 
@@ -258,13 +259,8 @@ def kore_to_kast(self, kore: Pattern) -> KInner:
         except ValueError as err:
             _LOGGER.warning(err)
 
-        _LOGGER.warning(f'Falling back to using `kast` for Kore -> Kast: {kore.text}')
-        proc_res = self._expression_kast(
-            kore.text,
-            input=KAstInput.KORE,
-            output=KAstOutput.JSON,
-        )
-        return kast_term(json.loads(proc_res.stdout), KInner)  # type: ignore # https://github.com/python/mypy/issues/4717
+        _LOGGER.warning(f'Falling back to using `kore-print` for Kore -> Kast: {kore.text}')
+        return kast_term(json.loads(kore_print(kore, self.definition_dir, PrintOutput.JSON)), KInner)  # type: ignore # https://github.com/python/mypy/issues/4717
 
     def kast_to_kore(self, kast: KInner, sort: KSort | None = None) -> Pattern:
         try:

src/pyk/ktool/krun.py

@@ -1,19 +1,14 @@
 from __future__ import annotations
 
-import json
 import logging
 from enum import Enum
 from pathlib import Path
 from subprocess import CalledProcessError
 from typing import TYPE_CHECKING
 
 from ..cli.utils import check_dir_path, check_file_path
-from ..cterm import CTerm
-from ..kast import kast_term
-from ..kast.inner import KInner, KLabel, KSort
-from ..konvert import unmunge
 from ..kore.parser import KoreParser
-from ..kore.syntax import DV, App, SortApp, String
+from ..kore.tools import PrintOutput, kore_print
 from ..utils import run_process
 from .kprint import KPrint
 
@@ -31,6 +26,17 @@
 _LOGGER: Final = logging.getLogger(__name__)
 
 
+class KRunOutput(Enum):
+    PRETTY = 'pretty'
+    PROGRAM = 'program'
+    KAST = 'kast'
+    BINARY = 'binary'
+    JSON = 'json'
+    LATEX = 'latex'
+    KORE = 'kore'
+    NONE = 'none'
+
+
 class KRun(KPrint):
     command: str
 
@@ -52,181 +58,120 @@ def __init__(
         )
         self.command = command
 
-    def run(
+    def run_kore_process(
         self,
-        pgm: KInner,
+        pgm: Pattern,
         *,
-        config: Mapping[str, KInner] | None = None,
+        cmap: Mapping[str, str] | None = None,
+        pmap: Mapping[str, str] | None = None,
+        term: bool = False,
         depth: int | None = None,
-        expand_macros: bool = False,
-        expect_rc: int | Iterable[int] = 0,
-    ) -> CTerm:
-        if config is not None and 'PGM' in config:
-            raise ValueError('Cannot supply both pgm and config with PGM variable.')
-        pmap = {k: 'cat' for k in config} if config is not None else None
-        cmap = {k: self.kast_to_kore(v).text for k, v in config.items()} if config is not None else None
+        expand_macros: bool = True,
+        search_final: bool = False,
+        no_pattern: bool = False,
+        output: KRunOutput | None = KRunOutput.PRETTY,
+        pipe_stderr: bool = True,
+        bug_report: BugReport | None = None,
+    ) -> CompletedProcess:
         with self._temp_file() as ntf:
-            ntf.write(self.pretty_print(pgm))
+            pgm.write(ntf)
             ntf.flush()
 
-            result = _krun(
+            return _krun(
                 command=self.command,
                 input_file=Path(ntf.name),
                 definition_dir=self.definition_dir,
-                output=KRunOutput.JSON,
+                output=KRunOutput.KORE,
                 depth=depth,
+                parser='cat',
                 cmap=cmap,
                 pmap=pmap,
+                term=term,
                 temp_dir=self.use_directory,
                 no_expand_macros=not expand_macros,
+                search_final=search_final,
+                no_pattern=no_pattern,
                 bug_report=self._bug_report,
-                check=(expect_rc == 0),
+                check=False,
+                pipe_stderr=pipe_stderr,
             )
 
-        self._check_return_code(result.returncode, expect_rc)
-
-        result_kast = kast_term(json.loads(result.stdout), KInner)  # type: ignore # https://github.com/python/mypy/issues/4717
-        return CTerm.from_kast(result_kast)
-
     def run_kore(
         self,
-        pgm: KInner,
+        pgm: Pattern,
         *,
-        sort: KSort | None = None,
+        cmap: Mapping[str, str] | None = None,
+        pmap: Mapping[str, str] | None = None,
+        term: bool = False,
         depth: int | None = None,
-        expand_macros: bool = False,
-        expect_rc: int | Iterable[int] = 0,
-    ) -> CTerm:
-        kore_pgm = self.kast_to_kore(pgm, sort=sort)
-        with self._temp_file() as ntf:
-            kore_pgm.write(ntf)
-            ntf.write('\n')
-            ntf.flush()
-
-            result = _krun(
-                command=self.command,
-                input_file=Path(ntf.name),
-                definition_dir=self.definition_dir,
-                output=KRunOutput.KORE,
-                parser='cat',
-                depth=depth,
-                temp_dir=self.use_directory,
-                no_expand_macros=not expand_macros,
-                bug_report=self._bug_report,
-                check=(expect_rc == 0),
-            )
-
-        self._check_return_code(result.returncode, expect_rc)
-
-        result_kore = KoreParser(result.stdout).pattern()
-        result_kast = self.kore_to_kast(result_kore)
-        return CTerm.from_kast(result_kast)
-
-    def run_kore_term(
-        self,
-        pattern: Pattern,
-        *,
-        depth: int | None = None,
-        expand_macros: bool = False,
+        expand_macros: bool = True,
         search_final: bool = False,
         no_pattern: bool = False,
+        output: KRunOutput | None = KRunOutput.PRETTY,
+        check: bool = False,
+        pipe_stderr: bool = True,
         bug_report: BugReport | None = None,
-        expect_rc: int | Iterable[int] = 0,
-    ) -> Pattern:
-        with self._temp_file() as ntf:
-            pattern.write(ntf)
-            ntf.write('\n')
-            ntf.flush()
-
-            proc_res = _krun(
-                command=self.command,
-                input_file=Path(ntf.name),
-                definition_dir=self.definition_dir,
-                output=KRunOutput.KORE,
-                parser='cat',
-                term=True,
-                depth=depth,
-                temp_dir=self.use_directory,
-                no_expand_macros=not expand_macros,
-                search_final=search_final,
-                no_pattern=no_pattern,
-                bug_report=self._bug_report,
-                check=(expect_rc == 0),
-            )
-
-        self._check_return_code(proc_res.returncode, expect_rc)
+    ) -> None:
+        result = self.run_kore_process(
+            pgm,
+            cmap=cmap,
+            pmap=pmap,
+            term=term,
+            depth=depth,
+            expand_macros=expand_macros,
+            search_final=search_final,
+            no_pattern=no_pattern,
+            output=output,
+            pipe_stderr=pipe_stderr,
+            bug_report=bug_report,
+        )
 
-        parser = KoreParser(proc_res.stdout)
-        res = parser.pattern()
-        assert parser.eof
-        return res
+        if output != KRunOutput.NONE:
+            output_kore = KoreParser(result.stdout).pattern()
+            match output:
+                case KRunOutput.JSON:
+                    print(self.kore_to_kast(output_kore).to_json())
+                case KRunOutput.KORE:
+                    print(output_kore.text)
+                case KRunOutput.PRETTY | KRunOutput.PROGRAM | KRunOutput.KAST | KRunOutput.BINARY | KRunOutput.LATEX:
+                    print(kore_print(output_kore, self.definition_dir, PrintOutput(output.value)))
+                case KRunOutput.NONE:
+                    raise AssertionError()
+
+        if check:
+            result.check_returncode()
 
-    def run_kore_config(
+    def run_kore_term(
         self,
-        config: Mapping[str, Pattern],
+        pattern: Pattern,
         *,
         depth: int | None = None,
         expand_macros: bool = False,
         search_final: bool = False,
         no_pattern: bool = False,
-        # ---
+        pipe_stderr: bool = True,
+        check: bool = False,
         bug_report: BugReport | None = None,
-        expect_rc: int = 0,
     ) -> Pattern:
-        def _config_var_token(s: str) -> DV:
-            return DV(SortApp('SortKConfigVar'), String(f'${s}'))
-
-        def _map_item(s: str, p: Pattern, sort: KSort) -> Pattern:
-            _map_key = self._add_sort_injection(_config_var_token(s), KSort('KConfigVar'), KSort('KItem'))
-            _map_value = self._add_sort_injection(p, sort, KSort('KItem'))
-            return App("Lbl'UndsPipe'-'-GT-Unds'", [], [_map_key, _map_value])
-
-        def _map(ps: list[Pattern]) -> Pattern:
-            if len(ps) == 0:
-                return App("Lbl'Stop'Map{}()", [], [])
-            if len(ps) == 1:
-                return ps[0]
-            return App("Lbl'Unds'Map'Unds'", [], [ps[0], _map(ps[1:])])
-
-        def _sort(p: Pattern) -> KSort:
-            if type(p) is DV:
-                return KSort(p.sort.name[4:])
-            if type(p) is App:
-                label = KLabel(unmunge(p.symbol[3:]))
-                return self.definition.return_sort(label)
-            raise ValueError(f'Cannot fast-compute sort for pattern: {p}')
-
-        config_var_map = _map([_map_item(k, v, _sort(v)) for k, v in config.items()])
-        term = App('LblinitGeneratedTopCell', [], [config_var_map])
-
-        return self.run_kore_term(
-            term,
+        proc_res = self.run_kore_process(
+            pattern,
             depth=depth,
+            term=True,
             expand_macros=expand_macros,
             search_final=search_final,
             no_pattern=no_pattern,
+            output=KRunOutput.NONE,
+            pipe_stderr=pipe_stderr,
             bug_report=bug_report,
-            expect_rc=expect_rc,
         )
 
-    @staticmethod
-    def _check_return_code(actual: int, expected: int | Iterable[int]) -> None:
-        if isinstance(expected, int):
-            expected = [expected]
+        if check:
+            proc_res.check_returncode()
 
-        if actual not in expected:
-            raise RuntimeError(f'Expected {expected} as exit code from krun, but got {actual}')
-
-
-class KRunOutput(Enum):
-    PRETTY = 'pretty'
-    PROGRAM = 'program'
-    KAST = 'kast'
-    BINARY = 'binary'
-    JSON = 'json'
-    LATEX = 'latex'
-    KORE = 'kore'
-    NONE = 'none'
+        parser = KoreParser(proc_res.stdout)
+        res = parser.pattern()
+        assert parser.eof
+        return res
 
 
 def _krun(
@@ -237,16 +182,16 @@ def _krun(
     output: KRunOutput | None = None,
     parser: str | None = None,
     depth: int | None = None,
-    pmap: Mapping[str, str] | None = None,
     cmap: Mapping[str, str] | None = None,
+    pmap: Mapping[str, str] | None = None,
     term: bool = False,
     temp_dir: Path | None = None,
     no_expand_macros: bool = False,
     search_final: bool = False,
     no_pattern: bool = False,
     # ---
     check: bool = True,
-    pipe_stderr: bool = False,
+    pipe_stderr: bool = True,
     logger: Logger | None = None,
     bug_report: BugReport | None = None,
 ) -> CompletedProcess:
@@ -259,6 +204,9 @@ def _krun(
     if depth and depth < 0:
         raise ValueError(f'Expected non-negative depth, got: {depth}')
 
+    if term and (cmap is not None or pmap is not None):
+        raise ValueError('Cannot supply both term and cmap/pmap')
+
     args = _build_arg_list(
         command=command,
         input_file=input_file,