@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"]. I had to resort to Obj.magic.
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)
Look at what we do in TACTIC EXTEND and friends. By no means you have to resort to obj.magic
You will have to do a bit of GADT trickery but it's not harder than writing dependently typed programs in Coq so...
(more precisely, Tacentries.eval_sign is probably a good start)
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 16 2021 at 09:07 UTC