kframework / k-legacy

The K tools (deprecated, see README)
http://kframework.org
Other
146 stars 61 forks source link

"end of list" token ambiguity #2386

Open incud opened 6 years ago

incud commented 6 years ago

Consider the language which parses a list of integer followed by a list of strings. Here the code (lists.k)

module LISTS-SYNTAX
    syntax ListA ::= List{Int, ","} [strict]
    syntax ListB ::= List{String, ","} [strict]
    syntax Program ::= ListA ListB
endmodule

module LISTS
    imports LISTS-SYNTAX
    configuration 
    <T>
        <k> $PGM:Program </k>
    </T>
    rule A:ListA B:ListB => A ~> B [structural]
    rule <k> ( N:Int, A:ListA => A ) ... </k>
    rule <k> ( .ListA => .K ) ... </k>
    rule <k> ( S:String, B:ListB => B ) ... </k>
    rule <k> ( .ListB => .K ) </k>
endmodule

and the following example file (example.lists)

1, 2, 3, 4
"b", "c", "d"

The code compiles correctly with kompile lists.k. When executing it with krun example.lists --debugger you can see this state

$ kompile lists.k
$ krun example.lists --debugger
KDebug> p
initTCell ( .Map $STDIN |-> "
" $IO |-> "off" $PGM |-> ( ( 1 , ( 2 , ( 3 , ( 4 , .ListA ) ) ) ) ( "b" , ( "c" , ( "d" , .ListA ) ) ) ) )
KDebug> 

While the .ListA after number 4 is correct, the .ListA after "d" is not. It should be .ListB. Obviously they will also match different rules. Here the code: lists.tar.gz

radumereuta commented 6 years ago

Try adding klabels to your lists. The automatic klabel generation doesn't look for collisions and in this case krun gets confused.

syntax ListA ::= List{Int, ","} [strict, klabel(IntList)]
syntax ListB ::= List{String, ","} [strict, klabel(StringList)]