Rodolphe Lepigre (Apr 21 2023 at 15:51): 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?
Gaëtan Gilbert (Apr 21 2023 at 15:55):what does running ltac2 from ocaml mean if you don't have an ast?
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.
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
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.
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.
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
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: Oct 12 2024 at 13:01 UTC