Janno (Jul 19 2022 at 07:37): Janno (Jul 19 2022 at 07:37):Is there a reason Ltac2 lists are not directly represented as OCaml lists? AFAICT the type is a built-in of the language. Maybe it merits its own valexpr constructor? This could help avoid intermediate lists produced at the FFI boundary.
Pierre-Marie Pédrot (Jul 19 2022 at 08:45):In theory we could, but I think it's more uniform to treat it as a simple ADT. Otherwise it would incur some ad-hoc code to compile it on the fly, as the constructor representation is used by the type-checker.
Pierre-Marie Pédrot (Jul 19 2022 at 08:46):Do you have a performance issue due to the O(n) conversion?
Janno (Jul 19 2022 at 11:00):I see. I hadn't thought about the typechecker. Luckily this is not a performance issue in practice, at least not in a way that I can measure right now.
Janno (Jul 19 2022 at 11:01):Our lists that are passed through the FFI are still quite small.. usually less than a hundred elements.
Rodolphe Lepigre (Jul 19 2022 at 17:15):If we really need to avoid paying that cost we could just switch to using the OCaml list module via the FFI, but the downside is that we would lose the ability to do pattern matching on the Ltac2 side.
Pierre-Marie Pédrot (Jul 19 2022 at 17:20):Note that if one day we compile directly Ltac2 to OCaml we wouldn't have to pay this price then.
Rodolphe Lepigre (Jul 19 2022 at 19:28):How would you implement that compilation to OCaml? Just calling the compiler and dynamically linking the result?
Alternatively, could you not manipulate (a subset of) OCaml values directly in Ltac2? (I mean, essentially defining type valexpr = Obj.t.)
Pierre-Marie Pédrot (Jul 19 2022 at 20:57):Indeed, just define valexpr as Obj.t, the Ltac2 runtime has been designed to be compatible with this viewpoint (barring soundness issues due to Coq functors)
Last updated: Dec 07 2023 at 08:01 UTC