KORE data structures guide

Please read the KAST and KORE guide first. This page assumes you're already familiar with the details of KAST and KORE, and only provides information on their usage as data structures.

The data structures are a programatic representation of KORE's syntax (the syntax may be a bit outdated until Radu merges from kast-in-k). Each production in the syntax has a corresponding Java interface or class with a very similar name. There are types (interfaces or classes) corresponding to each sort. For KAST (inner KORE), the types have the same name as the sort, e.g., we have the KList type corresponding to the KList sort. For outer KORE, the types have the same name as the sorts, with the K prefix dropped. For the KSentence sort, we have the Sentence type. The constructor for the type associated with each production is specified by the hook attribute of the production.

I know several people asked for JavaDoc, and I actually started working on them, but then realized that it is not such a good idea. Having JavaDoc allows me to describe a rather large API, which may contain bugs. Describing the API by hand, on the wiki, forces me to keep it small. Also, if the API is too large to be described in a wiki page, we have failed.

The KORE data structures live in org.kframework.kore. Before using any data structure, do the following static import:

import static org.kframework.Collections.*;

Inner KORE (KAST + K-STUFF)

In this section we describe the interfaces and the ADTs for the inner parts of KORE. Each sort in the K module (and its transitively included modules) has a corresponding Java interface with an identical name. The interfaces are described here using Scala traits, which get compiled to Java interfaces.

The front-end, compilers, and various backends have their own implementations of the interfaces. They can interact seamlessly as each tool is required to accept the general interface, not more specific classes, as its input and generate data structures which implement the interfaces as output. To this end, each tool is required to have an implementation of the Constructors interface.

Implementations of Constructors are inner-KORE object factories. For convenience, KORE provides a basic such constructor. Either instantiate KORE explicitly, or import a singleton version of it statically:

import static org.kframework.kore.KORE.*;

The following factory methods are provided by all implementors of Constructors:

  KLabel KLabel(String name)
  Sort Sort(String name)
  KList KList<KK extends K>(java.util.List<KK> items)
  KToken KToken(Sort sort, String s, Att att)
  KApply KApply(KLabel klabel, KList klist, Att att)
  KSequence KSequence<KK extends K>(java.util.List<KK> items, Att att)
  KVariable KVariable(String name, Att att)
  KRewrite KRewrite(K left, K right, Att att)
  InjectedKLabel InjectedKLabel(KLabel klabel, Att att)

Accessors

The data structures are immutable so there are no setter methods. By convention, all other properties of the data structures can be accessed using a getter which has exactly the same name as the parameter in the constructor (except kss which are described below). E.g., the left side of a KRewrite object r can be accessed with r.left().

Attributes

There is a non-K object Att(Set<K> attributes) which holds the attributes for each K. All constructors of K types have take an Att as the last argument.

For now, the Att class is very basic. We'll make it smarter as the need arises. I don't want to make it more complex then necessary by trying to anticipate future uses.

KCollection

KCollection represents a K which has child Ks. It provides for its extending classes the following methods:

• String mkString(String separator) concatenates all elements with the gives separator and returns the resulting String.
• List<K> items() of the children.
• java.util.stream.Stream[K] stream() of the children.

Extending the KORE classes

The KORE classes were designed with extensibility in mind. The first list of types above can be extended to create new classes which blend seamlessly. Frontends, backends, or compiler passes may add other classes for their own purposes, but those classes will not live in the .kore package. Still, following the interface will allow them to be pretty-printed, visited, etc. using the common infrastructure.

KORE outer classes

The KORE outer data structures live in org.kframework.definition. To enable their constructors (factory methods), do:

import static org.kframework.definition.Constructors.*;

The KORE outer classes follow very, very closely the syntax in kore.k. The data structure associated with each production is named in the hook attribute of the production. All list-like productions (assoc but not comm) become immutable lists in the data structures. All set-like productions (assoc comm) become immutable sets in the data structures. To create an immutable data structure programmatically, take the original data structure call immutable on it, e.g., a java.util.Set s is transformed to an immutable data structure by calling immutable(s).

To get a part of an outer structure, call the method named after that part. In general, the name is very intuitive (but we may try to find a way to annotate the kore.k syntax with the property names). E.g., to get the sentences of a module m call m.sentences(). It returns for now a Scala immutable data structure. Do not consider this data structure's API as part of the KORE API. Instead, consider it a an immutable black box of data. To use it, you need to convert it to whatever Java structure you like. If you want to iterate it, call iterable on it (e.g., iterable(s) where s is the immutable data structure, and you will get an java.lang.Iterable<CorrectType>. If you want to use the new Java 8 stream API, similarly, simply call stream on it.

NOTE: as this wiki is written by hand, there might be small differences between the implementation and the this description. Please let me know as soon as you encounter any differences and I'll fix them quickly.