0

我有一个形式的规则

rule <k> (try S1 catch(Param) S2 => S1 ~> foo) ~> K </k>
     <stack> .List => ListItem((bar)) ... </stack>

wherestack是我的配置中的列表类型单元格，它是k单元格的兄弟，并且foo是一个函数。

当我的程序卡住时，k单元格输出<k> try { baz } catch(p) { buz } </k>和stack单元格<stack> .List </stack>. 在我看来，这两者确实匹配，并且应该应用规则中定义的替换，但是krun卡在这里。输出的配置、语法和类型似乎匹配，所以我想知道是否还有其他原因导致不应用替换。

对于上下文，这是simple-typed-static对教程中语言的修改；为了清楚起见，我删除了部分规则和输出，尽管它们也都匹配。我正在使用 java 后端编译它。

编辑：我在下面添加了语法声明

syntax Stmt ::= "try" Block "catch" "(" Param ")" Block
syntax Block ::= "{" Stmts "}"
syntax Param ::= Type Id

除了标准k单元和其他一些（我认为）不相关的单元之外，配置还有，

<stack multiplicity="?"> .List </stack>

和foo具有以下形式的函数

syntax KItem ::= "foo"
rule <k> foo => . ... </k>
     <stack> ListItem(_) => .List ... </stack>
4

1 回答 1

0

p 不是排序参数，这就是为什么这个规则不适用。不过，我不确定您的术语是如何打错的。K 的 Java 后端相当陈旧，并且存在许多设计缺陷，可能会在重写时导致类型安全性受损。但是，如果没有更多信息，就不可能说出原因。我建议通过使用 krun --depth 将程序执行到不同的深度来逐步执行程序，并尝试确定当 Id 不是 Param 的子类时，您如何获得排序 Id 的术语，其中预期排序参数是术语.

于 2020-03-25T03:46:15.133 回答