implementation and delab

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/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 := 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

tests/lean/276.lean.expected.out

@@ -1,3 +1,3 @@
 276.lean:5:27-5:50: error: failed to elaborate eliminator, expected type is not available
-fun {α : Sort v} => @?m α : {α : Sort v} → @?m α
+fun {α : Sort v} => ?m(α) : {α : Sort v} → @?m α
 276.lean:9:33-9:56: error: failed to elaborate eliminator, expected type is not available

tests/lean/474.lean.expected.out

@@ -4,5 +4,5 @@ fun y_1 => y.add y_1
 fun y => Nat.add _fvar.1 y
 fun (y : Nat) => Nat.add y y
 ?m.add y
-Nat.add (?m #0) #0
+Nat.add ?m(y := #0) #0
 fun y => (y.add y).add y

tests/lean/delayedMVarSyntax.lean

@@ -0,0 +1,47 @@
+/-!
+# Syntax to create delayed assignment metavariables
+-/
+
+/-!
+Creating and reusing some synthetic holes using delayed assignment syntax.
+-/
+example : True := by
+  let f : Nat → Nat := fun x => ?a
+  let g : Nat → Nat → Nat := fun x y => ?b + ?b(x := 1) + ?b(y := 1) + ?a(x) + ?a(x := y)
+  let v := ?b(x := 4, y := 6)
+  trace_state
+  case b => exact 3 * x + y
+  trace_state
+  case a => exact x + 2
+  trace_state
+  trivial
+
+/-!
+Error: out of order
+-/
+example : True := by
+  let f : Nat → Nat → Nat := fun x y => ?a
+  let v := ?a(y := 1, x := 2)
+
+/-!
+Error: forward dependencies
+-/
+example : True := by
+  let f : (n : Nat) → (m : Fin n) → Nat := fun n m => ?a
+  let v := ?a(n := 1)
+
+/-!
+Using a metavariable later in a different context.
+-/
+example : (∀ x : Nat, x = x) ∧ (∀ x : Nat, x = x) := by
+  refine ⟨fun x => ?a, ?_⟩
+  · rfl
+  · intro y
+    exact ?a(x := y)
+
+/-!
+Using the metavariable later in a different context, in the same term.
+-/
+example : (∀ x : Nat, x = x) ∧ (∀ x : Nat, x = x) := by
+  refine ⟨fun x => ?a(x), fun x => ?a(x)⟩
+  · rfl

tests/lean/delayedMVarSyntax.lean.expected.out

@@ -0,0 +1,40 @@
+f : Nat → Nat := fun x => ?a(x)
+g : Nat → Nat → Nat := fun x y => ?b(x, y) + ?b(y, x := 1) + ?b(x, y := 1) + ?a(x) + ?a(x := y)
+v : Nat := ?b(x := 4, y := 6)
+⊢ True
+
+case b
+f : Nat → Nat := fun x => ?a(x)
+x y : Nat
+⊢ Nat
+
+case a
+x : Nat
+⊢ Nat
+f : Nat → Nat := fun x => ?a(x)
+g : Nat → Nat → Nat := fun x y => 3 * x + y + (3 * 1 + y) + (3 * x + 1) + ?a(x) + ?a(x := y)
+v : Nat := 3 * 4 + 6
+⊢ True
+
+case a
+x : Nat
+⊢ Nat
+f : Nat → Nat := fun x => x + 2
+g : Nat → Nat → Nat := fun x y => 3 * x + y + (3 * 1 + y) + (3 * x + 1) + (x + 2) + (y + 2)
+v : Nat := 3 * 4 + 6
+⊢ True
+delayedMVarSyntax.lean:24:11-24:29: error: local variables in delayed assignment syntax must appear in order according to the metavariable's local context:
+case a
+x y : Nat
+⊢ Nat
+delayedMVarSyntax.lean:22:18-24:29: error: unsolved goals
+f : Nat → Nat → Nat := fun x y => ?a(x, y)
+⊢ True
+delayedMVarSyntax.lean:31:11-31:21: error: local variables in delayed assignment syntax must not have forward dependencies in the metavariable's local context:
+case a
+n : Nat
+m : Fin n
+⊢ Nat
+delayedMVarSyntax.lean:29:18-31:21: error: unsolved goals
+f : (n : Nat) → Fin n → Nat := fun n m => ?a(n, m)
+⊢ True

tests/lean/funParen.lean.expected.out

@@ -1,4 +1,4 @@
 fun α [Repr α] => repr : (α : Type u_1) → [inst : Repr α] → α → Std.Format
 fun x y => x : (x : ?m) → ?m x → ?m
 funParen.lean:4:12-4:16: error: invalid pattern, constructor or constant marked with '[match_pattern]' expected
-fun x => ?m x : (x : ?m) → ?m x
+fun x => ?m(x✝ := x) : (x : ?m) → ?m x

tests/lean/interactive/hover.lean.expected.out

@@ -507,7 +507,7 @@
   "end": {"line": 252, "character": 10}},
  "contents":
  {"value":
-  "```lean\nℕ\n```\n***\nA placeholder term, to be synthesized by unification. ",
+  "```lean\nℕ\n```\n***\nA *hole* (or *placeholder term*), which stands for an unknown term that should be synthesized by unification.\nThe `_` syntax creates a fresh metavariable. ",
   "kind": "markdown"}}
 {"textDocument": {"uri": "file:///hover.lean"},
  "position": {"line": 252, "character": 11}}
