feat: port Init.Control.Combinators (#530)

- TODO: check if List.mfirst align is correct

Co-authored-by: Scott Morrison <scott.morrison@gmail.com>

Author: pechersky

Mathlib.lean

@@ -60,6 +60,7 @@ import Mathlib.Init.Algebra.Order
 import Mathlib.Init.Align
 import Mathlib.Init.CcLemmas
 import Mathlib.Init.Classical
+import Mathlib.Init.Control.Combinators
 import Mathlib.Init.Core
 import Mathlib.Init.Data.Bool.Basic
 import Mathlib.Init.Data.Bool.Lemmas

Mathlib/Init/Control/Combinators.lean

@@ -0,0 +1,86 @@
+/-
+Copyright (c) 2016 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Jeremy Avigad, Leonardo de Moura
+-/
+import Std.Data.List.Init.Lemmas
+import Mathlib.Mathport.Rename
+
+/-! ## Monad combinators, as in Haskell's Control.Monad. -/
+
+universe u v w
+
+#align list.mmap List.mapM
+
+#align list.mmap' List.mapM'
+
+def joinM {m : Type u → Type u} [Monad m] {α : Type u} (a : m (m α)) : m α :=
+  bind a id
+
+#align mjoin joinM
+
+#align list.mfilter List.filterM
+
+#align list.mfoldl List.foldlM
+
+#align list.mfoldr List.foldrM
+
+#align list.mfirst List.firstM
+
+def when {m : Type → Type} [Monad m] (c : Prop) [Decidable c] (t : m Unit) : m Unit :=
+  ite c t (pure ())
+
+def condM {m : Type → Type} [Monad m] {α : Type} (mbool : m Bool) (tm fm : m α) : m α := do
+  let b ← mbool
+  cond b tm fm
+
+#align mcond condM
+
+def whenM {m : Type → Type} [Monad m] (c : m Bool) (t : m Unit) : m Unit :=
+  condM c t (return ())
+
+#align mwhen whenM
+
+
+export List (mapM mapM' filterM foldlM)
+
+namespace Monad
+
+def mapM :=
+  @List.mapM
+#align monad.mapm Monad.mapM
+
+def mapM' :=
+  @List.mapM'
+#align monad.mapm' Monad.mapM'
+
+def join :=
+  @joinM
+
+def filter :=
+  @filterM
+
+def foldl :=
+  @List.foldlM
+
+def cond :=
+  @condM
+
+def sequence {m : Type u → Type v} [Monad m] {α : Type u} : List (m α) → m (List α)
+  | [] => return []
+  | h :: t => do
+    let h' ← h
+    let t' ← sequence t
+    return (h' :: t')
+
+def sequence' {m : Type → Type u} [Monad m] {α : Type} : List (m α) → m Unit
+  | [] => return ()
+  | h :: t => h *> sequence' t
+
+def whenb {m : Type → Type} [Monad m] (b : Bool) (t : m Unit) : m Unit :=
+  _root_.cond b t (return ())
+
+def unlessb {m : Type → Type} [Monad m] (b : Bool) (t : m Unit) : m Unit :=
+  _root_.cond b (return ()) t
+
+end Monad

scripts/nolints.json

@@ -44,6 +44,9 @@
  ["docBlame", "bit1"],
  ["docBlame", "decidable_eq_of_bool_pred"],
  ["docBlame", "instHNeg"],
+ ["docBlame", "condM"],
+ ["docBlame", "joinM"],
+ ["docBlame", "whenM"],
  ["docBlame", "setOf"],
  ["docBlame", "«term_+ᵥ_»"],
  ["docBlame", "«term_-ᵥ_»"],
@@ -57,6 +60,9 @@
  ["docBlame", "to_additive_ignore_args"],
  ["docBlame", "to_additive_relevant_arg"],
  ["docBlame", "to_additive_reorder"],
+ ["docBlame", "variables"],
+ ["docBlame", "when"],
+ ["docBlame", "AddCancelCommMonoid.add_comm"],
  ["docBlame", "AddCancelCommMonoid.toCancelMonoid"],
  ["docBlame", "AddCancelMonoid.add_right_cancel"],
  ["docBlame", "AddCommGroup.toCancelCommMonoid"],
@@ -193,8 +199,24 @@
  ["docBlame", "List.card"],
  ["docBlame", "List.equiv"],
  ["docBlame", "List.inj_on"],
+ ["docBlame", "List.mfilter"],
+ ["docBlame", "List.mfirst"],
+ ["docBlame", "List.mfoldl"],
+ ["docBlame", "List.mfoldr"],
+ ["docBlame", "List.mmap"],
+ ["docBlame", "List.mmap'"],
  ["docBlame", "List.remove"],
  ["docBlame", "List.«term_~_»"],
+ ["docBlame", "Monad.cond"],
+ ["docBlame", "Monad.filter"],
+ ["docBlame", "Monad.foldl"],
+ ["docBlame", "Monad.join"],
+ ["docBlame", "Monad.mapM"],
+ ["docBlame", "Monad.mapM'"],
+ ["docBlame", "Monad.sequence"],
+ ["docBlame", "Monad.sequence'"],
+ ["docBlame", "Monad.unlessb"],
+ ["docBlame", "Monad.whenb"],
  ["docBlame", "MonadWriter.listen"],
  ["docBlame", "MonadWriter.pass"],
  ["docBlame", "MonadWriter.tell"],
@@ -698,4 +720,4 @@
  ["docBlame", "Lean.Parser.Tactic.rcasesPat.explicit"],
  ["docBlame", "Mathlib.Tactic.Sat.buildReify.mkPS"],
  ["unusedArguments", "Combinator.K"],
- ["unusedArguments", "Decidable.not_or_iff_and_not"]]
+ ["unusedArguments", "Decidable.not_or_iff_and_not"]]