-
Notifications
You must be signed in to change notification settings - Fork 640
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
Introducing a proper interpretation path for t.(f) distinct from (f t) when f is a primitive projection #14640
Conversation
6346178
to
ec3e89d
Compare
ec3e89d
to
98cf1a8
Compare
98cf1a8
to
76a8276
Compare
The job library:ci-fiat_crypto_legacy has failed in allow failure mode |
76a8276
to
591dcbd
Compare
591dcbd
to
6f14904
Compare
6f14904
to
3a9fde6
Compare
…yping. This was formally in constrextern.ml. We also activate the x.(f) notation for non-primitive projections by default.
… class. More generally, we identify projections under their Const and Proj forms in coercion classes.
…ctions. To be continued when the goal is clearer (remove unfold, check reduction, add a table to make proj opaque, ... ?).
…not be Proj. They must remain Const since the main argument is missing.
3a9fde6
to
505bad7
Compare
This effectively removes the projection boolean, so the next step towards merging is to find a way to reduce the breakage and/or provide overlays |
Current status of bugs/closed failures:
|
The "needs: rebase" label was set more than 30 days ago. If the PR is not rebased in 30 days, it will be automatically closed. |
This PR was not rebased after 30 days despite the warning, it is now closed. |
Kind: "feature"
Depends on #14606 (merged), #14706 (merged) and #14598 (merged).
PR #14598 introduced a specific node for projections in
glob_term
andnotation_term
but #14598 preserved an equivalence between theGProj
representation and theGApp
-based representation.This PR makes the interpretation path for
t.(f)
, and more generallyt.(f params)
, clearly distinct from thef params t
path:f params t
whenf
is a primitive projection is now bound to a kernelApp
(not optimized) rather than to a kernelProj
(dropping the parameters) as beforeGProj
, thenCProj
and thus always printed ast.(f _ ⣀ _)
while before they were directed toGApp
(losing the proj status) and re-directed toCProj
only when the flagPrinting Projections
was setf params t
and tot.(f params)
are no more identified whenf
is primitiveThe code for
pretype_proj
is temporary. Afaiu, @ppedrot has somewhere a code ready for projections.A next step is to decide whether the
f params t
path should eventually be fully removed, or kept only for partially applied projections, or kept as an non-optimized alternative (see coq/ceps#57).