Enrico Tassi (Jun 22 2021 at 15:14): Enrico Tassi (Jun 22 2021 at 15:14):@Pierre-Marie Pédrot I think you designed the Pcoq.Rule API having in mind coqpp, which knows statically the rules and can compile them down to instances of a GADT. I tried to write a piece of code which (at run time) takes a list of strings and generates a grammar rule/action that parses X.Y.Z.f given ["X"; "Y";"Z";"f"]. I had to resort to Obj.magic.
https://github.com/LPCIC/coq-elpi/pull/257/files#diff-d405c80864017f27456cdc9c73a7e65eba7c531c886b58329ac763ac883eb4c0R868
would it be possible to do better? For my use case a next function which does not gather the argument, but that is a little ad hoc. Alternatively a next which does not curry the argument could also work (from a->b to a*c->b)
Pierre-Marie Pédrot (Jun 22 2021 at 16:19):Look at what we do in TACTIC EXTEND and friends. By no means you have to resort to obj.magic
Pierre-Marie Pédrot (Jun 22 2021 at 16:21):You will have to do a bit of GADT trickery but it's not harder than writing dependently typed programs in Coq so...
Pierre-Marie Pédrot (Jun 22 2021 at 16:24):(more precisely, Tacentries.eval_sign is probably a good start)
Pierre-Marie Pédrot (Jun 22 2021 at 16:25):You have to define a GADT that captures your domain (so a list of string indexed with the types) + an evaluation function from list of string to an existential type wrapping this + the evaluation function
Last updated: Oct 12 2024 at 13:01 UTC