feat: prec DSL

src/Init/Meta.lean

@@ -633,6 +633,21 @@ private def quoteOption {α : Type} [Quote α] : Option α → Syntax
 instance Option.hasQuote {α : Type} [Quote α] : Quote (Option α) where
   quote := quoteOption
 
+/- Evaluator for `prec` DSL -/
+partial def evalPrec : Syntax → MacroM Nat
+  | `(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
+    if prec.getKind == choiceKind then
+      evalPrec prec[0]
+    else
+      match (← expandMacro? prec) with
+      | some prec => evalPrec prec
+      | _ =>  Macro.throwErrorAt prec "unexpected precedence"
+
+macro "evalPrec! " p:prec:max : term => return quote (← evalPrec p)
+
 end Lean
 
 namespace Array

src/Init/Notation.lean

@@ -8,6 +8,15 @@ Notation for operators defined at Prelude.lean
 prelude
 import Init.Prelude
 
+-- DSL for specifying parser precedences
+syntax ident : prec
+syntax num : prec
+syntax:65 prec " + " prec:66 : prec
+syntax:65 prec " - " prec:66 : prec
+macro "max"  : prec => `(1024)
+macro "lead" : prec => `(1023)
+macro "(" p:prec ")" : prec => p
+
 -- Basic notation for defining parsers
 syntax   stx "+" : stx
 syntax   stx "*" : stx