Baltoli
commented
6 months ago The problem here is this rule:
<locals> L => L[N <- V] ...</locals>What you actually want to write is:
<locals> L => L[N <- V] </locals>because the rule is updating the entire map L (rather than a single element using the structural framing dots).
An alternative formulation for the rule would be (under the assumption that the key N already exists in the map, which might not hold in general):
<locals> N |-> (_ => V) ...</locals>Note here that the pattern in the cell isn't binding the entire map to a variable L, just the single element N |-> _.
If you're interested, the reason this happens is that the dots on the RHS are equivalent here to an anonymous variable of sort Map. As originally written, your rule is equivalent to:
<locals> (L => L[N <- V]) _Rest:Map </locals>The pattern matching compiler here greedily binds the contents of the cell to the variable L, meaning that there's nothing left to bind to _Rest.
We should absolutely provide a better error here, though, you're correct. Thanks for pointing this out!
What component is the issue in?
None
Which command
What K Version?
v7.0.61
Operating System
Linux
K Definitions (If Possible)
Steps to Reproduce
Expected Results
I would expect kompile to either successfully compile or give a more-or-less human readable error message (not sure which since I don't yet understand much about what I'm doing). I'm trying to implement something like Python VM, which is a stack machine.