Merge branch 'noah/anti-unify-sort-fix' of https://github.com/runtimeverification/pyk into noah/anti-unify-sort-fix

Author: nwatson22

deps/k_release

@@ -1 +1 @@
-6.0.44
+6.0.50

package/version

@@ -1 +1 @@
-0.1.405
+0.1.412

pyproject.toml

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

src/pyk/__init__.py

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

src/pyk/kast/markdown.py

@@ -0,0 +1,203 @@
+from __future__ import annotations
+
+import re
+from abc import ABC, abstractmethod
+from dataclasses import dataclass
+from typing import TYPE_CHECKING, NamedTuple, final
+
+if TYPE_CHECKING:
+    from collections.abc import Container, Iterable, Iterator
+    from typing import Final
+
+
+def select_code_blocks(text: str, selector: str | None = None) -> str:
+    _selector = SelectorParser(selector).parse() if selector else None
+
+    def selected(code_block: CodeBlock) -> bool:
+        if _selector is None:
+            return True
+
+        tags = parse_tags(code_block.info)
+        return _selector.eval(tags)
+
+    return '\n'.join(code_block.code for code_block in code_blocks(text) if selected(code_block))
+
+
+class CodeBlock(NamedTuple):
+    info: str
+    code: str
+
+
+_CODE_BLOCK_PATTERN: Final = re.compile(
+    r'(^|(?<=\n)) {0,3}(?P<fence>```+)(?!`)(?P<info>.*)\n(?P<code>(.*\n)*?) {0,3}(?P=fence)`*'
+)
+
+
+def code_blocks(text: str) -> Iterator[CodeBlock]:
+    return (CodeBlock(match['info'], match['code'].rstrip()) for match in _CODE_BLOCK_PATTERN.finditer(text))
+
+
+def parse_tags(text: str) -> set[str]:
+    def check_tag(tag: str) -> None:
+        if not (tag and all(c.isalnum() or c == '_' for c in tag)):
+            raise ValueError(f'Invalid tag: {tag!r}')
+
+    if not text:
+        return set()
+
+    if text[0] != '{':
+        check_tag(text)
+        return {text}
+
+    if text[-1] != '}':
+        raise ValueError("Expected '}', found: {text[-1]!r}")
+
+    res: set[str] = set()
+    tags = text[1:-1].split()
+    for tag in tags:
+        if tag[0] != '.':
+            raise ValueError("Expected '.', found: {tag[0]!r}")
+        check_tag(tag[1:])
+        res.add(tag[1:])
+
+    return res
+
+
+# ----------------------
+# Selector mini-language
+# ----------------------
+
+
+class Selector(ABC):
+    @abstractmethod
+    def eval(self, atoms: Container[str]) -> bool:
+        ...
+
+
+@final
+@dataclass(frozen=True)
+class Atom(Selector):
+    name: str
+
+    def eval(self, atoms: Container[str]) -> bool:
+        return self.name in atoms
+
+
+@final
+@dataclass(frozen=True)
+class Not(Selector):
+    op: Selector
+
+    def eval(self, atoms: Container[str]) -> bool:
+        return not self.op.eval(atoms)
+
+
+@final
+@dataclass(frozen=True)
+class And(Selector):
+    ops: tuple[Selector, ...]
+
+    def eval(self, atoms: Container[str]) -> bool:
+        return all(op.eval(atoms) for op in self.ops)
+
+
+@final
+@dataclass(frozen=True)
+class Or(Selector):
+    ops: tuple[Selector, ...]
+
+    def eval(self, atoms: Container[str]) -> bool:
+        return any(op.eval(atoms) for op in self.ops)
+
+
+_SPECIAL = tuple('!&|()')
+
+
+def selector_lexer(it: Iterable[str]) -> Iterator[str]:
+    it = iter(it)
+    la = next(it, '')
+    while True:
+        while la.isspace():
+            la = next(it, '')
+
+        if not la:
+            yield ''
+            return
+
+        if la in _SPECIAL:
+            yield la
+            la = next(it, '')
+            continue
+
+        buf: list[str] = []
+        while la.isalnum() or la == '_':
+            buf.append(la)
+            la = next(it, '')
+
+        if not buf:
+            raise ValueError(f'Unexpected character: {la!r}')
+
+        yield ''.join(buf)
+
+
+class SelectorParser:
+    _la: str
+    _it: Iterator[str]
+
+    def __init__(self, selector: str):
+        self._it = selector_lexer(selector)
+        self._consume()
+
+    def _consume(self) -> None:
+        self._la = next(self._it, '')
+
+    def _match(self, token: str) -> None:
+        if self._la != token:
+            raise ValueError('Unexpected token: {token}')
+        self._consume()
+
+    def parse(self) -> Selector:
+        res = self._or()
+        if self._la:
+            raise ValueError(f'Expected EOF, found: {self._la}')
+        return res
+
+    def _or(self) -> Selector:
+        ops = [self._and()]
+        while self._la == '|':
+            self._consume()
+            ops.append(self._and())
+        if len(ops) > 1:
+            return Or(tuple(ops))
+        return ops[0]
+
+    def _and(self) -> Selector:
+        ops = [self._lit()]
+        while self._la == '&':
+            self._consume()
+            ops.append(self._lit())
+        if len(ops) > 1:
+            return And(tuple(ops))
+        return ops[0]
+
+    def _lit(self) -> Selector:
+        if not self._la:
+            raise ValueError('Unexpected EOF')
+
+        if self._la == '(':
+            self._consume()
+            expr = self._or()
+            self._match(')')
+            return expr
+
+        if self._la == '!':
+            self._consume()
+            lit = self._lit()
+            return Not(lit)
+
+        if len(self._la) > 1 or self._la.isalnum() or self._la == '-':
+            atom = self._la
+            self._consume()
+            return Atom(atom)
+
+        raise ValueError(f'Unexpected token: {self._la}')

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: