runtimeverification / k

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

Flat representation for associative KAST terms #4399

Open tothtamas28 opened 5 months ago

tothtamas28 commented 5 months ago

The most important functions in pyk that operate on KAST terms (e.g. KAST-to-KORE, KAST-to-JSON, etc.) are implemented iteratively to avoid stack overflow on deeply nested objects. However, we're still getting stack overflows from the standard library.

KORE has {left,right}-assoc to avoid deeply nested object graphs. We need a similar solution for KAST.

Baltoli commented 5 months ago

The frontend should emit the KAST JSON format using a new inner syntax subclass of KApply (KApplyAssoc? - or perhaps not). Then consumers (Pyk) can be updated.

tothtamas28 commented 5 months ago

In the Python code, I'd probably extract a common superclass:

class KApplyLike(ABC):
    label: KLabel
    args: tuple[KInner, ...]

(And make sure it can be pattern matched.)

Baltoli commented 5 months ago

Yep, I think that makes sense compared to what we were discussing in the meeting earlier.

tothtamas28 commented 5 months ago

Once this is addressed maybe we can eliminate the KSequence abstraction and treat #KSequence as any other symbol.