K-user mailing list

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

Hi Daejun,

2013/11/30 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?

There is a specific line in the kompile sources which checks whether the item sort of a list is subsorted to KResult, and, if so, it subsorts the entire list to KResult.

This is done in order to capture the idea that lists are "hybrid", i.e., they become results when all their elements are results.

 

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.

This is an issue with the pretty printer, which should probably detect (and avoid  printing) empty lists if the parent constructor is a language construct

best wishes,

Traian

 

Thanks in advance!

Best regards,

Daejun

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