K-user mailing list

[Dorel Lucanu <dlucanu AT info.uaic.ro>]

Hi Bram,

The current version of K does not support "associative lists", as you expected.
Only the "cons" lists are supprted, i.e. lists where only constructors are the empty list
and that defined by separator. The constructor defined by the separator has a list item
and a list as arguments; it is similar to cons from Lisp lists.
The correct definition (as a cons list) for your declaration is:
 - .FunctionDeclList is a FunctionDeclList
 - if F is FunctionDecl and and L a FunctionDeclList, then F L is a FunctionDeclList.

A solution for your problem is to use sets for keeping function declarations in the cell "decls".
There is a wrapper, "SetItem" that injects K into Set.
Here is the declaration of the cell

<decls> .Set </decls>

and here is the modified rule:

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

(I guess that the rule is incomplete because in this form it can be infinitely applied).
Note that the syntactical  categories of your language are subsorted to K. In your case,
FunctionDecl and FunctionDeclLists are subsorts of K; therefore the compiler supposed that
in the cell "decls" is a K list, which is associative.

I hope this is of help for you.
Dorel

On 9/10/12 10:56 AM, Bram Geron wrote:

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

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