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