Merge master into branch

Author: nwatson22

deps/k_release

@@ -1 +1 @@
-6.0.50
+6.0.52

package/version

@@ -1 +1 @@
-0.1.412
+0.1.413

pyproject.toml

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

src/pyk/__init__.py

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

src/pyk/cterm.py

@@ -5,7 +5,8 @@
 from itertools import chain
 from typing import TYPE_CHECKING
 
-from .kast.inner import KApply, KAtt, KInner, KRewrite, KToken, KVariable, Subst, bottom_up
+from .kast.inner import KApply, KInner, KRewrite, KToken, KVariable, Subst, bottom_up
+from .kast.kast import KAtt
 from .kast.manip import (
     abstract_term_safely,
     apply_existential_substitutions,

src/pyk/kast/inner.py

@@ -9,14 +9,13 @@
 from typing import TYPE_CHECKING, final, overload
 
 from ..utils import EMPTY_FROZEN_DICT, FrozenDict
-from .kast import EMPTY_ATT, KAst, KAtt, WithKAtt
+from .kast import KAst
 
 if TYPE_CHECKING:
     from collections.abc import Callable, Iterator
     from typing import Any, Final, TypeVar
 
     T = TypeVar('T', bound='KAst')
-    W = TypeVar('W', bound='WithKAtt')
     KI = TypeVar('KI', bound='KInner')
     A = TypeVar('A', bound='Any')
     B = TypeVar('B', bound='Any')
@@ -249,21 +248,16 @@ def __lt__(self, other: Any) -> bool:
     @classmethod
     def from_dict(cls: type[KVariable], d: Mapping[str, Any]) -> KVariable:
         cls._check_node(d)
-        att = KAtt.from_dict(d['att']) if d.get('att') else EMPTY_ATT
-
-        sort: KSort | None
-        if KAtt.SORT in att:
-            sort = KSort.from_dict(att[KAtt.SORT])
-        else:
-            sort = None
-
+        sort = None
+        if 'sort' in d:
+            sort = KSort.from_dict(d['sort'])
         return KVariable(name=d['name'], sort=sort)
 
     def to_dict(self) -> dict[str, Any]:
-        _att = KAtt({})
+        _d: dict[str, Any] = {'node': 'KVariable', 'name': self.name}
         if self.sort is not None:
-            _att = _att.update({KAtt.SORT: self.sort.to_dict()})
-        return {'node': 'KVariable', 'name': self.name, 'att': _att.to_dict()}
+            _d['sort'] = self.sort.to_dict()
+        return _d
 
     def let(self, *, name: str | None = None, sort: str | KSort | None = None) -> KVariable:
         name = name if name is not None else self.name
@@ -456,7 +450,7 @@ def from_dict(cls: type[KAs], d: Mapping[str, Any]) -> KAs:
     def to_dict(self) -> dict[str, Any]:
         return {'node': 'KAs', 'pattern': self.pattern.to_dict(), 'alias': self.alias.to_dict()}
 
-    def let(self, *, pattern: KInner | None = None, alias: KInner | None = None, att: KAtt | None = None) -> KAs:
+    def let(self, *, pattern: KInner | None = None, alias: KInner | None = None) -> KAs:
         pattern = pattern if pattern is not None else self.pattern
         alias = alias if alias is not None else self.alias
         return KAs(pattern=pattern, alias=alias)
@@ -470,14 +464,13 @@ def match(self, term: KInner) -> Subst | None:
 
 @final
 @dataclass(frozen=True)
-class KRewrite(KInner, WithKAtt):
+class KRewrite(KInner):
     lhs: KInner
     rhs: KInner
 
-    def __init__(self, lhs: KInner, rhs: KInner, att: KAtt = EMPTY_ATT):
+    def __init__(self, lhs: KInner, rhs: KInner):
         object.__setattr__(self, 'lhs', lhs)
         object.__setattr__(self, 'rhs', rhs)
-        object.__setattr__(self, 'att', att)
 
     def __iter__(self) -> Iterator[KInner]:
         return iter([self.lhs, self.rhs])
@@ -494,31 +487,24 @@ def from_dict(cls: type[KRewrite], d: Mapping[str, Any]) -> KRewrite:
         return KRewrite(
             lhs=KInner.from_dict(d['lhs']),
             rhs=KInner.from_dict(d['rhs']),
-            att=KAtt.from_dict(d['att']) if d.get('att') else EMPTY_ATT,
         )
 
     def to_dict(self) -> dict[str, Any]:
         return {
             'node': 'KRewrite',
             'lhs': self.lhs.to_dict(),
             'rhs': self.rhs.to_dict(),
-            'att': self.att.to_dict(),
         }
 
     def let(
         self,
         *,
         lhs: KInner | None = None,
         rhs: KInner | None = None,
-        att: KAtt | None = None,
     ) -> KRewrite:
         lhs = lhs if lhs is not None else self.lhs
         rhs = rhs if rhs is not None else self.rhs
-        att = att if att is not None else self.att
-        return KRewrite(lhs=lhs, rhs=rhs, att=att)
-
-    def let_att(self, att: KAtt) -> KRewrite:
-        return self.let(att=att)
+        return KRewrite(lhs=lhs, rhs=rhs)
 
     def map_inner(self: KRewrite, f: Callable[[KInner], KInner]) -> KRewrite:
         return self.let(lhs=f(self.lhs), rhs=f(self.rhs))

src/pyk/kast/kast.py

@@ -21,6 +21,10 @@
 
 
 class KAst(ABC):
+    @staticmethod
+    def version() -> int:
+        return 3
+
     @classmethod
     def from_dict(cls: type[T], d: Mapping[str, Any]) -> T:
         from . import inner, outer
@@ -175,7 +179,7 @@ def kast_term(dct: Mapping[str, Any], cls: type[T] = KAst) -> T:  # type: ignore
     if dct['format'] != 'KAST':
         raise ValueError(f"Invalid format: {dct['format']}")
 
-    if dct['version'] != 2:
+    if dct['version'] != KAst.version():
         raise ValueError(f"Invalid version: {dct['version']}")
 
     return cls.from_dict(dct['term'])

src/pyk/ktool/kprint.py

@@ -11,7 +11,7 @@
 from typing import TYPE_CHECKING
 
 from ..cli.utils import check_dir_path, check_file_path
-from ..kast import kast_term
+from ..kast import KAst, kast_term
 from ..kast.inner import KInner
 from ..kast.outer import read_kast_definition
 from ..kast.pretty import PrettyPrinter
@@ -29,7 +29,6 @@
     from tempfile import _TemporaryFileWrapper
     from typing import Final
 
-    from ..kast import KAst
     from ..kast.inner import KSort, KToken
     from ..kast.outer import KDefinition, KFlatModule
     from ..kast.pretty import SymbolTable
@@ -270,7 +269,7 @@ def kast_to_kore(self, kast: KInner, sort: KSort | None = None) -> Pattern:
             _LOGGER.warning(ve)
 
         _LOGGER.warning(f'Falling back to using `kast` for KAst -> Kore: {kast}')
-        kast_json = {'format': 'KAST', 'version': 2, 'term': kast.to_dict()}
+        kast_json = {'format': 'KAST', 'version': KAst.version(), 'term': kast.to_dict()}
         proc_res = self._expression_kast(
             json.dumps(kast_json),
             input=KAstInput.JSON,

src/pyk/ktool/krun.py

@@ -72,6 +72,7 @@ def run_kore_process(
         output: KRunOutput | None = KRunOutput.PRETTY,
         pipe_stderr: bool = True,
         bug_report: BugReport | None = None,
+        debugger: bool = False,
     ) -> CompletedProcess:
         with self._temp_file() as ntf:
             pgm.write(ntf)
@@ -94,6 +95,7 @@ def run_kore_process(
                 bug_report=self._bug_report,
                 check=False,
                 pipe_stderr=pipe_stderr,
+                debugger=debugger,
             )
 
     def run_kore(
@@ -111,6 +113,7 @@ def run_kore(
         check: bool = False,
         pipe_stderr: bool = True,
         bug_report: BugReport | None = None,
+        debugger: bool = False,
     ) -> None:
         result = self.run_kore_process(
             pgm,
@@ -124,6 +127,7 @@ def run_kore(
             output=output,
             pipe_stderr=pipe_stderr,
             bug_report=bug_report,
+            debugger=debugger,
         )
 
         if output != KRunOutput.NONE:
@@ -152,6 +156,7 @@ def run_kore_term(
         pipe_stderr: bool = True,
         check: bool = False,
         bug_report: BugReport | None = None,
+        debugger: bool = False,
     ) -> Pattern:
         proc_res = self.run_kore_process(
             pattern,
@@ -163,6 +168,7 @@ def run_kore_term(
             output=KRunOutput.NONE,
             pipe_stderr=pipe_stderr,
             bug_report=bug_report,
+            debugger=debugger,
         )
 
         if check:
@@ -194,6 +200,7 @@ def _krun(
     pipe_stderr: bool = True,
     logger: Logger | None = None,
     bug_report: BugReport | None = None,
+    debugger: bool = False,
 ) -> CompletedProcess:
     if input_file:
         check_file_path(input_file)
@@ -221,6 +228,7 @@ def _krun(
         no_expand_macros=no_expand_macros,
         search_final=search_final,
         no_pattern=no_pattern,
+        debugger=debugger,
     )
 
     if bug_report is not None:
@@ -232,7 +240,7 @@ def _krun(
             bug_report.add_command(args)
 
     try:
-        return run_process(args, check=check, pipe_stderr=pipe_stderr, logger=logger or _LOGGER)
+        return run_process(args, check=check, pipe_stderr=pipe_stderr, logger=logger or _LOGGER, exec_process=debugger)
     except CalledProcessError as err:
         raise RuntimeError(
             f'Command krun exited with code {err.returncode} for: {input_file}', err.stdout, err.stderr
@@ -254,6 +262,7 @@ def _build_arg_list(
     no_expand_macros: bool,
     search_final: bool,
     no_pattern: bool,
+    debugger: bool,
 ) -> list[str]:
     args = [command]
     if input_file:
@@ -280,4 +289,6 @@ def _build_arg_list(
         args += ['--search-final']
     if no_pattern:
         args += ['--no-pattern']
+    if debugger:
+        args += ['--debugger']
     return args

src/pyk/utils.py

@@ -382,6 +382,7 @@ def run_process(
     cwd: str | Path | None = None,
     env: Mapping[str, str] | None = None,
     logger: Logger | None = None,
+    exec_process: bool = False,
 ) -> CompletedProcess:
     if cwd is not None:
         cwd = Path(cwd)
@@ -400,6 +401,15 @@ def run_process(
     stderr = subprocess.PIPE if pipe_stderr else None
 
     logger.info(f'Running: {command}')
+
+    if exec_process:
+        sys.stdout.flush()
+        sys.stderr.flush()
+        if type(args) is str:
+            args = shlex.split(args)
+        argslist = list(args)
+        os.execvp(argslist[0], argslist)
+
     start_time = time.time()
 
     res = subprocess.run(args, input=input, cwd=cwd, env=env, stdout=stdout, stderr=stderr, text=True)