From 0447966b72e9a77b0fb9da9eaf3bf7f35f8b90f7 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Tue, 6 Oct 2020 06:51:45 -0700
Subject: [PATCH] chore: adjust elaborator to new syntax

---
 src/Lean/Elab/Do.lean                         |  6 +--
 .../termparsertest1.lean.expected.out         | 49 ++++++++-----------
 2 files changed, 24 insertions(+), 31 deletions(-)

diff --git a/src/Lean/Elab/Do.lean b/src/Lean/Elab/Do.lean
index 62108003ec..07fcaf42f5 100644
--- a/src/Lean/Elab/Do.lean
+++ b/src/Lean/Elab/Do.lean
@@ -447,9 +447,9 @@ pure {
 
 private def getDoSeqElems (doSeq : Syntax) : List Syntax :=
 if doSeq.getKind == `Lean.Parser.Term.doSeqBracketed then
-  (doSeq.getArg 1).getArgs.getSepElems.toList
+  (doSeq.getArg 1).getArgs.toList.map fun arg => arg.getArg 0
 else if doSeq.getKind == `Lean.Parser.Term.doSeqIndent then
-  (doSeq.getArg 0).getArgs.getSepElems.toList
+  (doSeq.getArg 0).getArgs.toList.map fun arg => arg.getArg 0
 else
   []
 
@@ -526,7 +526,7 @@ else
   throwError "unexpected kind of reassignment"
 
 def toDoSeq (doElem : Syntax) : Syntax :=
-mkNode `Lean.Parser.Term.doSeqIndent #[mkNullNode #[doElem, mkNullNode]]
+mkNode `Lean.Parser.Term.doSeqIndent #[mkNullNode #[mkNullNode #[doElem, mkNullNode]]]
 
 /-
   Recall that the `doIf` syntax is of the form
diff --git a/tests/compiler/termparsertest1.lean.expected.out b/tests/compiler/termparsertest1.lean.expected.out
index d9046fbdba..d44d8cd08d 100644
--- a/tests/compiler/termparsertest1.lean.expected.out
+++ b/tests/compiler/termparsertest1.lean.expected.out
@@ -275,39 +275,32 @@ do
 (Term.do
  "do"
  (Term.doSeqIndent
-  [(Term.doLetArrow "let" (Term.doIdDecl `x [] "←" (Term.app `f [`a])))
-   [";"]
-   (Term.doLetArrow "let" (Term.doIdDecl `x [(Term.typeSpec ":" `Nat)] "←" (Term.app `f [`a])))
-   [";"]
-   (Term.doExpr (Term.app `g [`x]))
-   [";"]
-   (Term.doLet "let" (Term.letDecl (Term.letIdDecl `y [] [] ":=" (Term.app `g [`x]))))
-   [";"]
-   (Term.doLetArrow
-    "let"
-    (Term.doPatDecl (Term.paren "(" [`a [(Term.tupleTail "," [`b])]] ")") "<-" (Term.app `h [`x `y]) []))
-   [";"]
-   (Term.doLet
-    "let"
-    (Term.letDecl
-     (Term.letPatDecl
-      (Term.paren "(" [`a [(Term.tupleTail "," [`b])]] ")")
-      []
-      []
-      ":="
-      (Term.paren "(" [`b [(Term.tupleTail "," [`a])]] ")"))))
-   [";"]
-   (Term.doExpr (Term.app `pure [(Term.paren "(" [(Term.add `a "+" `b) []] ")")]))
-   []]))
+  [[(Term.doLetArrow "let" (Term.doIdDecl `x [] "←" (Term.app `f [`a]))) [";"]]
+   [(Term.doLetArrow "let" (Term.doIdDecl `x [(Term.typeSpec ":" `Nat)] "←" (Term.app `f [`a]))) [";"]]
+   [(Term.doExpr (Term.app `g [`x])) [";"]]
+   [(Term.doLet "let" (Term.letDecl (Term.letIdDecl `y [] [] ":=" (Term.app `g [`x])))) [";"]]
+   [(Term.doLetArrow
+     "let"
+     (Term.doPatDecl (Term.paren "(" [`a [(Term.tupleTail "," [`b])]] ")") "<-" (Term.app `h [`x `y]) []))
+    [";"]]
+   [(Term.doLet
+     "let"
+     (Term.letDecl
+      (Term.letPatDecl
+       (Term.paren "(" [`a [(Term.tupleTail "," [`b])]] ")")
+       []
+       []
+       ":="
+       (Term.paren "(" [`b [(Term.tupleTail "," [`a])]] ")"))))
+    [";"]]
+   [(Term.doExpr (Term.app `pure [(Term.paren "(" [(Term.add `a "+" `b) []] ")")])) []]]))
 do { let x ← f a; pure $ a + a }
 (Term.do
  "do"
  (Term.doSeqBracketed
   "{"
-  [(Term.doLetArrow "let" (Term.doIdDecl `x [] "←" (Term.app `f [`a])))
-   [";"]
-   (Term.doExpr (Term.dollar `pure "$" (Term.add `a "+" `a)))
-   []]
+  [[(Term.doLetArrow "let" (Term.doIdDecl `x [] "←" (Term.app `f [`a]))) [";"]]
+   [(Term.doExpr (Term.dollar `pure "$" (Term.add `a "+" `a))) []]]
   "}"))
 let f : Nat → Nat → Nat
    | 0, a   => a + 10