7

可変長の引数リストをループする Ltac 定義を作成しようとしているときに、Coq 8.4pl2 で次の予期しない動作に遭遇しました。誰かが私にそれを説明できますか？

Ltac ltac_loop X :=
  match X with
  | 0 => idtac "done"
  | _ => (fun Y => idtac "hello"; ltac_loop Y)
  end.

Goal True.
  ltac_loop 0.  (* prints "done" as expected *)
  ltac_loop 1 0.  (* prints "hello" then "done" as expected *)
  ltac_loop 1 1 0.  (* unexpectedly yields "Error: Illegal tactic application." *)
4

1 に答える 1

6

ltac_loopの最後の呼び出しを展開して、何が起こっているかを見てみましょう。

ltac_loop 1 1 0
-> (fun Y => idtac "hello"; ltac_loop Y) 1 0
-> (idtac "hello"; ltac_loop 1) 0

そこに問題があることがわかります。関数ではないものを引数に適用しようとしており、その結果、見たエラーが発生します。解決策は、タクティックを継続渡しスタイルに書き直すことです。

Ltac ltac_loop_aux k X :=
  match X with
  | 0 => k
  | _ => (fun Y => ltac_loop_aux ltac:(idtac "hello"; k) Y)
  end.

Ltac ltac_loop X := ltac_loop_aux ltac:(idtac "done") X.
于 2014-03-30T21:44:16.687 に答える