K-user mailing list

[Patrick Meredith <pmeredit AT gmail.com>]

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