Discrepency in JSON encoding of Left/Right assoc between pyk and Haskell backend

[goodlyrottenapple]

Pyk expects the children of a Left/RightAssoc to be a symbol application under App:

https://github.com/runtimeverification/pyk/blob/959a505f9f7c477d30b345ec741205ceba803ec0/src/pyk/kore/syntax.py#L1708-L1711

i.e. {"tag": "RightAssoc" "app": {"tag": "App", "name": <symbol>, "sorts": ..., "args":[<a1>, ... <an>]}}

however, the JSON schema in the haskell backend defines Left/RightAssoc as:

{"tag": "RightAssoc", "symbol": <symbol>, "sorts":..., "argss":[<a1>, ... <an>]}

Do we go with pyk as source of truth here? The nesting of an App inside a Left/RightAssoc seems unnecessary and would make the to/fromJSON instances in Haskell awkward to write (they are auto-generated atm, which would no longer be the case)

[tothtamas28]

The pyk implementation of these classes mirrors the textual syntax, e.g.:

"\mu" "{" "}" "(" <set-variable> "," <pattern> ")"

is represented as

@final
@dataclass(frozen=True)
class Mu(MLFixpoint):
    var: SVar
    pattern: Pattern

But indeed, the JSON format seems to inline non-Pattern children:

{
    'tag': 'Mu',
    'var': self.var.name,
    'varSort': self.var.sort.dict,
    'arg': self.pattern.dict,
}

So based on this, I think the adjustment has to be made in pyk.

[tothtamas28]

Btw @goodlyrottenapple, what's the advantage of inlining these structures? Is it so that a Pattern can be conveniently traversed with some f :: Pattern -> a?

[goodlyrottenapple]

In python you can easily write

https://github.com/runtimeverification/pyk/blob/959a505f9f7c477d30b345ec741205ceba803ec0/src/pyk/kore/syntax.py#L1665-L1666

which forces the child of Left/RightAssocto be an App. However there is no nice way to do this in Haskell without losing auto derived JSON instances. You could either allow any kore JSON term as child, bu then you would be allowing nonsensical constructs, such as \rightAssoc{\dv ...} or do what we currently do and flatten/inline the children of App into the assoc constructor. However, this either means that the JSON is also flattened or we have to write the JSON serializer/deserializer by hand, which, again is not optimal.