有没有办法在挂钩排序Int中添加一个新的构造函数

Question

我正在尝试迁移使用以下版本生成的语义：K tool, version 3.6(是的…(。我们有这样的规则：

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>

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