Frontend generates invalid Kore

[h0nzZik]

When I kompile the following definition

module IMP-SYNTAX
  imports DOMAINS-SYNTAX

  syntax Pgm ::= Int
endmodule


module IMP
  imports IMP-SYNTAX
  imports DOMAINS
  syntax KResult ::= Int | Bool

  configuration <T color="yellow">
                  <k color="green"> $PGM:Pgm </k>
                  <cpp-enums>
                    <cppenum multiplicity="*" type="Map">
                      <enum-id> .K </enum-id>
                      <enum-type> .K </enum-type>
                      <scoped> false </scoped>
                    </cppenum>
                  </cpp-enums>
                </T>

  syntax Enum

  syntax CppenumCell
  syntax IncompleteInfo ::= "#incomplete"
  syntax EnumInfo ::= CppenumCell | IncompleteInfo
     syntax EnumInfo ::= #getEnumInfo(Enum) [function]

     rule [[ #getEnumInfo(X::Enum) => <cppenum> <enum-id> X </enum-id> B </cppenum> ]]
          <cppenum> <enum-id> X </enum-id> B::Bag </cppenum>

     rule #getEnumInfo(_) => #incomplete [owise]

endmodule

and run kore-parser imp-kompiled/definition.kore --no-print-definition, it outputs:

kore-parser: Error in module 'IMP' -> axiom declaration -> \implies (imp-kompiled/definition.kore 3185:21) -> \and (imp-kompiled/definition.kore 3186:10) -> \not (imp-kompiled/definition.kore 3187:12) -> \or (imp-kompiled/definition.kore 3188:13) -> \exists 'Var'Unds'3' (imp-kompiled/definition.kore 3189:19) -> \exists 'Var'Unds'8' (imp-kompiled/definition.kore 3190:29) -> \exists 'Var'Unds'6' (imp-kompiled/definition.kore 3191:29) -> \exists 'Var'Unds'7' (imp-kompiled/definition.kore 3192:29) -> \exists 'Var'Unds'5' (imp-kompiled/definition.kore 3193:29) -> \exists 'Var'Unds'9' (imp-kompiled/definition.kore 3194:29) -> \exists 'Var'Unds'4' (imp-kompiled/definition.kore 3195:29) -> \and (imp-kompiled/definition.kore 3196:18) -> \and (imp-kompiled/definition.kore 3198:20) -> \and (imp-kompiled/definition.kore 3203:25) -> \ceil (imp-kompiled/definition.kore 3204:47) -> \and (imp-kompiled/definition.kore 3205:24) -> \and (imp-kompiled/definition.kore 3207:26) -> symbol or alias 'Lbl'-LT-'generatedTop'-GT-'' (imp-kompiled/definition.kore 3207:50) -> symbol or alias 'Lbl'-LT-'T'-GT-'' (imp-kompiled/definition.kore 3207:80) -> symbol or alias 'Lbl'-LT-'cpp-enums'-GT-'' (imp-kompiled/definition.kore 3207:122) -> symbol or alias 'Lbl'Unds'CppenumCellMap'Unds'' (imp-kompiled/definition.kore 3207:149) -> symbol or alias 'LblCppenumCellMapItem' (imp-kompiled/definition.kore 3207:181) -> symbol or alias 'Lbl'-LT-'enum-id'-GT-'' (imp-kompiled/definition.kore 3207:205) -> (imp-kompiled/definition.kore 221:35, imp-kompiled/definition.kore 3207:241): Expecting sort 'SortK{}' but got 'SortEnum{}'.
CallStack (from HasCallStack):
  error, called at app/parser/Main.hs:207:33 in main:Main

. This error originally manifested in C++ translation semantics.

[ttuegel]

The cell symbol is defined like this:

symbol Lbl'-LT-'enum-id'-GT-'{}(SortK{}) : SortEnumIdCell{} [...]

and the symbol is used like this:

\and{SortGeneratedTopCell{}}(Lbl'-LT-'generatedTop'-GT-'{}(Lbl'-LT-'T'-GT-'{}(Var'Unds'4:SortKCell{},Lbl'-LT-'cpp-enums'-GT-'{}(Lbl'Unds'CppenumCellMap'Unds'{}(LblCppenumCellMapItem{}(
    
    Lbl'-LT-'enum-id'-GT-'{}(Var'Unds'3:SortEnum{}),

Lbl'-LT-'cppenum'-GT-'{}(
  
    Lbl'-LT-'enum-id'-GT-'{}(kseq{}(inj{SortEnum{}, SortKItem{}}(Var'Unds'3:SortEnum{}),dotk{}())),

Var'Unds'5:SortEnumTypeCell{},Var'Unds'6:SortScopedCell{})),Var'Unds'7:SortCppenumCellMap{}))),Var'Unds'8:SortGeneratedCounterCell{}),Var'Unds'9:SortGeneratedTopCell{})

I changed the formatting to emphasize the two occurrences. The second occurrence is correct: the argument of <enum-id> has sort K. The first one is not correct; the variable Var'Unds'3:SortEnum{} needs to be injected into SortKItem and put at the head of a kseq. Or, fix the declaration of the <enum-id> cell so that it expects an Enum argument. This is a problem in the frontend.

[h0nzZik]

Or, fix the declaration of the cell so that it expects an Enum argument.

How do I do that? Do I need to pick up some value of sort Enum and put it to the configuration?