kframework / k-legacy

The K tools (deprecated, see README)
http://kframework.org
Other
146 stars 61 forks source link

strange ambiguity due to brackets #735

Open dlucanu opened 10 years ago

dlucanu commented 10 years ago

The following definition

module TEST
  syntax Exp ::= Id | Int
  syntax Pred ::= Exp "<" Exp 
                | "(" Pred ")" [bracket]
  syntax Form ::= Pred 
                | "(" Form ")" [bracket]
                > Form "/\\" Form 

  configuration <k> $PGM:K </k>
endmodule

compiles but when it is executed on the program "(0 < IDS) /\ (IDS < N)" the following ambiguity is reported:

$ krun ex.test 
<k>
    ((0 < IDS) /\ (IDS < N))
</k>
[Warning] Inner Parser: Parsing ambiguity. Arbitrarily choosing the first.
1: 
   (0 < IDS)
2: 
   (0 < IDS)
    File: ex.test
    Location: (1,1,1,10)
    Compilation Phase: Ambiguity filter
[Warning] Inner Parser: Parsing ambiguity. Arbitrarily choosing the first.
1: 
   (IDS < N)
2: 
   (IDS < N)
    File: ex.test
    Location: (1,14,1,23)
    Compilation Phase: Ambiguity filter

If we remove/comment the line including | "(" Pred ")" [bracket] then the execution finishes normally.

radumereuta commented 10 years ago

It's an ambiguity between the two brackets. I admit, the error message is kind of bad because it doesn't point to the original productions. I will fix this in the new parser.