From fae768fb3eedbb2714a700316d60fb3b4b5bafec Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Fri, 6 Feb 2026 17:00:33 +0100 Subject: [PATCH] fix: ensure `List.filterMap` is always `csimp`ed (#12348) Shake accidentally broke this from missing dependency tracking (TBD) --- src/Init/Data/List/Basic.lean | 8 +-- src/Init/Data/List/Impl.lean | 6 ++ src/Init/System/IO.lean | 1 + src/Std/Sat/CNF/RelabelFin.lean | 1 + tests/lean/csimpCore.lean | 61 +++++++++++++++++ tests/lean/csimpCore.lean.expected.out | 92 ++++++++++++++++++++++++++ 6 files changed, 162 insertions(+), 7 deletions(-) create mode 100644 tests/lean/csimpCore.lean create mode 100644 tests/lean/csimpCore.lean.expected.out diff --git a/src/Init/Data/List/Basic.lean b/src/Init/Data/List/Basic.lean index 72cbdf71bc..1fa816369c 100644 --- a/src/Init/Data/List/Basic.lean +++ b/src/Init/Data/List/Basic.lean @@ -506,7 +506,7 @@ Example: [10, 14, 14] ``` -/ -@[specialize] def filterMap (f : α → Option β) : List α → List β +noncomputable def filterMap (f : α → Option β) : List α → List β | [] => [] | a::as => match f a with @@ -737,12 +737,6 @@ Examples: @[simp, grind =] def rightpad (n : Nat) (a : α) (l : List α) : List α := l ++ replicate (n - length l) a -/-! ### reduceOption -/ - -/-- Drop `none`s from a list, and replace each remaining `some a` with `a`. -/ -@[inline] def reduceOption {α} : List (Option α) → List α := - List.filterMap id - /-! ## List membership * `L.contains a : Bool` determines, using a `[BEq α]` instance, whether `L` contains an element `· == a`. diff --git a/src/Init/Data/List/Impl.lean b/src/Init/Data/List/Impl.lean index e7d073ac1a..dccd927f55 100644 --- a/src/Init/Data/List/Impl.lean +++ b/src/Init/Data/List/Impl.lean @@ -120,6 +120,12 @@ Example: split <;> simp [*] exact (go l #[]).symm +/-! ### reduceOption -/ + +/-- Drop `none`s from a list, and replace each remaining `some a` with `a`. -/ +@[inline] def reduceOption {α} : List (Option α) → List α := + List.filterMap id + /-! ### foldr -/ /-- diff --git a/src/Init/System/IO.lean b/src/Init/System/IO.lean index deeabdd6e5..506432b08e 100644 --- a/src/Init/System/IO.lean +++ b/src/Init/System/IO.lean @@ -15,6 +15,7 @@ public import Init.Data.String.Basic import Init.Data.List.MapIdx import Init.Data.Ord.UInt import Init.Data.ToString.Macro +import Init.Data.List.Impl public section diff --git a/src/Std/Sat/CNF/RelabelFin.lean b/src/Std/Sat/CNF/RelabelFin.lean index 49823b78eb..cf8e7e9b68 100644 --- a/src/Std/Sat/CNF/RelabelFin.lean +++ b/src/Std/Sat/CNF/RelabelFin.lean @@ -11,6 +11,7 @@ public import Std.Sat.CNF.Relabel import Init.Data.List.MinMax import Init.Data.Option.Lemmas import Init.Omega +import Init.Data.List.Impl @[expose] public section diff --git a/tests/lean/csimpCore.lean b/tests/lean/csimpCore.lean new file mode 100644 index 0000000000..ff88b69d64 --- /dev/null +++ b/tests/lean/csimpCore.lean @@ -0,0 +1,61 @@ +import Std +import Lean + +open Lean Compiler LCNF + +/-! +`@[csimp]` should only be applied to `noncomputable` defs so we never compile against the wrong +version. The following list shows where this is not yet the case. +-/ + +/-- +info: (Acc.rec, Acc.recC) +(Array.instDecidableEmpEq, Array.instDecidableEmpEqImpl) +(Array.instDecidableEq, Array.instDecidableEqImpl) +(Array.instDecidableEqEmp, Array.instDecidableEqEmpImpl) +(Array.pmap, Array.pmapImpl) +(ByteArray.append, ByteArray.fastAppend) +(List.append, List.appendTR) +(List.dropLast, List.dropLastTR) +(List.erase, List.eraseTR) +(List.eraseP, List.erasePTR) +(List.filter, List.filterTR) +(List.findRev?, List.findRev?TR) +(List.flatMap, List.flatMapTR) +(List.flatten, List.flattenTR) +(List.foldr, List.foldrTR) +(List.insertIdx, List.insertIdxTR) +(List.intercalate, List.intercalateTR) +(List.intersperse, List.intersperseTR) +(List.leftpad, List.leftpadTR) +(List.length, List.lengthTR) +(List.map, List.mapTR) +(List.merge, List.MergeSort.Internal.mergeTR) +(List.mergeSort, List.MergeSort.Internal.mergeSortTR₂) +(List.modify, List.modifyTR) +(List.pmap, List.pmapImpl) +(List.range', List.range'TR) +(List.replace, List.replaceTR) +(List.replicate, List.replicateTR) +(List.set, List.setTR) +(List.take, List.takeTR) +(List.takeWhile, List.takeWhileTR) +(List.unzip, List.unzipTR) +(List.zipIdx, List.zipIdxTR) +(List.zipWith, List.zipWithTR) +(Nat.all, Nat.allTR) +(Nat.any, Nat.anyTR) +(Nat.fold, Nat.foldTR) +(Nat.rec, Nat.recCompiled) +(Nat.repeat, Nat.repeatTR) +(String.utf8EncodeChar, String.utf8EncodeCharFast) +(Thunk.fn, Thunk.fnImpl) +(Vector.pmap, Vector.pmapImpl) +(String.Slice.Pos.next, String.Slice.Pos.nextFast) +-/ +#guard_msgs in +run_elab do + let env ← getEnv + for (l, r) in CSimp.ext.getState env |>.map.toList.mergeSort (le := (·.1.lt ·.1)) do + if !isNoncomputable env l then + IO.println (l, r) diff --git a/tests/lean/csimpCore.lean.expected.out b/tests/lean/csimpCore.lean.expected.out new file mode 100644 index 0000000000..62c46a0d21 --- /dev/null +++ b/tests/lean/csimpCore.lean.expected.out @@ -0,0 +1,92 @@ +(Acc.rec, Acc.recC) +(Array.instDecidableEmpEq, Array.instDecidableEmpEqImpl) +(Array.instDecidableEq, Array.instDecidableEqImpl) +(Array.instDecidableEqEmp, Array.instDecidableEqEmpImpl) +(Array.pmap, Array.pmapImpl) +(ByteArray.append, ByteArray.fastAppend) +(List.append, List.appendTR) +(List.dropLast, List.dropLastTR) +(List.erase, List.eraseTR) +(List.eraseIdx, List.eraseIdxTR) +(List.eraseP, List.erasePTR) +(List.filter, List.filterTR) +(List.findRev?, List.findRev?TR) +(List.findSomeRev?, List.findSomeRev?TR) +(List.flatMap, List.flatMapTR) +(List.flatten, List.flattenTR) +(List.foldr, List.foldrTR) +(List.insertIdx, List.insertIdxTR) +(List.intercalate, List.intercalateTR) +(List.intersperse, List.intersperseTR) +(List.leftpad, List.leftpadTR) +(List.length, List.lengthTR) +(List.map, List.mapTR) +(List.merge, List.MergeSort.Internal.mergeTR) +(List.mergeSort, List.MergeSort.Internal.mergeSortTR₂) +(List.modify, List.modifyTR) +(List.pmap, List.pmapImpl) +(List.range', List.range'TR) +(List.replace, List.replaceTR) +(List.replicate, List.replicateTR) +(List.set, List.setTR) +(List.take, List.takeTR) +(List.takeWhile, List.takeWhileTR) +(List.unzip, List.unzipTR) +(List.zipIdx, List.zipIdxTR) +(List.zipWith, List.zipWithTR) +(Nat.all, Nat.allTR) +(Nat.any, Nat.anyTR) +(Nat.fold, Nat.foldTR) +(Nat.rec, Nat.recCompiled) +(Nat.repeat, Nat.repeatTR) +(String.utf8EncodeChar, String.utf8EncodeCharFast) +(Thunk.fn, Thunk.fnImpl) +(Vector.pmap, Vector.pmapImpl) +(String.Slice.Pos.next, String.Slice.Pos.nextFast) +csimpCore.lean:56:0-56:11: error: ❌️ Docstring on `#guard_msgs` does not match generated message: + + info: (Acc.rec, Acc.recC) + (Array.instDecidableEmpEq, Array.instDecidableEmpEqImpl) + (Array.instDecidableEq, Array.instDecidableEqImpl) + (Array.instDecidableEqEmp, Array.instDecidableEqEmpImpl) + (Array.pmap, Array.pmapImpl) + (ByteArray.append, ByteArray.fastAppend) + (List.append, List.appendTR) + (List.dropLast, List.dropLastTR) + (List.erase, List.eraseTR) ++ (List.eraseIdx, List.eraseIdxTR) + (List.eraseP, List.erasePTR) + (List.filter, List.filterTR) + (List.findRev?, List.findRev?TR) ++ (List.findSomeRev?, List.findSomeRev?TR) + (List.flatMap, List.flatMapTR) + (List.flatten, List.flattenTR) + (List.foldr, List.foldrTR) + (List.insertIdx, List.insertIdxTR) + (List.intercalate, List.intercalateTR) + (List.intersperse, List.intersperseTR) + (List.leftpad, List.leftpadTR) + (List.length, List.lengthTR) + (List.map, List.mapTR) + (List.merge, List.MergeSort.Internal.mergeTR) + (List.mergeSort, List.MergeSort.Internal.mergeSortTR₂) + (List.modify, List.modifyTR) + (List.pmap, List.pmapImpl) + (List.range', List.range'TR) + (List.replace, List.replaceTR) + (List.replicate, List.replicateTR) + (List.set, List.setTR) + (List.take, List.takeTR) + (List.takeWhile, List.takeWhileTR) + (List.unzip, List.unzipTR) + (List.zipIdx, List.zipIdxTR) + (List.zipWith, List.zipWithTR) + (Nat.all, Nat.allTR) + (Nat.any, Nat.anyTR) + (Nat.fold, Nat.foldTR) + (Nat.rec, Nat.recCompiled) + (Nat.repeat, Nat.repeatTR) + (String.utf8EncodeChar, String.utf8EncodeCharFast) + (Thunk.fn, Thunk.fnImpl) + (Vector.pmap, Vector.pmapImpl) + (String.Slice.Pos.next, String.Slice.Pos.nextFast)