From a883042dc85ef28bd5353eec8de093041bd79350 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Wed, 3 Apr 2019 07:40:28 -0700
Subject: [PATCH] chore(library/init): fold functions argument order
 consistency

---
 library/init/data/hashmap/basic.lean |  6 ++---
 library/init/data/rbmap/basic.lean   | 37 +++++++++++++++-------------
 library/init/data/rbtree/basic.lean  | 16 ++++++------
 library/init/lean/parser/trie.lean   |  2 +-
 tests/playground/map_perf.lean       |  4 +--
 tests/playground/rbmap.library.lean  |  2 +-
 6 files changed, 35 insertions(+), 32 deletions(-)

diff --git a/library/init/data/hashmap/basic.lean b/library/init/data/hashmap/basic.lean
index a7663ae763..ce45dbecf1 100644
--- a/library/init/data/hashmap/basic.lean
+++ b/library/init/data/hashmap/basic.lean
@@ -57,7 +57,7 @@ match m with
   let ⟨i, h⟩ := mkIdx buckets.property (hash a) in
   (buckets.val.idx i h).contains a
 
-def fold {δ : Type w} (m : HashMapImp α β) (d : δ) (f : δ → α → β → δ) : δ :=
+def fold {δ : Type w} (f : δ → α → β → δ) (d : δ) (m : HashMapImp α β) : δ :=
 foldBuckets m.buckets d f
 
 def insert [HasBeq α] [Hashable α] (m : HashMapImp α β) (a : α) (b : β) : HashMapImp α β :=
@@ -125,9 +125,9 @@ match m with
 match m with
 | ⟨ m, _ ⟩ := m.contains a
 
-@[inline] def fold {δ : Type w} (m : HashMap α β) (d : δ) (f : δ → α → β → δ) : δ :=
+@[inline] def fold {δ : Type w} (f : δ → α → β → δ) (d : δ) (m : HashMap α β) : δ :=
 match m with
-| ⟨ m, _ ⟩ := m.fold d f
+| ⟨ m, _ ⟩ := m.fold f d
 
 @[inline] def size (m : HashMap α β) : Nat :=
 match m with
diff --git a/library/init/data/rbmap/basic.lean b/library/init/data/rbmap/basic.lean
index 628d9988c5..9d8772558a 100644
--- a/library/init/data/rbmap/basic.lean
+++ b/library/init/data/rbmap/basic.lean
@@ -34,17 +34,20 @@ protected def max : RBNode α β → Option (Σ k : α, β k)
 | (node _ _ k v leaf)   := some ⟨k, v⟩
 | (node _ _ k v r)      := max r
 
-@[specialize] def fold (f : Π (k : α), β k → σ → σ) : RBNode α β → σ → σ
-| leaf b               := b
-| (node _ l k v r)   b := fold r (f k v (fold l b))
+@[specialize] def fold (f : σ → Π (k : α), β k → σ) : σ → RBNode α β → σ
+| b leaf             := b
+| b (node _ l k v r) := fold (f (fold b l) k v) r
 
