Skip to content

Revert "[NKI-352] Make sure BIR AP lowers fully in lower AP pass" #575

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

Merged
ppotapov-aws merged 1 commit into from
Jan 20, 2026
Merged

Revert "[NKI-352] Make sure BIR AP lowers fully in lower AP pass" #575

Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
11 changes: 2 additions & 9 deletions KLR/Core/LowerAP.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -34,17 +34,10 @@ abbrev LowerAP := StateT LowerAPState KLR.Err
/-- Function to convert an Access to an AccessPattern.
Note: This lowering does not work in all cases, for example, if the Access in an AccessBasic whose
Par dimension takes steps that are not equal to 1. Returns a None in this case. -/
partial def Access.lowerAccessPattern (a : Access) : LowerAP BirAccessPattern := do
def Access.lowerAccessPattern (a : Access) : LowerAP BirAccessPattern := do
-- Don't violate invariants of proved code
if let .birPattern b := a then
-- Lower vectorOffset if it exists and isn't already lowered
let vectorOffset <- b.vectorOffset.mapM fun vo =>
match vo with
| .birPattern _ => pure vo
| _ => do
let lowered <- vo.lowerAccessPattern
pure (.birPattern lowered)
return { b with vectorOffset }
return b

-- The layout of a tensor in memory
-- Note that because accesses are values, we have are forced to assume that all tensors are
Expand Down
Loading