From d651bc1ded8dde355a91a41e8dfdb09dbca6437c Mon Sep 17 00:00:00 2001 From: ppotapov-aws Date: Tue, 20 Jan 2026 13:26:19 -0500 Subject: [PATCH] Revert "[NKI-352] Make sure BIR AP lowers fully in lower AP pass" This reverts commit b3480603544c02eb72e4754deb27295b5e0b3094. --- KLR/Core/LowerAP.lean | 11 ++--------- 1 file changed, 2 insertions(+), 9 deletions(-) diff --git a/KLR/Core/LowerAP.lean b/KLR/Core/LowerAP.lean index 52365ee2..c08d81f5 100644 --- a/KLR/Core/LowerAP.lean +++ b/KLR/Core/LowerAP.lean @@ -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