K-user mailing list

[Radu Mereuta <headness13 AT gmail.com>]

Hi Cosmin,

Yes, currently, K uses SDF to parse programs and rules, although, we altered a bit the default behavior.

Here is a sample module that shows pretty much all the possibilities of controlling the syntax of your program with K:

module TEST
   syntax Exp ::= "++" Exp
                      | left:
                        Exp "*" Exp [mul]
                      | Exp "/" Exp [div]
                     > left:
                       Exp "-" Exp
                     | Exp "+" Exp

                     | Exp "[" Exp "]" [array]
                    > Exp "=" Exp [right]

   syntax left: mul div '_-_ '_+_
   syntax priority mul div > '_-_ '_+_

   syntax "+" -/- [\+]

// lexical variant 1

   syntax Id ::= Lexer{[a-zA-Z0-9\_]+}
   syntax Id -/- [a-zA-Z0-9]

// lexical variant 2 - the follow restriction will be inferred automatically in simple cases like this one

    syntax Id ::= Token{[a-zA-Z0-9\_]+} 

endmodule

The difference from SDF lies in two places:

1. The priority filter is only applied on the outermost terms (left and right for addition, but only on the left side for arrays)

2. The priority filter is applied over subsorts.

This last item allows you to write your syntax with inserted values. Take for example the case of lambda calculus:

syntax Exp ::= Exp Exp | Val

syntax Val ::= "lambda" Id "." Exp

syntax priority 'lambda_._ > '__

Normally SDF wouldn't apply the priority filter between application and lambda because of the subsort relation. We implemented this extension for cases just like this one that reduces the number of ambiguities and allows for more semantic information in the syntax declaration.

Radu

K dev.

On Sat, Oct 5, 2013 at 12:37 AM, Cosmin Radoi <cos AT illinois.edu> wrote:

I understand that k, unless coerced otherwise, used the SDF implementation from spoofax/metaborg. So they probably have the most detailed documentation for it - I guess this one:

http://metaborg.org/wiki/sdf

What I don't fully understand is how the k syntax definition syntax is mapped to theirs. For example, how can I define restrictions, or priorities across non-terminals? Is this mapping documented somewhere?

On a related note:
https://github.com/kframework/k/issues/63

Thanks,

Cosmin


_______________________________________________
k-user mailing list
k-user AT cs.uiuc.edu
http://lists.cs.uiuc.edu/mailman/listinfo/k-user