K-user mailing list

[Bram Geron <bgeron AT gmail.com>]

Hi guys,

I'm working with Vlad Rusu as an intern, and we're modeling an assembler language using K.

I stumbled upon the following. We have a configuration with a cell

<decls> .FunctionDeclList </decls>

where

syntax FunctionDeclList ::= List{FunctionDecl,""}

which is included in a module from another file. Then we have a rule

  rule [linearize-func2]:
    <decls> ... F:FunctionDecl ... </decls>
    <nextLabel> L => L +Int 1 </nextLabel>
    [transition]

and the <decls> matcher compiles to the following Maude fragment with _~>_, as if it was in a K cell:

< decls > ?C5:K ~> F:KItem ~> ?C6:K </ decls >
 (infix form for readability)

Instead, I expected it to match with __, like it would when matching a FunctionDeclList. Indeed, if we replace both ellipses by _:FunctionDeclList, we get this Maude fragment:

< decls > ('__).KLabel(??6:KItem,,('__).KLabel(F:KItem,,??7:KItem)) </ decls > (infix form for readability)

But the generated PDF looks less pretty o:)

My question: is it possible to match user-defined lists with ..., or is the ellipsis only possible for K cells?

I'm using k-latest.tgz downloaded on 3 September, on Ubuntu 12.04.1.

Cheers, Bram