K-user mailing list

["Park, Daejun" <dpark69 AT illinois.edu>]

Hi,

I have two quick questions about List{…}.

First, it seems that K automatically infers a List of KResult's to be a KResult. Am I right?

For example, suppose that I want to translate the following program:

{ 1 + 10, 2 + 20 }

to

{ 11, 22 }

Then, a K definition could be:

module X

  syntax Pgm ::= "{" Exps "}" [strict(1)]

  syntax Exps ::= List{Exp,","} [seqstrict]

  syntax Exp ::= Int "+" Int

               | Int

  syntax Vals ::= List{Int,","}

  syntax KResult ::= Vals // THIS IS NOT REQUIRED

  syntax KResult ::= Int

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

  rule I1:Int + I2:Int => I1 +Int I2

endmodule

One thing I cannot understand is that the above definition works even if the following line is not given:

  syntax KResult ::= Vals // THIS IS NOT REQUIRED

How it works without the information?

Second question is:

When I tried to translate the following program (with the same K definition):

{ }

what I expected was:

{ }

but K returns

{ .List{","} }

How can I remove the annotation? Or, how can I make K parse the annotated program?

Indeed, my scenario is that there exist two K definitions, where

- the first K definition translates a given program to a simpler form,

- and, the second K definition reads the translated program and does something..

In that case, I need a way to either remove the annotation (because K parser cannot parse that annotation), or make the K parser parse that annotation.

Thanks in advance!

Best regards,

Daejun