Emit KoreJson \right-assoc for collections #3651
Conversation
| . fromPattern | ||
| . from @_ @(Kore.Pattern _ (TermLike.TermAttributes VariableName)) | ||
| . Kore.Syntax.Json.Internal.fromTermLike |
There was a problem hiding this comment.
We should completely delete Internal.fromPattern and rewrite the unit tests to use the new fromTermLike to retain the test coverage.
There was a problem hiding this comment.
Not sure what the best way to go about this is tbh. fromPattern is basically unused, but we use the inverse toParsedPattern in a lot of places. The problem is we go from KorePattern to ParsedPattern which at some point gets turned into a TermLike which we then turn back into a KorePattern. Perhaps that path should be added and we keep the other unit tests??
| -- If the structure has exactly one child, we just get the child. | ||
| -- This child will be an application of internalElement symbol to its arguments | ||
| -- For multiple children we will get a \right-assoc{concatSymbol}(x1,...x_n) | ||
| foldApplication Kore.Symbol{symbolConstructor = unitSymbolConstructor, symbolParams = unitSymbolParams} Kore.Symbol{symbolConstructor = concatSymbolConstructor, symbolParams = concatSymbolParams} = foldAux |
There was a problem hiding this comment.
For reference: https://github.com/runtimeverification/haskell-backend/blob/master/kore/src/Kore/Internal/TermLike/TermLike.hs#L1385-L1440 differs in foldApplication only.
Unfortunately there is no good way to avoid the duplication.
This reverts commit dd56839.
This PR modifies the encoding of lists, maps and sets to use
\right-assoc{concatSymbol}(...)to remove differences in bracketing. THis should also make it easier to write a diffing application which ignores the order of/sorts the list of children.