Michael Soegtrop (Mar 18 2021 at 17:13): Michael Soegtrop (Mar 18 2021 at 17:13):I wonder how I could call ring_simplify with an Ltac2 constr list. Is there a better way than having a separate ring_simplify wrapper for 1..10 arguments?
Pierre-Marie Pédrot (Mar 18 2021 at 20:40):You can probably hack your way around with a wrapper Ltac1 function + the Ltac2/Ltac1 FFI
Pierre-Marie Pédrot (Mar 18 2021 at 20:42):ring is not a reasonable example of what you can / should do with Ltac1
Michael Soegtrop (Mar 19 2021 at 09:35):ring is not a reasonable example of what you can / should do with Ltac1
Aren't ring and ring_simplify OCaml tactics meanwhile?
The issue with ring_simplify is that it takes an arbitrary number of terms as argument. These are simplified together with the same variable indexing. If one ring_simplifies ring equivalent terms separately, one might (and does) get different results. Only when one simplifies all equivalent terms together, there is a guarantee that they are equal after simplification.
I don't see a way to handle this with the FFI other than singling out the case for n=1,..,N for some small N. But this is not that bad - in case the Ltac2 list is larger than N it throws an error and it is trivial to extend and I don't expect N to get ever larger than 10. So I can live with this, it is just not very elegant.
Pierre-Marie Pédrot (Mar 19 2021 at 10:50):No, you can use Ltac1 module to build the runtime equivalent of Ltac1 constr list out of Ltac2 lists. Then you pass this to an Ltac1 function that is just a wrapper around the list notation, and it should hopefully work.
Pierre-Marie Pédrot (Mar 19 2021 at 10:51):(lists and constrs are the only exported Ltac1 type cast FFI currently)
Michael Soegtrop (Mar 19 2021 at 13:43):Thanks, I found the tactic notation for ring_simplify now (I thought it was immediately an OCaml tactic). It should indeed be doable.
Last updated: Oct 08 2024 at 14:01 UTC