0

我对了解 K 前奏特别感兴趣（它的结构，为什么它的内容是这样的，“kompile”如何计算依赖关系等）。主要问题是：将 K 前奏曲中的钩子符号复制到生成的 Kore 文件中的标准是什么？

这里有一些潜在问题的例子：

  1. 符号andBool与其关联的重写规则一起复制，符号in_keys似乎不是这种情况，它只是在没有重写规则的情况下复制。其他符号似乎是无用的（对于 IMP 语义），但在生成的 Kore 文件中存在，无论是否有其重写规则，例如countAllOccurrences、findChar、signExtendBitRangeInt或Float2String。

  2. 似乎SortId是由 line 生成的syntax Id [token]。但是，线条"syntax Bool ::= "true" [token]并syntax Bool ::= "false" [token]不会生成真假符号。（此外，是否选择true和false是值而不是构造函数？）

  3. 以下示例未生成名为SortId的排序，而一些生成的挂钩符号依赖于此排序。IMP 语义不存在这个问题。

module MAX-OW-SYNTAX
    imports INT
    imports BOOL
    syntax Exp ::= Int | "(" Exp ")" [bracket]
                 | "max" Exp Exp
endmodule
        
module MAX-OW
    imports MAX-OW-SYNTAX
    syntax KResult ::= Int
        
    rule max X Y => Y requires X <Int Y
    rule max X _ => X [owise]
endmodule

  1. 在每个后端的每种语言中都实现了 K prelude 是否正确，并且在 K prelude 中可以使用 Kore 语言的实现？你有必要的接口来实现一个新的后端吗？（例如，Bag是过时的，但不是Set，List和Map，但我不知道新后端必须提供的集合运算符、映射运算符等的列表。）

  2. andThenBool和andBool一旦在 Kore 语法（布尔模块）中实现后具有相同的语义，有什么原因吗？

  3. 为==Bool定义的重写规则在哪里，在=/=Bool（布尔模块）的定义中使用？

4

1 回答 1

1

K 内部结构的最佳参考点是用户手册，以及前奏的 K 源。尽我所能回答您的具体问题：

  1. in_keys只有适用于符号后端的简化规则。这些不适用于具体的后端，因此这些后端使用 hooked implementation MAP.in_keys。某些功能（例如andBool）既可以在 K 中实现，也可以作为高效的后端挂钩来实现。例如，在 K LLVM 后端，andBool是通过代码生成来实现的。如果后端不支持该钩子，则将使用（相对）低效的 K 重写实现。
  2. 为了方便起见，Id排序是内置的。它表示程序标识符。
  3. DOMAINS在此示例中您尚未导入。这样做将引入Id排序和相关的重写。
  4. 非常粗略，主要用于内部目的。您是否考虑过假设的 K 后端，或者是否有某种方式使 K 提供的 LLVM / Haskell 后端不足以满足您的特定用例？
  5. andThenBool需要将其论点短路；允许短路，但可以严格评估两个参数andBool。使两者都执行短路的实现是有效的。
  6. ==Bool仅根据hook实现。在domains.md中，您可以看到hook(BOOL.eq)指示如何==Bool实现的属性。

如果您还有其他问题，或者想帮助在 K 中实现特定语义，请告诉我们。

于 2022-02-14T10:51:04.547 回答