Document ... in the K User Manual

[tothtamas28]

The symbol ... is syntactic sugar for a few different things that are mentioned in certain parts of the K Tutorial.

In the K User Manual, there's only a single mention:

k/docs/user_manual.md

Line 1088 in 14e33b6

framing `...` to indicate the missing cells, they will receive the default

It'd be nice to have a dedicated section in the K User Manual that describes all uses of ... in one place as a reference for the feature.

Documented uses of ...

In a <k> cell:

k/k-distribution/k-tutorial/1_basic/13_rewrite_rules/README.md

Line 254 in 14e33b6

Here we have placed the symbol `...` immediately prior to the `</k>` which ends

In a cell containing other cells:

k/k-distribution/k-tutorial/1_basic/15_configurations/README.md

Line 241 in 14e33b6

second is that we have introduced the concept of `...` once again. When a cell

In a cell containing a Map:

k/k-distribution/k-tutorial/1_basic/16_collections/README.md

Line 100 in 14e33b6

Finally, we have used the `...` syntax on a cell containing a Map. In this

In a cell containing a List:

k/k-distribution/k-tutorial/1_basic/16_collections/README.md

Line 174 in 14e33b6

The `...` syntax is allowed on cells containing lists as well. In this case,

In a cell containing a Set:

k/k-distribution/k-tutorial/1_basic/16_collections/README.md

Line 297 in 14e33b6

Like `Map`, the `...` syntax on a set is syntactic sugar for an anonymous

Questions

• Is the above list of uses complete?
• From the list above, are all uses distinct cases of the feature? (I.e. is some of them a special case of some other?)

[Baltoli]

There's a better reference directly in kast.md: https://github.com/runtimeverification/k/blob/14e33b62c6de8889c7d64e636d5183f31c361005/k-distribution/include/kframework/builtin/kast.md#syntax-of-cells

There is also the implementation of the compiler pass that turns dots into correct variables: https://github.com/runtimeverification/k/blob/14e33b62c6de8889c7d64e636d5183f31c361005/kernel/src/main/java/org/kframework/compile/CloseCells.java

And the full cell concretization process: https://github.com/runtimeverification/k/blob/14e33b62c6de8889c7d64e636d5183f31c361005/kernel/src/main/java/org/kframework/compile/ConcretizeCells.java

The semantics of closing cells is specified by the assoc / comm attributes:

k/kore/src/main/scala/org/kframework/compile/LabelInfoFromModule.scala

Line 7 in 14e33b6

class LabelInfoFromModule(module: Module) extends LabelInfo {

You can pretty easily get the compiler to accept dotted cells over your own sorts by giving the appropriate productions assoc and unit attributes as appropriate; we could perhaps document this in the user manual. Cell productions are just one instance of this working.

[Baltoli]

@dwightguth cautions that this part of the compiler is probably the oldest remaining part of the K frontend and may be a bit janky.