K-user mailing list

[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