kframework - 如何在 K 中使用 [binder]？

Question

我有语法：

syntax Process ::= KVar "(" KVar ")" "." Process  [binder]
                 | "new" KVar "." Process         [binder]
syntax Program ::= KVar "(" KVarVec ")" "=" Process [binder]
syntax KVarVec ::= KVar | KVar "," KVarVec

这两种语法具有三个不同绑定的产生式：

1. a(x).P, where xis bound in P, 但是a是一个不受该术语约束的名称。

2. new a.P像 lambda 一样绑定a。P

3. f(a,b,c) = P绑定in的向量a,b,c。向量中的每个都应该绑定在.KVarPKVarP

我如何知道binder在生产中绑定特定变量？有什么binder(2)可以告诉它第二个KVar应该被绑定的吗？如果它的几个KVars 由另一种语法定义怎么办？

Answer 1

目前 binder 属性的一个限制是变量 bound 必须是产生式中的第一个非终结符，并且绑定它的项必须是最后一个非终结符。随意对您在 GitHub 上提出的概括提出功能请求，我会在某个时候处理它。不过可能不会马上。