@@ -573,7 +573,7 @@
  {"start": {"line": 269, "character": 2}, "end": {"line": 269, "character": 3}},
  "contents":
  {"value":
-  "```lean\nlet x :=\n  match 0 with\n  | x => 0;\nℕ\n```\n***\nA placeholder term, to be synthesized by unification. ",
+  "```lean\nlet x :=\n  match 0 with\n  | x => 0;\nℕ\n```\n***\nA *hole* (or *placeholder term*), which stands for an unknown term that should be synthesized by unification.\nThe `_` syntax creates a fresh metavariable. ",
   "kind": "markdown"}}
 {"textDocument": {"uri": "file:///hover.lean"},
  "position": {"line": 272, "character": 4}}

tests/lean/interactive/hoverBinderUndescore.lean.expected.out

@@ -4,45 +4,45 @@
  {"start": {"line": 1, "character": 5}, "end": {"line": 1, "character": 6}},
  "contents":
  {"value":
-  "```lean\nNat\n```\n***\nA placeholder term, to be synthesized by unification. ",
+  "```lean\nNat\n```\n***\nA *hole* (or *placeholder term*), which stands for an unknown term that should be synthesized by unification.\nThe `_` syntax creates a fresh metavariable. ",
   "kind": "markdown"}}
 {"textDocument": {"uri": "file:///hoverBinderUndescore.lean"},
  "position": {"line": 1, "character": 7}}
 {"range":
  {"start": {"line": 1, "character": 7}, "end": {"line": 1, "character": 8}},
  "contents":
  {"value":
-  "```lean\nBool\n```\n***\nA placeholder term, to be synthesized by unification. ",
+  "```lean\nBool\n```\n***\nA *hole* (or *placeholder term*), which stands for an unknown term that should be synthesized by unification.\nThe `_` syntax creates a fresh metavariable. ",
   "kind": "markdown"}}
 {"textDocument": {"uri": "file:///hoverBinderUndescore.lean"},
  "position": {"line": 6, "character": 6}}
 {"range":
  {"start": {"line": 6, "character": 6}, "end": {"line": 6, "character": 7}},
  "contents":
  {"value":
-  "```lean\nNat\n```\n***\nA placeholder term, to be synthesized by unification. ",
+  "```lean\nNat\n```\n***\nA *hole* (or *placeholder term*), which stands for an unknown term that should be synthesized by unification.\nThe `_` syntax creates a fresh metavariable. ",
   "kind": "markdown"}}
 {"textDocument": {"uri": "file:///hoverBinderUndescore.lean"},
  "position": {"line": 6, "character": 8}}
 {"range":
  {"start": {"line": 6, "character": 8}, "end": {"line": 6, "character": 9}},
  "contents":
  {"value":
-  "```lean\nBool\n```\n***\nA placeholder term, to be synthesized by unification. ",
+  "```lean\nBool\n```\n***\nA *hole* (or *placeholder term*), which stands for an unknown term that should be synthesized by unification.\nThe `_` syntax creates a fresh metavariable. ",
   "kind": "markdown"}}
 {"textDocument": {"uri": "file:///hoverBinderUndescore.lean"},
  "position": {"line": 11, "character": 6}}
 {"range":
  {"start": {"line": 11, "character": 6}, "end": {"line": 11, "character": 7}},
  "contents":
  {"value":
-  "```lean\nNat\n```\n***\nA placeholder term, to be synthesized by unification. ",
+  "```lean\nNat\n```\n***\nA *hole* (or *placeholder term*), which stands for an unknown term that should be synthesized by unification.\nThe `_` syntax creates a fresh metavariable. ",
   "kind": "markdown"}}
 {"textDocument": {"uri": "file:///hoverBinderUndescore.lean"},
  "position": {"line": 11, "character": 8}}
 {"range":
  {"start": {"line": 11, "character": 8}, "end": {"line": 11, "character": 9}},
  "contents":
  {"value":
-  "```lean\nBool\n```\n***\nA placeholder term, to be synthesized by unification. ",
+  "```lean\nBool\n```\n***\nA *hole* (or *placeholder term*), which stands for an unknown term that should be synthesized by unification.\nThe `_` syntax creates a fresh metavariable. ",
   "kind": "markdown"}}

