Stream: Coq devs & plugin devs

Topic: Generating "projections" for internal purpose

Hugo Herbelin (Aug 19 2021 at 15:33):

For the purpose of inverting tuples in unification, I would need a way to automatically build projections associated to a singleton inductive type (e.g. out of prod or sigT). Such code already exists in record.ml but associated to named constants (or to primitive projections). What would be the best way to do it:

• to bind generation of projections on the scheme mechanism and to automatically produce an internal_prod_proj1 constant (equivalent to fst or proj2_sig) the first time some internal code needs it (as for dependent rewrite) and to later referring to it anytime it is needed again?
• to generate a standalone unnamed projection every time we need it (e.g. the way injection when it needs to invert a constructor)?

Any advice?

Pierre-Marie Pédrot (Aug 19 2021 at 15:35):

Don't use schemes. They're already broken enough.

Hugo Herbelin (Aug 20 2021 at 14:58):

Pierre-Marie Pédrot said:

Don't use schemes. They're already broken enough.

Broken?

Your recommendation is then to expand the code at each use?

Pierre-Marie Pédrot (Aug 20 2021 at 16:25):

Yes.

Gaëtan Gilbert (Aug 20 2021 at 16:27):

you could invert only those types which have registered projections

Hugo Herbelin (Aug 20 2021 at 16:48):

The basic types to invert are prod and sigT. So, we would need to first move them to Record (even if, in a first step, for compatibility reasons, not to primitive records).

But the principle of extracting subterms from patterns can be extended to non-record types. For instance, the x in S x can be extracted with a pred. So, eventually, we need canonical ways to invert the argument of any constructor (like in injection).

Anyway, for my current purpose (unification), expanding is ok.

Last updated: Apr 16 2024 at 10:01 UTC