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

chore: canonicalize constants #358

Merged
merged 19 commits into from
May 30, 2024
Merged

chore: canonicalize constants #358

merged 19 commits into from
May 30, 2024

Conversation

tobiasgrosser
Copy link
Collaborator

No description provided.

@tobiasgrosser tobiasgrosser force-pushed the canonicalize_constants branch from a0c5ab1 to c9f11f5 Compare May 29, 2024 18:16
@tobiasgrosser
Copy link
Collaborator Author

I pulled this PR out of #356, as this seems to be a self-contained change that can be verified rather mechanically. In #356, I made some of these statements new simp-lemma on BitVec which caused unrelated changes in BitVec.

@tobiasgrosser tobiasgrosser requested review from alexkeizer and bollu May 29, 2024 18:18
@tobiasgrosser
chore: canonicalize constants in alive output
00fcd55 
This will make subsequent patches for enabling reductions smaller,
as these canonicalization for some reason is not needed in that
case.
@tobiasgrosser tobiasgrosser force-pushed the canonicalize_constants branch from c9f11f5 to 00fcd55 Compare May 29, 2024 18:21
@github-actions GitHub Actions
Copy link

Alive Statistics: 30 / 93 (63 failed)

@tobiasgrosser tobiasgrosser marked this pull request as draft May 29, 2024 18:39
@tobiasgrosser
Copy link
Collaborator Author

Alive Statistics: 30 / 93 (63 failed)
Nice. These still need to be fixed.

@github-actions GitHub Actions
Copy link

Alive Statistics: 54 / 93 (39 failed)

@github-actions GitHub Actions
Copy link

Alive Statistics: 54 / 93 (39 failed)

@tobiasgrosser tobiasgrosser marked this pull request as ready for review May 30, 2024 04:25
@github-actions GitHub Actions
Copy link

Alive Statistics: 54 / 93 (39 failed)

@tobiasgrosser
Copy link
Collaborator Author

Nice. This is now ready to review (and merge). It should reduce a lot of the noise we saw in #356.

@github-actions GitHub Actions
Copy link

Alive Statistics: 54 / 93 (39 failed)

@github-actions GitHub Actions
Copy link

Alive Statistics: 54 / 93 (39 failed)

bollu
bollu requested changes May 30, 2024
View reviewed changes
Copy link
Collaborator

@bollu bollu left a comment

Choose a reason for hiding this comment

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

I think the theorem statements need to be in simp normal form before we can merge this. If they are not being normalized correctly, then we ought to write the correct simps to go between Int/Nat/OfNat.ofNat

@github-actions GitHub Actions
Copy link

Alive Statistics: 54 / 93 (39 failed)

@tobiasgrosser tobiasgrosser enabled auto-merge May 30, 2024 17:50
@github-actions GitHub Actions
Copy link

Alive Statistics: 54 / 93 (39 failed)

@bollu
Copy link
Collaborator

bollu commented May 30, 2024

Lgtm

@tobiasgrosser tobiasgrosser added this pull request to the merge queue May 30, 2024
Merged via the queue into main with commit 2818234 May 30, 2024
2 checks passed
alexkeizer
alexkeizer reviewed May 30, 2024
View reviewed changes
SSA/Projects/InstCombine/ForLean.lean
Comment on lines +126 to 128
lemma ofInt_ofNat' : BitVec.ofInt w (OfNat.ofNat (α := ℤ) x ) = x#w := rfl

-- @[simp]
Copy link
Collaborator

@alexkeizer alexkeizer May 30, 2024 •
edited
Loading

Choose a reason for hiding this comment

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

@tobiasgrosser it seems you didn't remove the primed lemma, but this one should not be needed after the no_index fix, right?

Copy link
Collaborator Author

Choose a reason for hiding this comment

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

Right. Sorry for this and thank you for the post-commit review: https://github.com/opencompl/ssa/pull/new/clean_unneeded_stmt.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@alexkeizer alexkeizer alexkeizer left review comments

@bollu bollu bollu approved these changes

Assignees
No one assigned
Labels
None yet
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.
3 participants
@tobiasgrosser @bollu @alexkeizer