feat: more than one optional argument can be omitted while pretty pri…

…nting (#4854)

Before, the delaborator was conservative about omitting optional
arguments, only omitting the very last one. Now it can omit arbitrarily
long sequences of optional arguments from the end.

For simplicity of implementation, every optional argument is delaborated
and then potentially discarded. It could save state and lazily
delaborate, but we're running under the hypothesis that most optional
arguments are for very simple values (like `true`, `false`, or a numeric
literal), so it is unlikely that efficiency gains, if any, are worth it.
In particular, in the future structure constructors will have optional
arguments, but `unexpandStructureInstance` assumes none of the optional
fields are omitted.

Closes #4812

src/Lean/PrettyPrinter/Delaborator/Builtins.lean

@@ -339,19 +339,22 @@ inductive AppImplicitArg
   | skip
   /-- A regular argument. -/
   | regular (s : Term)
+  /-- A regular argument that, if it comes as the last argument, may be omitted. -/
+  | optional (name : Name) (s : Term)
   /-- It's a named argument. Named arguments inhibit applying unexpanders. -/
   | named (s : TSyntax ``Parser.Term.namedArgument)
   deriving Inhabited
 
 /-- Whether unexpanding is allowed with this argument. -/
 def AppImplicitArg.canUnexpand : AppImplicitArg → Bool
-  | .regular .. | .skip => true
+  | .regular .. | .optional .. | .skip => true
   | .named .. => false
 
 /-- If the argument has associated syntax, returns it. -/
 def AppImplicitArg.syntax? : AppImplicitArg → Option Syntax
   | .skip => none
   | .regular s => s
+  | .optional _ s => s
   | .named s => s
 
 /--
@@ -371,25 +374,24 @@ def delabAppImplicitCore (unexpand : Bool) (numArgs : Nat) (delabHead : Delab) (
       appFieldNotationCandidate?
     else
       pure none
-  let (fnStx, args) ←
+  let (fnStx, args') ←
     withBoundedAppFnArgs numArgs
       (do return ((← delabHead), Array.mkEmpty numArgs))
-      (fun (fnStx, args) => do
-        let idx := args.size
-        let arg ← mkArg (numArgs - idx - 1) paramKinds[idx]!
-        return (fnStx, args.push arg))
+      (fun (fnStx, args) => return (fnStx, args.push (← mkArg paramKinds[args.size]!)))
+
+  -- Strip off optional arguments. We save the original `args'` for structure instance notation
+  let args := args'.popWhile (· matches .optional ..)
 
   -- App unexpanders
   if ← pure unexpand <&&> getPPOption getPPNotation then
     -- Try using an app unexpander for a prefix of the arguments.
     if let some stx ← (some <$> tryAppUnexpanders fnStx args) <|> pure none then
       return stx
 
-  let stx := Syntax.mkApp fnStx (args.filterMap (·.syntax?))
-
   -- Structure instance notation
-  if ← pure (unexpand && args.all (·.canUnexpand)) <&&> getPPOption getPPStructureInstances then
+  if ← pure (unexpand && args'.all (·.canUnexpand)) <&&> getPPOption getPPStructureInstances then
     -- Try using the structure instance unexpander.
+    let stx := Syntax.mkApp fnStx (args'.filterMap (·.syntax?))
     if let some stx ← (some <$> unexpandStructureInstance stx) <|> pure none then
       return stx
 
@@ -416,23 +418,24 @@ def delabAppImplicitCore (unexpand : Bool) (numArgs : Nat) (delabHead : Delab) (
         return Syntax.mkApp head (args'.filterMap (·.syntax?))
 
   -- Normal application
-  return stx
+  return Syntax.mkApp fnStx (args.filterMap (·.syntax?))
 where
   mkNamedArg (name : Name) : DelabM AppImplicitArg :=
     return .named <| ← `(Parser.Term.namedArgument| ($(mkIdent name) := $(← delab)))
   /--
   Delaborates the current argument.
   The argument `remainingArgs` is the number of arguments in the application after this one.
   -/
-  mkArg (remainingArgs : Nat) (param : ParamKind) : DelabM AppImplicitArg := do
+  mkArg (param : ParamKind) : DelabM AppImplicitArg := do
     let arg ← getExpr
     if ← getPPOption getPPAnalysisSkip then return .skip
     else if ← getPPOption getPPAnalysisHole then return .regular (← `(_))
     else if ← getPPOption getPPAnalysisNamedArg then
       mkNamedArg param.name
-    else if param.defVal.isSome && remainingArgs == 0 && param.defVal.get! == arg then
-      -- Assumption: `useAppExplicit` has already detected whether it is ok to omit this argument
-      return .skip
+    else if param.defVal.isSome && param.defVal.get! == arg then
+      -- Assumption: `useAppExplicit` has already detected whether it is ok to omit this argument, if it is the last one.
+      -- We will later remove all optional arguments from the end.
+      return .optional param.name (← delab)
     else if param.bInfo.isExplicit then
       return .regular (← delab)
     else if ← pure (param.name == `motive) <&&> shouldShowMotive arg (← getOptions) then

tests/lean/run/delabApp.lean

@@ -0,0 +1,79 @@
+/-!
+# Testing features of the app delaborator, including overapplication
+-/
+
+/-!
+Check that the optional value equality check is specialized to the supplied arguments
+(rather than, formerly, the locally-defined fvars from a telescope).
+-/
+def foo (α : Type) [Inhabited α] (x : α := default) : α := x
+
+/-- info: foo Nat : Nat -/
+#guard_msgs in #check foo Nat
+/-- info: foo Nat 1 : Nat -/
+#guard_msgs in #check foo Nat 1
+
+/-!
+Check that optional value omission is aware of unfolding.
+-/
+def Ty := (x : Nat := 1) → Fin (x + 1)
+
+def f (y : Nat := 2) : Ty := fun x => 0
+
+/-- info: f 3 4 : Fin (4 + 1) -/
+#guard_msgs in #check f 3 4
+/-- info: f 3 : Fin (1 + 1) -/
+#guard_msgs in #check f 3
+/-- info: f : Fin (1 + 1) -/
+#guard_msgs in #check (f)
+
+
+/-!
+Check that overapplied projections pretty print using projection notation.
+-/
+
+structure Foo where
+  f : Nat → Nat
+
+/-- info: ∀ (x : Foo), x.f 1 = 0 : Prop -/
+#guard_msgs in #check ∀ (x : Foo), x.f 1 = 0
+
+/-!
+Overapplied `letFun`
+-/
+/--
+info: (let_fun f := id;
+  f)
+  1 : Nat
+-/
+#guard_msgs in #check (have f := id; f) 1
+
+/-!
+Overapplied `OfNat.ofNat`
+-/
+instance : OfNat (Nat → Nat) 1 where
+  ofNat := id
+
+/-- info: 1 2 : Nat -/
+#guard_msgs in #check (1 : Nat → Nat) 2
+
+/-!
+Overapplied `dite`
+-/
+
+/-- info: (if _h : True then id else id) 1 : Nat -/
+#guard_msgs in #check (if _h : True then id else id) 1
+
+
+/-!
+Testing that multiple optional arguments are omitted rather than just the last (issue #4812)
+-/
+
+def g (a : Nat) (b := 1) (c := 2) (d := 3) := a + b + c + d
+
+/-- info: g 0 : Nat -/
+#guard_msgs in #check g 0
+
+-- Both the `start` and `stop` arguments are omitted.
+/-- info: fun a => Array.foldl (fun x y => x + y) 0 a : Array Nat → Nat -/
+#guard_msgs in #check fun (a : Array Nat) => a.foldl (fun x y => x + y) 0