I'm trying to port a Coq tactic (currently written in Ltac) to OCaml, in order to be able to extend that tactic more easily (and avoid the hacks I needed to emulate in Ltac some data structures that are otherwise quite standard in OCaml).
I am currently facing with the following problems:
- Can we define an OCaml tactic taking as argument a Ltac expression
k
(intended to be a continuation)? - How can we apply one such Ltac expression
k
to a given constrv
? - How can we call a given Ltac tactic
tac
from a plugin? - Can we pass a Ltac closure to one such tactic from the plugin code? (in order to implement the Ltac idiom
tac ltac:(fun r => ...)
in OCaml)
I did a grep on the Coq sources searching TACTIC EXTEND
but did not found some example of that kind of approach...
As a minimal example, below is a toy Ltac tactic running_example
that I'd like to port in OCaml, relying on the existing Ltac tactic 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) *)
So far I've obtained the code below (which only addresses point 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
Any pointers or suggestions are very welcome.