From eb8e7b9f3d0badc9cf57cd888cbaef75e031848a Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sat, 25 Jan 2020 16:15:30 -0800 Subject: [PATCH] feat: add new `let` syntax 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 --- src/Init/Lean/Parser/Term.lean | 13 +++++++------ 1 file changed, 7 insertions(+), 6 deletions(-) diff --git a/src/Init/Lean/Parser/Term.lean b/src/Init/Lean/Parser/Term.lean index 6fe74ac98b..e13a0222b6 100644 --- a/src/Init/Lean/Parser/Term.lean +++ b/src/Init/Lean/Parser/Term.lean @@ -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