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

Add qnorm argument to many kernel functions #18884

Draft
wants to merge 1 commit into
base: master
Choose a base branch
from
Draft

Add qnorm argument to many kernel functions #18884

wants to merge 1 commit into from

Conversation

yannl35133
Copy link
Contributor

@yannl35133 yannl35133 commented Apr 2, 2024 •
edited

Fixes / closes #18865

I expect this to need extensive reviewing and benchmarking

  • Added / updated test-suite.

@coqbot-app coqbot-app bot added the needs: full CI The latest GitLab pipeline that ran was a light CI. Say "@coqbot run full ci" to get a full CI. label Apr 2, 2024
@yannl35133 yannl35133 added needs: merge of dependency This PR depends on another PR being merged first. needs: benchmarking Performance testing is required. labels Apr 2, 2024
@SkySkimmer SkySkimmer changed the title Fix-cclosure-conv Add qnorm argument to many kernel functions Apr 4, 2024
@yannl35133 yannl35133 removed the needs: merge of dependency This PR depends on another PR being merged first. label Apr 5, 2024
SkySkimmer
SkySkimmer reviewed May 2, 2024
View reviewed changes
kernel/uGraph.mli
val check_leq_sort : t -> Sorts.t -> Sorts.t -> bool
val check_qconstraints : ?qnorm:(Sorts.QVar.t -> Sorts.Quality.t) -> Sorts.QConstraints.t -> bool
val check_eq_sort : ?qnorm:(Sorts.QVar.t -> Sorts.Quality.t) -> t -> Sorts.t -> Sorts.t -> bool
val check_leq_sort : ?qnorm:(Sorts.QVar.t -> Sorts.Quality.t) -> t -> Sorts.t -> Sorts.t -> bool
Copy link
Contributor

Choose a reason for hiding this comment

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

Not sure about carrying the API changes this far down, maybe better to call qnorm in conversion.ml

@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 May 15, 2024
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@SkySkimmer SkySkimmer SkySkimmer left review comments

At least 1 approving review is required to merge this pull request.

Assignees
No one assigned
Labels
needs: benchmarking Performance testing is required. needs: full CI The latest GitLab pipeline that ran was a light CI. Say "@coqbot run full ci" to get a full CI. needs: rebase Should be rebased on the latest master to solve conflicts or have a newer CI run.
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.

Conversion incompleteness with Definitional UIP
2 participants
@yannl35133 @SkySkimmer