Skip to content
This repository was archived by the owner on Apr 25, 2024. It is now read-only.
Merged
Show file tree
Hide file tree
Changes from 3 commits
Commits
File filter

Filter by extension

Filter by extension


Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
2 changes: 1 addition & 1 deletion package/version
Original file line number Diff line number Diff line change
@@ -1 +1 @@
0.1.339
0.1.340
2 changes: 1 addition & 1 deletion pyproject.toml
Original file line number Diff line number Diff line change
Expand Up @@ -4,7 +4,7 @@ build-backend = "poetry.core.masonry.api"

[tool.poetry]
name = "pyk"
version = "0.1.339"
version = "0.1.340"
description = ""
authors = [
"Runtime Verification, Inc. <[email protected]>",
Expand Down
17 changes: 17 additions & 0 deletions src/pyk/kast/outer.py
Original file line number Diff line number Diff line change
Expand Up @@ -1033,6 +1033,23 @@ def production_for_klabel(self, klabel: KLabel) -> KProduction:
_LOGGER.warning(
f'Discarding {len(prods) - len(_prods)} productions with `unparseAvoid` attribute for label: {klabel}'
)
# Automatically defined symbols like isInt may get multiple
# definitions in different modules.
unique_no_att: list[tuple[KProduction, KProduction]] = []
for prod in prods:
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

After fixing _freeze, a Counter-base solution should work (not thoroughly tested):

prod_cnt = Counter(prod.let_att(remove_source_map_from_katt(prod.att)) for prod in prods)
try:
    prod = single(prod_cnt)
except ValueError as err:
    raise ValueError(f'Expected a single production for label {klabel}, not: {list[prod_cnt]}') from err

num_eq_prods = prod_cnt[prod] - 1
if num_eq_prods:
    _LOGGER.warning(f'Discarding {num_eq_prods} equivalent productions')

self._production_for_klabel[klabel] = prod

This version always returns a production without source map. If retaining it is important (in the case whe there is a single production), a dict-based variant can be implemented with.

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Done.

equivalent = False
trimmed_prod = prod.let_att(KAtt({}))
for _, t in unique_no_att:
if t == trimmed_prod:
equivalent = True
break
if equivalent:
continue
unique_no_att.append((prod, trimmed_prod))
_prods = [p for p, _ in unique_no_att]
if len(_prods) < len(prods):
prods = _prods
_LOGGER.warning(f'Discarding {len(prods) - len(_prods)} equivalent productions')
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Wouldn't this always log

Discarding 0 equivalent productions

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Fixed. Sorry, I copy-pasted the code above without making sure that it works. I also fixed the original code.

try:
self._production_for_klabel[klabel] = single(prods)
except ValueError as err:
Expand Down