[Bug] [kompile] - Parsing token vs parsing variable name

Start by reproducing the failure with test.k using kompile --backend haskell, then inspect the reported parsing locations in include/kframework/builtin/domains.md. Determine why the token C conflicts with variable names across sorts, and consider the issue done when the definition compiles without the reported parser errors.

K Version

bd04f5fd32

Description

Tokens declared in one sort conflict with variables in another sort.

Input Files

File test.k:

module TEST
    imports INT

    configuration <k> $PGM:Contract </k>

    rule (A +Int B) +Int C:Int => A +Int (B +Int C:Int) [simplification]

    syntax Contract ::= "C"
endmodule

Reproduction Steps

Kompile the definition:

$ kompile --backend haskell test.k --output-definition test-kompiled                                                                                                                                                                                                              
[Error] Inner Parser: Parse error: unexpected token 'C' following token '+Int'.                                                                                                                                                                                                   
        Source(/home/dev/src/k/k-distribution/target/release/k/include/kframework/builtin/domains.md)                                                                                                                                                                             
        Location(1097,25,1097,26)                                                                                                                                                                                                                                                 
        1097 |    rule I1 +Int (I2 +Int C) => (I1 +Int I2) +Int C [concrete(I1, I2),                                                                                                                                                                                              
symbolic(C), simplification]                                                                                                                                                                                                                                                      
             .                          ^                                                                                                                                                                                                                                         
[Error] Inner Parser: Parse error: unexpected token 'C' following token '-Int'.                                                                                                                                                                                                   
        Source(/home/dev/src/k/k-distribution/target/release/k/include/kframework/builtin/domains.md)                                                                                                                                                                             
        Location(1098,25,1098,26)                                                                                                                                                                                                                                                 
        1098 |    rule I1 +Int (I2 -Int C) => (I1 +Int I2) -Int C [concrete(I1, I2),                                                                                                                                                                                              
symbolic(C), simplification]                                                                                                                                                                                                                                                      
             .                          ^                                                                                                                                                                                                                                         
[Error] Inner Parser: Parse error: unexpected token 'C' following token '+Int'.                                                                                                                                                                                                   
        Source(/home/dev/src/k/k-distribution/target/release/k/include/kframework/builtin/domains.md)                                                                                                                                                                             
        Location(1100,25,1100,26)                                                                                                                                                                                                                                                 
        1100 |    rule I1 -Int (I2 +Int C) => (I1 -Int I2) -Int C [concrete(I1, I2),                                                                                                                                                                                              
symbolic(C), simplification]                                                                                                                                                                                                                                                      
             .                          ^                                                                                                                                                                                                                                         
[Error] Inner Parser: Parse error: unexpected token 'C' following token '-Int'.                                                                                                                                                                                                   
        Source(/home/dev/src/k/k-distribution/target/release/k/include/kframework/builtin/domains.md)                                                                                                                                                                             
        Location(1101,25,1101,26)                                                                                                                                                                                                                                                 
        1101 |    rule I1 -Int (I2 -Int C) => (I1 -Int I2) +Int C [concrete(I1, I2),                                                                                                                                                                                              
symbolic(C), simplification]                                                                                                                                                                                                                                                      
             .                          ^                                                                                                                                                                                                                                         
[Error] Inner Parser: Parse error: unexpected token 'C' following token '('.                                                                                                                                                                                                      
        Source(/home/dev/src/k/k-distribution/target/release/k/include/kframework/builtin/domains.md)                                                                                                                                                                             
        Location(1102,9,1102,10)                                                                                                                                                                                                                                                  
        1102 |    rule (C -Int I2) -Int I3 => C -Int (I2 +Int I3) [concrete(I2, I3),                                                                                                                                                                                              
symbolic(C), simplification]                                                                                                                                                                                                                                                      
             .          ^                                                                                                                                                                                                                                                         
[Error] Inner Parser: Parse error: unexpected token 'C' following token '&Int'.                                                                                                                                                                                                   
        Source(/home/dev/src/k/k-distribution/target/release/k/include/kframework/builtin/domains.md)                                                                                                                                                                             
        Location(1104,25,1104,26)                                                                                                                                                                                                                                                 
        1104 |    rule I1 &Int (I2 &Int C) => (I1 &Int I2) &Int C [concrete(I1, I2),                                                                                                                                                                                              
symbolic(C), simplification]                                                                                                                                                                                         
             .                          ^                                                                                                                                                                            
[Error] Inner Parser: Parse error: unexpected token 'C' following token '#if'.                                                                                                                                       
        Source(/home/dev/src/k/k-distribution/target/release/k/include/kframework/builtin/domains.md)                                                                                                                
        Location(2128,12,2128,13)                                                                                                                                                                                    
        2128 |    rule #if C:Bool #then B1::K #else _ #fi => B1 requires C                                                                                                                                           
             .             ^                                                                                                                                                                                         
[Error] Inner Parser: Parse error: unexpected token 'C' following token '#if'.                                                                                                                                       
        Source(/home/dev/src/k/k-distribution/target/release/k/include/kframework/builtin/domains.md)                                                                                                                
        Location(2129,12,2129,13)                                                                         
        2129 |    rule #if C:Bool #then _ #else B2::K #fi => B2 requires notBool C                                                                                                                                   
             .             ^                                                                                                                                                                                         
[Error] Inner Parser: Parse error: unexpected token 'C' following token '+Int'.                            
        Source(/home/dev/src/k/test.k)                                                                                                                                                                               
        Location(6,26,6,27)                                                                               
        6 |         rule (A +Int B) +Int C => A +Int (B +Int C) [simplification]
          .                              ^                                                                                                                                                                           
[Error] Compiler: Had 9 parsing errors.                                       

Expected Behavior

I would like this case to be handled. The variable C in these rules cannot be of sort Contract, so we should be able to figure this out. Annotating the variable with it's sort (as C:Int), does not help.