`List{SORT, "separator"}` syntactic sugar creates two symbols with identical `smtlib` attribute

[jberthold]

When the special user list syntax List{SORT, "separator"} is used together with the smtlib attribute, the resulting definition.kore file contains two symbols (with different arity) with the same smtlib attribute. This can cause an issue with the SMT solver bindings in the Haskell backend(s) because an SMT function name will be declared twice, with different arity, and one of the kore symbols will be mistranslated, causing a solver error.

Example:

test.k

module TEST
  syntax Thing ::= This() | That()
  syntax Things ::= List{Thing, ""} [symbol("Things"), terminator-symbol(".Things"), smtlib("smt_things")]
endmodule

$ kompile --backend haskell --syntax-module TEST test.k`
$ grep smt_things test-kompiled/definition.kore 
  symbol Lbl'Stop'Things{}() : SortThings{} [constructor{}(), functional{}(), injective{}(), 
    ..., smtlib{}("smt_things"), symbol'Kywd'{}(".Things")]
  symbol LblThings{}(SortThing{}, SortThings{}) : SortThings{} [constructor{}(), functional{}(), injective{}(), 
    ..., smtlib{}("smt_things"), symbol'Kywd'{}("Things")]

Ideally, the symbol attributes would be disambiguated during desugaring (maybe by simply appending _nil to the zero-arity one).

[gtrepta]

A solution here would be to allow the smtlib attribute with no value. Then, when generating kore, we can add a value to the attribute based on the symbol name.

For backwards compatibility, we should emit a warning if there is an smtlib attribute with a value on sugared syntax.

[ehildenb]

I like the adding _nil to the end of the empty list constructor smtlib attribute, any reason to not do that? It allows the user some control over the name, while still keeping them distinct. I guess we would need to handle all the cases that this could happen for....