From b3b2a07ed0ebfd8459ff64303abcab8d5dabb1a1 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Mon, 25 Jul 2022 18:19:32 -0700
Subject: [PATCH] feat: support dotted notation and named arguments in patterns

---
 RELEASES.md                                   |  8 ++++++++
 src/Lean/Elab/PatternVar.lean                 |  7 ++++---
 tests/lean/run/dottedCtorNamedArgPattern.lean | 17 +++++++++++++++++
 3 files changed, 29 insertions(+), 3 deletions(-)
 create mode 100644 tests/lean/run/dottedCtorNamedArgPattern.lean

diff --git a/RELEASES.md b/RELEASES.md
index b02cff5e04..794717a7d0 100644
--- a/RELEASES.md
+++ b/RELEASES.md
@@ -1,6 +1,14 @@
 Unreleased
 ---------
 
+* Support dotted notation and named arguments in patterns. Example:
+  ```lean
+  def getForallBinderType (e : Expr) : Expr :=
+    match e with
+    | .forallE (binderType := type) .. => type
+    | _ => panic! "forall expected"
+  ```
+
 * "jump-to-definition" now works for function names embedded in the following attributes
   `@[implementedBy funName]`, `@[tactic parserName]`, `@[termElab parserName]`, `@[commandElab parserName]`,
   `@[builtinTactic parserName]`, `@[builtinTermElab parserName]`, and `@[builtinCommandElab parserName]`.
diff --git a/src/Lean/Elab/PatternVar.lean b/src/Lean/Elab/PatternVar.lean
index db85be5760..07f8e9bf96 100644
--- a/src/Lean/Elab/PatternVar.lean
+++ b/src/Lean/Elab/PatternVar.lean
@@ -219,12 +219,13 @@ where
   processCtorApp (stx : Syntax) : M Syntax := do
     let (f, namedArgs, args, ellipsis) ← expandApp stx true
     if f.getKind == ``Parser.Term.dotIdent then
-      unless namedArgs.isEmpty do
-        throwError "invalid dotted notation in a pattern, named arguments are not supported yet"
+      let namedArgsNew ← namedArgs.mapM fun
+        | { ref, name, val := Arg.stx arg } => withRef ref do `(Lean.Parser.Term.namedArgument| ($(mkIdentFrom ref name) := $(← collect arg)))
+        | _ => unreachable!
       let mut argsNew ← args.mapM fun | Arg.stx arg => collect arg | _ => unreachable!
       if ellipsis then
         argsNew := argsNew.push (mkNode ``Parser.Term.ellipsis #[mkAtomFrom stx ".."])
-      return Syntax.mkApp f argsNew
+      return Syntax.mkApp f (namedArgsNew ++ argsNew)
     else
       processCtorAppCore f namedArgs args ellipsis
 
diff --git a/tests/lean/run/dottedCtorNamedArgPattern.lean b/tests/lean/run/dottedCtorNamedArgPattern.lean
new file mode 100644
index 0000000000..7f75b9aec9
--- /dev/null
+++ b/tests/lean/run/dottedCtorNamedArgPattern.lean
@@ -0,0 +1,17 @@
+import Lean
+
+def f (x : Nat × Nat) :=
+  match x with
+  | .mk (snd := snd) .. => snd
+
+example : f (10, 20) = 20 := rfl
+
+open Lean
+def g (e : Expr) : Expr :=
+  match e with
+  | .forallE (binderType := type) .. => type
+  | e => e
+
+def h (x : Nat × Nat) :=
+  match x with
+  | .mk (α := .(Nat)) (snd := snd) .. => snd