Skip to content

Factor code between records and typeclasses #15877

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
Merged
merged 2 commits into from
Jun 26, 2022
Merged

Factor code between records and typeclasses #15877

merged 2 commits into from
Jun 26, 2022

Conversation

proux01
Copy link
Contributor

@proux01 proux01 commented Mar 31, 2022 •
edited
Loading

This is a followup of #12611 factoring some code between record and typeclass declarations.

Overlay (to be merged in sync with the PR):

@proux01 proux01 requested a review from a team as a code owner March 31, 2022 10:21
proux01 added a commit to proux01/coq-elpi that referenced this pull request Mar 31, 2022
@proux01
Adapt to rocq-prover/rocq#15877
64cd326
@ejgallego ejgallego self-assigned this Mar 31, 2022
@proux01 proux01 force-pushed the cleanup_class_record branch from a55314a to 7cf276b Compare April 1, 2022 08:48
@proux01 proux01 mentioned this pull request Apr 1, 2022
Merged
ejgallego
ejgallego reviewed Apr 1, 2022
View reviewed changes
@ejgallego
Copy link
Member

Sorry @proux01 , I'm having trouble following why this refactoring is an improvement. Could you summarize the idea a bit?

@proux01
Copy link
Contributor Author

proux01 commented Apr 1, 2022

@ejgallego the goal is to make more apparent what's common (and what differs) between record and class declarations. In particular the call to declare_structure that is common to both codes but was deeply burried in the class declaration functions.

@proux01
Copy link
Contributor Author

proux01 commented Apr 1, 2022

There was even a comment in the previous code:

(* declaring structures, common data to refactor *)

@ejgallego
Copy link
Member

Thanks, I'll have a look again hopefully soon.

@ejgallego ejgallego mentioned this pull request Apr 7, 2022
Merged
1 task
@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 Apr 27, 2022
@ejgallego
Copy link
Member

Hi @proux01 sorry for the delay, can you rebase?

@Alizter Alizter self-requested a review May 26, 2022 23:19
@coqbot-app
Copy link
Contributor

coqbot-app bot commented May 27, 2022

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 May 27, 2022
Alizter
Alizter reviewed May 27, 2022
View reviewed changes
proux01 added a commit to proux01/coq-elpi that referenced this pull request May 28, 2022
@proux01
Adapt to rocq-prover/rocq#15877
13e3e75
@proux01 proux01 force-pushed the cleanup_class_record branch from 7cf276b to 23167e3 Compare May 28, 2022 16:41
@coqbot-app coqbot-app bot removed needs: rebase Should be rebased on the latest master to solve conflicts or have a newer CI run. stale This PR will be closed unless it is rebased. labels May 28, 2022
@proux01 proux01 added the kind: cleanup Code removal, deprecation, refactorings, etc. label May 28, 2022
@Alizter Alizter added this to the 8.17+rc1 milestone May 28, 2022
@proux01
Copy link
Contributor Author

proux01 commented May 29, 2022

Hi @proux01 sorry for the delay, can you rebase?

@ejgallego done

ejgallego
ejgallego reviewed Jun 21, 2022
View reviewed changes
ejgallego
ejgallego reviewed Jun 21, 2022
View reviewed changes
ejgallego
ejgallego reviewed Jun 21, 2022
View reviewed changes
ejgallego
ejgallego reviewed Jun 21, 2022
View reviewed changes
ejgallego
ejgallego reviewed Jun 21, 2022
View reviewed changes
ejgallego
ejgallego reviewed Jun 21, 2022
View reviewed changes
vernac/record.ml
| Some _ -> implicits_of_context params @ impls in
let data = List.map (fun ({ DataR.implfs; _ } as d) -> { d with DataR.implfs = List.map adjust_impls implfs }) data in
(* let map (min_univ, arity, fieldimpls, fields) { Ast.name; is_coercion; cfs; idbuild; _ } = *)
let map rdata { Ast.name; is_coercion; cfs; idbuild; default_inhabitant_id; _ } =
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Let maybe lambda-lift this to its own function?

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Well it's used in a List.map2 so I'd find it a bit strange to have a separate function requiring two list of the same length.

ejgallego
ejgallego reviewed Jun 21, 2022
View reviewed changes
ejgallego
ejgallego approved these changes Jun 21, 2022
View reviewed changes
Copy link
Member

@ejgallego ejgallego left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Seem like an improvement to me, but the code is still in quite terrible shape. I wonder if instead of making more code common, we could separate the paths more, but have a more granular component view and have the separate paths share code relative to these common components.

I have left a few comments if you wanna do another pass.

@ejgallego ejgallego added part: typeclasses The typeclass mechanism. kind: internal API, ML documentation... part: records Record types, Structures, etc. needs: rebase Should be rebased on the latest master to solve conflicts or have a newer CI run. labels Jun 21, 2022
@github-actions github-actions bot removed the needs: rebase Should be rebased on the latest master to solve conflicts or have a newer CI run. label Jun 22, 2022
@proux01 proux01 force-pushed the cleanup_class_record branch 2 times, most recently from e0b8394 to 19227b4 Compare June 24, 2022 14:46
@proux01
Copy link
Contributor Author

proux01 commented Jun 24, 2022

Thanks @ejgallego for the careful review. Your comments should now be taken into account.
I agree it's still far from perfect. Note that situation should improve a bit when the whole #15802, #16224, #16230 thing will be sorted out in a few releases.

@ejgallego
Copy link
Member

Great! I will merge as soon as the CI pass.

@ejgallego
Copy link
Member

@coqbot: merge now

@coqbot-app coqbot-app bot merged commit 14014b8 into rocq-prover:master Jun 26, 2022
@coqbot-app
Copy link
Contributor

coqbot-app bot commented Jun 26, 2022

@ejgallego: Please take care of the following overlays:

  • 15877-proux01-cleanup_class_record.sh

@proux01 proux01 deleted the cleanup_class_record branch June 27, 2022 06:08
gares added a commit to LPCIC/coq-elpi that referenced this pull request Jun 27, 2022
@gares
Merge pull request #357 from proux01/coq_15877
8047989 
Adapt to rocq-prover/rocq#15877
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@ejgallego ejgallego ejgallego approved these changes

@Alizter Alizter Alizter approved these changes

Assignees

@ejgallego ejgallego

Labels
kind: cleanup Code removal, deprecation, refactorings, etc. kind: internal API, ML documentation... part: records Record types, Structures, etc. part: typeclasses The typeclass mechanism.
Projects
None yet
Milestone
8.17+rc1
Development

Successfully merging this pull request may close these issues.
3 participants
@proux01 @ejgallego @Alizter