K-user mailing list

[Ulrich Kühne <ulrichk AT informatik.uni-bremen.de>]

Hi Radu,

thanks for the hint with [prefer] and [avoid]. In this way, I can get rid of the compiler warnings. However, the runtime warnings remain. For example, using this grammar:

module AMBIG-SYNTAX
  syntax Exp ::= Int | Int "+" Int [strict,left]

  syntax Stmt ::= "var" Id
                | Id "=" Exp   [strict(2)]
                | "call" Id
        | "return" Exp [strict,prefer]
        | "return"     [avoid]
        | Exp          [avoid]
  syntax Stmts ::= Stmt > Stmt Stmts
endmodule

module AMBIG imports AMBIG-SYNTAX
  syntax Val ::= Int | "nothing"
  syntax KResult ::= Val

  rule <k>(return X:Int):Stmt =>X ...</k>
  rule <k>return => nothing ...</k>
endmodule

there is no more compiler warnings, but when I run a program like this:

return 42
return

I get the warning

[Warning] Parser: Parsing ambiguity between: Stmt Stmts (Stmts1438Syn), Stmt Stmts (Stmts1438Syn)    Arbitrarily choosing the first. in the following AST:
amb(
    (return 42) return,
    return (42 return)
)
    File: test.ambig
    Location: (1,1,2,9)
    Compilation Phase: Ambiguity filter

It's the "arbitrarily" which confuses me, since I thought my grammar would now be unique?


Concerning the context rules, I checked the tutorials, but could not find any content on this specific topic. For example, from the simple-typed-dynamic example, I get the meaning of the rule

context (HOLE => lvalue(HOLE)) = _

which looks like an ordinary rewrite rule. However, the rule

context rvalue(HOLE)

magically removes the rvalue around any evaluated _expression_. This is what I need, but why does it seem to do that?

Thanks
Ulrich


On 06/01/2013 10:23 AM, Radu Mereuta wrote:

Hi Ulrich,

Regarding the parsing issue. You could try using the prefer/avoid attributes like this:

"return" Exp [prefer, strict]

Precedences disallows for one production to be the direct child of another. They are mostly designed for binary operators, but in this case the ambiguities are at the top between unrelated productions.

Regarding the context question. Have you looked at the tutorials? http://k-framework.org/index.php/K_Tutorial

If you still don't find the right answer, please tell us. We would like to know if something is not clear.

Radu

K developer.

On Wed, May 29, 2013 at 5:51 PM, Ulrich Kühne <ulrichk AT informatik.uni-bremen.de> wrote:
Hi,

I have a (badly designed) imperative language, where statements are not separated by semicolons, which gives me plenty of ambiguous parsings. One example is return, since there is a plain "return" for void functions and "return Exp". Since Exp needs to be included as a valid statement, the parser cannot decide whether "return Exp" is one or two statements. How can I get rid of this behavior, i.e. I always want to have the "return Exp" (the maximum match) alternative? I tried using precedences, but I failed. Here is a small example:

module AMBIG-SYNTAX
  syntax Exp ::= Int | Int "+" Int [strict,left]

  syntax Stmt ::=
          "var" Id
        | Id "=" Exp [strict(2)]
        | "return" Exp [strict]
        > "return"
        > Exp
        > Stmt Stmt [right]
endmodule

module AMBIG imports AMBIG-SYNTAX
  syntax Val ::= Int | "nothing"
  syntax KResult ::= Val

  rule <k>return X:Int =>X ...</k>
  rule <k>return => nothing ...</k>
endmodule

resulting in the following warning (using K 3.0):

[Warning] Parser: Parsing ambiguity between: "return" Exp (Stmt1436Syn), Stmt Stmt (Stmt1438Syn)    Arbitrarily choosing the first. in the following AST:
amb(
    return X:Int,
    return X
)
    File: /home/.../ambig.k
    Location: (17,11,17,23)
    Compilation Phase: Ambiguity filter

My second question: can somebody please explain to me how context rules work? I already used some of them, mostly copied from the k-framework examples, but still I don't get the real meaning and how to use them properly.

Thanks!
Ulrich