问题标签 [kframework]

我有一个形式的规则

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

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

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

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

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

和foo具有以下形式的函数

我正在使用 LLVM 后端进行编译。它可以使用 Java 后端进行编译，但是 LLVM 后端会抛出以下错误： Compiler: No fresh generator defined for sort Optional[KVar]

该错误突出!M显示<abs> ... .Map => (!M |-> (T1 -> T2)) ... </abs>

我试图用以前用 Java 后端编译的 LLVM 后端编译一个文件，并得到这个警告：

然后在运行时出现以下错误：

这些是什么意思？

我想在一条规则中“要求”两件事。我写了类似的东西

但它不起作用。K 中有没有办法在一个规则上设置多个约束？

我写了类似的东西

但这似乎不是正确的语法。检查映射中是否不存在键值对的正确方法是什么？

我有以下作品：

这个错误是什么意思？

是否有规则的语法，例如：

或者我是否需要使用评估上下文重新定义语义？

Kframework 网站上有一本关于 2010 年的 Big-Step SOS 的书，使用的是旧语法：

它似乎可以满足我的要求，但我不确定是否存在新的语法。

在尝试为类似 Scheme 的语言定义语法时，我发现使用 java 后端的 kompiled 文件的运行结果

llvm 后端的行为不同

这是我的 scheme.k 代码：

这是我要运行的测试文件：

奇怪的是，使用java的kompiled版本可以正常运行这个测试用例，而使用llvm的kompiled版本卡在

可能的原因是什么？kompile 的版本信息是

我正在看一个教程练习（LOGIK 扩展练习），由于某种原因，其中一个宏规则只扩展了一次。logik.k除了将以下行添加到模块中之外，我没有进行任何更改，LOGIK因此 K 将实际运行文件：

然后我跑了：

我得到了（我添加了一些换行符以提高可读性）：

但我希望查询是

需要明确的是，以下规则似乎是问题所在，因为我希望这些规则会继续使用，直到它们不能再使用为止，而且我不明白为什么它们现在会停止。

我的主要问题是什么是“意外的连接项”。我对下面的错误有一些背景，尽管似乎还有许多其他问题可能会混淆这个错误。

我有一个foo排序术语Map和一个bar排序术语Map。foo接受一个表达式列表，目标是将它们全部放入Map. 为此，我调用bar它并连接每个表达式。从语法上Map我相信应该足够然后说bar(exp) foo(exps)得到整个Map.

这编译得很好，但是当我尝试在我重写后立即运行它时，bar(exp) foo(exps)我得到了一个 [Error] Critical: unexpected concatenated termfoo(...) while evaluating function _Map_. 为简洁起见，我删除了表达式本身。

我认为问题可能在于Map联合的优先级高于我的foo，bar因此我尝试将其分配bar为一个函数，因为bar它的参数很严格，这导致了排序错误KItem并且Exp不兼容。