From 0064f7d2b9c68fcdaeb8023ba8c2c4470b481afb Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Sun, 16 Aug 2020 15:41:53 -0700
Subject: [PATCH] chore: add `let+patterns` case

@Kha the patterns at `Binders.lean` for let-expressions are not matched correctly by
`match_syntax`. The problem is that we "reuse" kinds here:
```lean
def letIdDecl   : Parser := nodeWithAntiquot "letDecl" `Lean.Parser.Term.letDecl $ try (letIdLhs >> " := ") >> termParser
def letPatDecl  : Parser := node `Lean.Parser.Term.letDecl $ try (termParser >> pushNone >> optType >> " := ") >> termParser
def letEqnsDecl : Parser := node `Lean.Parser.Term.letDecl $ letIdLhs >> matchAlts false
def letDecl              := letIdDecl <|> letPatDecl <|> letEqnsDecl
```
This is a bad hack for implementing the `where` macro. I will remove it, and rewrite the code above as
```lean
def letIdDecl   := parser! try (letIdLhs >> " := ") >> termParser
def letPatDecl  := parser! try (termParser >> pushNone >> optType >> " := ") >> termParser
def letEqnsDecl := parser! letIdLhs >> matchAlts false
def letDecl     := parser! letIdDecl <|> letPatDecl <|> letEqnsDecl
```
Remark: we need the `letDecl` kind to be able to implement the `where`
macro.
I will do it tomorrow because it is a staging nightmare.
---
 src/Lean/Elab/Binders.lean | 8 ++++++++
 1 file changed, 8 insertions(+)

diff --git a/src/Lean/Elab/Binders.lean b/src/Lean/Elab/Binders.lean
index 79b4ef1c53..583147b66d 100644
--- a/src/Lean/Elab/Binders.lean
+++ b/src/Lean/Elab/Binders.lean
@@ -422,6 +422,10 @@ fun stx expectedType? => match_syntax stx with
    elabLetDeclAux id.getId args (mkHole stx) val body expectedType? true
 | `(let $id:ident $args* : $type := $val; $body) =>
    elabLetDeclAux id.getId args type val body expectedType? true
+| `(let $id:ident $args* | $alts:matchAlt*; $body) =>
+  throwError "invalid let-expression with pattern matching, type must be provided"
+| `(let $id:ident $args* : $type | $alts:matchAlt*; $body) =>
+  throwError "WIP" -- TODO
 | `(let $pat:term := $val; $body) => do
    stxNew ← `(let x := $val; match x with $pat => $body);
    withMacroExpansion stx stxNew $ elabTerm stxNew expectedType?
@@ -436,6 +440,10 @@ fun stx expectedType? => match_syntax stx with
    elabLetDeclAux id.getId args (mkHole stx) val body expectedType? false
 | `(let! $id:ident $args* : $type := $val; $body) =>
    elabLetDeclAux id.getId args type val body expectedType? false
+| `(let! $id:ident $args* | $alts:matchAlt*; $body) =>
+  throwError "invalid let-expression with pattern matching, type must be provided"
+| `(let! $id:ident $args* : $type | $alts:matchAlt*; $body) =>
+  throwError "WIP" -- TODO
 | `(let! $pat:term := $val; $body) => do
    stxNew ← `(let! x := $val; match x with $pat => $body);
    withMacroExpansion stx stxNew $ elabTerm stxNew expectedType?