From e70dd0334050aeb7ea835cbaaa0ce6ddb4b5e657 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Wed, 7 Oct 2020 10:01:04 -0700
Subject: [PATCH] chore: remove `forInMap`

---
 src/Init/Data/List/Control.lean          | 12 ---------
 src/Lean/Elab/Do.lean                    | 34 +++++++-----------------
 tests/lean/doNotation1.lean              |  4 +--
 tests/lean/doNotation1.lean.expected.out |  3 ++-
 tests/lean/run/doNotation2.lean          | 11 --------
 5 files changed, 13 insertions(+), 51 deletions(-)

diff --git a/src/Init/Data/List/Control.lean b/src/Init/Data/List/Control.lean
index 386b2258c5..7f2912f5bd 100644
--- a/src/Init/Data/List/Control.lean
+++ b/src/Init/Data/List/Control.lean
@@ -166,16 +166,4 @@ def forInAux {α : Type u} {β : Type v} {m : Type v → Type w} [Monad m] (f :
 @[inline] def forIn {α : Type u} {β : Type v} {m : Type v → Type w} [Monad m] (as : List α) (init : β) (f : α → β → m (ForInStep β)) : m β :=
 forInAux f as init
 
-@[specialize]
-def forInMapAux {α β : Type u} {m : Type u → Type v} [Monad m] (f : α → β → m (ForInStep (α × β))) : List α → List α → β →  m (List α × β)
-| [],    rs, b => pure (rs.reverse, b)
-| a::as, rs, b => do
-  s ← f a b;
-  match s with
-  | ForInStep.done (a, b)  => pure ((a :: rs).reverse ++ as, b)
-  | ForInStep.yield (a, b) => forInMapAux as (a::rs) b
-
-@[inline] def forInMap {α β : Type u} {m : Type u → Type v} [Monad m] (as : List α) (init : β) (f : α → β → m (ForInStep (α × β))) : m (List α × β) :=
-forInMapAux f as [] init
-
 end List
diff --git a/src/Lean/Elab/Do.lean b/src/Lean/Elab/Do.lean
index fc95262c65..9f726bbb54 100644
--- a/src/Lean/Elab/Do.lean
+++ b/src/Lean/Elab/Do.lean
@@ -613,7 +613,6 @@ inductive Kind
 | regular
 | forInNestedTerm
 | forIn
-| forInMap (x : Name)
 
 def Kind.isRegular : Kind → Bool
 | Kind.regular => true
@@ -658,7 +657,6 @@ match ctx.kind with
 | Kind.forInNestedTerm => do u ← mkUVarTuple ref; `(HasPure.pure (DoResult.«return» $u))
 | Kind.regular         => do r ← mkResultUVarTuple ref val; `(HasPure.pure $r)
 | Kind.forIn           => mkForInYield ref
-| Kind.forInMap x      => mkForInMapYield ref x
 
 def returnToTerm (ref : Syntax) (val : Syntax) : M Syntax := do
 r ← returnToTermCore ref val;
@@ -670,7 +668,6 @@ match ctx.kind with
 | Kind.regular         => unreachable!
 | Kind.forInNestedTerm => do u ← mkUVarTuple ref; `(HasPure.pure (DoResult.«continue» $u))
 | Kind.forIn           => mkForInYield ref
-| Kind.forInMap x      => mkForInMapYield ref x
 
 def continueToTerm (ref : Syntax) : M Syntax := do
 r ← continueToTermCore ref;
@@ -682,7 +679,6 @@ match ctx.kind with
 | Kind.regular         => unreachable!
 | Kind.forInNestedTerm => do u ← mkUVarTuple ref; `(HasPure.pure (DoResult.«break» $u))
 | Kind.forIn           => do u ← mkUVarTuple ref; `(HasPure.pure (ForInStep.done $u))
-| Kind.forInMap x      => do u ← mkUVarTuple ref; r ← liftM $ mkTuple ref #[mkIdentFrom ref x, u]; `(HasPure.pure (ForInStep.done $r))
 
 def breakToTerm (ref : Syntax) : M Syntax := do
 r ← breakToTermCore ref;
@@ -879,22 +875,15 @@ xs.forM fun x =>
 adaptReader (fun (ctx : Context) => { ctx with insideFor := true }) x
 
 structure ToForInTermResult :=
-(isForInMap : Bool)
 (uvars      : Array Name)
 (term       : Syntax)
 
 def toForInTerm  (x : Syntax) (forCodeBlock : CodeBlock) : M ToForInTermResult := do
 ctx ← read;
 let uvars := forCodeBlock.uvars;
-if x.isIdent && uvars.contains x.getId then do
-  -- It is a forInMap
-  let uvars := nameSetToArray (uvars.erase x.getId);
-  term ← liftMacroM $ ToTerm.run forCodeBlock.code ctx.m uvars (ToTerm.Kind.forInMap x.getId);
-  pure ⟨true, uvars, term⟩
-else do
-  let uvars := nameSetToArray uvars;
-  term ← liftMacroM $ ToTerm.run forCodeBlock.code ctx.m uvars ToTerm.Kind.forIn;
-  pure ⟨false, uvars, term⟩
+let uvars := nameSetToArray uvars;
+term ← liftMacroM $ ToTerm.run forCodeBlock.code ctx.m uvars ToTerm.Kind.forIn;
+pure ⟨uvars, term⟩
 
 def ensureInsideFor : M Unit := do
 ctx ← read;
@@ -992,20 +981,15 @@ partial def doSeqToCode : List Syntax → M CodeBlock
       let forElems  := getDoSeqElems (doElem.getArg 5);
       let newVars   := if x.isIdent then #[x.getId] else #[];
       forCodeBlock  ← withNewVars newVars $ withFor (doSeqToCode forElems);
-      ⟨isForInMap, uvars, forInBody⟩ ← toForInTerm x forCodeBlock;
+      ⟨uvars, forInBody⟩ ← toForInTerm x forCodeBlock;
       uvarsTuple ← liftMacroM $ mkTuple ref (uvars.map (mkIdentFrom ref));
-      if isForInMap then do
-        forInTerm ← `($(xs).forInMap $uvarsTuple fun $x $uvarsTuple => $forInBody);
-        auxDo ← `(do let r ← $forInTerm; $uvarsTuple:term := r.2; return ensureExpectedType! "type mismatch, 'for'" r.1);
+      forInTerm ← `($(xs).forIn $uvarsTuple fun $x $uvarsTuple => $forInBody);
+      if doElems.isEmpty then do
+        auxDo ← `(do let r ← $forInTerm; $uvarsTuple:term := r; return ensureExpectedType! "type mismatch, 'for'" PUnit.unit);
         doSeqToCode (getDoSeqElems (getDoSeq auxDo) ++ doElems)
       else do
-        forInTerm ← `($(xs).forIn $uvarsTuple fun $x $uvarsTuple => $forInBody);
-        if doElems.isEmpty then do
-          auxDo ← `(do let r ← $forInTerm; $uvarsTuple:term := r; return ensureExpectedType! "type mismatch, 'for'" PUnit.unit);
-          doSeqToCode (getDoSeqElems (getDoSeq auxDo) ++ doElems)
-        else do
-          auxDo ← `(do let r ← $forInTerm; $uvarsTuple:term := r);
-          doSeqToCode (getDoSeqElems (getDoSeq auxDo) ++ doElems)
+        auxDo ← `(do let r ← $forInTerm; $uvarsTuple:term := r);
+        doSeqToCode (getDoSeqElems (getDoSeq auxDo) ++ doElems)
     else if k == `Lean.Parser.Term.doMatch then do
       /- Recall that
          ```
diff --git a/tests/lean/doNotation1.lean b/tests/lean/doNotation1.lean
index 8bbb444f90..ac761c4cad 100644
--- a/tests/lean/doNotation1.lean
+++ b/tests/lean/doNotation1.lean
@@ -20,9 +20,9 @@ if b then
   v := Vector.cons 1 v
 Vector.cons 1 v
 
-def f5 (xs : List Nat) : List Bool := do
+def f5 (y : Nat) (xs : List Nat) : List Bool := do
 for x in xs do
-  x := true -- invalid reassigned
+  y := true -- invalid reassigned
 
 def f6 (xs : List Nat) : IO (List Nat) := do
 for x in xs do -- type error
diff --git a/tests/lean/doNotation1.lean.expected.out b/tests/lean/doNotation1.lean.expected.out
index 76c4a2492a..18c76b5d93 100644
--- a/tests/lean/doNotation1.lean.expected.out
+++ b/tests/lean/doNotation1.lean.expected.out
@@ -1,5 +1,6 @@
 doNotation1.lean:4:0: error: 'y' cannot be reassigned
 doNotation1.lean:8:2: error: 'y' cannot be reassigned
+doNotation1.lean:11:0: error: 'p' cannot be reassigned
 doNotation1.lean:20:7: error: invalid reassignment, value has type
   Vector Nat (n + 1)
 but is expected to have type
@@ -9,7 +10,7 @@ doNotation1.lean:25:7: error: invalid reassignment, value has type
 but is expected to have type
   Nat
 doNotation1.lean:24:0: error: type mismatch, 'for' has type
-  List Nat
+  PUnit
 but is expected to have type
   List Bool
 doNotation1.lean:28:0: error: type mismatch, 'for' has type
diff --git a/tests/lean/run/doNotation2.lean b/tests/lean/run/doNotation2.lean
index 234649c0eb..f5f711f966 100644
--- a/tests/lean/run/doNotation2.lean
+++ b/tests/lean/run/doNotation2.lean
@@ -62,17 +62,6 @@ return sum
 theorem ex5 : sumOdd [1, 2, 3, 4, 5, 6, 7, 9, 11, 101] 10 = 16 :=
 rfl
 
-def mapOdd (f : Nat → Nat) (xs : List Nat) : List Nat := do
-for x in xs do
-  if x % 2 == 1 then
-    x := f x
-  dbgTrace! ">> mapOdd x: " ++ toString x
-
-#eval mapOdd (·+10) [1, 2, 3, 4, 5, 6, 7, 9]
-
-theorem ex6 : mapOdd (·+10) [1, 2, 3, 4, 5, 6, 7, 9] = [11, 2, 13, 4, 15, 6, 17, 19] :=
-rfl
-
 -- We need `Id.run` because we still have `Monad Option`
 def find? (xs : List Nat) (p : Nat → Bool) : Option Nat := Id.run do
 let result := none