KORE for incomplete cells

This page describes an internal representation of cells as they can be written in concrete syntax, for internal use before the compiler rules that fix terms to respect the cell structure productions as described at KAST and KORE. This is probably not available to users writing in KORE syntax, so it's only of interest to K developers.

A few things separate the cell syntax users can write with full syntax from the productions used to declare configurations in KORE.

1. Cells can be written out of the declared order, or left out entirely
2. Cells can be written directly inside an ancestor cell, without wrapping it in all the intermediate parents.
3. Cells can be "open" with dots.

To accommodate these differences, some early compiler passes use a looser cell representation, which doesn't yet try to follow the syntax declared in the production.

1. Any cells written inside a parent cell in the concrete syntax are made immediate children of the cell label, up to arbitrary arity. For example, in the example configuration on the page KAST and KORE a valid pattern is

    <top><k>K</k><env>E</env><store>S</store></top>
   

   This would become a KORE term.

    `<top>`(`<k>(K),`<env>`(E),`<store>`(S))
   

2. Dots in a cell are represented by adding a special term `#dots`() as the first and/or last argument of the cell's label. For example,

    <k>I + J ...</k>
   

   becomes

    `<k>`(`_+_`(I,J),`#dots`())
   

3. A rewrite with zero or multiple cells on a side used the label #cells to wrap those cells into a single term.