From 7d1d7dc1710804e4d2b5b4eabe7dd716f4080371 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Mon, 14 Dec 2020 13:25:08 -0800
Subject: [PATCH] feat: `prec` DSL

---
 src/Init/Meta.lean     | 15 +++++++++++++++
 src/Init/Notation.lean |  9 +++++++++
 2 files changed, 24 insertions(+)

diff --git a/src/Init/Meta.lean b/src/Init/Meta.lean
index 540412f169..a85559992f 100644
--- a/src/Init/Meta.lean
+++ b/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
diff --git a/src/Init/Notation.lean b/src/Init/Notation.lean
index c694d61633..6c32ccb380 100644
--- a/src/Init/Notation.lean
+++ b/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