K-user mailing list

[Daejun Park <dpark69 AT illinois.edu>]

Thank you very much, Radu!

Can I ask you one more question? How to redefine the comments?
Is there an way to define my new comment syntax without modifying K itself?

What I've found is that the comments are parsed by: src/javasources/parsers/Concrete/syntax/Common.sdf. But I don't know how to redefine it in my K definition.

Many thanks!
Daejun

Radu Mereuta wrote:

Hi Daejun,

Unfortunately, SDF, the parser that we are using, doesn't really support unicode characters. And whitespace is an entire different discussion, but pretty much the same idea. SDF for whitespace sensitive languages -> not so great.

The #String sort, is the actual implementation of strings but from SDF. You can find the exact definition here: https://github.com/kframework/k/blob/master/src/javasources/parsers/Concrete/syntax/KBuiltinsBasic.sdf

I chose to write it directly in SDF because exact definition is a bit more complex than what we currently support in K. When you look at the definition for floats, that's even more visible.

I guess if you are trying to redefine the strings with single quote, you could try something like this:

syntax MyString ::= Lexer{"'" MyStringChar "'"}

syntax MyStringChar ::= Lexer{~[\"\n\r\\]}

syntax MyStringChar ::= Lexer{[\\]~[\n\r]}

WARNING: if you write that in the rule parser, you will get unexpected behaviors. Especially if you have klabels. You should reserve from using those to only programs (one of the attributes notInRules, notInGround or onlyLabel).

Also, if you are wondering what I wrote inside the lexer rule, that's just SDF. You can find more here: http://www.meta-environment.org/doc/books/syntax/sdf-disambiguation/sdf-disambiguation.html

Radu

On Fri, Nov 1, 2013 at 7:50 PM, Park, Daejun <dpark69 AT illinois.edu> wrote:
Hi all,

How can I parse a string enclosed by a single quote(')? More generally, how can I redefine the "String" sort?

What I've found is that it has something to do with the following line at builtins/string.k:
rule #parseToken("#String",S:String) => (S)
but I don't know where '#String' comes from.

Also, I want to know how to control the scanner (lexer) of K parser. For example, when it comes to handling unicode characters or parsing in a line break sensitive manner, what should I do?

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