1

我正在尝试将 Coq 策略（目前用 Ltac 编写）移植到 OCaml，以便能够更轻松地扩展该策略（并避免在 Ltac 中模拟一些在 OCaml 中非常标准的数据结构所需的黑客攻击）。

我目前面临以下问题：

  1. 我们可以定义一个 OCaml 策略，将 Ltac 表达式k（旨在作为延续）作为参数吗？
  2. 我们如何将一个这样的 Ltac 表达式k应用于给定的constr v？
  3. 我们如何tac从插件中调用给定的 Ltac 策略？
  4. 我们可以从插件代码中将 Ltac 闭包传递给这样一种策略吗？（为了tac ltac:(fun r => ...)在 OCaml 中实现 Ltac 成语）

我对 Coq 资源进行了 grep 搜索TACTIC EXTEND，但没有找到这种方法的一些例子......

running_example作为一个最小的例子，下面是我想在 OCaml 中移植的一个玩具 Ltac 策略，它依赖于现有的 Ltac 策略tac：

Require Import Reals.
Inductive type := Cstrict (ub : R) | Clarge (ub : R).

Ltac tac g k :=
  let aux c lb := k (c lb) in
  match g with
  | Rle ?x ?y => aux Clarge y
  | Rge ?x ?y => aux Clarge x
  | Rlt ?x ?y => aux Cstrict y
  | Rgt ?x ?y => aux Cstrict x
  end.

Ltac running_example expr (*point 1*) k :=
  let conc := constr:((R0 <= expr)%R) in
  tac (*point 3*) conc (*point 4*) ltac:(fun r => let v :=
    match r with
    | Clarge ?x => constr:((true, x))
    | Cstrict ?x => constr:((false, x))
    end in (*point 2*)
    k v).

Goal True.
running_example 12%R ltac:(fun r => idtac r).
(* Should display (true, 12%R) *)

到目前为止，我已经获得了以下代码（仅针对点 1）：

open Ltac_plugin
open Stdarg
open Tacarg

TACTIC EXTEND running_example
| [ "running_example" constr(expr) tactic0(k) ] ->
  [ Proofview.Goal.nf_enter begin fun gl ->
    (Tacinterp.tactic_of_value ist k) end ]
END

非常欢迎任何指示或建议。

4

0 回答 0