[Bug] pyk and kast disagree on kore terms

[ehildenb]

K Version

$ kompile --version
K version:    5.3.0
Build date:   Sat Jul 30 00:45:20 UTC 2022

Actually version e72bb80 with some modifications to pyk.

Description

pyk is writing a Kore term to text that the Frontend does not want to parse.

Input Files

File test.k:

requires "domains.md"

module TEST
    imports INT
    imports MAP
    imports BOOL

    configuration <k> $PGM:KItem </k>
                  <state> .Map </state>

    syntax Bool ::= pred1 ( Int ) [function, functional, klabel(pred1), symbol, no-evaluators]
    syntax KItem ::= "foo" | "bar"

    rule <k> foo => bar ... </k>
         <state> ... 3 |-> N ... </state>
      requires pred1(N)

endmodule

File test1.kore:

inj { SortBool { }, SortKItem { } } ( Lblpred1 { } ( \dv { SortInt { } } ( "3" ) ) ) 

File test2.kore:

inj { SortBool , SortKItem } ( Lblpred1 { } ( \dv { SortInt } ( "3" ) ) )

Reproduction Steps

Kompile the definition:

+ kompile --backend haskell test.k --output-definition test-kompiled

Kast the first file:

+ kast --input kore test1.kore --definition test-kompiled
[Error] Critical: Parse error
 (ParseError: ERROR: Line 1: Column 16: Expected '}' or ',', but '{'
inj { SortBool { }, SortKItem { } } ( Lblpred1 { } ( \dv { SortInt { } } ( "3"
) ) )
               ^)

Kast the second file:

+ kast --input kore test2.kore --definition test-kompiled
pred1(#token("3","K"))

Expected Behavior

The file test1.kore was generated by pyk on the KAST term pred1(#token('3', 'Int')). When removing the {} on SortBool, SortKItem, and SortInt{}, the frontend the allows it (that's test2.kore).

So either pyk should not be generating the kore term with the extra curlys, or the frontend should be able to parse the first file.

Additionally, the frontend is giving back pred1(#token('3', 'K')), when it should be giving back pred1(#token('3', 'Int')). So somehow it's losing sort information here.