runtimeverification / k

K Framework Tools 7.0
BSD 3-Clause "New" or "Revised" License
444 stars 145 forks source link

[KIP] - Better error mesage for "*" multiplicity map cell #2239

Open andreiburdusa opened 2 years ago

andreiburdusa commented 2 years ago

Motivation

Example K Code

module TEST
    configuration
        <cell multiplicity="*" type="Map"> .K </cell>

    rule <cell> _ </cell> => .Bag
endmodule

This definition doesn't compile because the <cell>s are translated internally to a map, and therefore need to be wrapped in a larger cell, like

    configuration
        <cells>
            <cell multiplicity="*" type="Map"> .K </cell>
        </cells>

But the error message draws attention to the rule instead:

[Error] Internal: Could not find binding for variable while compiling pattern
matching. (NoSuchElementException: key not found: Var'Unds'0)
    Source(/home/andrei/Documents/k-tutorial/lesson-17/issue/test.k)
    Location(5,10,5,34)

Documentation

The error should help the users realize they could fix the definition by adding a wrapper cell around <cell>s.

radumereuta commented 2 years ago

This should give you an error in the configuration. @andreiburdusa if you have more examples, please share them here. We would like to overhaul the error reporting around multiplicity cells.

andreiburdusa commented 2 years ago

This should give you an error in the configuration. @andreiburdusa if you have more examples, please share them here. We would like to overhaul the error reporting around multiplicity cells.

I got a similar error when I removed the <threads> cell around <thread> in this example from the K Tutorial