Skip to content
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.

Sign up for GitHub

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

Jump to bottom

Introducing a proper interpretation path for t.(f) distinct from (f t) when f is a primitive projection #14640

Closed
wants to merge 7 commits into from
Closed

Introducing a proper interpretation path for t.(f) distinct from (f t) when f is a primitive projection #14640

wants to merge 7 commits into from

Conversation

herbelin
Copy link
Member

@herbelin herbelin commented Jul 11, 2021 •
edited

Kind: "feature"

Depends on #14606 (merged), #14706 (merged) and #14598 (merged).

PR #14598 introduced a specific node for projections in glob_term and notation_term but #14598 preserved an equivalence between the GProj representation and the GApp-based representation.

This PR makes the interpretation path for t.(f), and more generally t.(f params), clearly distinct from the f params t path:

  • a syntactic expression f params t when f is a primitive projection is now bound to a kernel App (not optimized) rather than to a kernel Proj (dropping the parameters) as before
  • conversely, kernel (primitive) proj are directed to GProj, then CProj and thus always printed as t.(f _ ⣀ _) while before they were directed to GApp (losing the proj status) and re-directed to CProj only when the flag Printing Projections was set
  • notations referring to f params t and to t.(f params) are no more identified when f is primitive

The 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).

@herbelin herbelin added kind: feature New user-facing feature request or implementation. part: primitive records The primitive record and primitive projection mechanism. labels Jul 11, 2021
@herbelin herbelin added this to the 8.15+rc1 milestone Jul 11, 2021
@herbelin herbelin added the needs: merge of dependency This PR depends on another PR being merged first. label Jul 11, 2021
@herbelin herbelin force-pushed the master+print-kernel-proj-as-proj branch from 6346178 to ec3e89d Compare July 15, 2021 20:27
@github-actions github-actions bot added the needs: rebase Should be rebased on the latest master to solve conflicts or have a newer CI run. label Jul 19, 2021
@herbelin herbelin force-pushed the master+print-kernel-proj-as-proj branch from ec3e89d to 98cf1a8 Compare July 19, 2021 19:45
@coqbot-app coqbot-app bot removed the needs: rebase Should be rebased on the latest master to solve conflicts or have a newer CI run. label Jul 19, 2021
@herbelin herbelin force-pushed the master+print-kernel-proj-as-proj branch from 98cf1a8 to 76a8276 Compare July 19, 2021 20:19
@coqbot-app
Copy link
Contributor

coqbot-app bot commented Jul 19, 2021

The job library:ci-fiat_crypto_legacy has failed in allow failure mode
ping @JasonGross

@github-actions github-actions bot added the needs: rebase Should be rebased on the latest master to solve conflicts or have a newer CI run. label Jul 26, 2021
@herbelin herbelin force-pushed the master+print-kernel-proj-as-proj branch from 76a8276 to 591dcbd Compare July 26, 2021 18:38
@coqbot-app coqbot-app bot removed the needs: rebase Should be rebased on the latest master to solve conflicts or have a newer CI run. label Jul 26, 2021
@herbelin herbelin force-pushed the master+print-kernel-proj-as-proj branch from 591dcbd to 6f14904 Compare July 26, 2021 19:55
@github-actions github-actions bot added the needs: rebase Should be rebased on the latest master to solve conflicts or have a newer CI run. label Jul 31, 2021
@herbelin herbelin force-pushed the master+print-kernel-proj-as-proj branch from 6f14904 to 3a9fde6 Compare August 1, 2021 16:22
@coqbot-app coqbot-app bot removed the needs: rebase Should be rebased on the latest master to solve conflicts or have a newer CI run. label Aug 1, 2021
@herbelin herbelin mentioned this pull request Aug 2, 2021
Merged
3 tasks
@github-actions github-actions bot added the needs: rebase Should be rebased on the latest master to solve conflicts or have a newer CI run. label Aug 5, 2021
@herbelin
Mini-simplification
1f88e6d
@herbelin
Export kernel primitive projections to GProj.
2b62a2f
@herbelin
Moving translation non-primitive projections to x.(f) notation in det…
85cc661 
…yping.

This was formally in constrextern.ml.

We also activate the x.(f) notation for non-primitive projections by default.
@herbelin
Handle coercions represented using GProj.
db13fb4
@herbelin
Let find_class_type and class_of_global agree on finding a projection…
ebcb06f 
… class.

More generally, we identify projections under their Const and Proj
forms in coercion classes.
@herbelin
Experiment to cancel the difference between folded and unfolded proje…
a19a37c 
…ctions.

To be continued when the goal is clearer (remove unfold, check
reduction, add a table to make proj opaque, ... ?).
@herbelin
Fixes coq#11366: not enough-applied projections used as coercions can…
505bad7 
…not be Proj.

They must remain Const since the main argument is missing.
@herbelin herbelin force-pushed the master+print-kernel-proj-as-proj branch from 3a9fde6 to 505bad7 Compare August 6, 2021 09:59
@coqbot-app coqbot-app bot removed the needs: rebase Should be rebased on the latest master to solve conflicts or have a newer CI run. label Aug 6, 2021
@herbelin herbelin removed the needs: merge of dependency This PR depends on another PR being merged first. label Aug 18, 2021
@Zimmi48 Zimmi48 mentioned this pull request Sep 6, 2021
Open
@SkySkimmer
Copy link
Contributor

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

@herbelin
Copy link
Member Author

Current status of bugs/closed failures:

  • universe anomaly:
    • bugs/closed/bug_14221.v
  • a notation binds to Const vs to Proj:
    • bugs/closed/bug_3648.v
  • how unfold should behave on a non-applied projection in a primitive record type?
    • bugs/closed/bug_3656.v
    • bugs/closed/bug_3662.v
  • unification ?P x = x.(f) failing
    • bugs/closed/bug_3666.v
    • bugs/closed/bug_3625.v
  • unification ?P x = x.(f) failing + coercion missing
    • bugs/closed/bug_3453.v
  • unification ?x.(f) = t.(f) failing:
    • bugs/closed/bug_9508.v
    • bugs/closed/bug_3480.v
    • bugs/closed/bug_5215.v
    • bugs/closed/bug_5692.v
    • probably also bugs/closed/bug_4544.v
  • collision between hnf and simpl never
    • bugs/closed/bug_5245.v
  • new expected success?
    • bugs/closed/bug_3656.v (nop unfolding of a prim proj)
    • bugs/closed/bug_9512.v

@github-actions github-actions bot added the needs: rebase Should be rebased on the latest master to solve conflicts or have a newer CI run. label Oct 21, 2021
@SkySkimmer SkySkimmer removed this from the 8.15+rc1 milestone Nov 8, 2021
@coqbot-app
Copy link
Contributor

coqbot-app bot commented Nov 22, 2021

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.

@coqbot-app coqbot-app bot added the stale This PR will be closed unless it is rebased. label Nov 22, 2021
@coqbot-app
Copy link
Contributor

coqbot-app bot commented Dec 22, 2021

This PR was not rebased after 30 days despite the warning, it is now closed.

@coqbot-app coqbot-app bot closed this Dec 22, 2021
This was referenced Feb 10, 2022
Draft
Closed
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers
No reviews
Assignees
No one assigned
Labels
kind: feature New user-facing feature request or implementation. needs: rebase Should be rebased on the latest master to solve conflicts or have a newer CI run. part: primitive records The primitive record and primitive projection mechanism. stale This PR will be closed unless it is rebased.
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.

None yet
2 participants
@herbelin @SkySkimmer