kframework / k-legacy

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

Unparser cannot display the correct list units. #1433

Open liyili2 opened 9 years ago

liyili2 commented 9 years ago

If I have the following definition:

module TEST

   syntax ParamAttr ::= "sret"
   syntax FunAttr ::= "abc"
   syntax Types ::= "i32"
   syntax ArgType ::= FunAttrs Types ParamAttrs
   syntax ParamAttrs ::= List{ParamAttr," "}
   syntax FunAttrs ::= List{FunAttr," "}

   configuration <k> $PGM:ArgType </k>

endmodule

If I run the program "i32", the output of K will be:

<k>
    .FunAttrs i32 .FunAttrs
</k>

Even if the sort of FunAttrs is different the sort of ParamAttrs and the FunAttr and ParamAttr have not common terms, K cannot display the correct units for the two different lists.

grosu commented 9 years ago

Interesting. @laurayuwen, can you take a look to see if it can be fixed trivially? If not, let's then wait until we transit to KORE. On the other hand, if this is happening already in KORE, then we need to fix it asap.

laurayuwen commented 9 years ago

I also noticed this problem, when we don't assign different KLabels in List declaration, the list terminator is the same for lists using the same seperator, thus just seeing a list terminator, like in the example '.List{" "}(.KList), we don't know which list it is (FunAttrs or ParamAttrs). Just reasoning about the problem, I think of three solutions can be for the users to add different KLabels to different lists, or for the developers to change the representation of list terminators, or to perform some context analysis from syntax defined. The last two solutions are non-trivial. I will have a look at code to see if there is anything missing that can provide a trivial solution.

grosu commented 9 years ago

In KORE, each KLabel should have attached to it the production it comes from. That should be enough for the pretty printer to know what to do. Please don't spend much time on this, especially if @liyili2 is talking about the KIL pretty printer.

dwightguth commented 9 years ago

We need to test that this is correct in the new parser implementation.