feat: inferring namespace from expected type a la Swift

Now that `PatternVars.lean` has been redesigned, it is feasible to
implement issue #944.

closes #944

RELEASES.md

@@ -188,3 +188,28 @@ def head2 (x : Vector α (n+1)) : α :=
   match x with
   | a :: as => a -- `::` is `Vector.cons` here
 ```
+
+* New notation `.<identifier>` based on Swift. The namespace is inferred from the expected type. Examples:
+```lean
+def f (x : Nat) : Except String Nat :=
+  if x > 0 then
+    .ok x
+  else
+    .error "x is zero"
+
+namespace Lean.Elab
+open Lsp
+
+def identOf : Info → Option (RefIdent × Bool)
+  | .ofTermInfo ti => match ti.expr with
+    | .const n .. => some (.const n, ti.isBinder)
+    | .fvar id .. => some (.fvar id, ti.isBinder)
+    | _ => none
+  | .ofFieldInfo fi => some (.const fi.projName, false)
+  | _ => none
+
+def isImplicit (bi : BinderInfo) : Bool :=
+  bi matches .implicit
+
+end Lean.Elab
+```

src/Lean/Elab/App.lean

@@ -820,7 +820,7 @@ where
     | field::fields, false => LVal.fieldName field field.getId.toString none fIdent :: toLVals fields false
 
 private partial def elabAppFn (f : Syntax) (lvals : List LVal) (namedArgs : Array NamedArg) (args : Array Arg)
-    (expectedType? : Option Expr) (explicit ellipsis overloaded : Bool) (acc : Array (TermElabResult Expr)) : TermElabM (Array (TermElabResult Expr)) :=
+    (expectedType? : Option Expr) (explicit ellipsis overloaded : Bool) (acc : Array (TermElabResult Expr)) : TermElabM (Array (TermElabResult Expr)) := do
   if f.getKind == choiceKind then
     -- Set `errToSorry` to `false` when processing choice nodes. See comment above about the interaction between `errToSorry` and `observing`.
     withReader (fun ctx => { ctx with errToSorry := false }) do
@@ -853,6 +853,23 @@ private partial def elabAppFn (f : Syntax) (lvals : List LVal) (namedArgs : Arra
       elabAppFn (f.getArg 1) lvals namedArgs args expectedType? (explicit := true) ellipsis overloaded acc
     | `(@$t)     => throwUnsupportedSyntax -- invalid occurrence of `@`
     | `(_)       => throwError "placeholders '_' cannot be used where a function is expected"
+    | `(.$id:ident) =>
+       tryPostponeIfNoneOrMVar expectedType?
+       match expectedType? with
+       | none => throwError "invalid dotted identifier notation, expected type must be known"
+       | some expectedType =>
+         if let Expr.const declName .. := (← instantiateMVars expectedType).getAppFn then
+           let idNew := declName ++ id.getId.eraseMacroScopes
+           unless (← getEnv).contains idNew do
+             throwError "invalid dotted identifier notation, unknown identifier `{idNew}` from expected type{indentExpr expectedType}"
+           let fConst ← mkConst idNew
+           addTermInfo f fConst
+           let s ← observing do
+             let e ← elabAppLVals fConst lvals namedArgs args expectedType? explicit ellipsis
+             if overloaded then ensureHasType expectedType? e else pure e
+           return acc.push s
+         else
+           throwError "invalid dotted identifier notation, expected type is not of the form (C ...) where C is a constant{indentExpr expectedType}"
     | _ => do
       let catchPostpone := !overloaded
       /- If we are processing a choice node, then we should use `catchPostpone == false` when elaborating terms.
@@ -954,6 +971,7 @@ private def elabAtom : TermElab := fun stx expectedType? =>
 @[builtinTermElab ident] def elabIdent : TermElab := elabAtom
 /-- `x@e` matches the pattern `e` and binds its value to the identifier `x`. -/
 @[builtinTermElab namedPattern] def elabNamedPattern : TermElab := elabAtom
+@[builtinTermElab dotIdent] def elabDotIdent : TermElab := elabAtom
 /-- `x.{u, ...}` explicitly specifies the universes `u, ...` of the constant `x`. -/
 @[builtinTermElab explicitUniv] def elabExplicitUniv : TermElab := elabAtom
 /-- `e |>.x` is a shorthand for `(e).x`. It is especially useful for avoiding parentheses with repeated applications. -/

src/Lean/Elab/PatternVar.lean

@@ -142,6 +142,8 @@ partial def collect (stx : Syntax) : M Syntax := withRef stx <| withFreshMacroSc
   else if k == ``Lean.Parser.Term.anonymousCtor then
     let elems ← stx[1].getArgs.mapSepElemsM collect
     return stx.setArg 1 <| mkNullNode elems
+  else if k == ``Lean.Parser.Term.dotIdent then
+    return stx
   else if k == ``Lean.Parser.Term.structInst then
     /-
     ```
@@ -243,7 +245,15 @@ where
 
   processCtorApp (stx : Syntax) : M Syntax := do
     let (f, namedArgs, args, ellipsis) ← expandApp stx true
-    processCtorAppCore f namedArgs args ellipsis
+    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 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
+    else
+      processCtorAppCore f namedArgs args ellipsis
 
   processCtor (stx : Syntax) : M Syntax := do
     processCtorAppCore stx #[] #[] false

tests/lean/run/944.lean

@@ -0,0 +1,35 @@
+import Lean
+
+def f1 (x : Nat) : Except String Nat :=
+  if x > 0 then
+    .ok x
+  else
+    .error "argument is zero"
+
+namespace Lean.Elab
+open Lsp
+
+def identOf : Info → Option (RefIdent × Bool)
+  | .ofTermInfo ti => match ti.expr with
+    | .const n .. => some (.const n, ti.isBinder)
+    | .fvar id .. => some (.fvar id, ti.isBinder)
+    | _ => none
+  | .ofFieldInfo fi => some (.const fi.projName, false)
+  | _ => none
+
+def isConst (e : Expr) : Bool :=
+  e matches .const ..
+
+def isImplicit (bi : BinderInfo) : Bool :=
+  bi matches .implicit
+
+end Lean.Elab
+
+def f2 (xs : List Nat) : List Nat :=
+  .map (. + 1) xs
+
+def f3 : Nat :=
+  .zero
+
+def f4 (x : Nat) : Nat :=
+  .succ x