K-user mailing list

["Chen, Xiaohong" <xc3 AT illinois.edu>]

cc all.
-------------------------
Chen, Xiaohong
BSc, Peking University
PhD student, UIUC

________________________________________
From: Chen, Xiaohong
Sent: Wednesday, March 01, 2017 9:41 AM
To: 
daparpon AT dsic.upv.es
Subject: RE: [[K-user] ] Tags and attributes

Dear Daniel,

Thank you for choosing K.

The [function] tag is well explained in this post 
(https://github.com/kframework/k/wiki/Manual%20(to%20be%20processed)).

The [avoid] tag (and dually, the [prefer] tag) is used to specify parsing 
preferences. For example, the condition statement has the following two 
definitions:
IfExp ::= "if" BExp Exp
| "if" BExp Exp "else" Exp

which is ambiguous. Consider expression "n = 0; if false if true n = 1; else 
n = 2;". What is the value for n? Is it 0 or 2?

To overcome this ambiguity, we want to let K know to parse the above 
statement as "... if false (if ... else ...)", not the other way. This means 
when parsing (from left to right) and meeting an "if", always try *not* to 
expect an "else" unless you actually meet an "else". This makes "else" 
related to the nearest "if".

To achieve that, you can use [avoid] (or [prefer]) tag to let K know your 
preference.

I hope it helps.

Cheers,
Xiaohong

-------------------------
Chen, Xiaohong
BSc, Peking University
PhD student, UIUC

________________________________________
From: 
daparpon AT dsic.upv.es
 
[daparpon AT dsic.upv.es]
Sent: Wednesday, March 01, 2017 6:36 AM
To: 
k-user AT lists.cs.illinois.edu
Subject: [[K-user] ] Tags and attributes

Hi! I have a question about some tags that I have found within K's example
language definitions. In particular, I am interested in the tag "[avoid]",
associated to both language constructs and rules, and "[function]", associated
to language constructs, in the specification of KernelC. Do they have any
specific functionality as attributes? And, if they do, which one is it?

Thanks in advance,
Daniel