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.
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.
Do you have a performance issue due to the O(n) conversion?
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.
Our lists that are passed through the FFI are still quite small.. usually less than a hundred elements.
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.
Note that if one day we compile directly Ltac2 to OCaml we wouldn't have to pay this price then.
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.)
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