From 156e5603d6efc2011532797b05e7a08efb1bec03 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Sun, 5 Mar 2017 21:30:30 -0800
Subject: [PATCH] feat(library/init/category/combinators): put list combinators
 in the namespace list

In this way we can use them with the ^. notation
---
 library/init/category/combinators.lean   | 28 +++++++++++++-----------
 library/init/meta/smt/rsimp.lean         |  2 +-
 library/tools/mini_crush/default.lean    |  2 +-
 library/tools/mini_crush/nano_crush.lean |  2 +-
 4 files changed, 18 insertions(+), 16 deletions(-)

diff --git a/library/init/category/combinators.lean b/library/init/category/combinators.lean
index d034302bc0..dcf686a009 100644
--- a/library/init/category/combinators.lean
+++ b/library/init/category/combinators.lean
@@ -1,7 +1,7 @@
 /-
 Copyright (c) 2016 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Jeremy Avigad
+Authors: Jeremy Avigad, Leonardo de Moura
 
 Monad combinators, as in Haskell's Control.Monad.
 -/
@@ -9,19 +9,19 @@ prelude
 import init.category.monad init.data.list.basic
 universes u v w
 
-def mmap {m : Type u → Type v} [monad m] {α : Type w} {β : Type u} (f : α → m β) : list α → m (list β)
+def list.mmap {m : Type u → Type v} [monad m] {α : Type w} {β : Type u} (f : α → m β) : list α → m (list β)
 | []       := return []
-| (h :: t) := do h' ← f h, t' ← mmap t, return (h' :: t')
+| (h :: t) := do h' ← f h, t' ← list.mmap t, return (h' :: t')
 
-def mmap' {m : Type → Type v} [monad m] {α : Type u} {β : Type} (f : α → m β) : list α → m unit
+def list.mmap' {m : Type → Type v} [monad m] {α : Type u} {β : Type} (f : α → m β) : list α → m unit
 | []       := return ()
-| (h :: t) := f h >> mmap' t
+| (h :: t) := f h >> list.mmap' t
 
-def mfor {m : Type u → Type v} [monad m] {α : Type w} {β : Type u} (l : list α) (f : α → m β) : m (list β) :=
-mmap f l
+def list.mfor {m : Type u → Type v} [monad m] {α : Type w} {β : Type u} (l : list α) (f : α → m β) : m (list β) :=
+list.mmap f l
 
-def mfor' {m : Type → Type v} [monad m] {α : Type u} {β : Type} (l : list α) (f : α → m β) : m unit :=
-mmap' f l
+def list.mfor' {m : Type → Type v} [monad m] {α : Type u} {β : Type} (l : list α) (f : α → m β) : m unit :=
+list.mmap' f l
 
 infix ` =<< `:2 := λ u v, v >>= u
 
@@ -32,15 +32,15 @@ infix ` <=< `:2 := λ t s a, s a >>= t
 def mjoin {m : Type u → Type u} [monad m] {α : Type u} (a : m (m α)) : m α :=
 bind a id
 
-def mfilter {m : Type → Type v} [monad m] {α : Type} (f : α → m bool) : list α → m (list α)
+def list.mfilter {m : Type → Type v} [monad m] {α : Type} (f : α → m bool) : list α → m (list α)
 | []       := return []
-| (h :: t) := do b ← f h, t' ← mfilter t, cond b (return (h :: t')) (return t')
+| (h :: t) := do b ← f h, t' ← list.mfilter t, cond b (return (h :: t')) (return t')
 
-def mfoldl {m : Type u → Type v} [monad m] {s : Type u} {α : Type w} : (s → α → m s) → s → list α → m s
+def list.mfoldl {m : Type u → Type v} [monad m] {s : Type u} {α : Type w} : (s → α → m s) → s → list α → m s
 | f s [] := return s
 | f s (h :: r) := do
   s' ← f s h,
-  mfoldl f s' r
+  list.mfoldl f s' r
 
 def when {m : Type → Type} [monad m] (c : Prop) [h : decidable c] (t : m unit) : m unit :=
 ite c t (pure ())
@@ -51,6 +51,8 @@ do b ← mbool, cond b tm fm
 def mwhen {m : Type → Type} [monad m] (c : m bool) (t : m unit) : m unit :=
 mcond c t (return ())
 
+export list (mmap mmap' mfor mfor' mfilter mfoldl)
+
 namespace monad
 def mapm   := @mmap
 def mapm'  := @mmap'
diff --git a/library/init/meta/smt/rsimp.lean b/library/init/meta/smt/rsimp.lean
index e6ab9d3b4b..d6aaf37fc7 100644
--- a/library/init/meta/smt/rsimp.lean
+++ b/library/init/meta/smt/rsimp.lean
@@ -96,7 +96,7 @@ meta def repr_map := expr_map expr
 meta def mk_repr_map := expr_map.mk expr
 
 meta def to_repr_map (ccs : cc_state) : tactic repr_map :=
-mfoldl (λ S e, do r ← choose ccs e, return $ S^.insert e r) mk_repr_map ccs^.roots
+ccs^.roots^.mfoldl (λ S e, do r ← choose ccs e, return $ S^.insert e r) mk_repr_map
 
 meta def rsimplify (ccs : cc_state) (e : expr) (m : option repr_map := none) : tactic (expr × expr) :=
 do m ← match m with
diff --git a/library/tools/mini_crush/default.lean b/library/tools/mini_crush/default.lean
index 8aca83e6ac..995def3a22 100644
--- a/library/tools/mini_crush/default.lean
+++ b/library/tools/mini_crush/default.lean
@@ -48,7 +48,7 @@ e^.mfold s $ λ t _ s,
 
 meta def collect_revelant_fns : tactic name_set :=
 do ctx ← local_context,
-   s₁  ← mfoldl (λ s e, infer_type e >>= collect_revelant_fns_aux s) mk_name_set ctx,
+   s₁  ← ctx^.mfoldl (λ s e, infer_type e >>= collect_revelant_fns_aux s) mk_name_set,
    target >>= collect_revelant_fns_aux s₁
 
 meta def add_relevant_eqns (s : simp_lemmas) : tactic simp_lemmas :=
diff --git a/library/tools/mini_crush/nano_crush.lean b/library/tools/mini_crush/nano_crush.lean
index 4b30be17d1..3651e09cf3 100644
--- a/library/tools/mini_crush/nano_crush.lean
+++ b/library/tools/mini_crush/nano_crush.lean
@@ -46,7 +46,7 @@ e^.mfold s $ λ t _ s,
 
 meta def collect_revelant_fns : tactic name_set :=
 do ctx ← local_context,
-   s₁  ← mfoldl (λ s e, infer_type e >>= collect_revelant_fns_aux s) mk_name_set ctx,
+   s₁  ← ctx^.mfoldl (λ s e, infer_type e >>= collect_revelant_fns_aux s) mk_name_set,
    target >>= collect_revelant_fns_aux s₁
 
 meta def add_relevant_eqns (hs : hinst_lemmas) : tactic hinst_lemmas :=