kframework - 有没有办法向 hooked sort Int 添加新的构造函数？

Question

我正在尝试迁移使用该版本制作的语义：K tool, version 3.6 (yeah...)。我们有这个规则：

syntax Int
       ::= #cint(Int,Int)

当我用 K 版本编译语义时：5.1.16和 LLVM 后端，我得到这个错误：

[Error] Compiler: Cannot add new constructors to hooked sort Int

有没有办法支持这个版本的规则5.1.16？

Answer 1

后端不支持扩展钩子排序。

但是你可以使用宏来绕过它：

$ cat test.k
module TEST
    imports INT
    configuration <k> one +Int 2 </k>
    syntax Int ::= "one"
    rule one => 1 [macro]
endmodule
$ kompile test.k
$ krun
<k>
  3 ~> .
</k>

宏在前端处理，只要您以这种方式处理所有构造函数，您就可以摆脱扩展钩子排序。