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

feat: add new let syntax

Browse source 
It avoids hidden nonterminals, and store the equation case as a
separate rule. It would be great if we could have 3 independent rules,
but this is not possible because `longestMatch` would return a choice
for terms as simple as `let x := v; ...` The problem is that it is
both a `letSimpleDecl` and a `letPatDecl`. We resolve the ambiguity at
the parsing level using `<|>`.

cc @Kha
This commit is contained in:
Leonardo de Moura 2020-01-25 16:15:30 -08:00
parent 31f8b281c2
commit eb8e7b9f3d
1 changed files with 7 additions and 6 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

13
src/Init/Lean/Parser/Term.lean
View file

@ -91,13 +91,14 @@ def matchAlt := parser! " | " >> sepBy1 termParser ", " >> darrow >> termParser
@[builtinTermParser] def «match_syntax» := parser! "match_syntax" >> termParser >> " with " >> many1Indent matchAlt "'match_syntax' alternatives must be indented"
/- 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 bracktedBinder >> optType
def letIdDecl := parser! try (letIdLhs >> " := ") >> termParser
def letIdLhs : Parser := ident >> checkWsBefore "expected space before binders" >> many bracktedBinder >> optType
def letSimpleDecl : Parser := try (letIdLhs >> " := ") >> termParser
def letPatDecl : Parser := termParser >> optType >> " := " >> termParser
@[builtinTermParser] def letDecl := parser! "let " >> (letSimpleDecl <|> letPatDecl) >> "; " >> termParser
def equation := matchAlt
def letEqns := parser! try (letIdLhs >> lookahead " | ") >> many1Indent equation "equations must be indented"
def letPatDecl := parser! termParser >> optType >> " := " >> termParser
def letDecl := try letIdDecl <|> letEqns <|> letPatDecl
@[builtinTermParser] def «let» := parser! "let " >> letDecl >> "; " >> termParser
@[builtinTermParser] def letEqns :=
parser! "let " >> letIdLhs >> many1Indent equation "equations must be indented"
@[builtinTermParser] def «let_core» := parser! "let_core " >> termParser >> ":=" >> termParser >> "; " >> termParser