问题标签 [kframework]

我正在尝试将评估堆栈实现为 KItems 列表。

我有一个将评估上下文添加到堆栈中的规则：

但是，在将空 E 添加到堆栈时遇到了一个错误。

我试图用构造函数扩展 KItem：

但是，这会导致形式的规则

模式匹配失败。

有没有像我试图做的那样实现一堆评估上下文的正确方法？

编辑：

会立即卡在文件上：

如果我们删除MyContext,

语义卡在x + 1.

我怀疑我实际上在这里谈论的是不同的问题。但是一种模式如何正确匹配评估上下文呢？

解析器生成器是否有用于块、行或内联注释的内置标记？例如注释块"(*" Exp "*)"或内联注释"//" Exp。

在像 menhir 这样的解析器生成器中，我通常会通过与词法分析器的模式匹配来处理注释，因此注释不会成为 AST 的一部分。K中是否有等价物？

如果不是，推荐的实施意见的方式是什么？

我在文档中读到可以编写规则

我想randBounded(4,6)返回一些随机整数。但是，当我尝试它时，它会返回一个整数V0并设置约束V0 <=Int 10 ==K true。

相反，有没有办法为范围内的每个整数生成显式分支？

例如，我想--search产生 3 种配置：每个整数 4、整数 5 和整数 6 一个。

上下文通常是一种形式#freezer_;__BILS-SYNTAX1_ ( ! _1 )。我想编写一个遍历评估上下文的函数。一种模式如何匹配评估上下文并遍历它们？

编辑：举个例子，如果我想将到目前为止看到的评估上下文记录到文件中，我需要编写一个将评估上下文转换为字符串的函数，然后通过系统调用打印它。模式匹配评估上下文是否可行？或者，K 中是否有内置的“to-string”函数？

我一直在使用 Java 后端进行符号执行，因为它具有替换功能（例如E[V/X]）。Haskell 后端是否实现了替换？

是否可以在 K 中编写高阶函数？

Map特别是and之类的东西Fold，我遍历结构并将函数应用于每个元素。

例如，如果我有一个列表：

我想将一个函数映射F到列表的每个元素：

或者可能会产生折叠：

where Fis[function, functional]并且是用来评估的，而不是语法上的。

我正在尝试使用在函数规则中进行全局环境查找的语法来编译模块。当我尝试使用 Java 后端编译我的模块时，我收到错误Conversion of KAs unsupported on Java backend! (_0,(I),_1) #as #Configuration，可能与脱糖有关（尽管pending-documentation状态“这完全被 K 前端脱糖并且不需要后端的任何特殊支持。”...但由于它待定，我知道它可能并不总是完全准确）。

所以我尝试了 Haskell 后端。这也给了我一个关于 using 的错误#isConcrete，我注意到它被记录为 Haskell 后端不支持......但我没有使用#isConcrete. 但是，我发现如果我从使用的配置中删除单元格stdout，那么我将不再收到此错误。

是否可以同时使用这种语法并拥有stdout？理想情况下，我可以继续使用 Java 后端，因为这是我遇到的问题最少的地方。

下面是一个产生错误的简单示例：

程序很简单run(0)。

教程 1 第 8 课 ( mu-defined )

我的尝试是替换现有规则：“rule mu X . E => E[(mu X . E) / X]”

规则：

不幸的是，它不会编译。我究竟做错了什么 ？这个解决方案正确吗？

教程 1 第 8 课 (SK-combinators )

他们在练习的自述文件中有这一部分：

“例如，lambda x . if x then y else z不能按原样转换为组合子，但如果我们假设一个内置的条件函数常量，比如cond，然后对其脱糖if_then_else_，则可以。然后这个表达式变成 lambda x . (((cond x) y) z)，我们知道如何转换。”

我的斗争是与'说' cond，并if_then_else_对其进行脱糖。'

我该怎么做这部分？任何帮助，将不胜感激。

教程 2 第 4 课（纯句法）

他们在练习的自述文件中有这一部分：

'提示：进行顺序组合strict(1)or seqstrict，并让语句减少到{}而不是.; 并且不要忘记创建 {}一个KResult（您可能需要一个新的句法类别，它只包含{}并包含在 中KResult）。

我的斗争是与部分： ' 和有陈述减少到{}而不是.; 并且不要忘记创建 {}一个KResult（您可能需要一个新的句法类别，它只包含{}并包含在 中KResult）'

我该怎么做呢 ？有什么提示吗？

教程 2 第 4 课（未初始化变量）

我创建了以下模块：

但这会用“##”初始化变量。如何用“未定义”初始化变量？有什么提示吗？

教程 3 第 1 课 (callCC)

对于这个练习，我创建了一个与 callcc 非常相似的代码：

由于某种原因，它不会编译。我究竟做错了什么 ？这个解决方案正确吗？

嗨，我在 MacOS catalina 10.15.6 上，正在尝试使用安装 K-framework

我不断收到错误：

我重新安装了 ocaml 和 opam 并且工作正常，但上述错误仍然存​​在！

所以我brew uninstall kframework 然后brew install kframework但现在得到错误

任何帮助非常感谢？大卫

今天它安装时没有错误或警告：

尝试测试/使用 kompile 但所有使用 course_1/imp1.k 的尝试都失败了

这是因为 imp.k 已过时还是我的安装仍有问题？（如果 imp.k 已过期，我在哪里可以获得一些最新的 _.k 文件？）

没有发现问题，最近的文件都在工作。非常感谢。

我正在尝试将 erlang 语义从 K 3.6 更新到 5.0，但遇到了以下问题：

当我尝试编写没有语义转换的函数声明时，它工作正常：

规则名称：Atom(Args) -> Body 。=>。... [结构]

但是当我需要编写以下内容时，kompile 会输出[Error] Inner Parser: Parse error: unexpected token ')'。

规则名称：Atom(Args:Values) -> Body => 。... [结构]

为了重现，这是我的简化语法：

我的 K 版本是：RV-K 版本 1.0-SNAPSHOT Git 修订版：adf2f2d Git 分支：未知构建日期：2021 年 3 月 16 日星期二 16:43:04 CET