K-user mailing list

[Traian Florin Șerbănuță <traian.serbanuta AT info.uaic.ro>]

Hi Daniele,

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

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?

best wishes,
- traian

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