K框架-与玩具语言的混淆

Question

我正在尝试学习kframework，作为练习，我想尝试创建一种高级语言，它可以编译成视频游戏的脚本语言。这种高级语言并没有真正的执行，只是编译成具有重写规则的脚本语言。

下面是原始脚本语言语法的示例

variables {
  0: 'message'
}

init {
  SetVariable("message", "Test message");
}

rule("press button") {
  conditions {
    IsButtonPressed(EventPlayer, INTERACT_KEY);
  }
  actions {
    SendMessage(EventPlayer, GetVariable("message"))
  }
}

我希望我的高级语言允许正确的变量声明，这样我就可以编写类似这样的东西，它将编译成上面的脚本。

init {
  var message = "Test message";
}

rule("press button") {
  conditions {
    IsButtonPressed(EventPlayer, INTERACT_KEY);
  }
  actions {
    SendMessage(EventPlayer, message)
  }
}

我知道如何创建一个简单的重写规则，将变量声明var x = y替换为SetVariable("x", y)，但是我如何还能添加到顶部的变量声明块中呢？

我很可能误解了K的能力，或者我应该如何做。任何帮助都将不胜感激。

Answer 1

通常，在K中将一个输入程序转换为另一个输出程序的方法是，在构造输出程序时让输出单元格包含它，并具有一系列规则，这些规则迭代地从输入单元格中删除语句和声明，并以您期望的任何修改形式将它们添加到输出单元格中。如果您遇到这样的情况，您希望无序地插入某些内容，通常的做法是让第二个单元格包含输出程序的一部分，处理变量声明的规则修改两个输出单元格。然后，一些规则将在稍后进行匹配，并将输出组合在一起。在这种情况下，当输入程序耗尽时，该规则可能适用。

下面是它在K中的大致样子：

rule <k> var X:Id = E:Expr => . ... </k>
     <output> init { D:Declarations => append(D, SetVariable(Id2String(X), E)) } </output>
     <variables> variables { D:Declarations => append(D, !Y:Int : Id2String(X)) } </variables>
rule <k> . </k>
     <output> P:Program => append(P2, P) </output>
     <variables> P2:Program => . </variables>

请注意，您必须自己编写list append函数。如果你真的关心性能，你可能应该使用列表排序，或者追加到cons列表的前面，然后反转它，但为了解释的目的，我简化了它。