feat(library/init/lean/parser/command): add (some) notation commands

library/init/lean/parser/command.lean

@@ -85,6 +85,23 @@ def openRenamingItem := parser! ident >> unicodeSymbol "→" "->" >> ident
 def openRenaming     := parser! try ("(" >> "renaming") >> sepBy1 openRenamingItem ", " >> ")"
 @[builtinCommandParser] def «open»       := parser! "open " >> ident >> optional openOnly >> optional openRenaming >> optional openHiding
 
+/- Lean3 command declaration commands -/
+def maxPrec := parser! "max"
+def precedenceLit : Parser := numLit <|> maxPrec
+def «precedence» := parser! " : " >> precedenceLit
+def quotedSymbolPrec := parser! quotedSymbol >> optional «precedence»
+def symbol : Parser := quotedSymbolPrec <|> unquotedSymbol
+def «prefix»   := parser! "prefix"
+def «infix»    := parser! "infix"
+def «infixl»   := parser! "infixl"
+def «infixr»   := parser! "infixr"
+def «postfix»  := parser! "postfix"
+def mixfixKind := «prefix» <|> «infix» <|> «infixl» <|> «infixr» <|> «postfix»
+@[builtinCommandParser] def «reserve»  := parser! "reserve " >> mixfixKind >> quotedSymbolPrec
+def mixfixSymbol := quotedSymbolPrec <|> unquotedSymbol
+@[builtinCommandParser] def «mixfix»   := parser! mixfixKind >> mixfixSymbol >> " := " >> termParser
+@[builtinCommandParser] def «notation» := parser! "notation" >> quotedSymbol
+
 end Command
 end Parser
 end Lean

library/init/lean/parser/parser.lean

@@ -492,6 +492,9 @@ private def rawAux {k : ParserKind} (startPos : Nat) (trailingWs : Bool) : Parse
   let s := p a c s;
   if s.hasError then s else rawAux startPos trailingWs a c s
 
+@[inline] def chFn {k : ParserKind} (c : Char) (trailingWs := false) : ParserFn k :=
+rawFn (fun _ => satisfyFn (fun d => c == d) ("expected '" ++ toString c ++ "'")) trailingWs
+
 def hexDigitFn : BasicParserFn
 | c s :=
   let input := c.input;
@@ -906,7 +909,25 @@ fun _ c s =>
   info := mkAtomicInfo "ident" }
 
 @[inline] def rawIdent {k : ParserKind} : Parser k :=
-{ fn   := fun _ => rawIdentFn }
+{ fn := fun _ => rawIdentFn }
+
+def quotedSymbolFn {k : ParserKind} : ParserFn k :=
+nodeFn `quotedSymbol (andthenFn (andthenFn (chFn '`') (rawFn (fun _ => takeUntilFn (fun c => c == '`')))) (chFn '`' true))
+
+def quotedSymbol {k : ParserKind} : Parser k :=
+{ fn := quotedSymbolFn }
+
+def unquotedSymbolFn {k : ParserKind} : ParserFn k :=
+fun _ c s =>
+  let iniPos := s.pos;
+  let s      := tokenFn c s;
+  if s.hasError || s.stxStack.back.isIdent || s.stxStack.back.isOfKind strLitKind || s.stxStack.back.isOfKind numLitKind then
+    s.mkErrorAt "expected symbol" iniPos
+  else
+    s
+
+def unquotedSymbol {k : ParserKind} : Parser k :=
+{ fn := unquotedSymbolFn }
 
 def fieldIdxFn : BasicParserFn :=
 fun c s =>

tests/playground/cmdparsertest1.lean

@@ -29,5 +29,9 @@ test [
 ",
 "local attribute [instance] foo bla",
 "attribute [inline] test",
-"open Lean (hiding Name)"
+"open Lean (hiding Name)",
+"notation ` + `",
+"reserve infixr ` ∨ `:30",
+"reserve prefix `¬`:40",
+"infixr ` ^ ` := HasPow.pow"
 ]