K-user mailing list

["Park, Daejun" <dpark69 AT illinois.edu>]

Hi Tomofumi,

You can fix it as follows:
        (.Bag => <k> S </k>)
instead of
        (. => <k> S </k>)

The thing is that in K 4.0, the dot `.` is nothing but an alias for `.K`, and 
you have to specify sort-qualified dots (e.g., .List,  .Map).

BTW, you can take a look at the tutorial definitions under the directory:
        https://github.com/kframework/k/tree/master/k-distribution/tutorial
to figure out changes made since the K primer paper was written.

Best,
Daejun

On Feb 2, 2017, at 6:30 AM, 
tomofumi.yuki AT inria.fr
 wrote:

> Hi,
> 
> I just started using the K framework a couple of days ago while looking for 
> a
> good way to express semantics for parallel languages. I was initially using
> the virtual machine provided to get started with the tools, and since I was
> quite happy with what I was able to achieve, I decided to actually install 
> it
> on my machine.
> 
> The problem that I currently face is that the semantics I developed within 
> the
> virtual machine, which has version 3.4, does not kompile with the most 
> recent
> version from git (4.0.1).
> 
> It appears that the accepted syntax for the rewrite rules are more strict. I
> tried a heavily stripped down version of the EXP language in this article:
>  http://fsl.cs.illinois.edu/index.php/The_K_Primer_(version_3.3)
> copied at the end of the post, and many variants of it, but I was unable to
> get thread spawning to work. (From what I can see, it seems like the problem
> is around: . => )
> 
> I quickly went through the changelog, but I didn't spot any relevant changes
> to the syntax. I appreciate your help on how I can update my rules to work
> with 4.0.
> For now, what I want to know is how to write a rule for spawning of threads.
> 
> Thanks,
> Tomofumi Yuki
> 
> 
> module EXP-SYNTAX
> 
> syntax Exp ::= Int
> syntax Exp ::= "spawn" Exp
> 
> endmodule
> 
> module EXP
> 
> imports EXP-SYNTAX
> syntax KResult ::= Int
> configuration
>  <T><k multiplicity="*">$PGM:Exp</k></T>
> 
> rule <k> spawn S => . ...</k>
>     (. => <k> S </k>)
> 
> endmodule