From aaa6752e83fa7ccc3cb928df97a2da28e6f7a2fb Mon Sep 17 00:00:00 2001 From: Everett Hildenbrandt Date: Sat, 25 Apr 2026 03:16:46 +0000 Subject: [PATCH 01/11] test_definition: add unit tests for add_cell_map_items guard Tests both the positive path (wrap when parent production expects the cell map sort) and the negative path (no wrap when parent expects the individual cell element sort) introduced in 78bfdab101. The cell-map productions are merged into the existing single DEFN to keep the fixture count low. Co-Authored-By: Claude Sonnet 4.6 --- pyk/src/tests/unit/kast/test_definition.py | 250 +++++++++++++++++++++ 1 file changed, 250 insertions(+) create mode 100644 pyk/src/tests/unit/kast/test_definition.py diff --git a/pyk/src/tests/unit/kast/test_definition.py b/pyk/src/tests/unit/kast/test_definition.py new file mode 100644 index 0000000000..da397e3916 --- /dev/null +++ b/pyk/src/tests/unit/kast/test_definition.py @@ -0,0 +1,250 @@ +from __future__ import annotations + +from typing import TYPE_CHECKING + +import pytest + +from pyk.kast.att import Atts, KAtt +from pyk.kast.inner import KApply, KAs, KLabel, KSequence, KSort, KToken, KVariable +from pyk.kast.outer import KDefinition, KFlatModule, KNonTerminal, KProduction, KTerminal + +if TYPE_CHECKING: + from typing import Final + + from pyk.kast.inner import KInner + + +# --------------------------------------------------------------------------- +# Minimal test definition +# +# bar: syntax N ::= bar(N) -- result sort is the param directly +# foo: syntax MInt{N} ::= foo(MInt{N}) -- result/arg sorts nest the param +# #Equals: syntax S2 ::= #Equals{S1,S2}(S1, S1) -- ML pred, result sort context-dependent +# +# Cell map fragment: +# AccountCellMap ::= AccountCellMap AccountCellMap [cellCollection, element(AccountCellMapItem), wrapElement()] +# AccountCellMap ::= AccountCellMapItem(Int, AccountCell) +# AccountCell ::= (Int, Int) +# AccountCell ::= getEntry(AccountCell) -- takes element sort, NOT map sort +# --------------------------------------------------------------------------- + +INT: Final = KSort('Int') +N: Final = KSort('N') +S1: Final = KSort('S1') +S2: Final = KSort('S2') +MINT_N: Final = KSort('MInt', (N,)) +MINT_INT: Final = KSort('MInt', (INT,)) +SORT_PARAM: Final = KSort('#SortParam') +ACCOUNT_CELL_MAP: Final = KSort('AccountCellMap') +ACCOUNT_CELL: Final = KSort('AccountCell') + +_BAR_PROD: Final = KProduction( + sort=N, + items=[KTerminal('bar'), KTerminal('('), KNonTerminal(N), KTerminal(')')], + params=[N], + klabel='bar', +) + +_FOO_PROD: Final = KProduction( + sort=MINT_N, + items=[KTerminal('foo'), KTerminal('('), KNonTerminal(MINT_N), KTerminal(')')], + params=[N], + klabel='foo', +) + +_EQUALS_PROD: Final = KProduction( + sort=S2, + items=[KNonTerminal(S1), KNonTerminal(S1)], + params=[S1, S2], + klabel='#Equals', +) + +_ACCT_MAP_CONCAT: Final = KProduction( + sort=ACCOUNT_CELL_MAP, + items=[KNonTerminal(ACCOUNT_CELL_MAP), KNonTerminal(ACCOUNT_CELL_MAP)], + klabel='_AccountCellMap_', + att=KAtt(entries=[Atts.CELL_COLLECTION(None), Atts.ELEMENT('AccountCellMapItem'), Atts.WRAP_ELEMENT('')]), +) + +_ACCT_MAP_ITEM: Final = KProduction( + sort=ACCOUNT_CELL_MAP, + items=[ + KTerminal('AccountCellMapItem'), + KTerminal('('), + KNonTerminal(INT), + KTerminal(','), + KNonTerminal(ACCOUNT_CELL), + KTerminal(')'), + ], + klabel='AccountCellMapItem', +) + +_ACCOUNT_CELL: Final = KProduction( + sort=ACCOUNT_CELL, + items=[ + KTerminal(''), + KTerminal('('), + KNonTerminal(INT), + KTerminal(','), + KNonTerminal(INT), + KTerminal(')'), + ], + klabel='', +) + +_GET_ENTRY: Final = KProduction( + sort=ACCOUNT_CELL, + items=[KTerminal('getEntry'), KTerminal('('), KNonTerminal(ACCOUNT_CELL), KTerminal(')')], + klabel='getEntry', +) + +DEFN: Final = KDefinition( + 'TEST', + [ + KFlatModule( + 'TEST', [_BAR_PROD, _FOO_PROD, _EQUALS_PROD, _ACCT_MAP_CONCAT, _ACCT_MAP_ITEM, _ACCOUNT_CELL, _GET_ENTRY] + ) + ], +) + + +# --------------------------------------------------------------------------- +# KDefinition.sort +# --------------------------------------------------------------------------- + +SORT_DATA: Final = ( + # Basic leaf terms + ('ktoken', KToken('42', INT), INT), + ('kvariable_with_sort', KVariable('X', sort=INT), INT), + ('ksequence', KSequence([]), KSort('K')), + # KApply: result sort substituted directly from param + ('kapply_direct_result', KApply(KLabel('bar', [INT]), [KVariable('X', sort=INT)]), INT), + # KApply: result sort nests the param (MInt{N} with N→Int → MInt{Int}) + ('kapply_nested_result', KApply(KLabel('foo', [INT]), [KVariable('X', sort=MINT_INT)]), MINT_INT), + # KApply with unfilled sort params: sort() returns None rather than raising + ('kapply_unfilled_params', KApply(KLabel('foo'), [KVariable('X', sort=MINT_INT)]), None), + # KApply with unknown label: KeyError from symbols lookup → None + ('kapply_unknown_label', KApply(KLabel('nonexistent'), []), None), + # KAs: sort of the alias variable + ('kas_sorted_alias', KAs(KVariable('X', sort=MINT_INT), KVariable('Y', sort=MINT_INT)), MINT_INT), + # KAs whose alias has no sort annotation: returns None + ('kas_unsorted_alias', KAs(KVariable('X', sort=MINT_INT), KVariable('Y')), None), +) + + +@pytest.mark.parametrize( + 'test_id,term,expected', + SORT_DATA, + ids=[test_id for test_id, *_ in SORT_DATA], +) +def test_sort(test_id: str, term: KInner, expected: KSort | None) -> None: + assert DEFN.sort(term) == expected + + +# --------------------------------------------------------------------------- +# KDefinition.resolve_sorts +# --------------------------------------------------------------------------- + +RESOLVE_SORTS_DATA: Final = ( + # Direct substitution: result sort IS the param (N → Int) + ('direct_bar', KLabel('bar', [INT]), INT, (INT,)), + # Recursive substitution: result/arg sort nests the param (MInt{N} with N → Int → MInt{Int}) + ('nested_foo', KLabel('foo', [INT]), MINT_INT, (MINT_INT,)), +) + + +@pytest.mark.parametrize( + 'test_id,label,expected_result,expected_args', + RESOLVE_SORTS_DATA, + ids=[test_id for test_id, *_ in RESOLVE_SORTS_DATA], +) +def test_resolve_sorts(test_id: str, label: KLabel, expected_result: KSort, expected_args: tuple[KSort, ...]) -> None: + result, args = DEFN.resolve_sorts(label) + assert result == expected_result + assert args == expected_args + + +# --------------------------------------------------------------------------- +# KDefinition.add_sort_params +# --------------------------------------------------------------------------- + +ADD_SORT_PARAMS_DATA: Final = ( + # Label already has params filled: leave unchanged + ( + 'already_filled', + KApply(KLabel('bar', [INT]), [KVariable('X', sort=INT)]), + KApply(KLabel('bar', [INT]), [KVariable('X', sort=INT)]), + ), + # Direct sort param: psort IS the param (N ~ Int → N=Int) + ( + 'direct_param', + KApply(KLabel('bar'), [KVariable('X', sort=INT)]), + KApply(KLabel('bar', [INT]), [KVariable('X', sort=INT)]), + ), + # Nested sort param: psort = MInt{N}, asort = MInt{Int} → N=Int via unification + ( + 'nested_param', + KApply(KLabel('foo'), [KVariable('X', sort=MINT_INT)]), + KApply(KLabel('foo', [INT]), [KVariable('X', sort=MINT_INT)]), + ), + # ML pred: S1 inferred from args, S2 (result sort) filled with #SortParam sentinel + ( + 'ml_pred_sentinel', + KApply('#Equals', [KVariable('X', sort=INT), KVariable('Y', sort=INT)]), + KApply(KLabel('#Equals', [INT, SORT_PARAM]), [KVariable('X', sort=INT), KVariable('Y', sort=INT)]), + ), + # Unsortable argument (no sort annotation): cannot fill params, term returned unchanged + ( + 'unsortable_arg_unchanged', + KApply(KLabel('foo'), [KVariable('X')]), + KApply(KLabel('foo'), [KVariable('X')]), + ), +) + + +@pytest.mark.parametrize( + 'test_id,term,expected', + ADD_SORT_PARAMS_DATA, + ids=[test_id for test_id, *_ in ADD_SORT_PARAMS_DATA], +) +def test_add_sort_params(test_id: str, term: KInner, expected: KInner) -> None: + assert DEFN.add_sort_params(term) == expected + + +# --------------------------------------------------------------------------- +# KDefinition.add_cell_map_items +# --------------------------------------------------------------------------- + +_ACCT_1: Final = KApply('', [KVariable('X', sort=INT), KVariable('Y', sort=INT)]) +_ACCT_2: Final = KApply('', [KVariable('A', sort=INT), KVariable('B', sort=INT)]) + +ADD_CELL_MAP_ITEMS_DATA: Final = ( + # Parent expects AccountCellMap (the map sort) — children are wrapped in AccountCellMapItem. + ( + 'wraps_when_parent_expects_cell_map_sort', + KApply('_AccountCellMap_', [_ACCT_1, _ACCT_2]), + KApply( + '_AccountCellMap_', + [ + KApply('AccountCellMapItem', [KVariable('X', sort=INT), _ACCT_1]), + KApply('AccountCellMapItem', [KVariable('A', sort=INT), _ACCT_2]), + ], + ), + ), + # Parent expects AccountCell (the element sort) — the child must NOT be wrapped. + # Before the guard fix, _wrap_elements would incorrectly wrap here too. + ( + 'no_wrap_when_parent_expects_cell_element_sort', + KApply('getEntry', [_ACCT_1]), + KApply('getEntry', [_ACCT_1]), + ), +) + + +@pytest.mark.parametrize( + 'test_id,term,expected', + ADD_CELL_MAP_ITEMS_DATA, + ids=[test_id for test_id, *_ in ADD_CELL_MAP_ITEMS_DATA], +) +def test_add_cell_map_items(test_id: str, term: KInner, expected: KInner) -> None: + assert DEFN.add_cell_map_items(term) == expected From db94185b92552a5bdc3d05a701e6b446e49e5aef Mon Sep 17 00:00:00 2001 From: Everett Hildenbrandt Date: Sat, 25 Apr 2026 01:35:23 +0000 Subject: [PATCH 02/11] outer: add_cell_map_items wraps only when parent expects cell map sort The old _wrap_elements unconditionally wrapped any KApply matching a cell label, even when the parent production expected the individual cell sort (not the map sort). This caused double-wrapping in productions like EntryCellMapKey((...)) where the argument sort is EntryCell, not EntryCellMap. The new implementation inspects the parent production's expected argument sorts and only wraps when the expected sort matches the cell map sort (e.g. EntryCellMap). Co-Authored-By: Claude Sonnet 4.6 --- pyk/src/pyk/kast/outer.py | 30 +++++++++++++++++++++++++----- 1 file changed, 25 insertions(+), 5 deletions(-) diff --git a/pyk/src/pyk/kast/outer.py b/pyk/src/pyk/kast/outer.py index 774a004e5c..f58e5402ac 100644 --- a/pyk/src/pyk/kast/outer.py +++ b/pyk/src/pyk/kast/outer.py @@ -1515,15 +1515,35 @@ def add_cell_map_items(self, kast: KInner) -> KInner: # syntax AccountCellMap [cellCollection, hook(MAP.Map)] # syntax AccountCellMap ::= AccountCellMap AccountCellMap [assoc, avoid, cellCollection, comm, element(AccountCellMapItem), function, hook(MAP.concat), unit(.AccountCellMap), wrapElement()] - cell_wrappers = {} + # Maps cell label -> (element_constructor, cell_map_sort). + # Wrapping is correct only when the parent production expects the cell MAP sort (e.g. + # EntryCellMap), not when it expects the individual cell element sort (e.g. EntryCell). + # For example, EntryCellMapKey((...)) takes EntryCell — the must NOT be + # wrapped, whereas _EntryCellMap_((...), ...) expects EntryCellMap — wrapping is needed. + cell_wrappers: dict[str, tuple[str, KSort]] = {} for ccp in self.cell_collection_productions: if Atts.ELEMENT in ccp.att and Atts.WRAP_ELEMENT in ccp.att: - cell_wrappers[ccp.att[Atts.WRAP_ELEMENT]] = ccp.att[Atts.ELEMENT] + cell_label = ccp.att[Atts.WRAP_ELEMENT] + element_ctor = ccp.att[Atts.ELEMENT] + if element_ctor in self.symbols: + cell_wrappers[cell_label] = (element_ctor, self.symbols[element_ctor].sort) def _wrap_elements(_k: KInner) -> KInner: - if type(_k) is KApply and _k.label.name in cell_wrappers: - return KApply(cell_wrappers[_k.label.name], [_k.args[0], _k]) - return _k + if not isinstance(_k, KApply) or _k.label.name not in self.symbols: + return _k + prod = self.symbols[_k.label.name] + arg_sorts = prod.argument_sorts + if not arg_sorts or len(arg_sorts) != _k.arity: + return _k + new_args: list[KInner] = list(_k.args) + changed = False + for i, (arg_sort, arg) in enumerate(zip(arg_sorts, _k.args, strict=True)): + if isinstance(arg, KApply) and arg.label.name in cell_wrappers: + element_ctor, cell_map_sort = cell_wrappers[arg.label.name] + if arg_sort == cell_map_sort: + new_args[i] = KApply(element_ctor, [arg.args[0], arg]) + changed = True + return _k.let(args=new_args) if changed else _k # To ensure we don't get duplicate wrappers. _kast = self.remove_cell_map_items(kast) From 82117ea8cffee7494367e2a9bee2f0acbd619cdd Mon Sep 17 00:00:00 2001 From: Everett Hildenbrandt Date: Mon, 11 May 2026 22:38:10 +0000 Subject: [PATCH 03/11] pyk/test_definition: minimize to test definition just for cell map items --- pyk/src/tests/unit/kast/test_definition.py | 143 +-------------------- 1 file changed, 2 insertions(+), 141 deletions(-) diff --git a/pyk/src/tests/unit/kast/test_definition.py b/pyk/src/tests/unit/kast/test_definition.py index da397e3916..1b6f987be0 100644 --- a/pyk/src/tests/unit/kast/test_definition.py +++ b/pyk/src/tests/unit/kast/test_definition.py @@ -5,7 +5,7 @@ import pytest from pyk.kast.att import Atts, KAtt -from pyk.kast.inner import KApply, KAs, KLabel, KSequence, KSort, KToken, KVariable +from pyk.kast.inner import KApply, KSort, KVariable from pyk.kast.outer import KDefinition, KFlatModule, KNonTerminal, KProduction, KTerminal if TYPE_CHECKING: @@ -17,10 +17,6 @@ # --------------------------------------------------------------------------- # Minimal test definition # -# bar: syntax N ::= bar(N) -- result sort is the param directly -# foo: syntax MInt{N} ::= foo(MInt{N}) -- result/arg sorts nest the param -# #Equals: syntax S2 ::= #Equals{S1,S2}(S1, S1) -- ML pred, result sort context-dependent -# # Cell map fragment: # AccountCellMap ::= AccountCellMap AccountCellMap [cellCollection, element(AccountCellMapItem), wrapElement()] # AccountCellMap ::= AccountCellMapItem(Int, AccountCell) @@ -29,36 +25,9 @@ # --------------------------------------------------------------------------- INT: Final = KSort('Int') -N: Final = KSort('N') -S1: Final = KSort('S1') -S2: Final = KSort('S2') -MINT_N: Final = KSort('MInt', (N,)) -MINT_INT: Final = KSort('MInt', (INT,)) -SORT_PARAM: Final = KSort('#SortParam') ACCOUNT_CELL_MAP: Final = KSort('AccountCellMap') ACCOUNT_CELL: Final = KSort('AccountCell') -_BAR_PROD: Final = KProduction( - sort=N, - items=[KTerminal('bar'), KTerminal('('), KNonTerminal(N), KTerminal(')')], - params=[N], - klabel='bar', -) - -_FOO_PROD: Final = KProduction( - sort=MINT_N, - items=[KTerminal('foo'), KTerminal('('), KNonTerminal(MINT_N), KTerminal(')')], - params=[N], - klabel='foo', -) - -_EQUALS_PROD: Final = KProduction( - sort=S2, - items=[KNonTerminal(S1), KNonTerminal(S1)], - params=[S1, S2], - klabel='#Equals', -) - _ACCT_MAP_CONCAT: Final = KProduction( sort=ACCOUNT_CELL_MAP, items=[KNonTerminal(ACCOUNT_CELL_MAP), KNonTerminal(ACCOUNT_CELL_MAP)], @@ -100,117 +69,9 @@ DEFN: Final = KDefinition( 'TEST', - [ - KFlatModule( - 'TEST', [_BAR_PROD, _FOO_PROD, _EQUALS_PROD, _ACCT_MAP_CONCAT, _ACCT_MAP_ITEM, _ACCOUNT_CELL, _GET_ENTRY] - ) - ], -) - - -# --------------------------------------------------------------------------- -# KDefinition.sort -# --------------------------------------------------------------------------- - -SORT_DATA: Final = ( - # Basic leaf terms - ('ktoken', KToken('42', INT), INT), - ('kvariable_with_sort', KVariable('X', sort=INT), INT), - ('ksequence', KSequence([]), KSort('K')), - # KApply: result sort substituted directly from param - ('kapply_direct_result', KApply(KLabel('bar', [INT]), [KVariable('X', sort=INT)]), INT), - # KApply: result sort nests the param (MInt{N} with N→Int → MInt{Int}) - ('kapply_nested_result', KApply(KLabel('foo', [INT]), [KVariable('X', sort=MINT_INT)]), MINT_INT), - # KApply with unfilled sort params: sort() returns None rather than raising - ('kapply_unfilled_params', KApply(KLabel('foo'), [KVariable('X', sort=MINT_INT)]), None), - # KApply with unknown label: KeyError from symbols lookup → None - ('kapply_unknown_label', KApply(KLabel('nonexistent'), []), None), - # KAs: sort of the alias variable - ('kas_sorted_alias', KAs(KVariable('X', sort=MINT_INT), KVariable('Y', sort=MINT_INT)), MINT_INT), - # KAs whose alias has no sort annotation: returns None - ('kas_unsorted_alias', KAs(KVariable('X', sort=MINT_INT), KVariable('Y')), None), + [KFlatModule('TEST', [_ACCT_MAP_CONCAT, _ACCT_MAP_ITEM, _ACCOUNT_CELL, _GET_ENTRY])], ) - -@pytest.mark.parametrize( - 'test_id,term,expected', - SORT_DATA, - ids=[test_id for test_id, *_ in SORT_DATA], -) -def test_sort(test_id: str, term: KInner, expected: KSort | None) -> None: - assert DEFN.sort(term) == expected - - -# --------------------------------------------------------------------------- -# KDefinition.resolve_sorts -# --------------------------------------------------------------------------- - -RESOLVE_SORTS_DATA: Final = ( - # Direct substitution: result sort IS the param (N → Int) - ('direct_bar', KLabel('bar', [INT]), INT, (INT,)), - # Recursive substitution: result/arg sort nests the param (MInt{N} with N → Int → MInt{Int}) - ('nested_foo', KLabel('foo', [INT]), MINT_INT, (MINT_INT,)), -) - - -@pytest.mark.parametrize( - 'test_id,label,expected_result,expected_args', - RESOLVE_SORTS_DATA, - ids=[test_id for test_id, *_ in RESOLVE_SORTS_DATA], -) -def test_resolve_sorts(test_id: str, label: KLabel, expected_result: KSort, expected_args: tuple[KSort, ...]) -> None: - result, args = DEFN.resolve_sorts(label) - assert result == expected_result - assert args == expected_args - - -# --------------------------------------------------------------------------- -# KDefinition.add_sort_params -# --------------------------------------------------------------------------- - -ADD_SORT_PARAMS_DATA: Final = ( - # Label already has params filled: leave unchanged - ( - 'already_filled', - KApply(KLabel('bar', [INT]), [KVariable('X', sort=INT)]), - KApply(KLabel('bar', [INT]), [KVariable('X', sort=INT)]), - ), - # Direct sort param: psort IS the param (N ~ Int → N=Int) - ( - 'direct_param', - KApply(KLabel('bar'), [KVariable('X', sort=INT)]), - KApply(KLabel('bar', [INT]), [KVariable('X', sort=INT)]), - ), - # Nested sort param: psort = MInt{N}, asort = MInt{Int} → N=Int via unification - ( - 'nested_param', - KApply(KLabel('foo'), [KVariable('X', sort=MINT_INT)]), - KApply(KLabel('foo', [INT]), [KVariable('X', sort=MINT_INT)]), - ), - # ML pred: S1 inferred from args, S2 (result sort) filled with #SortParam sentinel - ( - 'ml_pred_sentinel', - KApply('#Equals', [KVariable('X', sort=INT), KVariable('Y', sort=INT)]), - KApply(KLabel('#Equals', [INT, SORT_PARAM]), [KVariable('X', sort=INT), KVariable('Y', sort=INT)]), - ), - # Unsortable argument (no sort annotation): cannot fill params, term returned unchanged - ( - 'unsortable_arg_unchanged', - KApply(KLabel('foo'), [KVariable('X')]), - KApply(KLabel('foo'), [KVariable('X')]), - ), -) - - -@pytest.mark.parametrize( - 'test_id,term,expected', - ADD_SORT_PARAMS_DATA, - ids=[test_id for test_id, *_ in ADD_SORT_PARAMS_DATA], -) -def test_add_sort_params(test_id: str, term: KInner, expected: KInner) -> None: - assert DEFN.add_sort_params(term) == expected - - # --------------------------------------------------------------------------- # KDefinition.add_cell_map_items # --------------------------------------------------------------------------- From 5747b8371b21d3b28678c488c591a36f16f1a99a Mon Sep 17 00:00:00 2001 From: Everett Hildenbrandt Date: Mon, 11 May 2026 23:02:23 +0000 Subject: [PATCH 04/11] __main__, cli/pyk, ktool/krun: add --parser flag to pyk run Forwards the krun --parser option through RunOptions and KRun.krun() so callers can supply a custom parser command, matching pyk run's behaviour to the full krun CLI. Co-Authored-By: Claude Sonnet 4.6 --- pyk/src/pyk/__main__.py | 2 +- pyk/src/pyk/cli/pyk.py | 3 +++ pyk/src/pyk/ktool/krun.py | 4 ++-- 3 files changed, 6 insertions(+), 3 deletions(-) diff --git a/pyk/src/pyk/__main__.py b/pyk/src/pyk/__main__.py index 7a9b63773d..f958936569 100644 --- a/pyk/src/pyk/__main__.py +++ b/pyk/src/pyk/__main__.py @@ -373,7 +373,7 @@ def exec_run(options: RunOptions) -> None: else: kompiled_directory = options.definition_dir krun = KRun(kompiled_directory) - rc, res = krun.krun(pgm_file) + rc, res = krun.krun(pgm_file, parser=options.parser) print(krun.pretty_print(res)) sys.exit(rc) diff --git a/pyk/src/pyk/cli/pyk.py b/pyk/src/pyk/cli/pyk.py index ad6523df64..432eaf7194 100644 --- a/pyk/src/pyk/cli/pyk.py +++ b/pyk/src/pyk/cli/pyk.py @@ -354,11 +354,13 @@ def get_argument_type() -> dict[str, Callable]: class RunOptions(LoggingOptions): pgm_file: str definition_dir: Path | None + parser: str | None @staticmethod def default() -> dict[str, Any]: return { 'definition_dir': None, + 'parser': None, } @staticmethod @@ -481,6 +483,7 @@ def create_argument_parser() -> ArgumentParser: ) run_args.add_argument('pgm_file', type=str, help='File program to run in it.') run_args.add_argument('--definition', type=dir_path, dest='definition_dir', help='Path to definition to use.') + run_args.add_argument('--parser', type=str, help='Command to use as a custom parser.') prove_args = pyk_args_command.add_parser( 'prove', diff --git a/pyk/src/pyk/ktool/krun.py b/pyk/src/pyk/ktool/krun.py index a48af64f85..5840eadb0d 100644 --- a/pyk/src/pyk/ktool/krun.py +++ b/pyk/src/pyk/ktool/krun.py @@ -294,8 +294,8 @@ def run_pattern( assert parser.eof return res - def krun(self, input_file: Path) -> tuple[int, KInner]: - result = _krun(input_file=input_file, definition_dir=self.definition_dir, output=KRunOutput.KORE) + def krun(self, input_file: Path, parser: str | None = None) -> tuple[int, KInner]: + result = _krun(input_file=input_file, definition_dir=self.definition_dir, output=KRunOutput.KORE, parser=parser) kore = KoreParser(result.stdout).pattern() kast = self.kore_to_kast(kore) return (result.returncode, kast) From f0132ab1eb4d168513305a2a15e2123b35500e94 Mon Sep 17 00:00:00 2001 From: Everett Hildenbrandt Date: Mon, 11 May 2026 23:02:28 +0000 Subject: [PATCH 05/11] regression-new: enable star-multiplicity, issue-582, krun-deserialize All three were skipped solely because pyk run lacked --parser support. Update baselines to reflect current compiler output: wrapper, cell, and updated map ordering. Co-Authored-By: Claude Sonnet 4.6 --- pyk/regression-new/issue-582/1.test.out | 11 +++++++--- .../krun-deserialize/sum.kore.imp.out | 22 +++++++++++-------- pyk/regression-new/skipped | 3 --- .../star-multiplicity/1.test.out | 11 ++++++---- 4 files changed, 28 insertions(+), 19 deletions(-) diff --git a/pyk/regression-new/issue-582/1.test.out b/pyk/regression-new/issue-582/1.test.out index 7a725d8aac..d07631500c 100644 --- a/pyk/regression-new/issue-582/1.test.out +++ b/pyk/regression-new/issue-582/1.test.out @@ -1,3 +1,8 @@ - - 7 ~> .K - + + + 7 ~> .K + + + 0 + + diff --git a/pyk/regression-new/krun-deserialize/sum.kore.imp.out b/pyk/regression-new/krun-deserialize/sum.kore.imp.out index d6373fd27e..1bdb52e2df 100644 --- a/pyk/regression-new/krun-deserialize/sum.kore.imp.out +++ b/pyk/regression-new/krun-deserialize/sum.kore.imp.out @@ -1,9 +1,13 @@ - - - .K - - - n |-> 0 - sum |-> 5050 - - + + + + .K + + + sum |-> 5050 n |-> 0 + + + + 0 + + diff --git a/pyk/regression-new/skipped b/pyk/regression-new/skipped index d3666d457a..1bf314d0a1 100644 --- a/pyk/regression-new/skipped +++ b/pyk/regression-new/skipped @@ -51,7 +51,6 @@ issue-3446 issue-3520-freshConfig issue-3647-debugTokens issue-3672-debugParse -issue-582 ite-bug itp json-input @@ -69,7 +68,6 @@ kprove-error-status kprove-java kprove-markdown kprove-var-equals -krun-deserialize llvm-kompile-type llvm-krun locations @@ -97,7 +95,6 @@ search-bound set-symbolic-tests set_unification spec-rule-application -star-multiplicity trace unification-lemmas useless diff --git a/pyk/regression-new/star-multiplicity/1.test.out b/pyk/regression-new/star-multiplicity/1.test.out index 72fcf775ce..36c612f81e 100644 --- a/pyk/regression-new/star-multiplicity/1.test.out +++ b/pyk/regression-new/star-multiplicity/1.test.out @@ -5,18 +5,21 @@ - 0 + 5 - 1 + 6 - 5 + 0 - 6 + 1 + + 0 + From d31f9c153788a5b6a5205d91867aa6295419fd01 Mon Sep 17 00:00:00 2001 From: Everett Hildenbrandt Date: Mon, 11 May 2026 23:16:35 +0000 Subject: [PATCH 06/11] outer: extract cell_map_item_info from add/remove_cell_map_items Both methods iterated cell_collection_productions and independently extracted the same (cell_label, element_ctor, cell_map_sort) triples. The new cached property cell_map_item_info centralises that extraction so each method reduces to a one-liner dict construction. Co-Authored-By: Claude Sonnet 4.6 --- pyk/src/pyk/kast/outer.py | 34 ++++++++++++++++++---------------- 1 file changed, 18 insertions(+), 16 deletions(-) diff --git a/pyk/src/pyk/kast/outer.py b/pyk/src/pyk/kast/outer.py index f58e5402ac..d9d9bc2e56 100644 --- a/pyk/src/pyk/kast/outer.py +++ b/pyk/src/pyk/kast/outer.py @@ -1135,6 +1135,22 @@ def cell_collection_productions(self) -> tuple[KProduction, ...]: """Returns the `KProduction` which are cell collection declarations transitively imported by the main module of this definition.""" return tuple(prod for module in self.modules for prod in module.cell_collection_productions) + @cached_property + def cell_map_item_info(self) -> dict[str, tuple[str, KSort]]: + """Map from cell label to (element-constructor label, cell-map sort). + + Derived from cell-collection productions that carry both ELEMENT and WRAP_ELEMENT + attributes and whose element constructor is a known symbol. + """ + result: dict[str, tuple[str, KSort]] = {} + for ccp in self.cell_collection_productions: + if Atts.ELEMENT in ccp.att and Atts.WRAP_ELEMENT in ccp.att: + cell_label = ccp.att[Atts.WRAP_ELEMENT] + element_ctor = ccp.att[Atts.ELEMENT] + if element_ctor in self.symbols: + result[cell_label] = (element_ctor, self.symbols[element_ctor].sort) + return result + @cached_property def rules(self) -> tuple[KRule, ...]: """Returns the `KRule` sentences transitively imported by the main module of this definition.""" @@ -1515,18 +1531,11 @@ def add_cell_map_items(self, kast: KInner) -> KInner: # syntax AccountCellMap [cellCollection, hook(MAP.Map)] # syntax AccountCellMap ::= AccountCellMap AccountCellMap [assoc, avoid, cellCollection, comm, element(AccountCellMapItem), function, hook(MAP.concat), unit(.AccountCellMap), wrapElement()] - # Maps cell label -> (element_constructor, cell_map_sort). # Wrapping is correct only when the parent production expects the cell MAP sort (e.g. # EntryCellMap), not when it expects the individual cell element sort (e.g. EntryCell). # For example, EntryCellMapKey((...)) takes EntryCell — the must NOT be # wrapped, whereas _EntryCellMap_((...), ...) expects EntryCellMap — wrapping is needed. - cell_wrappers: dict[str, tuple[str, KSort]] = {} - for ccp in self.cell_collection_productions: - if Atts.ELEMENT in ccp.att and Atts.WRAP_ELEMENT in ccp.att: - cell_label = ccp.att[Atts.WRAP_ELEMENT] - element_ctor = ccp.att[Atts.ELEMENT] - if element_ctor in self.symbols: - cell_wrappers[cell_label] = (element_ctor, self.symbols[element_ctor].sort) + cell_wrappers = self.cell_map_item_info def _wrap_elements(_k: KInner) -> KInner: if not isinstance(_k, KApply) or _k.label.name not in self.symbols: @@ -1551,14 +1560,7 @@ def _wrap_elements(_k: KInner) -> KInner: def remove_cell_map_items(self, kast: KInner) -> KInner: """Remove cell-map syntactical wrapper items that the frontend generates (see `KDefinition.add_cell_map_items`).""" - # example: - # syntax AccountCellMap [cellCollection, hook(MAP.Map)] - # syntax AccountCellMap ::= AccountCellMap AccountCellMap [assoc, avoid, cellCollection, comm, element(AccountCellMapItem), function, hook(MAP.concat), unit(.AccountCellMap), wrapElement()] - - cell_wrappers = {} - for ccp in self.cell_collection_productions: - if Atts.ELEMENT in ccp.att and Atts.WRAP_ELEMENT in ccp.att: - cell_wrappers[ccp.att[Atts.ELEMENT]] = ccp.att[Atts.WRAP_ELEMENT] + cell_wrappers = {ctor: label for label, (ctor, _) in self.cell_map_item_info.items()} def _wrap_elements(_k: KInner) -> KInner: if ( From 8ae515a04ed39570f7387402074d6d3dbe3e94e6 Mon Sep 17 00:00:00 2001 From: Everett Hildenbrandt Date: Mon, 11 May 2026 23:33:14 +0000 Subject: [PATCH 07/11] outer: simplify _wrap_elements in add_cell_map_items Finish inlining cell_map_item_info, add an early-exit check for the common case where no arg label appears in cell_map_item_info, and drop the changed flag in favour of an unconditional _k.let return. Co-Authored-By: Claude Sonnet 4.6 --- pyk/src/pyk/kast/outer.py | 26 ++++++++++++-------------- 1 file changed, 12 insertions(+), 14 deletions(-) diff --git a/pyk/src/pyk/kast/outer.py b/pyk/src/pyk/kast/outer.py index d9d9bc2e56..f34fc74ebf 100644 --- a/pyk/src/pyk/kast/outer.py +++ b/pyk/src/pyk/kast/outer.py @@ -1535,24 +1535,22 @@ def add_cell_map_items(self, kast: KInner) -> KInner: # EntryCellMap), not when it expects the individual cell element sort (e.g. EntryCell). # For example, EntryCellMapKey((...)) takes EntryCell — the must NOT be # wrapped, whereas _EntryCellMap_((...), ...) expects EntryCellMap — wrapping is needed. - cell_wrappers = self.cell_map_item_info - def _wrap_elements(_k: KInner) -> KInner: if not isinstance(_k, KApply) or _k.label.name not in self.symbols: return _k - prod = self.symbols[_k.label.name] - arg_sorts = prod.argument_sorts - if not arg_sorts or len(arg_sorts) != _k.arity: + arg_sorts = self.symbols[_k.label.name].argument_sorts + if not any(isinstance(arg, KApply) and arg.label.name in self.cell_map_item_info for arg in _k.args): return _k - new_args: list[KInner] = list(_k.args) - changed = False - for i, (arg_sort, arg) in enumerate(zip(arg_sorts, _k.args, strict=True)): - if isinstance(arg, KApply) and arg.label.name in cell_wrappers: - element_ctor, cell_map_sort = cell_wrappers[arg.label.name] - if arg_sort == cell_map_sort: - new_args[i] = KApply(element_ctor, [arg.args[0], arg]) - changed = True - return _k.let(args=new_args) if changed else _k + new_args: list[KInner] = [] + for arg_sort, arg in zip(arg_sorts, _k.args, strict=True): + new_arg = arg + if isinstance(arg, KApply): + if arg.label.name in self.cell_map_item_info: + element_ctor, element_ctor_sort = self.cell_map_item_info[arg.label.name] + if arg_sort == element_ctor_sort: + new_arg = KApply(element_ctor, [arg.args[0], arg]) + new_args.append(new_arg) + return _k.let(args=new_args) # To ensure we don't get duplicate wrappers. _kast = self.remove_cell_map_items(kast) From ed130c67503e66eb9ac6908049a2e863f2ecb283 Mon Sep 17 00:00:00 2001 From: Everett Hildenbrandt Date: Mon, 11 May 2026 23:36:40 +0000 Subject: [PATCH 08/11] pyk/kast/outer: move comment --- pyk/src/pyk/kast/outer.py | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/pyk/src/pyk/kast/outer.py b/pyk/src/pyk/kast/outer.py index f34fc74ebf..107bbfbe92 100644 --- a/pyk/src/pyk/kast/outer.py +++ b/pyk/src/pyk/kast/outer.py @@ -1142,6 +1142,9 @@ def cell_map_item_info(self) -> dict[str, tuple[str, KSort]]: Derived from cell-collection productions that carry both ELEMENT and WRAP_ELEMENT attributes and whose element constructor is a known symbol. """ + # example: + # syntax AccountCellMap [cellCollection, hook(MAP.Map)] + # syntax AccountCellMap ::= AccountCellMap AccountCellMap [assoc, avoid, cellCollection, comm, element(AccountCellMapItem), function, hook(MAP.concat), unit(.AccountCellMap), wrapElement()] result: dict[str, tuple[str, KSort]] = {} for ccp in self.cell_collection_productions: if Atts.ELEMENT in ccp.att and Atts.WRAP_ELEMENT in ccp.att: @@ -1527,9 +1530,6 @@ def _add_sort_params(_k: KInner) -> KInner: def add_cell_map_items(self, kast: KInner) -> KInner: """Wrap cell-map items in the syntactical wrapper that the frontend generates for them (see `KDefinition.remove_cell_map_items`).""" - # example: - # syntax AccountCellMap [cellCollection, hook(MAP.Map)] - # syntax AccountCellMap ::= AccountCellMap AccountCellMap [assoc, avoid, cellCollection, comm, element(AccountCellMapItem), function, hook(MAP.concat), unit(.AccountCellMap), wrapElement()] # Wrapping is correct only when the parent production expects the cell MAP sort (e.g. # EntryCellMap), not when it expects the individual cell element sort (e.g. EntryCell). From b869e6c8357603bc039ebd369e0fe62f93a9916a Mon Sep 17 00:00:00 2001 From: Everett Hildenbrandt Date: Mon, 11 May 2026 23:44:25 +0000 Subject: [PATCH 09/11] pyk/kast/outer: rename _wrap_elements => _unwrap_elements in remove_cel_map_items --- pyk/src/pyk/kast/outer.py | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/pyk/src/pyk/kast/outer.py b/pyk/src/pyk/kast/outer.py index 107bbfbe92..26fdc45d70 100644 --- a/pyk/src/pyk/kast/outer.py +++ b/pyk/src/pyk/kast/outer.py @@ -1560,7 +1560,7 @@ def remove_cell_map_items(self, kast: KInner) -> KInner: """Remove cell-map syntactical wrapper items that the frontend generates (see `KDefinition.add_cell_map_items`).""" cell_wrappers = {ctor: label for label, (ctor, _) in self.cell_map_item_info.items()} - def _wrap_elements(_k: KInner) -> KInner: + def _unwrap_elements(_k: KInner) -> KInner: if ( type(_k) is KApply and _k.label.name in cell_wrappers @@ -1571,7 +1571,7 @@ def _wrap_elements(_k: KInner) -> KInner: return _k.args[1] return _k - return bottom_up(_wrap_elements, kast) + return bottom_up(_unwrap_elements, kast) def empty_config(self, sort: KSort) -> KInner: """Given a cell-sort, compute an "empty" configuration for it (all the constructor structure of the configuration in place, but variables in cell positions).""" From f5f9abf9b0fc84adaca42800eadc0a923a5beb08 Mon Sep 17 00:00:00 2001 From: Everett Hildenbrandt Date: Tue, 12 May 2026 03:23:28 +0000 Subject: [PATCH 10/11] pyproject.toml: suppress pydocstyle D202 to resolve black conflict black inserts a blank line between a docstring and the first comment; D202 forbids it. Adding D202 to add-ignore lets both make format and make check pass. Co-Authored-By: Claude Sonnet 4.6 --- pyk/pyproject.toml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/pyk/pyproject.toml b/pyk/pyproject.toml index d8b1555df1..38af317691 100644 --- a/pyk/pyproject.toml +++ b/pyk/pyproject.toml @@ -79,7 +79,7 @@ include = ["src/pyk"] [tool.pydocstyle] convention = "google" add-select = "D204,D401,D404" -add-ignore = "D1" +add-ignore = "D1,D202" [tool.isort] profile = "black" From 84a24cfed53140e7fdc1f4eaee19c9fec36702f4 Mon Sep 17 00:00:00 2001 From: Everett Hildenbrandt Date: Tue, 12 May 2026 13:02:37 +0000 Subject: [PATCH 11/11] pyk/pyproject, pyk/kast/outer: adjust comments to be docstrings --- pyk/pyproject.toml | 2 +- pyk/src/pyk/kast/outer.py | 26 ++++++++++++++++---------- 2 files changed, 17 insertions(+), 11 deletions(-) diff --git a/pyk/pyproject.toml b/pyk/pyproject.toml index 38af317691..d8b1555df1 100644 --- a/pyk/pyproject.toml +++ b/pyk/pyproject.toml @@ -79,7 +79,7 @@ include = ["src/pyk"] [tool.pydocstyle] convention = "google" add-select = "D204,D401,D404" -add-ignore = "D1,D202" +add-ignore = "D1" [tool.isort] profile = "black" diff --git a/pyk/src/pyk/kast/outer.py b/pyk/src/pyk/kast/outer.py index 26fdc45d70..a0c8539a16 100644 --- a/pyk/src/pyk/kast/outer.py +++ b/pyk/src/pyk/kast/outer.py @@ -1139,12 +1139,12 @@ def cell_collection_productions(self) -> tuple[KProduction, ...]: def cell_map_item_info(self) -> dict[str, tuple[str, KSort]]: """Map from cell label to (element-constructor label, cell-map sort). - Derived from cell-collection productions that carry both ELEMENT and WRAP_ELEMENT - attributes and whose element constructor is a known symbol. + Derived from cell-collection productions that carry both ``ELEMENT`` and ``WRAP_ELEMENT`` attributes and whose element constructor is a known symbol. + + Example: + syntax AccountCellMap [cellCollection, hook(MAP.Map)] + syntax AccountCellMap ::= AccountCellMap AccountCellMap [assoc, avoid, cellCollection, comm, element(AccountCellMapItem), function, hook(MAP.concat), unit(.AccountCellMap), wrapElement()] """ - # example: - # syntax AccountCellMap [cellCollection, hook(MAP.Map)] - # syntax AccountCellMap ::= AccountCellMap AccountCellMap [assoc, avoid, cellCollection, comm, element(AccountCellMapItem), function, hook(MAP.concat), unit(.AccountCellMap), wrapElement()] result: dict[str, tuple[str, KSort]] = {} for ccp in self.cell_collection_productions: if Atts.ELEMENT in ccp.att and Atts.WRAP_ELEMENT in ccp.att: @@ -1529,12 +1529,18 @@ def _add_sort_params(_k: KInner) -> KInner: return bottom_up(_add_sort_params, kast) def add_cell_map_items(self, kast: KInner) -> KInner: - """Wrap cell-map items in the syntactical wrapper that the frontend generates for them (see `KDefinition.remove_cell_map_items`).""" + """Wrap cell-map items in the syntactical wrapper that the frontend generates for them. + + See :func:`KDefinition.remove_cell_map_items`. + + Note: + Wrapping is correct only when the parent production expects the cell MAP sort (e.g. ``EntryCellMap``), not when it expects the individual cell element sort (e.g. ``EntryCell``). + + Example: + ``EntryCellMapKey((...))``: takes ``EntryCell``, ```` must NOT be wrapped + ``_EntryCellMap_((...), ...)``: expects ``EntryCellMap``, wrapping is needed + """ - # Wrapping is correct only when the parent production expects the cell MAP sort (e.g. - # EntryCellMap), not when it expects the individual cell element sort (e.g. EntryCell). - # For example, EntryCellMapKey((...)) takes EntryCell — the must NOT be - # wrapped, whereas _EntryCellMap_((...), ...) expects EntryCellMap — wrapping is needed. def _wrap_elements(_k: KInner) -> KInner: if not isinstance(_k, KApply) or _k.label.name not in self.symbols: return _k