[K-Improvement] Metadata attribute

[sskeirik]

Motivation

Sometimes, K files are consumed programmatically (e.g. via pyk), but currently, there are only limited ways to pass additional contextual information to such tools.

Here I propose that a new metadata attribute be added to the grammar which is accepted wherever attributes are allowed to appear.

Example K Code

I have several possible syntax variations we could consider. Each variation would parse a bit differently and would give the metadata attribute different structure.

Of the options below, my preference is that metadata would have an implicit key-value structure, since I don't think it would be significantly more difficult than the other options but it would much nicer if K-based tooling needed to store multiple bits of metadata about a single K syntactic item.

Basic String Syntax

In this variation, the value of a metadata attribute is a string.

module MODULE [meta("module metadata")]
  imports INT
  syntax Foo ::= Foo(Int)
               | foo(Int) [function, meta("production metadata")]
  rule foo(5) => Foo(5 -Int 2) [meta("rule metadata")]
endmodule

String Syntax with Repeats

In this variation, the value of a metadata attribute is a string set.

module MODULE [meta("module metadata"), meta("module metadata 2")]
  imports INT
  syntax Foo ::= Foo(Int)
               | foo(Int) [function, meta("production metadata"), meta("production metadata 2")]
  rule foo(5) => Foo(5 -Int 2) [meta("rule metadata"), meta("rule metadata 2")]
endmodule

String Syntax with Key-Value Structure

In this variation, the value of a metadata attribute is a string->string map.

There would also be additional requirements:

1. it would be an error to map the same key for the same metadata attribute group twice to different values --- this also includes when a piece of syntax is redeclared with different metadata (if that is possible)
2. keys would have a very limited syntactic structure to ease parsing (presumably no spaces, starts with letter, alphanumerics, maybe underscore/dash --- and that's it)

module MODULE [meta(key1="module metadata", key2="module metadata 2")]
  imports INT
  syntax Foo ::= Foo(Int)
               | foo(Int) [function, meta(key2="production metadata",)]
  rule foo(5) => Foo(5 -Int 2) [meta(key3="rule metadata")]
endmodule

Non-String Syntax

All of the above syntaxes could be changed to not use string syntax and to have some other delimiter mechanism. However, I think that strings are probably the most natural since they are already supported by the tokenizer.

Documentation

K supports metadata attributes in all context where attributes are allowed to appear. The purpose of these attributes is to annotate certain parts of a K specification so that other tools which programmatically consume K specifications may read --- K itself does not examine these attributes except to pass them through to generated output files during compilation.

An example metadata attribute is as follows:

rule foo => bar [meta(phase="runtime", type="local")]

In this case, the K compiler, when generating code for this rule, will note that it has two key-value pairs in its metadata as specified above.

The syntax for these key-value pairs is as follows:

• keys: metadata attribute keys must start with a letter, followed by any number of ASCII letters, numbers, and underscores;
• values: metadata attribute values must be string tokens with any nested double quotes or special characters properly escaped;
• it is an error to specify the same key twice with separate values.

Potential Alternatives/Workarounds

Currently, the K grammar allows for symbol and group attributes to be set by the user --- these can be (ab)used to encode metadata --- but the process is somewhat hacky.

Testing Approach

Example files could be created with all possible metadata attribute styles in all possible contexts to ensure that they parse correctly.

Invalid metadata attribute examples could also be created to ensure that the parser can reject them.