search

runtimeverification / pyk

Python tools for the K Framework
BSD 3-Clause "New" or "Revised" License
13 stars 2 forks source link

Fix `as_subsort` #1046

Closed tothtamas28 closed 5 months ago

tothtamas28 commented 5 months ago

If symbol is present on a production, then it is not a subsort production, even if it has a single, non-terminal production item.

ehildenb commented 5 months ago

Can we test this? I guess it must have shown up in some definition somewhere as a bug.

tothtamas28 commented 5 months ago

Can we test this? I guess it must have shown up in some definition somewhere as a bug.

Good point. I added a simple test that checks the symbol and subsort table in the KORE definition (https://github.com/runtimeverification/k/pull/4143#issuecomment-2025660829) and that the corresponding data structures on the KAST definition work accordingly.