feat: syntax and delaborator for delayed assignment metavariables

src/Lean/Elab/BuiltinTerm.lean

@@ -100,6 +100,41 @@ private def elabOptLevel (stx : Syntax) : TermElabM Level :=
         else
           throwError "synthetic hole has already been defined with an incompatible local context"
 
+@[builtin_term_elab «delayedAssignedMVar»] def elabDelayedAssignedMVar : TermElab := fun stx expectedType? =>
+  match stx with
+  | `(?$arg($[$idents $[:= $terms]?],*)) => do
+    let mvar ←
+      if arg.raw.isIdent then
+        let userName := arg.raw.getId
+        match (← getMCtx).findUserName? userName with
+        | some mvarId => pure <| Expr.mvar mvarId
+        | none        => mkFreshExprMVar expectedType? .syntheticOpaque userName
+      else
+        mkFreshExprMVar expectedType? .syntheticOpaque
+    -- Resolve the fvars in the metavariable's local context and abstract the mvar
+    let mvarAbs ← mvar.mvarId!.withContext do
+      let fvars ← idents.mapM fun ident => do
+        let some fvar ← isLocalIdent? ident
+          | throwErrorAt ident "identifier '{ident}' is not a variable in the metavariable's local context:\n{mvar.mvarId!}"
+        addTermInfo ident fvar
+      let fwdDeps ← Meta.collectForwardDeps fvars false
+      if fwdDeps.size != fvars.size then
+        throwError "local variables in delayed assignment syntax must not have forward dependencies in the metavariable's local context:\n{mvar.mvarId!}"
+      if fwdDeps != fvars then
+        throwError "local variables in delayed assignment syntax must appear in order according to the metavariable's local context:\n{mvar.mvarId!}"
+      mkLambdaFVars fvars mvar >>= instantiateMVars
+    unless (← MetavarContext.isWellFormed (← getLCtx) mvarAbs) do
+      throwError "metavariable has incompatible local context for creating a delayed assignment"
+    -- Resolve the terms in the current local context
+    let (args, _) ← forallMetaBoundedTelescope (← inferType mvarAbs) idents.size
+    for i in [0:idents.size] do
+      let term := terms[i]!.getD ⟨idents[i]!⟩
+      let arg := args[i]!
+      let x ← elabTermEnsuringType term (← inferType arg)
+      arg.mvarId!.assign x
+    return mvarAbs.beta args
+  | _ => throwUnsupportedSyntax
+
 @[builtin_term_elab Lean.Parser.Term.omission] def elabOmission : TermElab := fun stx expectedType? => do
   logWarning m!"\
     The '⋯' token is used by the pretty printer to indicate omitted terms, and it should not be used directly. \

src/Lean/Parser/Term.lean

@@ -139,13 +139,55 @@ def optSemicolon (p : Parser) : Parser :=
 /-- The universe of propositions. `Prop ≡ Sort 0`. -/
 @[builtin_term_parser] def prop := leading_parser
   "Prop"
-/-- A placeholder term, to be synthesized by unification. -/
+/-- A *hole* (or *placeholder term*), which stands for an unknown term that should be synthesized by unification.
+The `_` syntax creates a fresh metavariable. -/
 @[builtin_term_parser] def hole := leading_parser
   "_"
-/-- Parses a "synthetic hole", that is, `?foo` or `?_`.
-This syntax is used to construct named metavariables. -/
+/--
+A *synthetic hole* (or *synthetic placeholder*), which stands for an unknown term that should should be synthesized using tactics.
+- `?_` creates a fresh synthetic metavariable with an auto-generated name.
+- `?foo` either refers to a pre-existing synthetic metavariable named `foo` or creates a fresh synthetic metavariable with that name.
+
+In particular, the synthetic hole syntax creates synthetic opaque metavariables,
+the same kind of metavariable used to represent goals in the tactic state.
+During elaboration, unification does not assign to synthetic opaque metavariables,
+since this can lead to counterintuitive behavior.
+
+Synthetic holes are similar to placeholders (the `_` syntax) in that they also stand for metavariables,
+but synthetic opaque metavariables have some different features:
+- In tactics such as `refine`, new synthetic holes yield new goals.
+- When synthetic holes appear under binders, they capture local variables using a more complicated mechanism known as delayed assignment.
+  (Delayed assignment metavariables pretty print as `?foo(x := a)`.)
+- During the course of elaboration, unification will not solve for synthetic opaque metavariables.
+-/
 @[builtin_term_parser] def syntheticHole := leading_parser
   "?" >> (ident <|> hole)
+def delayedAssignedMVarItem : Parser := leading_parser
+  ident >> optional (" := " >> termParser)
+/--
+A delayed assignment metavariable.
+- `?foo(x := a, y := b)` takes the metavariable for the synthetic hole `?foo`
+  and create a term that effectively substitutes `a` and `b`
+  as the values for the local variables `x` and `y` from the local context of the metavariable `?foo`.
+- `?foo(x, y)` is short for `?foo(x := x, y := y)`.
+
+Delayed assignment is a mechanism where values can be substituted into the local context of another metavariable.
+You can think of delayed assigment as being a purely syntactic way to "apply" a metavariable as if it were a lambda abstraction.
+
+The way it works is the following. Suppose `?foo : T` has local variables `x : A` and `y : B` and we have terms `a : A` and `b : B`.
+Then `?foo(x := a, y := b)` creates a new metavariable `?m : A → B → T` without `x` or `y` in context,
+registers a delayed assignment with the data that `?m` is waiting on `?foo`, and then elaborates to `?m a b`.
+Once `?foo` is fully assigned (in that once all its metavariables are recursively instantiated, it contains no metavariables),
+then `?m a b` is replaced by the value of `?foo` with `x` and `y` substituted for `a` and `b`, respectively.
+
+The delayed assignment mechanism is necessary for the implementation of the `intro` tactic.
+The tactic `intro x` creates a new metavariable `?goal` with a local variable named `x`,
+solves the current goal with the term `fun x' => ?goal(x := x')`, and then uses `?goal` for the new goal.
+Note that if you write `refine fun x => ?goal` and `?goal` is a fresh metavariable,
+a delayed assignment will automatically be created to account for the captured local context.
+-/
+@[builtin_term_parser] def delayedAssignedMVar := leading_parser
+  syntheticHole >> checkNoWsBefore >> "(" >> sepBy delayedAssignedMVarItem ", " (allowTrailingSep := true) >> ")"
 /--
 The `⋯` term denotes a term that was omitted by the pretty printer.
 The presence of `⋯` in pretty printer output is controlled by the `pp.deepTerms` and `pp.proofs` options,

src/Lean/PrettyPrinter/Delaborator/Builtins.lean

@@ -563,6 +563,41 @@ def withOverApp (arity : Nat) (x : Delab) : Delab := do
       withAnnotateTermInfo x
     delabAppCore (n - arity) delabHead (unexpand := false)
 
+@[builtin_delab app]
+def delabDelayedAssignment : Delab := whenPPOption getPPMVarsDelayed do
+  let .mvar mvarId := (← getExpr).getAppFn | failure
+  let some decl ← getDelayedMVarAssignment? mvarId | failure
+  let mvarIdPending := decl.mvarIdPending
+  let mvarDecl ← mvarIdPending.getDecl
+  let n :=
+    match mvarDecl.userName with
+    | Name.anonymous => mvarIdPending.name.replacePrefix `_uniq `m
+    | n => n
+  withOverApp decl.fvars.size do
+    let (head, _, items) ← withAppFnArgs
+      (do
+        let pos ← getPos
+        -- TODO(kmill): get formatter to tag the syntheticHole using its position
+        -- so that the whole syntheticHole is hoverable
+        let n := annotatePos pos <| ← if ← getPPOption getPPMVars then pure (mkIdent n) else `(_)
+        let head := annotatePos pos <| ← `(syntheticHole|?$n)
+        mvarIdPending.withContext <| addTermInfo pos head (.mvar mvarIdPending)
+        return (head, decl.fvars.toList, #[]))
+      (fun (head, fvars, items) => do
+        let fvar :: fvars' := fvars | unreachable!
+        let arg ← delab
+        let item ← mvarIdPending.withContext do
+          let name ← fvar.fvarId!.getUserName
+          if arg.raw.isIdent && arg.getId == name then
+            `(delayedAssignedMVarItem| $arg.raw:ident)
+          else
+            let pos ← nextExtraPos
+            let ident : Ident := annotatePos pos <| mkIdent name
+            addTermInfo pos ident fvar
+            `(delayedAssignedMVarItem| $ident := $arg)
+        return (head, fvars', items.push item))
+    `(delayedAssignedMVar| $head:syntheticHole($[$items],*))
+
 /-- State for `delabAppMatch` and helpers. -/
 structure AppMatchState where
   info        : MatcherInfo

