agda / agda

Agda is a dependently typed programming language / interactive theorem prover.
https://wiki.portal.chalmers.se/agda/pmwiki.php
Other
2.4k stars 339 forks source link

Fix #7193: persistently remember what is a projection #7252

Closed andreasabel closed 1 month ago

andreasabel commented 1 month ago

Introduces a new FunctionFlag FunProj that remembers whether this function is or came from a projection.
This flag is more stable than the funProjection data which relies on arity. This helps ruling out accessing irrelevant fields in irrelevant definitions without activating --irrelevant-projections.

Fixes #7193. (Hopefully, feels almost too good to be true.)

andreasabel commented 1 month ago

@dolio: Please review, if you are available.

dolio commented 1 month ago

It seems good to me. I think this is addressing the root cause, which was that Agda was losing track of which things are projections. I wasn't the one who originally came up with either trick, so it's possible that there are others I don't know about. But it fixes the ones I do.

I noticed that when you do the let open TSquash (emb x) in extract example, extract is still colored like a normal function (when irrelevant projections are on, or the projections aren't irrelevant). Is it possible to use this new information to color it pink like they are within the record, or when you open an unapplied record module? Seems like that'd be nice.

andreasabel commented 1 month ago

Thanks @dolio!

I noticed that when you do the let open TSquash (emb x) in extract example, extract is still colored like a normal function (when irrelevant projections are on, or the projections aren't irrelevant). Is it possible to use this new information to color it pink like they are within the record, or when you open an unapplied record module?

@nad requested the opposite, if I am not mistaken:

But maybe we can fix the following problem now: #3156. (No, we can only make things more pink, not less.)