K-user mailing list

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

Thanks!

Robby

On Tue, Oct 16, 2012 at 8:17 PM, Patrick Meredith 
<pmeredit AT gmail.com>
 wrote:
> 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