src/Lean/PrettyPrinter/Delaborator/Options.lean

@@ -95,6 +95,11 @@ register_builtin_option pp.mvars.withType : Bool := {
   group    := "pp"
   descr    := "(pretty printer) display metavariables with a type ascription"
 }
+register_builtin_option pp.mvars.delayed : Bool := {
+  defValue := true
+  group    := "pp"
+  descr    := "(pretty printer) display delayed assignment metavariables with '?m(x,y)' syntax"
+}
 register_builtin_option pp.beta : Bool := {
   defValue := false
   group    := "pp"
@@ -244,6 +249,7 @@ def getPPPrivateNames (o : Options) : Bool := o.get pp.privateNames.name (getPPA
 def getPPInstantiateMVars (o : Options) : Bool := o.get pp.instantiateMVars.name pp.instantiateMVars.defValue
 def getPPMVars (o : Options) : Bool := o.get pp.mvars.name pp.mvars.defValue
 def getPPMVarsWithType (o : Options) : Bool := o.get pp.mvars.withType.name pp.mvars.withType.defValue
+def getPPMVarsDelayed (o : Options) : Bool := o.get pp.mvars.delayed.name pp.mvars.delayed.defValue
 def getPPBeta (o : Options) : Bool := o.get pp.beta.name pp.beta.defValue
 def getPPSafeShadowing (o : Options) : Bool := o.get pp.safeShadowing.name pp.safeShadowing.defValue
 def getPPProofs (o : Options) : Bool := o.get pp.proofs.name (pp.proofs.defValue || getPPAll o)