Disallow sorts with case-insensitive equal names

[Baltoli]

Consider the following definition:

module TEST
  imports BOOL

  syntax Foo ::= "Foo"
  syntax FOO ::= "FOO"

  syntax KItem ::= result(KItem, Bool, Bool)
  rule F:Foo => result(F, isFoo(F), isFOO(F))
  rule F:FOO => result(F, isFoo(F), isFOO(F))
endmodule

We can see by inspection that there is no term X for which isFoo(X) and isFOO(X) are both true. However, on macOS, we can observe the following executions:

$ kompile test.k
$ krun -cPGM='Foo'
<k>
  result ( Foo , false , false ) ~> .K
</k>
$ krun -cPGM='FOO'
<k>
  result ( FOO , true , true ) ~> .K
</k>

That is, isFoo(Foo) => false, and isFOO(Foo) => true! Both of these rewrites are incorrect.

Some digging reveals that the reason for this is the case-insensitive filesystem on macOS; when decision trees are compiled, files LblisFoo.yaml and LblisFOO.yaml are both generated. However, one of them overwrites the other because of case-insensitivity. This means that the logic for all case-insensitive-equal sorts gets collapsed into one.

The solution (I think) is to disallow sorts that are equal up to casing.

[dwightguth]

I'm not sure this is the solution I would recommend. The problem is that even if you restrict sort names, you are still stuck with collisions in the casing of other symbols, and that's a potentially very restrictive thing to disallow completely. It's probably better to find a way to pick the filenames such that they are unique modulo case insensitivity.

[dwightguth]

One thing to note is that the llvm backend emits a table mapping symbol names to filenames, because we already have had problems in the past with filenames longer than the max filename length on Linux. So you probably just need to detect in the Scala code when files might collide and give them new names

[ehildenb]

Could we suffix each file with a hash of the original (case sensitive) sort name? Just the first 6 characters of the hash should be enough I guess.

[Baltoli]

Could we suffix each file with a hash of the original (case sensitive) sort name? Just the first 6 characters of the hash should be enough I guess.

Yeah I didn't think this through in sufficient detail last week when recording the issue - I think something like this is the right solution.