max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

chore: add let+patterns case

Browse source 
@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.
This commit is contained in:
Leonardo de Moura 2020-08-16 15:41:53 -07:00
parent fdd8978bfe
commit 0064f7d2b9
1 changed files with 8 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

8
src/Lean/Elab/Binders.lean
View file

@ -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?