Kore Design

This is an old page; see https://github.com/kframework/k/wiki/KAST-and-KORE.

The new Kore

We have more or less agreed on a design for Kore. Here's the syntax:

    KLabel ::= <label constants>
    KToken ::= #token(String,String) | #label(KLabel)
    KItem ::= KToken | KLabel(KList)
    KList ::= List{K}{,}{.KList}
    K ::= List{KItem}{~>}{.K}

The biggest change is that atomic values like tokens are now subsorted into KItem rather into KLabel (and then applied to an empty list).

Functions are now only allowed to take and return values falling under K, anything that appears to pass around a KLabel actually passes the label wrapped under #label. A rule matching a variable V:KLabel on the left hand side will instead match #label(V:KLabel). Note that only terms of syntactic sort KLabel can occur here, so such a pattern is either a constant label or a variable, and it should be easy to handle.

To support user code that uses a KLabel function in the argument position, we'll use #apply as the label of a function taking a wrapped label and a wrapped KList of additional arguments.

KLists will be made into KItem by putting them under the label #klist. Anything that passes or returns KLists can be written in K in terms of that wrapping, so we think we might remove support for KLists entirely.

Kore for Rules

To represent everything we need in rules, Kore must also support variables, rewrite arrows, and type annotations. Cells can probably be handled with a distinguished labels. These productions support variables:

    Sort ::= <sorts>
    KLabel ::= Variable
    KItem ::= Variable | KItem ":" Sort | KItem "::" Sort

Note that the Variable production in KItem also supports KList and K variables, because both of those sorts include K (A program manipulating Kore may of course internally use an AST that has variable constructors in KList and K if it likes).

For now, we believe that allowing rewrites only at sort K should be sufficient. We also add parentheses at sort K to allow delimiting the extend of the rewrite. A rewrite arrow is not allowed to appear as a descendant of another rewrite arrow.

    K ::= "(" K ")" | K "=>" K

Two design options

If matching on #label turns out to be a problem, we could add a construct KLabel ::= #fromKToken(KToken) which is a right inverse of #label.

To continue supporting KList arguments and results in K definitions, we could either have Kore translation assume the existence of additional functions for operating on wrapped KLists, like an #append, or perhaps extend the grammar with an operation for splicing a wrapped list into the surrounding list.

Translating KList and KLabel functions into the new Kore

This new design doesn't directly support functions returning KLabel or KList as we currently allow in the K frontend, but these can translated into the new design by wrapping a KLabel or KList into a KItem.

KLabel functions

A function accepting or returning a KLabel would be changed to accept or return a KToken made with the #label injection. This is done by wrapping any KLabel variable bound on the left hand side in #label, as well as any KLabel variable or literal on the right hand side which is returned, or an argument to a function expecting KLabel. For example, rules

    test(L::KLabel) => L(1,2)
    test2(true) => 'label1
    test2(false) => 'label2

would become

   test(#label(L)) => L(1,2)
   test2(true) => #label('label1)
   test2(false) => #label('label2)

The last case is using a KLabel-returning function directly as the label of a term, as in test2(B)(1,2). To translate that, we can rely on a single predefined function #apply, where #klist is just an ordinary KLabel, which shouldn't be defined as a function.

   #apply(#label(L),#klist(KL)) => L(KL)

With #apply for expressing applications, test2(B)(1,2) can be replaced #apply(test2(B),#klist(1,2)).

KList functions

A KList can be embedded into KItem simply by putting it under some agreed-upon label that isn't a function, we'll assume the label is #klist here, and wrapping and unwrapping it as for KLabel. For example, a function

    KList ::= rev(KList)

might be defined by rules

    rev(K::KItem,KL::KList) => rev(KL),K
    rev(.KList) => .KList

Besides returning a KList expression as the result or passing it as an argument, the other way to directly use a KList expression is putting it as an item in a larger KList so it will merge in by associativity, as with the rev call on the right hand side of the first rule.

This case can also be handled by defining a helper function, like this #append:

   #append(#klist(KL1),#klist(KL2)) => #klist(KL1,KL2)

Then reverse can be written as

    rev(#klist(K::KItem,KL::KList)) => #append(rev(KL),#klist(K))
    rev(#klist(.KList)) => #klist(.KList)