Stream: Coq devs & plugin devs

Topic: Generating "projections" for internal purpose


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

Any advice?

view this post on Zulip Pierre-Marie Pédrot (Aug 19 2021 at 15:35):

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

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

view this post on Zulip Pierre-Marie Pédrot (Aug 20 2021 at 16:25):

Yes.

view this post on Zulip Gaëtan Gilbert (Aug 20 2021 at 16:27):

you could invert only those types which have registered projections

view this post on Zulip 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: Oct 16 2021 at 02:03 UTC