问题标签 [kframework]

两个 K 项之间是否有内置的结构等价和 alpha 等价比较？

由于似乎有一个替代模块可以进行 alpha 转换，我想知道是否有一个等效模块。

如果没有，是否有可能以从被检查的特定语法中抽象出来的方式定义这样一个函数？例如，使用解析器的活页夹注释来检查任何两个术语，但是语法定义了它们。

对于非确定性规则，有没有办法在应用其他规则之前对某些规则进行优先级排序，直到它们无法再应用？

例如在以下规则中（在伪代码中）

其目的是在非确定性地应用规则 (2) 和 (3) 之前优先考虑非确定性结构规则，例如 (1)。即，如果允许负模式匹配，则仅适用 (2) 和 (3) 如果没有任何S形式是P|Q. 如果我没记错的话，我可以使用函数来达到类似的效果，但我想知道是否有更直接的方法。

此外，与上述规则有些相关，以下是查找表单多个元素的正确语法A + _吗？

那么是否可以更新它们？

K 是否有规则可以访问的全局状态的概念？例如说一个配置C => C'。我想转换 iffC'不存在于一组探索状态中，然后通过添加C'来更新全局探索状态集。

我正在尝试非确定性地探索程序的所有可达状态（使用 --search 选项）。但是，探索的每条路径都是独立的，这意味着如果我要在配置本身中传递探索集，则每条路径都不会知道在其他路径中看到的配置。

如果没有全局状态，这种行为的最佳实践是什么？有没有办法在每个独立路径都能够访问的更大环境中非确定性地探索转换？

是否有关于#as可用关键字以及如何使用它们的文档？

特别是#as意味着<k> S:Set </k> #as ASET是ASETSet 还是等于k其中包含的单元格S？

语法<k> ... SetItem(X) ... #as S </k>有效吗？

我有语法：

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

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 由另一种语法定义怎么办？

我想应用一个规则：

如果S不包含任何形式的项目SetItem( new X . P )or SetItem( P | Q )。

我在手册中读到存在一个:=和:/=模式匹配的运算符，但没有它的用​​法示例，我不知道它是否是我需要的。

我记得看到 K 对 Sets 没有负模式匹配，但有没有一些可以实现与:/=运算符等效的？

顺便说一句，K 是否可以同时匹配和修改一个集合中的两个项目？我尝试了规则：

但语义卡住了。这是有效的语法吗？

我希望 K 生成一堆配置，然后我可以在外部进行处理。但是，我可能想通过在每个配置上调用 K 来恢复计算。这可能吗？

我尝试查看krun --help选项，但我认为我没有看到我需要的内容。最接近的是术语解析，但我想传递完整的配置而不仅仅是一个术语。

或者，是否有用于 K 的 API 与 OCaml 一起使用？例如，如果我已经编译了 K 语义，是否有任何 API 可以在文件上调用 K、获得对 AST 的访问权并在它们上运行 K？

我有一个语法：

其中 lambda 项"fun" KVar "->" Exp是值和表达式。什么是同时成为和"fun" KVar "->" Exp的一部分的正确方法是什么？ExpVal

我尝试创建一个新的排序syntax Lambda ::= "fun" KVar "->" Exp并添加Lambda到两者Val和Exp. 但是，这与Lambda.

Pgm使用顶级格式的程序（例如）定义编程语言的语法，然后使用自动传递<k>的特殊变量限制单元格在配置声明中具有这种排序是一种常见的 K 习惯用法。这可以防止用户执行格式不正确的程序。我的问题是：$PGMkrunkrun

1. 是仅在启动时或每次规则评估后检查单元格类型吗？
2. 不同的单元格是否根据它们的身份（例如<k>单元格）或它们的类型（例如用户定义的类型与内置类型）显示不同的行为？

这是一个部分示例来说明我的意思：

对于<k>单元格，我的结论是它肯定只在启动时检查，因为程序评估通常将程序分解为一个表达式和一个延续（例如），因为它是内置ADD ~> ...的，所以不能再进行排序了。Pgm~>

那么，详细说明上面的问题（1-2），<k>细胞在这个意义上是例外的吗？

在 K 框架中，可以使用-cswitchkrun将其他变量传递给初始配置，然后是 default $PGM。例如，可能有以下代码：

并运行kompile imp.k; krun tests/sum.imp -cSOMEARG=3，$SOMEARG变量得到值3。但是，当我尝试传递字符串时遇到了问题：

之后kompile，命令

输出：

如何传递字符串参数？