I forgot to say that the builtin lists can be used in the same way
as the sets.
The injection of K into List is given by ListItem.
It is up to you whether you use the builtin sets or the bulitin
lists, the mecanisms are similar.
Dorel
On 9/10/12 11:25 AM, Dorel Lucanu
wrote:
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
_______________________________________________
k-user mailing list
k-user AT cs.uiuc.edu
http://lists.cs.uiuc.edu/mailman/listinfo/k-user
|