-@[specialize] def mfold {m : Type w → Type w'} [Monad m] (f : Π (k : α), β k → σ → m σ) : RBNode α β → σ → m σ
-| leaf b               := pure b
-| (node _ l k v r) b   := do b₁ ← mfold l b, b₂ ← f k v b₁, mfold r b₂
+@[specialize] def mfold {m : Type w → Type w'} [Monad m] (f : σ → Π (k : α), β k → m σ) : σ → RBNode α β → m σ
+| b leaf             := pure b
+| b (node _ l k v r) := do
+  b ← mfold b l,
+  b ← f b k v,
+  mfold b r
 
-@[specialize] def revFold (f : Π (k : α), β k → σ → σ) : RBNode α β → σ → σ
-| leaf b               := b
-| (node _ l k v r)   b := revFold l (f k v (revFold r b))
+@[specialize] def revFold (f : σ → Π (k : α), β k → σ) : σ → RBNode α β → σ
+| b leaf               := b
+| b (node _ l k v r)   := revFold (f (revFold b r) k v) l
 
 @[specialize] def all (p : Π k : α, β k → Bool) : RBNode α β → Bool
 | leaf                 := true
@@ -154,24 +157,24 @@ variables {α : Type u} {β : Type v} {σ : Type w} {lt : α → α → Bool}
 def depth (f : Nat → Nat → Nat) (t : RBMap α β lt) : Nat :=
 t.val.depth f
 
-@[inline] def fold (f : α → β → σ → σ) : RBMap α β lt → σ → σ
-| ⟨t, _⟩ b := t.fold f b
+@[inline] def fold (f : σ → α → β → σ) : σ → RBMap α β lt → σ
+| b ⟨t, _⟩ := t.fold f b
 
-@[inline] def revFold (f : α → β → σ → σ) : RBMap α β lt → σ → σ
-| ⟨t, _⟩ b := t.revFold f b
+@[inline] def revFold (f : σ → α → β → σ) : σ → RBMap α β lt → σ
+| b ⟨t, _⟩ := t.revFold f b
 
-@[inline] def mfold {m : Type w → Type w'} [Monad m] (f : α → β → σ → m σ) : RBMap α β lt → σ → m σ
-| ⟨t, _⟩ b := t.mfold f b
+@[inline] def mfold {m : Type w → Type w'} [Monad m] (f : σ → α → β → m σ) : σ → RBMap α β lt → m σ
+| b ⟨t, _⟩ := t.mfold f b
 
 @[inline] def mfor {m : Type w → Type w'} [Monad m] (f : α → β → m σ) (t : RBMap α β lt) : m PUnit :=
-t.mfold (λ k v _, f k v *> pure ⟨⟩) ⟨⟩
+t.mfold (λ _ k v,  f k v *> pure ⟨⟩) ⟨⟩
 
 @[inline] def isEmpty : RBMap α β lt → Bool
 | ⟨leaf, _⟩ := true
 | _         := false
 
 @[specialize] def toList : RBMap α β lt → List (α × β)
-| ⟨t, _⟩ := t.revFold (λ k v ps, (k, v)::ps) []
+| ⟨t, _⟩ := t.revFold (λ ps k v, (k, v)::ps) []
 
 @[inline] protected def min : RBMap α β lt → Option (α × β)
 | ⟨t, _⟩ :=
diff --git a/library/init/data/rbtree/basic.lean b/library/init/data/rbtree/basic.lean
index 8730cd219d..694ebae1ea 100644
--- a/library/init/data/rbtree/basic.lean
+++ b/library/init/data/rbtree/basic.lean
@@ -22,23 +22,23 @@ variables {α : Type u} {β : Type v} {lt : α → α → Bool}
 @[inline] def depth (f : Nat → Nat → Nat) (t : RBTree α lt) : Nat :=
 RBMap.depth f t
 
-@[inline] def fold (f : α → β → β) (t : RBTree α lt) (b : β) : β :=
-RBMap.fold (λ a _ r, f a r) t b
+@[inline] def fold (f : β → α → β) (b : β) (t : RBTree α lt) : β :=
+RBMap.fold (λ r a _, f r a) b t
 
-@[inline] def revFold (f : α → β → β) (t : RBTree α lt) (b : β) : β :=
-RBMap.revFold (λ a _ r, f a r) t b
+@[inline] def revFold (f : β → α → β) (b : β) (t : RBTree α lt) : β :=
+RBMap.revFold (λ r a _, f r a) b t
 
-@[inline] def mfold {m : Type v → Type w} [Monad m] (f : α → β → m β) (t : RBTree α lt) (b : β) : m β :=
-RBMap.mfold (λ a _ r, f a r) t b
+@[inline] def mfold {m : Type v → Type w} [Monad m] (f : β → α → m β) (b : β) (t : RBTree α lt) : m β :=
+RBMap.mfold (λ r a _, f r a) b t
 
 @[inline] def mfor {m : Type v → Type w} [Monad m] (f : α → m β) (t : RBTree α lt) : m PUnit :=
-t.mfold (λ a _, f a *> pure ⟨⟩) ⟨⟩
+t.mfold (λ _ a, f a *> pure ⟨⟩) ⟨⟩
 
 @[inline] def isEmpty (t : RBTree α lt) : Bool :=
 RBMap.isEmpty t
 
 @[specialize] def toList (t : RBTree α lt) : List α :=
-t.revFold (::) []
+t.revFold (λ as a, a::as) []
 
 @[inline] protected def min (t : RBTree α lt) : Option α :=
 match RBMap.min t with
diff --git a/library/init/lean/parser/trie.lean b/library/init/lean/parser/trie.lean
index c83860cbdd..9a8e0793f2 100644
--- a/library/init/lean/parser/trie.lean
+++ b/library/init/lean/parser/trie.lean
@@ -95,7 +95,7 @@ def oldMatchPrefix {α : Type} (t : Trie α) (it : String.OldIterator) : Option
 oldMatchPrefixAux it.remaining t it none
 
 private partial def toStringAux {α : Type} : Trie α → List Format
-| (Trie.Node val map) := flip RBNode.fold map (λ c t Fs,
+| (Trie.Node val map) := map.fold (λ Fs c t,
   toFormat (repr c) :: (Format.group $ Format.nest 2 $ flip Format.joinSep Format.line $ toStringAux t) :: Fs) []
 
 instance {α : Type} : HasToString (Trie α) :=
diff --git a/tests/playground/map_perf.lean b/tests/playground/map_perf.lean
index ff5e0b3e11..d2626333c6 100644
--- a/tests/playground/map_perf.lean
+++ b/tests/playground/map_perf.lean
@@ -17,12 +17,12 @@ mkMap2Aux n {}
 
 def tst1 (n : Nat) : IO Unit :=
 do let m := mkMap1 n,
-   let v := m.fold (λ (k : Nat) (v : Bool) (r : Nat), if v then r + 1 else r) 0,
+   let v := m.fold (λ (r : Nat) (k : Nat) (v : Bool), if v then r + 1 else r) 0,
    IO.println ("Result " ++ toString v)
 
 def tst2 (n : Nat) : IO Unit :=
 do let m := mkMap2 n,
-   let v := m.fold 0 (λ (r : Nat) (k : Nat) (v : Bool), if v then r + 1 else r),
+   let v := m.fold (λ (r : Nat) (k : Nat) (v : Bool), if v then r + 1 else r) 0,
    IO.println ("Result " ++ toString v)
 
 def main (xs : List String) : IO Unit :=
diff --git a/tests/playground/rbmap.library.lean b/tests/playground/rbmap.library.lean
index 2c845d006f..3d534d6bde 100644
--- a/tests/playground/rbmap.library.lean
+++ b/tests/playground/rbmap.library.lean
@@ -9,6 +9,6 @@ mkMapAux n {}
 
 def main (xs : List String) : IO UInt32 :=
 let m := mkMap xs.head.toNat in
-let v := RBMap.fold (λ (k : Nat) (v : Bool) (r : Nat), if v then r + 1 else r) m 0 in
+let v := m.fold (λ (r : Nat) (k : Nat) (v : Bool), if v then r + 1 else r) 0 in
 IO.println (toString v) *>
 pure 0