Stream: Coq devs & plugin devs

Topic: Pcoq.Rule API an dynamic code


view this post on Zulip 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)

view this post on Zulip 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

view this post on Zulip 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...

view this post on Zulip Pierre-Marie Pédrot (Jun 22 2021 at 16:24):

(more precisely, Tacentries.eval_sign is probably a good start)

view this post on Zulip 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 16 2021 at 09:07 UTC