From d0d3e2497513b1aacb7f1fcd4b46241e68463149 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Sat, 25 Jan 2020 20:14:50 -0800
Subject: [PATCH] chore: fix tests

---
 .../termparsertest1.lean.expected.out         | 56 +++++++++++--------
 tests/lean/StxQuot.lean.expected.out          |  4 +-
 2 files changed, 35 insertions(+), 25 deletions(-)

diff --git a/tests/compiler/termparsertest1.lean.expected.out b/tests/compiler/termparsertest1.lean.expected.out
index 165f453f8d..d8ee793485 100644
--- a/tests/compiler/termparsertest1.lean.expected.out
+++ b/tests/compiler/termparsertest1.lean.expected.out
@@ -266,9 +266,11 @@ match x with
  (null (Term.id `x (null)))
  (null)
  "with"
+ (null "|")
  (null
-  (Term.matchAlt "|" (null (Term.app (Term.id `some (null)) (null (Term.id `x (null))))) "=>" (Term.id `true (null)))
-  (Term.matchAlt "|" (null (Term.id `none (null))) "=>" (Term.id `false (null)))))
+  (Term.matchAlt (null (Term.app (Term.id `some (null)) (null (Term.id `x (null))))) "=>" (Term.id `true (null)))
+  "|"
+  (Term.matchAlt (null (Term.id `none (null))) "=>" (Term.id `false (null)))))
 
 match x with
 | some y => match y with
@@ -281,9 +283,9 @@ match x with
  (null (Term.id `x (null)))
  (null)
  "with"
+ (null "|")
  (null
   (Term.matchAlt
-   "|"
    (null (Term.app (Term.id `some (null)) (null (Term.id `y (null)))))
    "=>"
    (Term.match
@@ -291,17 +293,19 @@ match x with
     (null (Term.id `y (null)))
     (null)
     "with"
+    (null "|")
     (null
      (Term.matchAlt
-      "|"
       (null
        (Term.app
         (Term.id `some (null))
         (null (Term.paren "(" (null (Term.id `a (null)) (null (Term.tupleTail "," (null (Term.id `b (null)))))) ")"))))
       "=>"
       (Term.add (Term.id `a (null)) "+" (Term.id `b (null))))
-     (Term.matchAlt "|" (null (Term.id `none (null))) "=>" (Term.num (numLit "1"))))))
-  (Term.matchAlt "|" (null (Term.id `none (null))) "=>" (Term.num (numLit "0")))))
+     "|"
+     (Term.matchAlt (null (Term.id `none (null))) "=>" (Term.num (numLit "1"))))))
+  "|"
+  (Term.matchAlt (null (Term.id `none (null))) "=>" (Term.num (numLit "0")))))
 Type u
 (Term.sortApp (Term.type "Type") (Level.ident `u))
 Sort v
@@ -313,19 +317,19 @@ f Type 1
 let x := 0; x + 1
 (Term.let
  "let"
- (Term.letIdDecl `x (null) (null) ":=" (Term.num (numLit "0")))
+ (Term.letDecl `x (null) (null) ":=" (Term.num (numLit "0")))
  ";"
  (Term.add (Term.id `x (null)) "+" (Term.num (numLit "1"))))
 let x : Nat := 0; x + 1
 (Term.let
  "let"
- (Term.letIdDecl `x (null) (null (Term.typeSpec ":" (Term.id `Nat (null)))) ":=" (Term.num (numLit "0")))
+ (Term.letDecl `x (null) (null (Term.typeSpec ":" (Term.id `Nat (null)))) ":=" (Term.num (numLit "0")))
  ";"
  (Term.add (Term.id `x (null)) "+" (Term.num (numLit "1"))))
 let f (x : Nat) := x + 1; f 0
 (Term.let
  "let"
- (Term.letIdDecl
+ (Term.letDecl
   `f
   (null (Term.explicitBinder "(" (null `x) (null ":" (Term.id `Nat (null))) (null) ")"))
   (null)
@@ -336,7 +340,7 @@ let f (x : Nat) := x + 1; f 0
 let f {α : Type} (a : α) : α := a; f 10
 (Term.let
  "let"
- (Term.letIdDecl
+ (Term.letDecl
   `f
   (null
    (Term.implicitBinder "{" (null `α) (null ":" (Term.type "Type")) "}")
@@ -349,7 +353,7 @@ let f {α : Type} (a : α) : α := a; f 10
 let f (x) := x + 1; f 10 + f 20
 (Term.let
  "let"
- (Term.letIdDecl
+ (Term.letDecl
   `f
   (null (Term.explicitBinder "(" (null `x) (null) (null) ")"))
   (null)
@@ -363,9 +367,10 @@ let f (x) := x + 1; f 10 + f 20
 let (x, y) := f 10; x + y
 (Term.let
  "let"
- (Term.letPatDecl
+ (Term.letDecl
   (Term.paren "(" (null (Term.id `x (null)) (null (Term.tupleTail "," (null (Term.id `y (null)))))) ")")
   (null)
+  (null)
   ":="
   (Term.app (Term.id `f (null)) (null (Term.num (numLit "10")))))
  ";"
@@ -373,13 +378,14 @@ let (x, y) := f 10; x + y
 let { fst := x, .. } := f 10; x + x
 (Term.let
  "let"
- (Term.letPatDecl
+ (Term.letDecl
   (Term.structInst
    "{"
    (null)
    (null (Term.structInstField `fst ":=" (Term.id `x (null))) "," (Term.structInstSource ".." (null)))
    "}")
   (null)
+  (null)
   ":="
   (Term.app (Term.id `f (null)) (null (Term.num (numLit "10")))))
  ";"
@@ -387,15 +393,16 @@ let { fst := x, .. } := f 10; x + x
 let x.y := f 10; x
 (Term.let
  "let"
- (Term.letIdDecl `x.y (null) (null) ":=" (Term.app (Term.id `f (null)) (null (Term.num (numLit "10")))))
+ (Term.letDecl `x.y (null) (null) ":=" (Term.app (Term.id `f (null)) (null (Term.num (numLit "10")))))
  ";"
  (Term.id `x (null)))
 let x.1 := f 10; x
 (Term.let
  "let"
- (Term.letPatDecl
+ (Term.letDecl
   (Term.proj (Term.id `x (null)) "." (fieldIdx "1"))
   (null)
