K-user mailing list

[Daniele Filaretti <dfilaretti AT gmail.com>]

Hi All, 
little technical question, in an IMP++ setting (actually only IMP, but with 
environment + store).

The following is a variable assignment rule that, in case the variable 
doesn’t exists, it creates it. In order to do this, it does the standard 
things - adding an entry in the environment and in the store, using a fresh 
allocated address.

However, I’m not using K’s builtin “fresh” predicate but I’d like to use my 
own allocation function “alloc” which takes the whole configuration as an 
input:

  rule [assign-create]:
             <k> X = I:Int; => . ... </k>
             <env> M:Map => M[alloc(State)/X] </env>
             <store> ... . => alloc(State) |-> I ... </store>
             <nextAddr> I:Int => I +Int 1 </nextAddr>)
         when notBool (X in keys(M))

As you can see, I use “alloc(State)”, where I would like “State” to match the 
entire configuration. Is that even possible? 
I’ve tried with 

  rule [assign-create]:
             State:Bag(
                        <k> X = I:Int; => . ... </k>
                        <env> M:Map => M[alloc(State)/X] </env>
                        <store> ... . => alloc(State) |-> I ... </store>
                        <nextAddr> I:Int => I +Int 1 </nextAddr>)
                )
         when notBool (X in keys(M))

but in this case “State” matches the empty bag (I guess) as it’s parsed as 
(Config1 Config2). Is there a way to match entire configuration (simply “give 
it a name”) and at the same time, match part of its content - all in one rule?

Thank you very much! 

Regards, 

Daniele