1

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

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

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

configuration 
  <mylang>
    <k> $PGM:Pgm </k>
    <env> .Env:Env </env> // Env is a custom map structure defined for environments
    <store> .Map </store> // For the store we use the K builtin Map
    ...
  </mylang>

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

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

4

1 回答 1

1

每条规则都会在kompile时间进行排序检查以保持排序，因此不需要在运行时进行检查。如果有正确种类的东西进来，就会有正确种类的东西出来。

单元格<k>得到 sort K，至少例如，在这个定义中：https ://github.com/kframework/evm-semantics/blob/272608d70f363ed3d8d921887b98a26102a03032/evm.md#configuration

它导致compiled.txt（在 找到.build/defn/java/driver-kompiled/compiled.txt），它看起来像：

...

  syntax KCell ::= "project:KCell" "(" K ")" [function, projection]
  syntax KCell ::= "initKCell" "(" Map ")" [function, initializer, noThread]
  syntax KCell ::= "<k>" K "</k>" [cell, cellName(k), contentStartColumn(7), contentStartLine(31), format(%1%i%n%2%d%n%3), maincell, org.kframework.definition.Production(syntax #RuleContent ::= #RuleBody [klabel(#ruleNoConditions), symbol])]
...

但其他细胞得到更具体的种类：

...
  syntax JumpDestsCell ::= "project:JumpDestsCell" "(" K ")" [function, projection]
  syntax JumpDestsCell ::= "initJumpDestsCell" [function, initializer, noThread]
  syntax JumpDestsCell ::= "<jumpDests>" Set "</jumpDests>" [cell, cellName(jumpDests), contentStartColumn(7), contentStartLine(31), format(%1%i%n%2%d%n%3), org.kframework.definition.Production(syntax #RuleContent ::= #RuleBody [klabel(#ruleNoConditions), symbol])]
...

我不确定 K 如何决定<k>单元格需要排序K，但我认为它不是基于分析规则。我认为它很可能$PGM在该单元格中看到，因此它添加了maincell您看到的属性并赋予它 sort K。Everthing 是K.

我相当确定它在配置中没有任何 $变量赋予它 sort K，因为<chainID>KEVM 中的单元格获取这些声明：

...
  syntax ChainIDCell ::= "project:ChainIDCell" "(" K ")" [function, projection]
  syntax ChainIDCell ::= "initChainIDCell" "(" Map ")" [function, initializer, noThread]
  syntax ChainIDCell ::= "<chainID>" Int "</chainID>" [cell, cellName(chainID), contentStartColumn(7), contentStartLine(31), format(%1%i%n%2%d%n%3), org.kframework.definition.Production(syntax #RuleContent ::= #RuleBody [klabel(#ruleNoConditions), symbol])]
...

请注意，运算符并没有什么特别之处_~>_。它在这里声明：https ://github.com/kframework/k/blob/135469ea0ebea96dacf0f9a49261ff1171440c20/k-distribution/include/kframework/builtin/kast.k#L57

于 2020-06-10T21:43:08.667 回答