Merge branch 'develop' into _update-deps/runtimeverification/haskell-backend

Author: jberthold

deps/pyproject-build-systems

@@ -1 +1 @@
-dbfc0483b5952c6b86e36f8b3afeb9dde30ea4b5
+795a980d25301e5133eca37adae37283ec3c8e66

deps/uv2nix

@@ -1 +1 @@
-b6ed0901aec29583532abe65117b18d86a49b617
+c8cf711802cb00b2e05d5c54d3486fce7bfc8f7c

deps/uv_release

@@ -1 +1 @@
-0.9.2
+0.9.9

flake.lock

@@ -15,7 +15,7 @@
 
     flake-utils.follows = "llvm-backend/utils";
 
-    uv2nix.url = "github:pyproject-nix/uv2nix/b6ed0901aec29583532abe65117b18d86a49b617";
+    uv2nix.url = "github:pyproject-nix/uv2nix/c8cf711802cb00b2e05d5c54d3486fce7bfc8f7c";
     # uv2nix requires a newer version of nixpkgs
     # therefore, we pin uv2nix specifically to a newer version of nixpkgs
     # until we replaced our stale version of nixpkgs with an upstream one as well
@@ -24,7 +24,7 @@
     nixpkgs-unstable.url = "github:NixOS/nixpkgs/nixos-unstable";
     uv2nix.inputs.nixpkgs.follows = "nixpkgs-unstable";
     # uv2nix.inputs.nixpkgs.follows = "nixpkgs";
-    pyproject-build-systems.url = "github:pyproject-nix/build-system-pkgs/dbfc0483b5952c6b86e36f8b3afeb9dde30ea4b5";
+    pyproject-build-systems.url = "github:pyproject-nix/build-system-pkgs/795a980d25301e5133eca37adae37283ec3c8e66";
     pyproject-build-systems = {
       inputs.nixpkgs.follows = "nixpkgs";
       inputs.uv2nix.follows = "uv2nix";

flake.nix

@@ -30,6 +30,7 @@
     top_down,
 )
 from .kast import kast_term
+from .prelude.k import K_ITEM, K
 from .rewrite import indexed_rewrite
 
 if TYPE_CHECKING:
