Hi all, I would like to call some Ltac2 code from Ocaml. Let's say for instance I have an Ltac2 function :
Ltac2 myfunc (x : bool) (y : int list) : unit := ...
Can I call this function from an Ocaml plugin ? And can I pass standard Ocaml values (of type bool
and int list
) as arguments ?
it's possible
something like
let tac = Tac2interp.interp Tac2interp.empty_environment (GTacApp (GTacRef kn, Tac2ffi.[of_bool true; of_list of_int [1; 2; 3]])) in
Proofview.Monad.map Tac2ffi.to_unit tac
has type unit Proofview.tactic
where kn
is the name of your function, buit by doing something like https://github.com/coq/coq/blob/e564bef2404475ec83061cf7bf4b0759d58aca85/plugins/ltac2/tac2quote.ml#L43 I guess
see Tac2interp Tac2ffi etc for more info
if you're not already in tactics you can run the tactic with https://github.com/coq/coq/blob/e564bef2404475ec83061cf7bf4b0759d58aca85/engine/proofview.mli#L158
whether that is a good idea I'm not sure
Thanks ! I'm already in a tactic on the Ocaml side so no worries.
GTacApp
expects a list of glb_tacexpr
but Tac2ffi
produces values of type Tac2val.valexpr
, but I can't seem to find how to convert from valexpr
to glb_tacexpr
?
oh right
something like
let tac = Tac2val.apply_val (Tac2interp.eval_global kn) Tac2ffi.[of_bool true; etc] in
then
I can't seem to get the kernel name of the Ltac2 constant. I'm building the same kernel name as I would for a standard Coq definition, is that correct ?
Is there a way to access a list of all Ltac2 constants from Ocaml similar to Environ.Globals ?
I'm building the same kernel name as I would for a standard Coq definition, is that correct ?
I don't know what exactly you mean by that so I don't know if it's correct.
Is there a way to access a list of all Ltac2 constants from Ocaml similar to Environ.Globals ?
There's Tac2env.globals
Last updated: Oct 13 2024 at 01:02 UTC