K-user mailing list

[Daniele Filaretti <dfilaretti AT gmail.com>]

Dear Traian, 
thanks a lot for your reply!

On 10 Sep 2012, at 21:55, Traian Florin Șerbănuță wrote:

> W.r.t. the first question, I hope Radu will find a good answer for you
> as he is our parsing expert.

I was using the version of K that appeared a couple of weeks ago. I saw today 
that there is a very new version (out today), I'll check it (if that was a 
bug I but I guess it is fixed now).
Anyway the question is still open...

> For the KOOL-related question, I would say that although we don't
> check for class name duplicates in the definition, I think we do that
> in the definition of the type checker.
> 
> Otherwise, you are of course right; one could use a map and check that
> the key is not already present in the map before adding a new mapping.
> 
> is this satisfactory?

Yes, it is, thanks! :) 
Actually I read the "KOOL-untyped" (there are various versions -typed and 
untyped- in the example folder), but I've got the point.

BTW, I'll submit my work to you guys soon... 

Thanks again, 

Daniele

> 2012/9/7 Daniele Filaretti 
> <dfilaretti AT gmail.com>:
>> Dear all,
>> I recently started using the new version of K and the parser seems to
>> work better than before (as well as having better correct-line error
>> messages, better handling of precedences and so on).
>> I have a couple of questions...
>> 
>> Question 1:
>> 
>> Regarding precedences: in my syntax I have something like:
>> 
>> Syntax Exp ::=
>>        ...
>>        |Exp "/" Exp          [ left, strict ]
>>> Exp "+" Exp      [ left, strict ]
>>       | Exp "<=" Exp     [ seqstrict, latex({#1}\l
>>> VarId "=" Exp   [ strict(2) ]
>>       | VarId "=" "&" VarId
>>        ...
>> 
>> This way, an expression like
>> 
>> a = b + c
>> 
>> it correctly parsed as
>> 
>> a = (b + c)
>> 
>> because binary operators (in particular "+") have precedence over
>> assignment (using ">" in syntax definition).
>> 
>> Now, I've been trying to group the various binary operations into a
>> separate category:
>> 
>>  syntax BinOpExp ::=
>>         Exp "/" Exp    [ left, strict ]
>>> Exp "+" Exp  [ left, strict ]
>>       | Exp "<=" Exp   [ seqstrict, latex({#1}\l
>> 
>>   syntax Exp ::=
>>        ...
>>       | BinOpExp // See above!
>>> VarId "=" Exp                                     [ strict(2)]
>>       ...
>> 
>> but this doesn't work, i.e. when I run 'krun' on the same expression
>> 'a = b + c' I got an error msg saying that there is a parsing
>> ambiguity between "=" and "+", and that the first is chosen arbitrary.
>> Hence, the expression is parsed as
>> 
>> (a = b) + c
>> 
>> The two definitions looks equivalent to me. Is this a bug/problem in
>> the current K tool implementation or I'm missing something?
>> 
>> Question 2:
>> 
>> I'm reading the KOOL language definition contained in the example
>> folde, as I'm interested in modelling classes and objects in K.
>> Regarding class declaration:
>> 
>> /*@ \subsection{Class declaration}
>> Initially, the classes forming the program are moved into their
>> corresponding cells: */
>> rule <k> class Class1:Id extends Class2:Id { Ss:Stmts } => . ...</k>
>>      <classes>... (. => <class>
>>                           <className> Class1 </className>
>>                           <extends> Class2 </extends>
>>                           <declarations> Ss </declarations>
>>                       </class>)
>>      ...</classes>  [structural]
>> 
>> It seems to me that this way it is possible to have multiple classes
>> sharing the same name (i.e. there is no check wether "Class1" already
>> exists or not). Is it correct? If yes, is there a way of checking
>> wether the name "Class1" is unique?
>> 
>> If this is not the case I would use a mapping from names to "classes",
>> but I'm not sure...
>> 
>> Thank you very much for your advice, and have a nice day!
>> 
>> Best regards,
>> 
>> --
>> Daniele Filaretti
>> _______________________________________________
>> k-user mailing list
>> k-user AT cs.uiuc.edu
>> http://lists.cs.uiuc.edu/mailman/listinfo/k-user