From e55badef051ab2ad81fd67b13645933c32dce51c Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Mon, 24 Oct 2022 19:42:29 -0700 Subject: [PATCH] feat: `List.mapMono` --- src/Init/Data/List/BasicAux.lean | 23 +++++++++++++++++++++++ 1 file changed, 23 insertions(+) diff --git a/src/Init/Data/List/BasicAux.lean b/src/Init/Data/List/BasicAux.lean index 5fda7289d8..d573de18fb 100644 --- a/src/Init/Data/List/BasicAux.lean +++ b/src/Init/Data/List/BasicAux.lean @@ -184,4 +184,27 @@ theorem le_antisymm [LT α] [s : Antisymm (¬ · < · : α → α → Prop)] {as instance [LT α] [Antisymm (¬ · < · : α → α → Prop)] : Antisymm (· ≤ · : List α → List α → Prop) where antisymm h₁ h₂ := le_antisymm h₁ h₂ +@[inline] private unsafe def mapMonoMImp [Monad m] (as : List α) (f : α → m α) : m (List α) := do + match as with + | [] => return as + | b :: bs => + let b' ← f b + let bs' ← mapMonoMImp bs f + if ptrEq b' b && ptrEq bs' bs then + return as + else + return b' :: bs' + +/-- +Monomorphic `List.mapM`. The internal implementation uses pointer equality, and does not allocate a new list +if the result of each `f a` is a pointer equal value `a`. +-/ +@[implemented_by mapMonoMImp] def mapMonoM [Monad m] (as : List α) (f : α → m α) : m (List α) := + match as with + | [] => return [] + | a :: as => return (← f a) :: (← mapMonoM as f) + +def mapMono (as : List α) (f : α → α) : List α := + Id.run <| as.mapMonoM f + end List