Stream: Ltac2

Topic: Calling Ltac2 from OCaml


view this post on Zulip Rodolphe Lepigre (Apr 21 2023 at 15:51):

Is there any better way to run Ltac2 from OCaml than to hand-build some AST and call Ltac2_plugin.Tac2interp.interp?

view this post on Zulip Gaëtan Gilbert (Apr 21 2023 at 15:55):

what does running ltac2 from ocaml mean if you don't have an ast?

view this post on Zulip Rodolphe Lepigre (Apr 21 2023 at 16:08):

I don't have the AST, but I think my only way to call a specific Ltac2 function is to somehow build an AST for the call, and use interp.

view this post on Zulip Gaëtan Gilbert (Apr 21 2023 at 16:13):

you mean something like Tac2interp.(interp_value empty_environment (GTacRef some_name))? that should work fine

view this post on Zulip Rodolphe Lepigre (Apr 21 2023 at 16:20):

Yeah, that's exactly what I plan to do, except that the expression to evaluate is gonna be a lot more complicated since it requires many arguments to be built (including record values, ...). So that's gonna be a pain, hence my question to see if I missed any other alternative.

view this post on Zulip Rodolphe Lepigre (Apr 21 2023 at 16:22):

I guess I could inject my value into some CTacExt node, and then have some extra back and forth between OCaml and Ltac2.

view this post on Zulip Gaëtan Gilbert (Apr 21 2023 at 16:22):

you can apply it with Tac2ffi.(apply (to_closure Tac2interp.(interp_value ...))) [arg1;arg2;...]
building the args in type valexpr instead of glb_tacexpr

view this post on Zulip Rodolphe Lepigre (Apr 21 2023 at 16:26):

Oh that's perfect actually, I missed the fact that I could do that. Thanks!


Last updated: May 20 2024 at 22:01 UTC