feat: prio DSL

src/Init/Meta.lean

@@ -652,6 +652,14 @@ def evalOptPrec : Option Syntax → MacroM Nat
   | some prec => evalPrec prec
   | none      => return 0
 
+def evalPrio (stx : Syntax) : MacroM Nat :=
+  evalPrec stx
+
+macro "evalPrio! " p:prio:max : term => return quote (← evalPrio p)
+
+def evalOptPrio (stx : Option Syntax) : MacroM Nat :=
+  evalOptPrec stx
+
 end Lean
 
 namespace Array

src/Init/Notation.lean

@@ -8,19 +8,27 @@ Notation for operators defined at Prelude.lean
 prelude
 import Init.Prelude
 
--- DSL for specifying parser precedences
+-- DSL for specifying parser precedences and priorities
 
 namespace Lean.Parser.Syntax
 
 syntax:65 [addPrec] prec " + " prec:66 : prec
 syntax:65 [subPrec] prec " - " prec:66 : prec
 
+syntax:65 [addPrio] prio " + " prio:66 : prio
+syntax:65 [subPrio] prio " - " prio:66 : prio
+
 end Lean.Parser.Syntax
 
 macro "max"  : prec => `(1024)
 macro "lead" : prec => `(1023)
 macro "(" p:prec ")" : prec => p
 
+macro "default" : prio => `(1000)
+macro "low" : prio => `(100)
+macro "(" p:prio ")" : prio => p
+macro_rules | `(prio| high) => `(10000) -- the 'high' parser is builtin because it is used at `Prelude.lean`
+
 -- Basic notation for defining parsers
 syntax   stx "+" : stx
 syntax   stx "*" : stx