4

我正在尝试编写一个返回值的策略，并且在这样做的过程中它需要检查某些东西是否是一个 evar。

不幸的是，我不能使用is_evar，因为那时该策略不被视为返回值（而是另一种策略）。下面是一个例子。

有什么建议么？

Ltac reify_wrt values ls :=
  match ls with
  | nil => constr:(@nil nat)
  | ?a :: ?ls' => let i := lookup a values in
                 let idx := reify_wrt values ls' in
                 constr:(i :: idx)
  | ?e :: ?ls' => is_evar e; 
                  let i := constr:(100) in 
                  let idx := reify_wrt values ls' in
                  constr:(i :: idx)
  end.
4

2 回答 2

5

在 Coq >= 8.5 中，你可以使用一个巧妙（或讨厌）的小技巧将策略执行插入到 constr 构造中：将其包装在match goal.

Ltac reify_wrt 值 ls :=
  匹配 ls
  | nil => constr:(@nil nat)
  | ?a :: ?ls' => 让 i := 在其中查找一个值
                 让 idx := reify_wrt values ls' in
                 constr:(i :: idx)
  | ?e :: ?ls' => let check := match goal with _ => is_evar e end in
                  让 i := constr:(100) 在
                  让 idx := reify_wrt values ls' in
                  constr:(i :: idx)
  结尾。

因为编程语言的奥秘让我着迷，所以我现在要告诉你的可能比你想知道的更多关于 Ltac 现在和过去的执行模型。

战术评估有两个阶段：战术表达评估和战术运行。在战术运行期间，执行排序、优化、重写等。在策略表达式评估期间，如果在策略表达式的头部位置找到以下结构，则会评估以下结构：

  • 战术调用被解决/跟随/内联/展开
  • let ... in ...将其参数的表达式评估绑定到名称，并进行替换
  • constr:(...)被评估和类型检查
  • lazymaytch ... with ... end被评估（带有回溯），并返回成功表达式评估的第一个匹配分支
  • match ... with ... end被评估（带有回溯）并且分支被急切地执行。请注意，在这张图片中，match它很奇怪，因为它迫使策略的执行提前到来。如果您曾经在 Coq < 8.5 中看到“本地定义中不允许立即匹配生成策略”，那是一条错误消息，明确禁止我在上面利用的行为。我猜这是因为这种奇怪的行为match是实现 Ltac 的原始开发人员想要隐藏的一个缺陷。因此，您在 Coq 8.4 中唯一可以注意到它的地方是，如果您坚持match内部lazymatch并使用失败级别，并注意当您通常认为它会失败时，它lazymatch会回溯到内部战术执行失败。match

在 Coq 8.5 中，战术引擎被重写以处理相关子目标。这引起了语义上的细微变化，;只有在使用多个目标之间共享的 eva 时才能观察到这些变化。在重写中，开发者将语义更改为lazymatch“match不回溯”，并取消了对“立即匹配产生策略”的限制。因此，您可以做一些奇怪的事情，例如：

let dummy := match goal with _ => rewrite H end in
constr:(true)

并具有产生副作用的策略。但是，您不能再执行以下操作：

let tac := lazymatch b with
                | true => tac1
                | false => tac2
                end in
tac long args.

因为在 Coq >= 8.5 中，lazymatch也急切地评估它的分支。

于 2017-09-12T14:19:10.457 回答
2

这是 Ltac 的一个众所周知的限制：你不能编写一个有时返回一个值，有时又返回另一个策略的策略。解决方案是以持续传递风格重写您的策略。不幸的是，我无法详细解释如何执行此操作，但 Adam Chlipala 的 CDPT 有一章关于 Ltac描述了该问题；只需在文本中寻找“继续”。

于 2017-08-30T00:17:52.473 回答