K-user mailing list

[Daniel Schnetzer Fava <danielsf AT ifi.uio.no>]

Hi,

I would like to encode a rule that replaces, for example, all Map values of 0 
by 1 (regardless of their key).  I suppose there are many ways of doing this. 
 Perhaps one of them is something like:

  <a> ... _ |-> (0 => 1) ... </a>

that assume that <a> contains some map, for example: <a> AMap: Map </a>


I've encoded such a rule, and what I've observed is that K matches on one 
value of the map (apparently the first that was added), but does not match 
the rest.  I feel like the rule should have applied to all 0 values.

Here is a full example:

$ cat issue.k
module ISSUE-SYNTAX
  syntax K ::= "init" | continue(Int)
endmodule

module ISSUE
  import ISSUE-SYNTAX
  configuration <k> $PGM:K </k> <a> .Map </a>

  rule <k> init => continue(0) </k>
       <a> AMap:Map => ((AMap[ 0 <- 0 ])[ 1 <- 0])[ 2 <- 0 ] </a> // A Map of 
0 to 0, 1 to 0, and 2 to 0

  rule <k> continue(C:Int => C +Int 1) </k>
       <a> ... _ |-> (0 => 1) ... </a>  // Replace all values of 0 by 1
endmodule

The program simply contains the string "init"

$ cat test.issue
init

This is the output produced showing that the rule matches one of the values 
in the Map, but not the others:

$ krun --debug test.issue | pprint
<generatedTop>
        <k> continue ( 1 ) </k>
        <a> 0 |-> 1 1 |-> 0 2 |-> 0 </a>
</generatedTop>

The output I was expecting is something more like:
<generatedTop>
        <k> continue ( 3 ) </k>
        <a> 0 |-> 1 1 |-> 1 2 |-> 1 </a>
</generatedTop>

Note that I am using git commit 35df078e85e83f23d1b45e7eee5481a8cb9e8939, 
which I believe is the top of tree.

Could this be an issue?

Thank you,

Daniel Fava