Coq: перенести тактику Ltac с использованием стиля CPS на тактику ML (плагин OCaml)

Question

Я пытаюсь перенести тактику Coq (в настоящее время написанную на Ltac) на OCaml, чтобы иметь возможность более легко расширять эту тактику (и избежать хаков, которые мне понадобились для эмуляции в Ltac некоторых структур данных, которые в остальном вполне стандартны в OCaml).

В настоящее время я сталкиваюсь со следующими проблемами:

1. Можем ли мы определить тактику OCaml, принимая в качестве аргумента выражение Ltac k (предназначен для продолжения)?
2. Как мы можем применить одно такое выражение Ltac k для данного constr v?
3. Как мы можем назвать данную тактику Ltac tac из плагина?
4. Можем ли мы передать закрытие Ltac одной такой тактике из кода плагина? (для того, чтобы реализовать идиому Ltac tac ltac:(fun r => ...) в OCaml)

Я сделал grep на поиск источников 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

Любые указатели или предложения очень приветствуются.