+  (null)
   ":="
   (Term.app (Term.id `f (null)) (null (Term.num (numLit "10")))))
  ";"
@@ -403,9 +410,10 @@ let x.1 := f 10; x
 let x[i].y := f 10; x
 (Term.let
  "let"
- (Term.letPatDecl
+ (Term.letDecl
   (Term.proj (Term.arrayRef (Term.id `x (null)) "[" (Term.id `i (null)) "]") "." `y)
   (null)
+  (null)
   ":="
   (Term.app (Term.id `f (null)) (null (Term.num (numLit "10")))))
  ";"
@@ -413,9 +421,10 @@ let x[i].y := f 10; x
 let x[i] := f 20; x
 (Term.let
  "let"
- (Term.letPatDecl
+ (Term.letDecl
   (Term.arrayRef (Term.id `x (null)) "[" (Term.id `i (null)) "]")
   (null)
+  (null)
   ":="
   (Term.app (Term.id `f (null)) (null (Term.num (numLit "20")))))
  ";"
@@ -448,7 +457,7 @@ do
   ";"
   (Term.doExpr (Term.app (Term.id `g (null)) (null (Term.id `x (null)))))
   ";"
-  (Term.doLet "let" (Term.letIdDecl `y (null) (null) ":=" (Term.app (Term.id `g (null)) (null (Term.id `x (null))))))
+  (Term.doLet "let" (Term.letDecl `y (null) (null) ":=" (Term.app (Term.id `g (null)) (null (Term.id `x (null))))))
   ";"
   (Term.doPat
    (Term.paren "(" (null (Term.id `a (null)) (null (Term.tupleTail "," (null (Term.id `b (null)))))) ")")
@@ -458,9 +467,10 @@ do
   ";"
   (Term.doLet
    "let"
-   (Term.letPatDecl
+   (Term.letDecl
     (Term.paren "(" (null (Term.id `a (null)) (null (Term.tupleTail "," (null (Term.id `b (null)))))) ")")
     (null)
+    (null)
     ":="
     (Term.paren "(" (null (Term.id `b (null)) (null (Term.tupleTail "," (null (Term.id `a (null)))))) ")")))
   ";"
@@ -484,19 +494,19 @@ let f : Nat → Nat → Nat
 f 20
 (Term.let
  "let"
- (Term.letEqns
+ (Term.letDecl
   `f
   (null)
   (null
    (Term.typeSpec ":" (Term.arrow (Term.id `Nat (null)) "→" (Term.arrow (Term.id `Nat (null)) "→" (Term.id `Nat (null))))))
+  "|"
   (null
    (Term.matchAlt
-    "|"
     (null (Term.num (numLit "0")) "," (Term.id `a (null)))
     "=>"
     (Term.add (Term.id `a (null)) "+" (Term.num (numLit "10"))))
+   "|"
    (Term.matchAlt
-    "|"
     (null (Term.add (Term.id `n (null)) "+" (Term.num (numLit "1"))) "," (Term.id `b (null)))
     "=>"
     (Term.mul (Term.id `n (null)) "*" (Term.id `b (null))))))
@@ -509,6 +519,6 @@ failed as expected, error: <input>:1:10 found '→' as expected, but brackets ar
 (x := 20)
 failed as expected, error: <input>:1:3 expected ':' or ')'
 let x 10; x
-failed as expected, error: <input>:1:8 expected ':='
+failed as expected, error: <input>:1:6 expected '|'
 let x := y
 failed as expected, error: <input>:1:10 expected ';'
diff --git a/tests/lean/StxQuot.lean.expected.out b/tests/lean/StxQuot.lean.expected.out
index 669f57dbe3..4dd381b37b 100644
--- a/tests/lean/StxQuot.lean.expected.out
+++ b/tests/lean/StxQuot.lean.expected.out
@@ -25,5 +25,5 @@
 "(Term.simpleBinder (null (Term.hole \"_\")))"
 "`a._@.UnhygienicMain._hyg.1"
 "(Term.id `a._@.UnhygienicMain._hyg.1 (null (Term.explicitUniv \".{\" (null (Level.num (numLit \"0\"))) \"}\")))"
-"#[(Term.matchAlt \"|\" (null (Term.id `a._@.UnhygienicMain._hyg.1 (null))) \"=>\" (Term.num (numLit \"1\"))), (Term.matchAlt \"|\" (null (Term.hole \"_\")) \"=>\" (Term.num (numLit \"2\")))]"
-"#[(Term.matchAlt \"|\" (null (Term.id `a._@.UnhygienicMain._hyg.1 (null))) \"=>\" (Term.num (numLit \"1\"))), (Term.matchAlt \"|\" (null (Term.hole \"_\")) \"=>\" (Term.num (numLit \"2\")))]"
+"#[]"
+StxQuot.lean:40:74: error: expected '⇒', '=>'