From f95a450894d28cfe04780124a33cee5cd6943113 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Mon, 14 Dec 2020 15:05:39 -0800
Subject: [PATCH] feat: add builtin prec/prio parsers

---
 src/Init/Meta.lean          | 2 +-
 src/Init/Notation.lean      | 5 ++---
 src/Lean/Parser/Syntax.lean | 5 +++++
 3 files changed, 8 insertions(+), 4 deletions(-)

diff --git a/src/Init/Meta.lean b/src/Init/Meta.lean
index a85559992f..75ccba4825 100644
--- a/src/Init/Meta.lean
+++ b/src/Init/Meta.lean
@@ -635,7 +635,7 @@ instance Option.hasQuote {α : Type} [Quote α] : Quote (Option α) where
 
 /- Evaluator for `prec` DSL -/
 partial def evalPrec : Syntax → MacroM Nat
-  | `(prec| $num:numLit) => return num.isNatLit?.getD 0
+--  | `(prec| $num:numLit) => return num.isNatLit?.getD 0
   | `(prec| $a + $b) => return (← evalPrec a) + (← evalPrec b)
   | `(prec| $a - $b) => return (← evalPrec a) - (← evalPrec b)
   | prec => Macro.withIncRecDepth prec do
diff --git a/src/Init/Notation.lean b/src/Init/Notation.lean
index dbb1b55a5d..492026f42c 100644
--- a/src/Init/Notation.lean
+++ b/src/Init/Notation.lean
@@ -12,14 +12,13 @@ import Init.Prelude
 
 namespace Lean.Parser.Syntax
 
-syntax [numPrec] num : prec
 syntax:65 [addPrec] prec " + " prec:66 : prec
 syntax:65 [subPrec] prec " - " prec:66 : prec
 
 end Lean.Parser.Syntax
 
-macro "max"  : prec => `(1024)
-macro "lead" : prec => `(1023)
+-- macro "max"  : prec => `(1024)
+-- macro "lead" : prec => `(1023)
 macro "(" p:prec ")" : prec => p
 
 -- Basic notation for defining parsers
diff --git a/src/Lean/Parser/Syntax.lean b/src/Lean/Parser/Syntax.lean
index a260cd3922..a60dfe1563 100644
--- a/src/Lean/Parser/Syntax.lean
+++ b/src/Lean/Parser/Syntax.lean
@@ -37,6 +37,11 @@ def «precedence» := parser! ":" >> precedenceLit
 def optPrecedence := optional (atomic «precedence»)
 
 namespace Syntax
+@[builtinPrecParser] def numPrec := checkPrec maxPrec >> numLit
+
+@[builtinPrioParser] def numPrio  := checkPrec maxPrec >> numLit
+@[builtinPrioParser] def highPrio := parser!:maxPrec nonReservedSymbol "high" true
+
 @[builtinSyntaxParser] def paren           := parser! "(" >> many1 syntaxParser >> ")"
 @[builtinSyntaxParser] def cat             := parser! ident >> optPrecedence
 @[builtinSyntaxParser] def unary           := parser! ident >> checkNoWsBefore >> "(" >> many1 syntaxParser >> ")"