How do I make an item optional or repeatable in K syntax rule?

Question

How can I convert this EBNF rules below with K Framework ?

An element can be used to mean zero or more of the previous:

items ::= {"," item}*

For now, I am using a List from the Domain module. But inline List declarations are not allowed, like this one:

syntax Foo ::= Stmt List{Id, ""}

For now, I have to create a new syntax rule for the listed item to counter the problem:

syntax Ids ::= List{Id, ""} 
syntax Foo ::= Stmt Ids 

Is there another way to counter this creation of a new rule?

An element can appear zero or one time. In other words it can be optional:

array-decl ::= <variable> "[" {Int}? "]"

Where we want to accept: a[4] and a[]. For now, to bypass this one I create 2 rules, where one branch has the item and the other not. But this solution duplicate rules in an unnecessary way in my opinion.

An element can appear one or more of the previous:

e ::= {a-z}+

Where we don't accept any non-zero length sequence of lower case letters. Right now, I didn't find a way to simulate this.

Thank you in advance!

Answer 1

Inline zero-or-more productions have been restricted in the K-framework because the backend doesn't support terms with a variable number of arguments.

Therefore we ask that each list is declared as a separate production which will produce a cons list. Typical functional style matching can be used to process the AST.

Your typical EBNF extensions would look something like this:
{Id ","}* - syntax Ids ::= List{Id, ","}
{Id ","}+ - syntax Ids ::= NeList{Id, ","}
Id? - syntax OptionalId ::= "" [klabel(none)] | Id [klabel(some)]

The optional (?) production has the same problem. So we ask the user to specify labels that can be referenced by rules. Note that the empty production is not allowed in the semantics module because it may interfere with parsing the concrete syntax in rules. So you will need to create a COMMON module with most of the syntax, and a *-SYNTAX module with the productions that can interfere with rule parsing (empty productions and tokens that can conflict with K variables).

Answer 2

1. No, there is currently no mechanism to do this without the extra production.

2. I typically do this as follows:

   syntax MaybeFoo ::= ".MaybeFoo" | Foo
   syntax ArrayDecl ::= Variable "[" MaybeFoo "]"
   

3. Non-empty lists may be declared similar to lists:

   syntax Bars ::= NeList{Bar, ","}