K 框架：宏不递归扩展答案

【问题标题】：K Framework: Macros not recursively expandingK 框架：宏不递归扩展
【发布时间】：2020-05-03 19:33:05
【问题描述】：

我正在查看其中一个教程练习（LOGIK extended 练习），由于某种原因，其中一个宏规则只扩展了一次。除了将以下几行添加到 LOGIK 模块之外，我没有更改 logik.k 中的任何内容，因此 K 将实际运行文件：

syntax KResult ::= Val 
configuration <T> <k> $PGM:Pgm </k> </T>

然后我跑了：

kompile  --backend java  logik.k -d .
krun tests/list-member-1.logik

我得到了（我添加了一些换行符以提高可读性）：

<T>
  <k>
    member ( X , [ X , .Terms | _ ] , .Terms ) . 
    member ( X , [ _ , .Terms | T ] , .Terms ) :- member ( X , T , .Terms ) , .Predicates . 
    ?- member ( 5 , [ 1 , .Terms | [ 2 , 3 , 4 , 5 , 6 , 5 , .Terms | [ .Terms ] ] ] , .Terms ) , .Predicates .
  </k>
</T>

但我希望查询是

?- member ( 5 , [ 1 , .Terms | [ 2 , .Terms | [ 3 , .Terms | [4 , .Terms | [5 , .Terms | [6 , .Terms | [5 , .Terms | [ .Terms ] ] ] ] ] ] ] ] , .Terms ).

需要明确的是，以下规则似乎是问题所在，因为我希望这些规则会继续使用，直到它们不再可用为止，而且我不明白为什么它们现在会停止。

  rule [T1:Term,T2:Term,Ts:Terms|T':Term] => [T1|[T2,Ts|T']]      [macro]
  rule [T:Term,Ts:Terms] => [T,Ts|[.Terms]]                      [macro]

【问题讨论】：

标签： kframework

【解决方案1】：

我们将macro 的含义转换为“非递归宏”。您需要使用macro-rec 告诉 K 这是您要递归应用的宏。

这里发生了变化：https://github.com/kframework/k/pull/592

【讨论】：

谢谢，成功了。我必须完全删除 logik-kompiled/ 才能使更改生效——这是预期的吗？
存在一个与仅更改规则属性和 kompile 实现的解析器缓存相关的已知问题。一般来说，如果你改变了规则的属性而不是规则的主体，你将不得不删除kompiled目录，是的。