K-user mailing list

[Tomofumi Yuki <tomofumi.yuki AT inria.fr>]

Dear Daejun,

Thank you for your help. With this bit of extra typing in mind, I was able to 
get my specification fully working in 4.0 again.

Regards,
Tomofumi Yuki

----- Original Message -----
> From: "Daejun Park" 
> <dpark69 AT illinois.edu>
> To: "tomofumi yuki" 
> <tomofumi.yuki AT inria.fr>
> Cc: 
> k-user AT lists.cs.illinois.edu
> Sent: Sunday, February 5, 2017 11:50:23 PM
> Subject: Re: [[K-user] ] Problem migrating from 3.4 to 4.0
> 
> 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
> 
>