diff --git a/deps/haskell-backend_release b/deps/haskell-backend_release index 3e9fab84ad3..fac8924a184 100644 --- a/deps/haskell-backend_release +++ b/deps/haskell-backend_release @@ -1 +1 @@ -v0.1.25 +v0.1.29 diff --git a/flake.lock b/flake.lock index ca2739a69a1..b0ebac8573b 100644 --- a/flake.lock +++ b/flake.lock @@ -63,16 +63,16 @@ "z3": "z3" }, "locked": { - "lastModified": 1719489268, - "narHash": "sha256-J480ZO5k/WjMbwCIfrhy+Kg4p+r5qgbIbCunkn1DhnA=", + "lastModified": 1719881076, + "narHash": "sha256-t9RTbVarwaobMiJkQjXykP8Qt+26miKzr3inONULvck=", "owner": "runtimeverification", "repo": "haskell-backend", - "rev": "e82bc74a95ce6a78c6f8fec7cb255a36aa99e0c6", + "rev": "11265424aeb138168bc73f1f028273de192b5be4", "type": "github" }, "original": { "owner": "runtimeverification", - "ref": "v0.1.25", + "ref": "v0.1.29", "repo": "haskell-backend", "type": "github" } diff --git a/flake.nix b/flake.nix index a7047ef0364..f795fd2aec8 100644 --- a/flake.nix +++ b/flake.nix @@ -1,7 +1,7 @@ { description = "K Framework"; inputs = { - haskell-backend.url = "github:runtimeverification/haskell-backend/v0.1.25"; + haskell-backend.url = "github:runtimeverification/haskell-backend/v0.1.29"; nixpkgs.follows = "llvm-backend/nixpkgs"; flake-utils.url = "github:numtide/flake-utils"; llvm-backend = { diff --git a/haskell-backend/src/main/native/haskell-backend b/haskell-backend/src/main/native/haskell-backend index e82bc74a95c..11265424aeb 160000 --- a/haskell-backend/src/main/native/haskell-backend +++ b/haskell-backend/src/main/native/haskell-backend @@ -1 +1 @@ -Subproject commit e82bc74a95ce6a78c6f8fec7cb255a36aa99e0c6 +Subproject commit 11265424aeb138168bc73f1f028273de192b5be4 diff --git a/k-distribution/include/kframework/ktest-common.mak b/k-distribution/include/kframework/ktest-common.mak index ec11dbef7a1..ce1a6102c5a 100644 --- a/k-distribution/include/kframework/ktest-common.mak +++ b/k-distribution/include/kframework/ktest-common.mak @@ -28,5 +28,4 @@ LLVM_KRUN=${K_BIN}/llvm-krun # and kdep KDEP=${K_BIN}/kdep # command to strip paths from test outputs -# REMOVE_PATHS=| sed 's!\('`pwd`'\|'${BUILTIN_DIR}'\|/nix/store/.\+/include/kframework/builtin\)/\(\./\)\{0,2\}!!g' -REMOVE_PATHS=| sed 's!\('`pwd`'\)/\(\./\)\{0,2\}!!g' | sed 's!\('${BUILTIN_DIR}'\)/\(\./\)\{0,2\}!!g' | sed 's!\('/nix/store/.\+/include/kframework/builtin'\)/\(\./\)\{0,2\}!!g' +REMOVE_PATHS=| sed 's!\('`pwd`'\)/\(\./\)\{0,2\}!!g' | sed 's!\('${BUILTIN_DIR}'\)/\(\./\)\{0,2\}!!g' | sed 's!\('/nix/store/..*/include/kframework/builtin'\)/\(\./\)\{0,2\}!!g' diff --git a/pyk/src/pyk/kllvm/convert.py b/pyk/src/pyk/kllvm/convert.py index bdb6e9b067c..a705ab8f170 100644 --- a/pyk/src/pyk/kllvm/convert.py +++ b/pyk/src/pyk/kllvm/convert.py @@ -6,13 +6,16 @@ ML_SYMBOLS, AliasDecl, App, + Assoc, Axiom, Claim, Definition, EVar, Import, + LeftAssoc, MLPattern, Module, + RightAssoc, SortApp, SortDecl, SortVar, @@ -110,6 +113,8 @@ def pattern_to_llvm(pattern: Pattern) -> kllvm.Pattern: return kllvm.VariablePattern(name, sort_to_llvm(sort)) case App(symbol, sorts, args): return _composite_pattern(symbol, sorts, args) + case Assoc(): + return _composite_pattern(pattern.kore_symbol(), [], [pattern.app]) case MLPattern(): return _composite_pattern(pattern.symbol(), pattern.sorts, pattern.ctor_patterns) case _: @@ -206,6 +211,11 @@ def llvm_to_pattern(pattern: kllvm.Pattern) -> Pattern: symbol, sorts, patterns = _unpack_composite_pattern(pattern) if symbol in ML_SYMBOLS: return MLPattern.of(symbol, sorts, patterns) + elif symbol in [r'\left-assoc', r'\right-assoc']: + (app,) = patterns + assert isinstance(app, App) + assoc = LeftAssoc if symbol == r'\left-assoc' else RightAssoc + return assoc(app.symbol, app.sorts, app.args) else: return App(symbol, sorts, patterns) case _: diff --git a/pyk/src/pyk/kore/manip.py b/pyk/src/pyk/kore/manip.py index 90fb2cb2d93..8c20e70f2c2 100644 --- a/pyk/src/pyk/kore/manip.py +++ b/pyk/src/pyk/kore/manip.py @@ -2,7 +2,7 @@ from typing import TYPE_CHECKING -from .syntax import And, Assoc, EVar, MLQuant, Top +from .syntax import And, EVar, MLQuant, Top if TYPE_CHECKING: from collections.abc import Collection @@ -28,9 +28,6 @@ def collect(pattern: Pattern, bound_vars: set[str]) -> None: else: occurrences[pattern.name] = [pattern] - elif isinstance(pattern, Assoc): - collect(pattern.app, bound_vars) - elif isinstance(pattern, MLQuant): new_bound_vars = {pattern.var.name}.union(bound_vars) collect(pattern.pattern, new_bound_vars) diff --git a/pyk/src/pyk/kore/match.py b/pyk/src/pyk/kore/match.py index 89f28d83b41..db85a73f9d1 100644 --- a/pyk/src/pyk/kore/match.py +++ b/pyk/src/pyk/kore/match.py @@ -25,15 +25,15 @@ def match_dv(pattern: Pattern, sort: Sort | None = None) -> DV: return dv -def match_symbol(app: App, symbol: str) -> None: - if app.symbol != symbol: - raise ValueError(f'Expected symbol {symbol}, found: {app.symbol}') +def match_symbol(actual: str, expected: str) -> None: + if actual != expected: + raise ValueError(f'Expected symbol {expected}, found: {actual}') def match_app(pattern: Pattern, symbol: str | None = None) -> App: app = check_type(pattern, App) if symbol is not None: - match_symbol(app, symbol) + match_symbol(app.symbol, symbol) return app @@ -41,8 +41,11 @@ def match_inj(pattern: Pattern) -> App: return match_app(pattern, 'inj') -def match_left_assoc(pattern: Pattern) -> LeftAssoc: - return check_type(pattern, LeftAssoc) +def match_left_assoc(pattern: Pattern, symbol: str | None = None) -> LeftAssoc: + assoc = check_type(pattern, LeftAssoc) + if symbol is not None: + match_symbol(assoc.symbol, symbol) + return assoc def match_list(pattern: Pattern) -> tuple[Pattern, ...]: @@ -50,9 +53,8 @@ def match_list(pattern: Pattern) -> tuple[Pattern, ...]: match_app(pattern, "Lbl'Stop'List") return () - assoc = match_left_assoc(pattern) - cons = match_app(assoc.app, "Lbl'Unds'List'Unds'") - items = (match_app(arg, 'LblListItem') for arg in cons.args) + assoc = match_left_assoc(pattern, "Lbl'Unds'List'Unds'") + items = (match_app(arg, 'LblListItem') for arg in assoc.args) elems = (item.args[0] for item in items) return tuple(elems) @@ -62,9 +64,8 @@ def match_set(pattern: Pattern) -> tuple[Pattern, ...]: match_app(pattern, "Lbl'Stop'Set") return () - assoc = match_left_assoc(pattern) - cons = match_app(assoc.app, "Lbl'Unds'Set'Unds'") - items = (match_app(arg, 'LblSetItem') for arg in cons.args) + assoc = match_left_assoc(pattern, "Lbl'Unds'Set'Unds'") + items = (match_app(arg, 'LblSetItem') for arg in assoc.args) elems = (item.args[0] for item in items) return tuple(elems) @@ -79,9 +80,8 @@ def match_map(pattern: Pattern, *, cell: str | None = None) -> tuple[tuple[Patte match_app(pattern, stop_symbol) return () - assoc = match_left_assoc(pattern) - cons = match_app(assoc.app, cons_symbol) - items = (match_app(arg, item_symbol) for arg in cons.args) + assoc = match_left_assoc(pattern, cons_symbol) + items = (match_app(arg, item_symbol) for arg in assoc.args) entries = ((item.args[0], item.args[1]) for item in items) return tuple(entries) diff --git a/pyk/src/pyk/kore/parser.py b/pyk/src/pyk/kore/parser.py index 682da60411c..3235896ceca 100644 --- a/pyk/src/pyk/kore/parser.py +++ b/pyk/src/pyk/kore/parser.py @@ -405,7 +405,7 @@ def _assoc(self, token_type: TokenType, cls: type[AS]) -> AS: self._match(TokenType.LPAREN) app = self.app() self._match(TokenType.RPAREN) - return cls(app) # type: ignore + return cls(app.symbol, app.sorts, app.args) # type: ignore def left_assoc(self) -> LeftAssoc: return self._assoc(TokenType.ML_LEFT_ASSOC, LeftAssoc) diff --git a/pyk/src/pyk/kore/prelude.py b/pyk/src/pyk/kore/prelude.py index aec8c6ffd09..bba3714ed19 100644 --- a/pyk/src/pyk/kore/prelude.py +++ b/pyk/src/pyk/kore/prelude.py @@ -186,12 +186,10 @@ def kseq(kitems: Iterable[Pattern], *, dotvar: EVar | None = None) -> Pattern: if len(args) == 1: return tail - app = App(KSEQ, (), args) - if len(args) == 2: - return app + return App(KSEQ, (), args) - return RightAssoc(app) + return RightAssoc(KSEQ, (), args) def k_config_var(var: str) -> DV: @@ -224,7 +222,7 @@ def top_cell_initializer(config: Mapping[str, Pattern]) -> App: def list_pattern(*args: Pattern) -> Pattern: if not args: return STOP_LIST - return LeftAssoc(App(LBL_LIST, args=(App(LBL_LIST_ITEM, args=(arg,)) for arg in args))) + return LeftAssoc(LBL_LIST, args=(App(LBL_LIST_ITEM, args=(arg,)) for arg in args)) STOP_SET: Final = App("Lbl'Stop'Set") @@ -235,7 +233,7 @@ def list_pattern(*args: Pattern) -> Pattern: def set_pattern(*args: Pattern) -> Pattern: if not args: return STOP_SET - return LeftAssoc(App(LBL_SET, args=(App(LBL_SET_ITEM, args=(arg,)) for arg in args))) + return LeftAssoc(LBL_SET, args=(App(LBL_SET_ITEM, args=(arg,)) for arg in args)) STOP_MAP: Final = App("Lbl'Stop'Map") @@ -249,7 +247,7 @@ def map_pattern(*args: tuple[Pattern, Pattern], cell: str | None = None) -> Patt cons_symbol = SymbolId(f"Lbl'Unds'{cell}Map'Unds'") if cell else LBL_MAP item_symbol = SymbolId(f'Lbl{cell}MapItem') if cell else LBL_MAP_ITEM - return LeftAssoc(App(cons_symbol, args=(App(item_symbol, args=arg) for arg in args))) + return LeftAssoc(cons_symbol, args=(App(item_symbol, args=arg) for arg in args)) STOP_RANGEMAP: Final = App("Lbl'Stop'RangeMap") @@ -263,10 +261,8 @@ def rangemap_pattern(*args: tuple[tuple[Pattern, Pattern], Pattern]) -> Pattern: return STOP_RANGEMAP return LeftAssoc( - App( - LBL_RANGEMAP, - args=(App(LBL_RANGEMAP_ITEM, args=(App(LBL_RANGEMAP_RANGE, args=arg[0]), arg[1])) for arg in args), - ) + LBL_RANGEMAP, + args=(App(LBL_RANGEMAP_ITEM, args=(App(LBL_RANGEMAP_RANGE, args=arg[0]), arg[1])) for arg in args), ) @@ -306,7 +302,7 @@ def json_object(pattern: Pattern) -> App: def jsons(patterns: Iterable[Pattern]) -> RightAssoc: - return RightAssoc(App(LBL_JSONS, (), chain(patterns, (STOP_JSONS,)))) + return RightAssoc(LBL_JSONS, (), chain(patterns, (STOP_JSONS,))) def json_key(key: str) -> App: @@ -370,10 +366,10 @@ def kore_to_json(pattern: Pattern) -> Any: def _iter_json_list(app: App) -> Iterator[Pattern]: from . import match as km - km.match_symbol(app, LBL_JSON_LIST.value) + km.match_app(app, LBL_JSON_LIST.value) curr = km.match_app(app.args[0]) while curr.symbol != STOP_JSONS.symbol: - km.match_symbol(curr, LBL_JSONS.value) + km.match_app(curr, LBL_JSONS.value) yield curr.args[0] curr = km.match_app(curr.args[1]) @@ -381,10 +377,10 @@ def _iter_json_list(app: App) -> Iterator[Pattern]: def _iter_json_object(app: App) -> Iterator[tuple[str, Pattern]]: from . import match as km - km.match_symbol(app, LBL_JSON_OBJECT.value) + km.match_app(app, LBL_JSON_OBJECT.value) curr = km.match_app(app.args[0]) while curr.symbol != STOP_JSONS.symbol: - km.match_symbol(curr, LBL_JSONS.value) + km.match_app(curr, LBL_JSONS.value) entry = km.match_app(curr.args[0], LBL_JSON_ENTRY.value) key = km.kore_str(km.inj(entry.args[0])) value = entry.args[1] diff --git a/pyk/src/pyk/kore/syntax.py b/pyk/src/pyk/kore/syntax.py index 6d112e60a7b..6727fa99531 100644 --- a/pyk/src/pyk/kore/syntax.py +++ b/pyk/src/pyk/kore/syntax.py @@ -275,7 +275,7 @@ def _tag(cls) -> str: # TODO This should be an abstract immutable class attribu def dict(self) -> dict[str, Any]: stack: list = [ self, - self.app.args if isinstance(self, Assoc) else self.patterns, + self.patterns, [], ] @@ -295,7 +295,7 @@ def dict(self) -> dict[str, Any]: else: pattern = patterns[idx] stack.append(pattern) - stack.append(pattern.app.args if isinstance(pattern, Assoc) else pattern.patterns) + stack.append(pattern.patterns) stack.append([]) @property @@ -533,6 +533,158 @@ def write(self, output: IO[str]) -> None: output.write(')') +class Assoc(Pattern): + symbol: str + sorts: tuple[Sort, ...] + args: tuple[Pattern, ...] + + @classmethod + @abstractmethod + def kore_symbol(cls) -> str: ... + + @property + @abstractmethod + def pattern(self) -> Pattern: ... + + @property + def patterns(self) -> tuple[Pattern, ...]: + return self.args + + @cached_property + def app(self) -> App: + return App(symbol=self.symbol, sorts=self.sorts, args=self.args) + + def _dict(self, dicts: list) -> dict[str, Any]: + return { + 'tag': self._tag(), + 'symbol': self.symbol, + 'sorts': [sort.dict for sort in self.sorts], + 'argss': dicts, + } + + def write(self, output: IO[str]) -> None: + output.write(self.kore_symbol()) + output.write('{}(') + self.app.write(output) + output.write(')') + + +@final +@dataclass(frozen=True) +class LeftAssoc(Assoc): + symbol: str + sorts: tuple[Sort, ...] + args: tuple[Pattern, ...] + + def __init__(self, symbol: str | SymbolId, sorts: Iterable[Sort] = (), args: Iterable[Pattern] = ()): + if isinstance(symbol, str): + symbol = SymbolId(symbol) + + args = tuple(args) + if not args: + raise ValueError("Expected non-empty iterable for 'args'") + + object.__setattr__(self, 'symbol', symbol.value) + object.__setattr__(self, 'sorts', tuple(sorts)) + object.__setattr__(self, 'args', args) + + def let( + self, + *, + symbol: str | SymbolId | None = None, + sorts: Iterable | None = None, + args: Iterable | None = None, + ) -> LeftAssoc: + symbol = symbol if symbol is not None else self.symbol + sorts = sorts if sorts is not None else self.sorts + args = args if args is not None else self.args + return LeftAssoc(symbol=symbol, sorts=sorts, args=args) + + def let_patterns(self, patterns: Iterable[Pattern]) -> LeftAssoc: + return self.let(args=patterns) + + @property + def pattern(self) -> Pattern: + res = self.args[0] + for arg in self.args[1:]: + res = App(self.symbol, self.sorts, (res, arg)) + return res + + @classmethod + def _tag(cls) -> str: + return 'LeftAssoc' + + @classmethod + def kore_symbol(cls) -> str: + return '\\left-assoc' + + @classmethod + def _from_dict(cls: type[LeftAssoc], dct: Mapping[str, Any], patterns: list[Pattern]) -> LeftAssoc: + return LeftAssoc( + symbol=dct['symbol'], + sorts=tuple(Sort.from_dict(sort) for sort in dct['sorts']), + args=patterns, + ) + + +@final +@dataclass(frozen=True) +class RightAssoc(Assoc): + symbol: str + sorts: tuple[Sort, ...] + args: tuple[Pattern, ...] + + def __init__(self, symbol: str | SymbolId, sorts: Iterable[Sort] = (), args: Iterable[Pattern] = ()): + if isinstance(symbol, str): + symbol = SymbolId(symbol) + + args = tuple(args) + if not args: + raise ValueError("Expected non-empty iterable for 'args'") + + object.__setattr__(self, 'symbol', symbol.value) + object.__setattr__(self, 'sorts', tuple(sorts)) + object.__setattr__(self, 'args', args) + + def let( + self, + *, + symbol: str | SymbolId | None = None, + sorts: Iterable | None = None, + args: Iterable | None = None, + ) -> RightAssoc: + symbol = symbol if symbol is not None else self.symbol + sorts = sorts if sorts is not None else self.sorts + args = args if args is not None else self.args + return RightAssoc(symbol=symbol, sorts=sorts, args=args) + + def let_patterns(self, patterns: Iterable[Pattern]) -> RightAssoc: + return self.let(args=patterns) + + @property + def pattern(self) -> Pattern: + res = self.args[-1] + for arg in reversed(self.args[:-1]): + res = App(self.symbol, (), (arg, res)) + return res + + @classmethod + def _tag(cls) -> str: + return 'RightAssoc' + + @classmethod + def kore_symbol(cls) -> str: + return '\\right-assoc' + + @classmethod + def _from_dict(cls: type[RightAssoc], dct: Mapping[str, Any], patterns: list[Pattern]) -> RightAssoc: + return RightAssoc( + symbol=dct['symbol'], + sorts=tuple(Sort.from_dict(sort) for sort in dct['sorts']), + args=patterns, + ) + + class MLPattern(Pattern): @classmethod @abstractmethod @@ -563,7 +715,7 @@ def sorts(self) -> tuple[Sort, ...]: ... def ctor_patterns(self) -> tuple[Pattern, ...]: """Return patterns used to construct the term with `of`. - Except for `Assoc`, `DV`, `MLFixpoint` and `MLQuant` this coincides with `patterns`. + Except for `DV`, `MLFixpoint` and `MLQuant` this coincides with `patterns`. """ return self.patterns @@ -1609,150 +1761,6 @@ def _dict(self, dicts: list) -> dict[str, Any]: return {'tag': 'DV', 'sort': self.sort.dict, 'value': self.value.value} -class MLSyntaxSugar(MLPattern): ... - - -# TODO AppAssoc, OrAssoc -class Assoc(MLSyntaxSugar): - app: App - - @property - @abstractmethod - def pattern(self) -> Pattern: ... - - @property - def sorts(self) -> tuple[()]: - return () - - @property - def patterns(self) -> tuple[()]: - return () - - @property - def ctor_patterns(self) -> tuple[App]: - return (self.app,) - - def _dict(self, dicts: list) -> dict[str, Any]: - return { - 'tag': self._tag(), - 'symbol': self.app.symbol, - 'sorts': [sort.dict for sort in self.app.sorts], - 'argss': dicts, - } - - -@final -@dataclass(frozen=True) -class LeftAssoc(Assoc): - app: App - - def let(self, *, app: App | None = None) -> LeftAssoc: - app = app if app is not None else self.app - return LeftAssoc(app=app) - - def let_patterns(self, patterns: Iterable[Pattern]) -> LeftAssoc: - () = patterns - return self - - @property - def pattern(self) -> Pattern: - if len(self.app.sorts) > 0: - raise ValueError(f'Cannot associate a pattern with sort parameters: {self}') - if len(self.app.args) == 0: - raise ValueError(f'Cannot associate a pattern with no arguments: {self}') - ret = self.app.args[0] - for a in self.app.args[1:]: - ret = App(self.app.symbol, (), (ret, a)) - return ret - - @classmethod - def _tag(cls) -> str: - return 'LeftAssoc' - - @classmethod - def symbol(cls) -> str: - return '\\left-assoc' - - @classmethod - def of( - cls: type[LeftAssoc], - symbol: str, - sorts: Iterable[Sort] = (), - patterns: Iterable[Pattern] = (), - ) -> LeftAssoc: - cls._check_symbol(symbol) - () = sorts - (app,) = patterns - app = check_type(app, App) - return LeftAssoc(app=app) - - @classmethod - def _from_dict(cls: type[LeftAssoc], dct: Mapping[str, Any], patterns: list[Pattern]) -> LeftAssoc: - return LeftAssoc( - app=App( - symbol=dct['symbol'], - sorts=tuple(Sort.from_dict(sort) for sort in dct['sorts']), - args=patterns, - ), - ) - - -@final -@dataclass(frozen=True) -class RightAssoc(Assoc): - app: App - - def let(self, *, app: App | None = None) -> RightAssoc: - app = app if app is not None else self.app - return RightAssoc(app=app) - - def let_patterns(self, patterns: Iterable[Pattern]) -> RightAssoc: - () = patterns - return self - - @property - def pattern(self) -> Pattern: - if len(self.app.sorts) > 0: - raise ValueError(f'Cannot associate a pattern with sort parameters: {self}') - if len(self.app.args) == 0: - raise ValueError(f'Cannot associate a pattern with no arguments: {self}') - ret = self.app.args[-1] - for a in reversed(self.app.args[:-1]): - ret = App(self.app.symbol, (), (a, ret)) - return ret - - @classmethod - def _tag(cls) -> str: - return 'RightAssoc' - - @classmethod - def symbol(cls) -> str: - return '\\right-assoc' - - @classmethod - def of( - cls: type[RightAssoc], - symbol: str, - sorts: Iterable[Sort] = (), - patterns: Iterable[Pattern] = (), - ) -> RightAssoc: - cls._check_symbol(symbol) - () = sorts - (app,) = patterns - app = check_type(app, App) - return RightAssoc(app=app) - - @classmethod - def _from_dict(cls: type[RightAssoc], dct: Mapping[str, Any], patterns: list[Pattern]) -> RightAssoc: - return RightAssoc( - app=App( - symbol=dct['symbol'], - sorts=tuple(Sort.from_dict(sort) for sort in dct['sorts']), - args=patterns, - ), - ) - - ML_SYMBOLS: Final = { r'\top': Top, r'\bottom': Bottom, @@ -1772,8 +1780,6 @@ def _from_dict(cls: type[RightAssoc], dct: Mapping[str, Any], patterns: list[Pat r'\next': Next, r'\rewrites': Rewrites, r'\dv': DV, - r'\left-assoc': LeftAssoc, - r'\right-assoc': RightAssoc, } diff --git a/pyk/src/pyk/ktool/kfuzz.py b/pyk/src/pyk/ktool/kfuzz.py index b2d02971564..8e1a6ad0b88 100644 --- a/pyk/src/pyk/ktool/kfuzz.py +++ b/pyk/src/pyk/ktool/kfuzz.py @@ -8,7 +8,7 @@ from ..kast.inner import KSort from ..konvert import _kast_to_kore from ..kore.parser import KoreParser -from ..kore.syntax import Assoc, EVar +from ..kore.syntax import EVar from ..prelude.k import inj from ..prelude.kint import intToken from .krun import llvm_interpret_raw @@ -80,10 +80,6 @@ def fuzz( def test(subst_case: Mapping[EVar, Pattern]) -> None: def sub(p: Pattern) -> Pattern: - if isinstance(p, Assoc): - symbol = p.symbol() - args = (arg.top_down(sub) for arg in p.app.args) - return p.of(symbol, patterns=(p.app.let(args=args),)) if p in subst_case: assert isinstance(p, EVar) return subst_case[p] diff --git a/pyk/src/tests/integration/ktool/test_fuzz.py b/pyk/src/tests/integration/ktool/test_fuzz.py index 76d34f9d6af..6e8b00a8f01 100644 --- a/pyk/src/tests/integration/ktool/test_fuzz.py +++ b/pyk/src/tests/integration/ktool/test_fuzz.py @@ -8,7 +8,7 @@ from pyk.kast.inner import KSort from pyk.kore.parser import KoreParser from pyk.kore.prelude import inj, top_cell_initializer -from pyk.kore.syntax import DV, App, Assoc, EVar, SortApp, String +from pyk.kore.syntax import DV, App, EVar, SortApp, String from pyk.ktool.kfuzz import fuzz, kintegers from pyk.ktool.kprint import _kast from pyk.testing import KompiledTest @@ -38,10 +38,6 @@ class TestImpFuzz(KompiledTest): def check(p: Pattern) -> None: def check_inner(p: Pattern) -> Pattern: match p: - case Assoc(): - symbol = p.symbol() - args = (arg.top_down(check_inner) for arg in p.app.args) - return p.of(symbol, patterns=(p.app.let(args=args),)) case App("Lbl'UndsPipe'-'-GT-Unds'", args=(key, val)): match key, val: case ( diff --git a/pyk/src/tests/unit/kore/test_ml_pattern.py b/pyk/src/tests/unit/kore/test_ml_pattern.py index b74357e024a..7b1fc1df4bc 100644 --- a/pyk/src/tests/unit/kore/test_ml_pattern.py +++ b/pyk/src/tests/unit/kore/test_ml_pattern.py @@ -18,7 +18,6 @@ Iff, Implies, In, - LeftAssoc, MLPattern, Mu, Next, @@ -26,7 +25,6 @@ Nu, Or, Rewrites, - RightAssoc, SortApp, String, SVar, @@ -71,8 +69,6 @@ ('next', r'\next', (s,), (x,), Next(s, x)), ('rewrites', r'\rewrites', (s,), (x, y), Rewrites(s, x, y)), ('dv', r'\dv', (s,), (val,), DV(s, val)), - ('left-assoc', r'\left-assoc', (), (app,), LeftAssoc(app)), - ('right-assoc', r'\right-assoc', (), (app,), RightAssoc(app)), )