K-user mailing list

[Robby Findler <robby AT eecs.northwestern.edu>]

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