Kore Design

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.

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.

Replacing KList and KLabel functions

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)