search

runtimeverification / k

K Framework Tools 7.0
BSD 3-Clause "New" or "Revised" License
430 stars 141 forks source link

Iterate over an Assoc's elements with top_down/bottom_up #4466

Closed gtrepta closed 1 week ago

gtrepta commented 1 week ago

The top_down and bottom_up operations on a Kore structure don't iterate over the arguments in a LeftAssoc or RightAssoc. This fixes that.

gtrepta commented 1 week ago

https://github.com/runtimeverification/k/blob/24146661eeff13489d5138000c13d83251003a88/pyk/src/pyk/kore/syntax.py#L1616-L1617

Maybe this could be...?

class Assoc(MLSyntaxSugar):
    symbol: str
    args: tuple[Pattern, ...]

Then the pattern method can just build the App with symbol. And top_down/bottom_up transformers can match on an Assoc and do a let over symbol if they want.

tothtamas28 commented 1 week ago

Maybe this could be...?

class Assoc(MLSyntaxSugar):
    symbol: str
    args: tuple[Pattern, ...]

Good idea, let's go with this solution.