0

我正在看一个教程练习（LOGIK 扩展练习），由于某种原因，其中一个宏规则只扩展了一次。logik.k除了将以下行添加到模块中之外，我没有进行任何更改，LOGIK因此 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]
4

1 回答 1

2

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

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

于 2020-05-03T20:12:20.080 回答