K-user mailing list

["Moore, Brandon Michael" <bmmoore AT illinois.edu>]

I don't know of any easy way to grab everything like that. I think you just 
have to explicitly name the "rest" of every cell, and put it together 
yourself.

Cutting down to one call to alloc would help, if you need to explicitly 
assemble the state yourself.
You can define a new kind of item to put in the K cell to hold and use the 
result, like this:

  rule [assign-create]:
             <k> X = V:Int; => do_alloc(X
            
alloc(Bag(<k>KRest</k><env>M</env><store>S</store><nextAttr>I</nextAddr>),V) 
KRest </k>
             <env>M</env>
             <store>S</store>
             <nextAddr>I</nextAddr>
         when notBool (X in keys(M))

(I changed "I" to "V" in the assignment, assuming you didn't mean the rule to 
apply only when you were asigning a value that happened to match nextAddr).

then you give do_alloc semantics with a rule like
  rule [do-alloc]:
             <k> do_alloc(X,Loc,V) => . ...</k>
             <env>M => M[Loc/X]</env>
             <store>... . => Loc |-> V ...</store>
             <nextAddr> I => I+Int 1 </nextAddr>

We've thought a little bit about whether there is some way to give rules 
read-only access to the whole configuration (or maybe cell completion style 
access to cells near the call?), but don't have any concrete design or plans 
for it.
Maybe you could say a little more about how your alloc works, and which 
information it needs.

Brandon
________________________________________
From: 
k-user-bounces AT cs.uiuc.edu
 
[k-user-bounces AT cs.uiuc.edu]
 on behalf of Daniele Filaretti 
[dfilaretti AT gmail.com]
Sent: Tuesday, July 08, 2014 10:30 AM
To: 
k-user AT cs.uiuc.edu
Subject: [K-user] matching entire configuration while also matching its 
components

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
_______________________________________________
k-user mailing list
k-user AT cs.uiuc.edu
http://lists.cs.uiuc.edu/mailman/listinfo/k-user