coq:将使用cps样式的ltac策略移植到ml策略(ocaml插件)

我正在尝试将coq策略(目前用ltac编写)移植到ocaml,以便能够更容易地扩展该策略(并避免在ltac中模拟一些在ocaml中非常标准的数据结构所需的黑客攻击)。

我目前面临以下问题:

1. 我们可以定义一个以ltac表达式作为参数的ocaml策略吗? k (打算作为延续)?
2. 我们如何应用这样的ltac表达式 K 一个给定的解释 v ?
3. 我们如何调用给定的ltac策略 tac 从插件?
4. 我们可以从插件代码中将ltac闭包传递给这样的策略吗?(为了实现ltac习惯用法 tac ltac:(fun r => ...) 在OCAML中)

我做了一个很好的COQ来源搜索 TACTIC EXTEND 但没有找到那种方法的例子…

作为一个最小的例子,下面是一个玩具ltac战术 running_example 我想移植到ocaml中,依靠现有的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

任何意见或建议都是非常受欢迎的。