From cae6aa95dcda0e8cc3608ea1577efd3a2ce1fbbb Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Thu, 12 Nov 2020 13:25:38 -0800
Subject: [PATCH] feat: support `simpleBinder` at `letDecl`

---
 src/Lean/Parser/Do.lean          |  6 +++++-
 src/Lean/Parser/Term.lean        |  2 +-
 tests/lean/run/depElim1.lean     | 16 +++++++++-------
 tests/lean/run/newfrontend1.lean | 10 ++++++++++
 4 files changed, 25 insertions(+), 9 deletions(-)

diff --git a/src/Lean/Parser/Do.lean b/src/Lean/Parser/Do.lean
index 32afe9ecd6..f9152d859d 100644
--- a/src/Lean/Parser/Do.lean
+++ b/src/Lean/Parser/Do.lean
@@ -32,7 +32,11 @@ def doIdDecl   := parser! «try» (ident >> optType >> leftArrow) >> doElemParse
 def doPatDecl  := parser! «try» (termParser >> leftArrow) >> doElemParser >> optional (" | " >> doElemParser)
 @[builtinDoElemParser] def doLetArrow      := parser! "let " >> optional "mut " >> (doIdDecl <|> doPatDecl)
 
-@[builtinDoElemParser] def doReassign      := parser! notFollowedByRedefinedTermToken >> (letIdDecl <|> letPatDecl)
+-- We use `letIdDeclNoBinders` to define `doReassign`.
+-- Motivation: we do not reassign functions, and avoid parser conflict
+def letIdDeclNoBinders := node `Lean.Parser.Term.letIdDecl $ «try» (ident >> pushNone >> optType >> " := ") >> termParser
+
+@[builtinDoElemParser] def doReassign      := parser! notFollowedByRedefinedTermToken >> (letIdDeclNoBinders <|> letPatDecl)
 @[builtinDoElemParser] def doReassignArrow := parser! notFollowedByRedefinedTermToken >> (doIdDecl <|> doPatDecl)
 @[builtinDoElemParser] def doHave     := parser! "have " >> Term.haveDecl
 /-
diff --git a/src/Lean/Parser/Term.lean b/src/Lean/Parser/Term.lean
index c7273e5b7d..2d303a59bb 100644
--- a/src/Lean/Parser/Term.lean
+++ b/src/Lean/Parser/Term.lean
@@ -150,7 +150,7 @@ def optExprPrecedence := optional («try» ":" >> termParser maxPrec)
 @[builtinTermParser] def «match_syntax» := parser!:leadPrec "match_syntax" >> termParser >> " with " >> matchAlts
 
 /- Remark: we use `checkWsBefore` to ensure `let x[i] := e; b` is not parsed as `let x [i] := e; b` where `[i]` is an `instBinder`. -/
-def letIdLhs    : Parser := ident >> checkWsBefore "expected space before binders" >> many (ppSpace >> bracketedBinder) >> optType
+def letIdLhs    : Parser := ident >> checkWsBefore "expected space before binders" >> many (ppSpace >> (simpleBinder <|> bracketedBinder)) >> optType
 def letIdDecl   := node `Lean.Parser.Term.letIdDecl   $ «try» (letIdLhs >> " := ") >> termParser
 def letPatDecl  := node `Lean.Parser.Term.letPatDecl  $ «try» (termParser >> pushNone >> optType >> " := ") >> termParser
 def letEqnsDecl := node `Lean.Parser.Term.letEqnsDecl $ letIdLhs >> matchAlts false
diff --git a/tests/lean/run/depElim1.lean b/tests/lean/run/depElim1.lean
index e6dd22639b..de31858848 100644
--- a/tests/lean/run/depElim1.lean
+++ b/tests/lean/run/depElim1.lean
@@ -243,11 +243,11 @@ def ex6 (α : Type u) (n : Nat) (xs : Vec α n) :
 × LHS (forall (N : Nat) (XS : Vec α N), Pat (inaccessible N) × Pat XS) :=
 arbitrary _
 
-set_option trace.Meta.Match.match true
-set_option trace.Meta.Match.debug true
+-- set_option trace.Meta.Match.match true
+-- set_option trace.Meta.Match.debug true
 
 #eval test `ex6 2 `elimTest6
-#print elimTest6
+-- #print elimTest6
 
 def ex7 (α : Type u) (n : Nat) (xs : Vec α n) :
   LHS (forall (a : α), Pat (inaccessible 1) × Pat (Vec.cons a Vec.nil))
@@ -255,7 +255,7 @@ def ex7 (α : Type u) (n : Nat) (xs : Vec α n) :
 arbitrary _
 
 #eval test `ex7 2 `elimTest7
-#check elimTest7
+-- #check elimTest7
 
 def isSizeOne {n : Nat} (xs : Vec Nat n) : Bool :=
 elimTest7 _ (fun _ _ => Bool) n xs (fun _ => true) (fun _ _ => false)
@@ -351,7 +351,7 @@ def ex14 (x y : Nat) :
 × LHS (forall (x y : Nat), Pat x × Pat y) :=
 arbitrary _
 
-set_option trace.Meta.Match true
+-- set_option trace.Meta.Match true
 
 #eval test `ex14 2 `elimTest14
 #print elimTest14
@@ -372,7 +372,7 @@ def ex15 (xs : Array (List Nat)) :
 arbitrary _
 
 #eval test `ex15 1 `elimTest15
-#check elimTest15
+-- #check elimTest15
 
 def h3 (xs : Array (List Nat)) : Nat :=
 elimTest15 (fun _ => Nat) xs
@@ -393,9 +393,11 @@ arbitrary _
 
 #eval test `ex16 1 `elimTest16
 
-#check elimTest16
+-- #check elimTest16
 #print elimTest16
 
+
+
 def h4 (xs : List Nat) : List Nat :=
 elimTest16 (fun _ => List Nat) xs
   (fun a xs b ys => xs)
diff --git a/tests/lean/run/newfrontend1.lean b/tests/lean/run/newfrontend1.lean
index 3b6a4610f8..b1eeaac621 100644
--- a/tests/lean/run/newfrontend1.lean
+++ b/tests/lean/run/newfrontend1.lean
@@ -361,3 +361,13 @@ theorem simple24 (x y z : Nat) : y = z → x = x → y = x → x = z :=
 fun h1 _ h3 =>
   have h : x = y by apply Eq.symm; assumption
   Eq.trans h (by assumption)
+
+def f1 (x : Nat) : Nat :=
+  let double x := x + x
+  let rec loop x :=
+    match x with
+    | 0   => 0
+    | x+1 => loop x + double x
+  loop x
+
+#eval f1 5