From 99fad9fc4de4b1a534fca9d5d000690d42fc4f2a Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Sat, 14 Nov 2020 07:32:44 -0800
Subject: [PATCH] feat: goodies for writing notation with binders

---
 src/Init.lean                      |  1 +
 src/Init/NotationExtra.lean        | 67 ++++++++++++++++++++++++++++++
 tests/lean/run/binderNotation.lean | 16 +++++++
 3 files changed, 84 insertions(+)
 create mode 100644 src/Init/NotationExtra.lean
 create mode 100644 tests/lean/run/binderNotation.lean

diff --git a/src/Init.lean b/src/Init.lean
index fb942e2302..cf76308fb6 100644
--- a/src/Init.lean
+++ b/src/Init.lean
@@ -16,3 +16,4 @@ import Init.Util
 import Init.Fix
 import Init.Meta
 import Init.Tactics
+import Init.NotationExtra
diff --git a/src/Init/NotationExtra.lean b/src/Init/NotationExtra.lean
new file mode 100644
index 0000000000..db24b1a5b7
--- /dev/null
+++ b/src/Init/NotationExtra.lean
@@ -0,0 +1,67 @@
+/-
+Copyright (c) 2020 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Leonardo de Moura
+
+Extra notation that depends on Init/Meta
+-/
+prelude
+import Init.Meta
+
+namespace Lean
+-- Auxiliary parsers and functions for declaring notation with binders
+
+syntax binderIdent                := ident <|> "_"
+syntax unbracktedExplicitBinders  := binderIdent+ (" : " term)?
+syntax bracketedExplicitBinders   := "(" binderIdent+ " : " term ")"
+syntax explicitBinders            := bracketedExplicitBinders+ <|> unbracktedExplicitBinders
+
+def expandExplicitBindersAux (combinator : Syntax) (idents : Array Syntax) (type? : Option Syntax) (body : Syntax) : MacroM Syntax :=
+  let rec loop (i : Nat) (acc : Syntax) := do
+    match i with
+    | 0   => pure acc
+    | i+1 =>
+      let ident := idents[i][0]
+      let acc ← match ident.isIdent, type? with
+        | true,  none      => `($combinator fun $ident => $acc)
+        | true,  some type => `($combinator fun $ident:ident : $type => $acc)
+        | false, none      => `($combinator fun _ => $acc)
+        | false, some type => `($combinator fun _ : $type => $acc)
+      loop i (acc.copyInfo (← getRef))
+  loop idents.size body
+
+def expandBrackedBindersAux (combinator : Syntax) (binders : Array Syntax) (body : Syntax) : MacroM Syntax :=
+  let rec loop (i : Nat) (acc : Syntax) := do
+    match i with
+    | 0   => pure acc
+    | i+1 =>
+      let idents := binders[i][1].getArgs
+      let type   := binders[i][3]
+      loop i (← expandExplicitBindersAux combinator idents (some type) acc)
+  loop binders.size body
+
+def expandExplicitBinders (combinatorDeclName : Name) (explicitBinders : Syntax) (body : Syntax) : MacroM Syntax := do
+  let combinator := mkIdentFrom (← getRef) combinatorDeclName
+  let explicitBinders := explicitBinders[0]
+  if explicitBinders.getKind == `Lean.unbracktedExplicitBinders then
+    let idents   := explicitBinders[0].getArgs
+    let type? := if explicitBinders[1].isNone then none else some explicitBinders[1][1]
+    expandExplicitBindersAux combinator idents type? body
+  else if explicitBinders.getArgs.all (·.getKind == `Lean.bracketedExplicitBinders) then
+    expandBrackedBindersAux combinator explicitBinders.getArgs body
+  else
+    Macro.throwError "unexpected explicit binder"
+
+def expandBrackedBinders (combinatorDeclName : Name) (bracketedExplicitBinders : Syntax) (body : Syntax) : MacroM Syntax := do
+  let combinator := mkIdentFrom (← getRef) combinatorDeclName
+  expandBrackedBindersAux combinator #[bracketedExplicitBinders] body
+
+end Lean
+
+open Lean
+
+macro "∃"  xs:explicitBinders ", " b:term : term => expandExplicitBinders `Exists xs b
+macro "Σ"  xs:explicitBinders ", " b:term : term => expandExplicitBinders `Sigma xs b
+macro "Σ'" xs:explicitBinders ", " b:term : term => expandExplicitBinders `PSigma xs b
+macro:25 xs:bracketedExplicitBinders "×" b:term : term => expandBrackedBinders `Sigma xs b
+macro:25 xs:bracketedExplicitBinders "×'" b:term : term => expandBrackedBinders `PSigma xs b
diff --git a/tests/lean/run/binderNotation.lean b/tests/lean/run/binderNotation.lean
new file mode 100644
index 0000000000..195aae9ef7
--- /dev/null
+++ b/tests/lean/run/binderNotation.lean
@@ -0,0 +1,16 @@
+#check ∃ x, x > 1
+#check ∃ (x y : Nat), x > y
+#check ∃ x y : Nat, x > y
+#check ∃ (x : Nat) (y : Nat), x > y
+
+theorem ex1 : (∃ x y : Nat, x > y) = (∃ (x : Nat) (y : Nat), x > y) := rfl
+
+abbrev Vector α n := { a : Array α // a.size = n }
+
+#check Σ α n, Vector α n
+#check Σ (α : Type) (n : Nat), Vector α n
+#check (α : Type) × (n : Nat) × Vector α n
+
+#check Σ' α n, Vector α n
+#check Σ' (α : Type) (n : Nat), Vector α n
+#check (α : Type) ×' (n : Nat) ×' Vector α n