K-user mailing list

[Chris Hathhorn <chathhorn AT gmail.com>]

On Sun, Aug 18, 2013 at 4:24 PM, Ömer Sinan Ağacan 
<omeragacan AT gmail.com>
 wrote:
>
> I want to have a rule like this: (I want this only for learning
> purposes, this rule may not be very meaningful and/or useful)
>
>     rule <k> I:Int => . ... </k>
>          <someMap> ... _ |-> (N => N +Int I) ... </someMap>

This rule matches a single element in someMap, one that could have any
value as a key. So if someMap contains multiple elements, it'll match
against any particular one of them, but it won't match against them
all simultaneously (as I think you're intending).

>
> What I'm trying to say here is that when encountered with an int, I
> want to increment each element in my map configuration by that int,
> ie. if I have 10 in my program and my someMap state is like:
>
>     <someMap>
>       identifier1 |-> 10
>       identifier2 |-> 20
>     </someMap>
>
> I want to update this to:
>
>     <someMap>
>       identifier1 |-> 20
>       identifier2 |-> 30
>     </someMap>
>
> But currently this rule only updates first element in map(namely,
> indetifier1 in this example). Why is that? And how can I do what I
> want to do here?
>

I don't think there's a way to write a rule like you have in mind.
Instead, you'll probably want to enumerate all the keys in the map and
increment each value individually.

E.g.:

syntax K ::= incSomeMap(Set, Int)

rule <k> I:Int => incSomeMap(keys M, I) ...</k>
  <someMap> M:Map </someMap>

rule <k> incSomeMap((SetItem(K:K) => .Set) _:Set, I:Int) ...</k>
  <someMap> ... K |-> (X:Int => X +Int I) ...</someMap>

rule incSomeMap(.Set, _) => .

Chris