From 794edcb18c7f470df7fa612679010995413d9b47 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Fri, 5 Jul 2019 18:31:03 -0700
Subject: [PATCH] chore(library/init/lean/parser): minor modifications

---
 library/init/lean/parser/parser.lean | 17 ++++++++++++-----
 library/init/lean/parser/term.lean   |  4 ++--
 2 files changed, 14 insertions(+), 7 deletions(-)

diff --git a/library/init/lean/parser/parser.lean b/library/init/lean/parser/parser.lean
index 8b2bb69840..1471bf60f6 100644
--- a/library/init/lean/parser/parser.lean
+++ b/library/init/lean/parser/parser.lean
@@ -728,11 +728,14 @@ def symbolInfo (sym : String) (lbp : Option Nat) : ParserInfo :=
 @[inline] def symbolFn {k : ParserKind} (sym : String) : ParserFn k :=
 fun _ => symbolFnAux sym ("expected '" ++ sym ++ "'")
 
-@[inline] def symbol {k : ParserKind} (sym : String) (lbp : Option Nat := none) : Parser k :=
+@[inline] def symbolAux {k : ParserKind} (sym : String) (lbp : Option Nat := none) : Parser k :=
 let sym := sym.trim;
 { info := symbolInfo sym lbp,
   fn   := symbolFn sym }
 
+@[inline] def symbol {k : ParserKind} (sym : String) (lbp : Nat) : Parser k :=
+symbolAux sym lbp
+
 partial def strAux (sym : String) (errorMsg : String) : Nat → BasicParserFn
 | j c s :=
   if sym.atEnd j then s
@@ -757,11 +760,14 @@ fun leading c s =>
 symbolNoWsFnAux sym ("expected '" ++ sym ++ "' without whitespaces arount it")
 
 /- Similar to `symbol`, but succeeds only if there is no space whitespace after leading term and after `sym`. -/
-@[inline] def symbolNoWs (sym : String) (lbp : Option Nat := none) : TrailingParser :=
+@[inline] def symbolNoWsAux (sym : String) (lbp : Option Nat) : TrailingParser :=
 let sym := sym.trim;
 { info := symbolInfo sym lbp,
   fn   := symbolNoWsFn sym }
 
+@[inline] def symbolNoWs (sym : String) (lbp : Nat) : TrailingParser :=
+symbolNoWsAux sym lbp
+
 def unicodeSymbolFnAux (sym asciiSym : String) (errorMsg : String) : BasicParserFn :=
 satisfySymbolFn (fun s => s == sym || s == asciiSym) errorMsg
 
@@ -824,7 +830,7 @@ fun c s =>
   info := mkAtomicInfo "fieldIdx" }
 
 instance string2basic {k : ParserKind} : HasCoe String (Parser k) :=
-⟨symbol⟩
+⟨symbolAux⟩
 
 namespace ParserState
 
@@ -953,7 +959,8 @@ match stx with
   | (_, some tk) => (s, tk.lbp.getOrElse 0)
   | _            => (s, 0)
 | some (Syntax.ident _ _ _ _ _) => (s, maxPrec)
-| some (Syntax.node k _ _)      => if k == numLitKind || k == strLitKind then (s, maxPrec) else (s, 0)
+-- TODO(Leo): add support for associating lbp with syntax node kinds.
+| some (Syntax.node k _ _)      => if k == numLitKind || k == strLitKind || k == fieldIdxKind then (s, maxPrec) else (s, 0)
 | _                             => (s, 0)
 
 def indexed {α : Type} (map : TokenMap α) (c : ParserContext) (s : ParserState) : ParserState × List α :=
@@ -990,7 +997,7 @@ partial def trailingLoop (kind : String) (tables : ParsingTables) (rbp : Nat) (c
     let iniSz   := s.stackSize;
     let (s, ps) := indexed tables.trailingTable c s;
     if ps.isEmpty && tables.trailingParsers.isEmpty then
-      s.pushSyntax left -- no available trail
+      s.pushSyntax left -- no available trailing parser
     else
       let s := orelseFn (longestMatchFn ps) (anyOfFn tables.trailingParsers) left c s;
       if s.hasError then s
diff --git a/library/init/lean/parser/term.lean b/library/init/lean/parser/term.lean
index 2bcbab2743..c5d8dcb3c2 100644
--- a/library/init/lean/parser/term.lean
+++ b/library/init/lean/parser/term.lean
@@ -31,7 +31,7 @@ namespace Term
 @[builtinTermParser] def cdot := parser! symbol "·" maxPrec
 @[inline] def parenSpecial : Parser := optional (", " >> sepBy termParser ", " <|> " : " >> termParser)
 @[builtinTermParser] def paren := parser! symbol "(" maxPrec >> optional (termParser >> parenSpecial) >> ")"
-@[builtinTermParser] def anonymousCtor := parser! symbol "⟨" maxPrec >> sepBy1 termParser ", " >> symbol "⟩"
+@[builtinTermParser] def anonymousCtor := parser! symbol "⟨" maxPrec >> sepBy1 termParser ", " >> "⟩"
 @[inline] def optIdent : Parser := optional (try (ident >> " : "))
 @[builtinTermParser] def «if»  := parser! "if " >> optIdent >> termParser >> " then " >> termParser >> " else " >> termParser
 def fromTerm   := parser! " from " >> termParser
@@ -49,7 +49,7 @@ def optType : Parser := optional typeSpec
 @[builtinTermParser] def list := parser! symbol "[" maxPrec >> sepBy termParser "," true >> "]"
 
 @[builtinTermParser] def app  := tparser! pushLeading >> termParser maxPrec
-@[builtinTermParser] def proj := tparser! pushLeading >> symbolNoWs "." (some (maxPrec+1)) >> (fieldIdx <|> ident)
+@[builtinTermParser] def proj := tparser! pushLeading >> symbolNoWs "." (maxPrec+1) >> (fieldIdx <|> ident)
 
 end Term