tests/lean/match1.lean.expected.out

@@ -21,7 +21,7 @@ constructor expected
 [false, true, true]
 match1.lean:136:7-136:22: error: invalid match-expression, type of pattern variable 'a' contains metavariables
   ?m
-fun x => ?m x : ?m × ?m → ?m
+fun x => ?m(x✝ := x) : ?m × ?m → ?m
 fun x =>
   match x with
   | (a, b) => a + b : Nat × Nat → Nat

tests/lean/mulcommErrorMessage.lean.expected.out

@@ -1,5 +1,5 @@
 mulcommErrorMessage.lean:8:13-13:25: error: type mismatch
-  fun a b => ?m a b
+  fun a b => ?m(a, b)
 has type
   (a : ?m) → (b : ?m a) → ?m a b : Sort (imax ?u ?u ?u)
 but is expected to have type
@@ -21,7 +21,7 @@ has type
 but is expected to have type
   false = true : Prop
 mulcommErrorMessage.lean:16:3-17:47: error: type mismatch
-  fun a b => ?m a b
+  fun a b => ?m(a, b)
 has type
   (a : ?m) → (b : ?m a) → ?m a b : Sort (imax ?u ?u ?u)
 but is expected to have type

tests/lean/namedHoles.lean.expected.out

@@ -9,10 +9,10 @@ but is expected to have type
 f ?x (sorryAx Bool true) : Nat
 g ?x ?x : Nat
 20
-foo (fun x => ?m x) ?hole : Nat
+foo (fun x => ?hole(x)) ?hole : Nat
 bla ?hole fun x => ?hole : Nat
 namedHoles.lean:35:38-35:43: error: synthetic hole has already been defined with an incompatible local context
-boo (fun x => ?m x) fun y => sorryAx Nat true : Nat
+boo (fun x => ?hole(x)) fun y => sorryAx Nat true : Nat
 11
 12
 namedHoles.lean:58:26-58:31: error: synthetic hole has already been defined and assigned to value incompatible with the current context

tests/lean/run/4144.lean

@@ -18,7 +18,7 @@ case refine'_4
 ⊢ ?refine'_1
 
 case refine'_5
-⊢ ¬(fun x => ?m.17 x) ?refine'_3 = (fun x => ?m.17 x) ?refine'_4
+⊢ ¬(fun x => ?m.16(x✝ := x)) ?refine'_3 = (fun x => ?m.16(x✝ := x)) ?refine'_4
 -/
 #guard_msgs in
 example : False := by

tests/lean/run/anonymous_ctor_error_msg.lean

@@ -30,7 +30,7 @@ error: invalid constructor ⟨...⟩, expected type must be an inductive type 
 info: let x1 := { n := 1 };
 let x2 := { n := 2 };
 let x3 := { n := 3 };
-let x4 := ?_ x1 x2 x3;
+let x4 := ?_(x1, x2, x3);
 let x5 := { n := 5 };
 let x6 := { n := 6 };
 Foo.sum [x1, x2, x3, x5, x6] : Foo

tests/lean/run/meta7.lean

@@ -112,7 +112,7 @@ set_option pp.mvars false in
 info: [Meta.debug] ----- tst4 -----
 [Meta.debug] x y : Nat
     ⊢ Nat
-[Meta.debug] ?_ (Add.add 10 y) y
+[Meta.debug] ?_(z := Add.add 10 y) y
 [Meta.debug] x z y : Nat
     ⊢ Nat
 [Meta.debug] x y z
@@ -175,7 +175,7 @@ set_option pp.mvars false in
 info: [Meta.debug] ----- tst6 -----
 [Meta.debug] x y : Nat
     ⊢ Nat
-[Meta.debug] ?_ (Add.add 10 y)
+[Meta.debug] ?_(z := Add.add 10 y)
 [Meta.debug] x y z : Nat
     ⊢ Nat
 [Meta.debug] x y z

tests/lean/withAssignableSyntheticOpaqueBug.lean.expected.out

@@ -1,4 +1,4 @@
-fun x => ?m x
+fun x => ?m(x)
 none
 (some (OfNat.ofNat.{0} Nat 0 (instOfNatNat 0)))
 0