@@ -1460,13 +1461,15 @@ def transform(
                         for t, a in zip(prod.argument_sorts, term.args, strict=True):
                             if type(a) is KVariable:
                                 occurrences[a.name].append(a.let_sort(t))
-            elif isinstance(term, KSequence) and term.arity > 0:
-                for a in term.items[0:-1]:
-                    if type(a) is KVariable:
-                        occurrences[a.name].append(a.let_sort(KSort('KItem')))
-                last_a = term.items[-1]
-                if type(last_a) is KVariable:
-                    occurrences[last_a.name].append(last_a.let_sort(KSort('K')))
+            elif isinstance(term, KSequence):
+                for i, item in enumerate(term.items):
+                    if isinstance(item, KVariable):
+                        if item.sort is not None:
+                            occurrences[item.name].append(item)
+                        elif i == term.arity - 1:
+                            occurrences[item.name].append(item.let_sort(K))
+                        else:
+                            occurrences[item.name].append(item.let_sort(K_ITEM))
             return (term, occurrences)
 
         (new_term, var_occurrences) = bottom_up_with_summary(transform, kast)

pyk/src/pyk/kast/outer.py

@@ -82,41 +82,43 @@ def kast_to_kore(definition: KDefinition, kast: KInner, sort: KSort | None = Non
     kast = definition.sort_vars(kast, sort)
     kast = definition.add_cell_map_items(kast)
     kast = definition.add_sort_params(kast)
-    kast = _replace_ksequence_by_kapply(kast)
+    kast = _replace_ksequence_by_kapply(definition, kast)
     kast = _add_sort_injections(definition, kast, sort)
     kore = _kast_to_kore(kast)
     return kore
 
 
-def _replace_ksequence_by_kapply(term: KInner) -> KInner:
+def _replace_ksequence_by_kapply(definition: KDefinition, term: KInner) -> KInner:
     dotk = KApply('dotk')
     kseq = KLabel('kseq')
+    append = KLabel('append')
 
-    def transform(term: KInner) -> KInner:
-        match term:
-            case KSequence(items):
-                return transform_items(items)
-            case _:
-                return term
+    def kapply(x: KInner, y: KInner) -> KApply:
+        return append(x, y) if definition.sort_strict(x) == K else kseq(x, y)
+
+    def ksequence_to_kapply(term: KInner) -> KInner:
+        if not isinstance(term, KSequence):
+            return term
+
+        items = term.items
 
-    def transform_items(items: tuple[KInner, ...]) -> KInner:
         if not items:
             return dotk
 
         unit: KInner
         args: tuple[KInner, ...]
 
         last = items[-1]
-        if isinstance(last, KVariable) and last.sort == K:
+        if definition.sort_strict(last) == K:
             unit = last
             args = items[:-1]
         else:
             unit = dotk
             args = items
 
-        return reduce(lambda x, y: kseq(y, x), reversed(args), unit)
+        return reduce(lambda x, y: kapply(y, x), reversed(args), unit)
 
-    return top_down(transform, term)
+    return top_down(ksequence_to_kapply, term)
 
 
 def _add_sort_injections(definition: KDefinition, term: KInner, sort: KSort) -> KInner:
@@ -179,6 +181,8 @@ def _argument_sorts(definition: KDefinition, term: KInner) -> tuple[KSort, ...]:
                     return (K_ITEM, K)
                 case 'dotk':
                     return ()
+                case 'append':
+                    return (K, K)
                 case '#Forall' | '#Exists':
                     _, argument_sorts = definition.resolve_sorts(term.label)
                     _, argument_sort = argument_sorts
@@ -202,7 +206,7 @@ def _let_arguments(term: KInner, args: list[KInner]) -> KInner:
 def _inject(definition: KDefinition, term: KInner, sort: KSort) -> KInner:
     actual_sort: KSort
     match term:
-        case KApply(KLabel('kseq' | 'dotk')):  # Special case: pseudo-labels
+        case KApply(KLabel('kseq' | 'dotk' | 'append')):  # Special case: pseudo-labels
             actual_sort = K
         case _:
             actual_sort = definition.sort_strict(term)
@@ -437,7 +441,7 @@ def _kapply_to_pattern(kapply: KApply, patterns: list[Pattern]) -> Pattern:
 
 
 def _label_to_kore(label: str) -> str:
-    if label in ['inj', 'kseq', 'dotk']:  # pseudo-labels introduced during KAST-to-KORE tranformation
+    if label in ['inj', 'kseq', 'dotk', 'append']:  # pseudo-labels introduced during KAST-to-KORE tranformation
         return label
 
     if label in ML_PATTERN_LABELS:

pyk/src/pyk/konvert/_kast_to_kore.py

@@ -93,6 +93,10 @@ def _pattern_to_kast(pattern: Pattern, terms: list[KInner]) -> KInner:
                     _, _ = terms
                     return KSequence(terms)
 
+                elif symbol == 'append':
+                    _, _ = terms
+                    return KSequence(terms)
+
                 else:
                     klabel = KLabel(unmunge(symbol[3:]))
                     return KApply(klabel, terms)

pyk/src/pyk/konvert/_kore_to_kast.py

@@ -3,10 +3,11 @@
 import json
 import logging
 from abc import ABC, abstractmethod
+from collections.abc import Iterator
 from dataclasses import dataclass
 from functools import partial
 from http.server import BaseHTTPRequestHandler, HTTPServer
-from typing import TYPE_CHECKING, Any, Final, NamedTuple
+from typing import TYPE_CHECKING, NamedTuple
 
 from typing_extensions import Protocol
 
@@ -15,6 +16,7 @@
 if TYPE_CHECKING:
     from collections.abc import Callable
     from pathlib import Path
+    from typing import Any, Final
 
 
 _LOGGER: Final = logging.getLogger(__name__)
@@ -86,7 +88,7 @@ class JsonRpcBatchRequest(NamedTuple):
 class JsonRpcResult(ABC):
 
     @abstractmethod
-    def encode(self) -> bytes: ...
+    def encode(self) -> Iterator[bytes]: ...
 
 
 @dataclass(frozen=True)
@@ -96,7 +98,7 @@ class JsonRpcError(JsonRpcResult):
     message: str
     id: str | int | None
 
-    def to_json(self) -> dict[str, Any]:
+    def wrap_response(self) -> dict[str, Any]:
         return {
             'jsonrpc': JsonRpcServer.JSONRPC_VERSION,
             'error': {
@@ -106,32 +108,40 @@ def to_json(self) -> dict[str, Any]:
             'id': self.id,
         }
 
-    def encode(self) -> bytes:
-        return json.dumps(self.to_json()).encode('ascii')
+    def encode(self) -> Iterator[bytes]:
+        yield json.dumps(self.wrap_response()).encode('utf-8')
 
 
 @dataclass(frozen=True)
 class JsonRpcSuccess(JsonRpcResult):
     payload: Any
     id: Any
 
-    def to_json(self) -> dict[str, Any]:
-        return {
-            'jsonrpc': JsonRpcServer.JSONRPC_VERSION,
-            'result': self.payload,
-            'id': self.id,
-        }
-
-    def encode(self) -> bytes:
-        return json.dumps(self.to_json()).encode('ascii')
+    def encode(self) -> Iterator[bytes]:
+        id_encoded = json.dumps(self.id)
+        version_encoded = json.dumps(JsonRpcServer.JSONRPC_VERSION)
+        yield f'{{"jsonrpc": {version_encoded}, "id": {id_encoded}, "result": '.encode()
+        if isinstance(self.payload, Iterator):
+            yield from self.payload
+        else:
+            yield json.dumps(self.payload).encode('utf-8')
+        yield b'}'
 
 
 @dataclass(frozen=True)
 class JsonRpcBatchResult(JsonRpcResult):
     results: tuple[JsonRpcError | JsonRpcSuccess, ...]
 
-    def encode(self) -> bytes:
-        return json.dumps([result.to_json() for result in self.results]).encode('ascii')
+    def encode(self) -> Iterator[bytes]:
+        yield b'['
+        first = True
+        for result in self.results:
+            if not first:
+                yield b','
+            else:
+                first = False
+            yield from result.encode()
+        yield b']'
 
 
 class JsonRpcRequestHandler(BaseHTTPRequestHandler):
@@ -143,8 +153,10 @@ def __init__(self, methods: dict[str, JsonRpcMethod], *args: Any, **kwargs: Any)
 
     def _send_response(self, response: JsonRpcResult) -> None:
         self.send_response_headers()
-        response_bytes = response.encode()
-        self.wfile.write(response_bytes)
+        response_body = response.encode()
+        for chunk in response_body:
+            self.wfile.write(chunk)
+        self.wfile.flush()
 
     def send_response_headers(self) -> None:
         self.send_response(200)