时间戳

首页 > 解决方案 > 如何在 K 语法规则中使项目可选或可重复？

kframework - 如何在 K 语法规则中使项目可选或可重复？

问题描述

如何使用 K Framework 转换以下 EBNF 规则？

一个元素可以用来表示前面的零个或多个：

items ::= {"," item}*

现在，我正在使用Domain 模块中的 List 。但是内联List声明是不允许的，比如这个：

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

现在，我必须为列出的项目创建一个新的语法规则来解决这个问题：

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

是否有另一种方法来对抗这种新规则的创建？

一个元素可以出现零次或一次。换句话说，它可以是可选的：

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

我们要接受的地方：a[4]和a[]。现在，为了绕过这个，我创建了 2 条规则，其中一个分支有项目，另一个没有。但在我看来，这个解决方案以不必要的方式重复了规则。

一个元素可以出现以下一个或多个：

e ::= {a-z}+

我们不接受任何非零长度的小写字母序列。现在，我没有找到模拟这个的方法。

先感谢您！

标签： kframework

解决方案

内联零个或多个产生式在 K 框架中受到限制，因为后端不支持具有可变数量参数的术语。

因此我们要求将每个列表声明为一个单独的产生式，这将产生一个 cons 列表。典型的功能风格匹配可用于处理 AST。

您的典型 EBNF 扩展看起来像这样：
{Id ","}*- syntax Ids ::= List{Id, ","}
{Id ","}+- syntax Ids ::= NeList{Id, ","}
Id?-syntax OptionalId ::= "" [klabel(none)] | Id [klabel(some)]

可选的 ( ?) 产生式也有同样的问题。所以我们要求用户指定可以被规则引用的标签。请注意，语义模块中不允许使用空产生式，因为它可能会干扰解析规则中的具体语法。因此，您将需要创建一个具有大部分语法的 COMMON 模块，以及一个*-SYNTAX包含可能干扰规则解析的产生式的模块（空产生式和可能与 K 变量冲突的令牌）。

推荐阅读