K-user mailing list

["Rosu, Grigore" <grosu AT illinois.edu>]

=> is greedy, so you need parens to limit its scope.

Sent from DROID

Grigore

-----Original message-----

From: Patrick Meredith <pmeredit AT gmail.com>
To: Robby Findler <robby AT eecs.northwestern.edu>
Cc: "k-user AT cs.uiuc.edu" <k-user AT cs.uiuc.edu>
Sent: Wed, Oct 17, 2012 01:17:30 GMT+00:00
Subject: Re: [K-user] k local rewrite could not be eliminated here.

I'm not sure exactly how it is parsing your rule there, but it's not parsing it the way you want, that's for sure.  Here is what you want:

 rule <k> (spawn S => skip)  ...</k> 

       (. => <thread> <k> S </k> </thread>) 

(just add the parens)

I think it may be trying to rewrite <k> ... </k> to <thread> <k> ... </k> </thread>, which it wouldn't like.

-Patrick

On Tue, Oct 16, 2012 at 7:59 PM, Robby Findler <robby AT eecs.northwestern.edu> wrote:

I don't understand the error I'm getting for the program below when I
kompile it. This looks like it should be the same as the spawn in the
imp++ example, but apparently something is different. Am I just doing
something stupid?

Here's the error:

Error: K local rewrite could not be eliminated here. maybe you have a rewrite
    within another rewrite?
 Term: _=>_(_`(_`)('spawn_,S:K),_`(_`)('skip,.List`{K`}))
 Context: -> _~>_ -> <_>_</_> -> __ -> <_>_</_>
Location: /Users/robby/git/robby/395-2012/imp.k:17:3:18:42
 Compilation phase: MAKE-K-RULES


Here's the program:

module IMP
  syntax Stmt ::= StmtVal
                > "spawn" Stmt
  syntax StmtVal ::= "skip"

  syntax KResult ::= Bool | Int | String | StmtVal

  configuration <C color="yellow">
                  <threads>
                    <thread multiplicity="*">
                      <k color="green"> $PGM:K </k>
                    </thread>
                  </threads>
                </C>


  rule <k> (spawn S => skip)  ...</k>
       . => <thread> <k> S </k> </thread>
endmodule


Thanks,
Robby
_______________________________________________
k-user mailing list
k-user AT cs.uiuc.edu
http://lists.cs.uiuc.edu/mailman/listinfo/k-user

--
-Patrick