K-user mailing list

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

2013/6/4 Radu Mereuta <headness13 AT gmail.com>

Regarding the other ambiguity. Try declaring statement composition like this: syntax Stmts ::= Stmt | Stmts Stmts [left]

About contexts, Traian will give you a better answer shortly.

Radu

K developer

On Tue, Jun 4, 2013 at 11:41 AM, Ulrich Kühne <ulrichk AT informatik.uni-bremen.de> wrote:

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)

Hi Ulrich,

What you say seems strange to me. Actually, it is rvalue(HOLE) which is the simple context :-)

briefly saying rvalue(HOLE) is like adding the strict attribute to  rvalue in its syntax declaration,

and you can think of it as generating two rules:

rule rvalue(E) => E ~> rvalue(HOLE) 

and

rule E ~> rvalue(HOLE) => rvalue(E)

Note that the rules are inverse to eachother.

However, in the implementation, the first rule is constrained to only apply when E is not a value and the second to apply only when E is a value.

W.r.t. the first context, context (HOLE => lvalue(HOLE)) = _

it also generates two rules, but slightly different:

rule (E1 = E2) => (lvalue(E1) ~> (HOLE = E2))

and

rule (lvalue(E1) ~> (HOLE = E2)) => (E1 = E2)

Note, again, that these two rules are also mutually inverse.

Again, in the implementation, the first rule is constrained to only apply when E1 is not a value and the second to apply only when E1 is a value.

usually the lvalue type of context is used only when you want to prevent normal evaluating rules from applying on the redex, like we want for lvalue (we want it to evaluate to a location, instead of a value as it would normally happen).

hope that helps.

best wishes,

Traian

 

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

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