From 50abc3e295d63f172b690427a6d9f623d4c185ff Mon Sep 17 00:00:00 2001 From: Gabriel Ebner Date: Tue, 11 Jan 2022 15:51:45 +0100 Subject: [PATCH] fix: correctly pretty-print `@Eq` --- .../PrettyPrinter/Delaborator/Builtins.lean | 12 +++++++-- tests/lean/366.lean.expected.out | 2 +- tests/lean/439.lean | 4 +-- tests/lean/439.lean.expected.out | 2 +- tests/lean/PPRoundtrip.lean | 4 +++ tests/lean/PPRoundtrip.lean.expected.out | 3 +++ .../autoBoundImplicits1.lean.expected.out | 2 +- tests/lean/diamond2.lean.expected.out | 4 +-- tests/lean/diamond5.lean.expected.out | 2 +- tests/lean/diamond7.lean.expected.out | 2 +- tests/lean/elseifDoErrorPos.lean.expected.out | 2 +- tests/lean/infoTree.lean.expected.out | 26 +++++++++---------- .../lean/interactive/hover.lean.expected.out | 2 +- tests/lean/openScoped.lean.expected.out | 2 +- tests/lean/pplevel.lean.expected.out | 2 +- tests/lean/sizeof.lean.expected.out | 2 +- 16 files changed, 44 insertions(+), 29 deletions(-) diff --git a/src/Lean/PrettyPrinter/Delaborator/Builtins.lean b/src/Lean/PrettyPrinter/Delaborator/Builtins.lean index 9454b87062..fa4a258d10 100644 --- a/src/Lean/PrettyPrinter/Delaborator/Builtins.lean +++ b/src/Lean/PrettyPrinter/Delaborator/Builtins.lean @@ -161,12 +161,12 @@ where k (xs ++ ys) b @[builtinDelab app] -def delabAppExplicit : Delab := whenPPOption getPPExplicit do +def delabAppExplicit : Delab := do let paramKinds ← getParamKinds let (fnStx, _, argStxs) ← withAppFnArgs (do let stx ← delabAppFn - let needsExplicit := paramKinds.any (fun param => !param.isRegularExplicit) && stx.getKind != `Lean.Parser.Term.explicit + let needsExplicit := stx.getKind != ``Lean.Parser.Term.explicit let stx ← if needsExplicit then `(@$stx) else pure stx pure (stx, paramKinds.toList, #[])) (fun ⟨fnStx, paramKinds, argStxs⟩ => do @@ -252,6 +252,14 @@ def delabAppImplicit : Delab := do if ← getPPOption getPPExplicit then if paramKinds.any (fun param => !param.isRegularExplicit) then failure + -- If the application has an implicit function type, fall back to delabAppExplicit. + -- This is e.g. necessary for `@Eq`. + let isImplicitApp ← try + let ty ← whnf (← inferType (← getExpr)) + ty.isForall && (ty.binderInfo == BinderInfo.implicit || ty.binderInfo == BinderInfo.instImplicit) + catch _ => false + if isImplicitApp then failure + let (fnStx, _, argStxs) ← withAppFnArgs (return (← delabAppFn, paramKinds.toList, #[])) (fun (fnStx, paramKinds, argStxs) => do diff --git a/tests/lean/366.lean.expected.out b/tests/lean/366.lean.expected.out index 527ce50f29..ccac7ce637 100644 --- a/tests/lean/366.lean.expected.out +++ b/tests/lean/366.lean.expected.out @@ -2,7 +2,7 @@ [Meta.synthInstance] [Meta.synthInstance] main goal Inhabited Nat [Meta.synthInstance.newSubgoal] Inhabited Nat - [Meta.synthInstance.globalInstances] Inhabited Nat, [instInhabited, instInhabitedNat] + [Meta.synthInstance.globalInstances] Inhabited Nat, [@instInhabited, instInhabitedNat] [Meta.synthInstance.generate] instance instInhabitedNat [Meta.synthInstance.tryResolve] [Meta.synthInstance.tryResolve] Inhabited Nat =?= Inhabited Nat diff --git a/tests/lean/439.lean b/tests/lean/439.lean index 073b73d5f5..dc17bd0687 100644 --- a/tests/lean/439.lean +++ b/tests/lean/439.lean @@ -10,9 +10,9 @@ class Bar.{w} (P : Sort u) := variable {P : Sort u} (B : Bar P) variable (fn : Fn ((p : P) -> B.fn p) ({p : P} -> B.fn p)) -#check coeFun fn -- Result is as expected (implicit) +#check (@fn : {p : P} → Bar.fn p) -- Result is as expected (implicit) /- - fn : {p : P} → Bar.fn p + fn.imp : {p : P} → Bar.fn p -/ variable (p : P) diff --git a/tests/lean/439.lean.expected.out b/tests/lean/439.lean.expected.out index 89ab5dd910..5bdbaf3fc4 100644 --- a/tests/lean/439.lean.expected.out +++ b/tests/lean/439.lean.expected.out @@ -1,4 +1,4 @@ -fn : {p : P} → Bar.fn p +fn.imp : {p : P} → Bar.fn p 439.lean:20:7-20:12: error: function expected at Fn.imp fn term has type diff --git a/tests/lean/PPRoundtrip.lean b/tests/lean/PPRoundtrip.lean index 46b006eed8..21e3e01098 100644 --- a/tests/lean/PPRoundtrip.lean +++ b/tests/lean/PPRoundtrip.lean @@ -39,6 +39,10 @@ set_option format.width 20 -- #eval checkM `(Type _) -- #eval checkM `(Type (_ + 2)) +#eval checkM `(@max Nat) +#eval checkM `(@HEq Nat 1) +#eval checkM `(@List.nil) + #eval checkM `(Nat) #eval checkM `(List Nat) #eval checkM `(id Nat) diff --git a/tests/lean/PPRoundtrip.lean.expected.out b/tests/lean/PPRoundtrip.lean.expected.out index 7be96bef83..2c793cbda5 100644 --- a/tests/lean/PPRoundtrip.lean.expected.out +++ b/tests/lean/PPRoundtrip.lean.expected.out @@ -2,6 +2,9 @@ Prop Type Type Type 1 +@max Nat +@HEq Nat 1 +@List.nil Nat List Nat id Nat diff --git a/tests/lean/autoBoundImplicits1.lean.expected.out b/tests/lean/autoBoundImplicits1.lean.expected.out index 6892ceb092..5b32f11d50 100644 --- a/tests/lean/autoBoundImplicits1.lean.expected.out +++ b/tests/lean/autoBoundImplicits1.lean.expected.out @@ -10,6 +10,6 @@ autoBoundImplicits1.lean:24:37-24:38: error: unknown identifier 'β' autoBoundImplicits1.lean:24:46-24:47: error: unknown identifier 'β' autoBoundImplicits1.lean:24:48-24:49: error: unknown identifier 'n' autoBoundImplicits1.lean:25:18-25:23: warning: declaration uses 'sorry' -f : {α : Type} → {n : Nat} → Vec α n → Vec α n +@f : {α : Type} → {n : Nat} → Vec α n → Vec α n f mkVec : Vec ?m 0 f mkVec : Vec Nat 0 diff --git a/tests/lean/diamond2.lean.expected.out b/tests/lean/diamond2.lean.expected.out index 9267669f29..08aa1d34c4 100644 --- a/tests/lean/diamond2.lean.expected.out +++ b/tests/lean/diamond2.lean.expected.out @@ -1,5 +1,5 @@ -Foo1.mk : {α : Type} → Bar (α → α) → (β : Type) → (α → β) → Foo1 α -Foo2.mk : {α : Type} → Bar (α → α) → (β : Type) → (α → β) → α → α → Foo2 α +@Foo1.mk : {α : Type} → Bar (α → α) → (β : Type) → (α → β) → Foo1 α +@Foo2.mk : {α : Type} → Bar (α → α) → (β : Type) → (α → β) → α → α → Foo2 α def Foo2.toBar : {α : Type} → Foo2 α → Bar (α → α) := fun α self => self.1 def Foo2.toBoo2 : {α : Type} → Foo2 α → Boo2 α := diff --git a/tests/lean/diamond5.lean.expected.out b/tests/lean/diamond5.lean.expected.out index 0fb80ebdc1..ed3861d384 100644 --- a/tests/lean/diamond5.lean.expected.out +++ b/tests/lean/diamond5.lean.expected.out @@ -1 +1 @@ -D.toC_1 : {α : Type} → [self : D α] → C α +@D.toC_1 : {α : Type} → [self : D α] → C α diff --git a/tests/lean/diamond7.lean.expected.out b/tests/lean/diamond7.lean.expected.out index 3f4121a174..c322b31722 100644 --- a/tests/lean/diamond7.lean.expected.out +++ b/tests/lean/diamond7.lean.expected.out @@ -27,7 +27,7 @@ fun (α : Type u) [self : CommMonoid.{u} α] => def CommGroup.toCommMonoid.{u} : {α : Type u} → [self : CommGroup.{u} α] → CommMonoid.{u} α := fun (α : Type u) [self : CommGroup.{u} α] => @CommMonoid.mk.{u} α (@Group.toMonoid.{u} α (@CommGroup.toGroup.{u} α self)) (@CommGroup.mul_comm.{u} α self) -Field.mk : {α : Type u_1} → [toDivisionRing : DivisionRing α] → (∀ (a b : α), a * b = b * a) → Field α +@Field.mk : {α : Type u_1} → [toDivisionRing : DivisionRing α] → (∀ (a b : α), a * b = b * a) → Field α def Field.toDivisionRing.{u} : {α : Type u} → [self : Field.{u} α] → DivisionRing.{u} α := fun (α : Type u) [self : Field.{u} α] => self.1 def Field.toCommRing.{u} : {α : Type u} → [self : Field.{u} α] → CommRing.{u} α := diff --git a/tests/lean/elseifDoErrorPos.lean.expected.out b/tests/lean/elseifDoErrorPos.lean.expected.out index edd1b3b090..87c5f1ad9a 100644 --- a/tests/lean/elseifDoErrorPos.lean.expected.out +++ b/tests/lean/elseifDoErrorPos.lean.expected.out @@ -1,5 +1,5 @@ elseifDoErrorPos.lean:4:7-7:14: error: application type mismatch - ite x + @ite ?m x argument x has type diff --git a/tests/lean/infoTree.lean.expected.out b/tests/lean/infoTree.lean.expected.out index 1bdc9102e4..1199c388f7 100644 --- a/tests/lean/infoTree.lean.expected.out +++ b/tests/lean/infoTree.lean.expected.out @@ -26,7 +26,7 @@ ===> Prod.mk✝ x x (x, x) : Nat × Nat @ ⟨14, 11⟩†-⟨14, 16⟩ @ Lean.Elab.Term.elabApp - Prod.mk : {α β : Type} → α → β → α × β @ ⟨14, 11⟩†-⟨14, 17⟩† + @Prod.mk : {α β : Type} → α → β → α × β @ ⟨14, 11⟩†-⟨14, 17⟩† x : Nat @ ⟨14, 12⟩-⟨14, 13⟩ @ Lean.Elab.Term.elabIdent x : Nat @ ⟨14, 12⟩-⟨14, 13⟩ x : Nat @ ⟨14, 15⟩-⟨14, 16⟩ @ Lean.Elab.Term.elabIdent @@ -34,7 +34,7 @@ y : Nat × Nat @ ⟨14, 6⟩-⟨14, 7⟩ id y : Nat × Nat @ ⟨15, 2⟩-⟨15, 6⟩ @ Lean.Elab.Term.elabApp [.] `id : some Prod.{0 0} Nat Nat @ ⟨15, 2⟩-⟨15, 4⟩ - id : {α : Type} → α → α @ ⟨15, 2⟩-⟨15, 4⟩ + @id : {α : Type} → α → α @ ⟨15, 2⟩-⟨15, 4⟩ y : Nat × Nat @ ⟨15, 5⟩-⟨15, 6⟩ @ Lean.Elab.Term.elabIdent y : Nat × Nat @ ⟨15, 5⟩-⟨15, 6⟩ f : Nat → Nat × Nat @ ⟨13, 4⟩-⟨13, 5⟩ @@ -166,7 +166,7 @@ ===> Prod.mk✝ (x + y) (x - y) (x + y, x - y) : Nat × Nat @ ⟨23, 18⟩†-⟨23, 31⟩ @ Lean.Elab.Term.elabApp - Prod.mk : {α β : Type} → α → β → α × β @ ⟨23, 18⟩†-⟨23, 32⟩† + @Prod.mk : {α β : Type} → α → β → α × β @ ⟨23, 18⟩†-⟨23, 32⟩† x + y : Nat @ ⟨23, 19⟩-⟨23, 24⟩ @ «_aux_Init_Notation___macroRules_term_+__2» Macro expansion x + y @@ -193,11 +193,11 @@ let z1 := z + w; z + z1 : Nat @ ⟨23, 4⟩†-⟨25, 10⟩ @ Lean.Elab.Term.elabMatch x✝ : Nat × Nat @ ⟨23, 4⟩†-⟨25, 10⟩† - Prod.mk : {α : Type ?u} → {β : Type ?u} → α → β → α × β @ ⟨23, 4⟩†-⟨25, 10⟩† + @Prod.mk : {α : Type ?u} → {β : Type ?u} → α → β → α × β @ ⟨23, 4⟩†-⟨25, 10⟩† [.] `z : none @ ⟨23, 9⟩-⟨23, 10⟩ [.] `w : none @ ⟨23, 12⟩-⟨23, 13⟩ (z, w) : Nat × Nat @ ⟨23, 4⟩†-⟨23, 13⟩ @ Lean.Elab.Term.elabApp - Prod.mk : {α β : Type} → α → β → α × β @ ⟨23, 4⟩†-⟨25, 10⟩† + @Prod.mk : {α β : Type} → α → β → α × β @ ⟨23, 4⟩†-⟨25, 10⟩† Nat : Type @ ⟨23, 4⟩†-⟨23, 13⟩† @ Lean.Elab.Term.elabHole Nat : Type @ ⟨23, 4⟩†-⟨23, 13⟩† @ Lean.Elab.Term.elabHole z : Nat @ ⟨23, 9⟩-⟨23, 10⟩ @ Lean.Elab.Term.elabIdent @@ -264,14 +264,14 @@ s : Nat × Array (Array Nat) @ ⟨27, 8⟩-⟨27, 9⟩ Array.push (Array.getOp s.snd 1) s.fst : Array Nat @ ⟨28, 2⟩-⟨28, 17⟩ @ Lean.Elab.Term.elabApp s : Nat × Array (Array Nat) @ ⟨28, 2⟩-⟨28, 3⟩ - Prod.snd : {α β : Type} → α × β → β @ ⟨28, 4⟩-⟨28, 5⟩ - Array.getOp : {α : Type} → [inst : Inhabited α] → Array α → Nat → α @ ⟨28, 5⟩-⟨28, 6⟩ + @Prod.snd : {α β : Type} → α × β → β @ ⟨28, 4⟩-⟨28, 5⟩ + @Array.getOp : {α : Type} → [inst : Inhabited α] → Array α → Nat → α @ ⟨28, 5⟩-⟨28, 6⟩ 1 : Nat @ ⟨28, 6⟩-⟨28, 7⟩ @ Lean.Elab.Term.elabNumLit [.] Array.getOp s.snd 1 : Array Nat @ ⟨28, 2⟩-⟨28, 8⟩ : some Array.{0} Nat - Array.push : {α : Type} → Array α → α → Array α @ ⟨28, 9⟩-⟨28, 13⟩ + @Array.push : {α : Type} → Array α → α → Array α @ ⟨28, 9⟩-⟨28, 13⟩ s.fst : Nat @ ⟨28, 14⟩-⟨28, 17⟩ @ Lean.Elab.Term.elabProj s : Nat × Array (Array Nat) @ ⟨28, 14⟩-⟨28, 15⟩ - Prod.fst : {α β : Type} → α × β → α @ ⟨28, 16⟩-⟨28, 17⟩ + @Prod.fst : {α β : Type} → α × β → α @ ⟨28, 16⟩-⟨28, 17⟩ f3 : Nat × Array (Array Nat) → Array Nat @ ⟨27, 4⟩-⟨27, 6⟩ [Elab.info] command @ ⟨30, 0⟩-⟨31, 20⟩ @ Lean.Elab.Command.elabDeclaration B : Type @ ⟨30, 14⟩-⟨30, 15⟩ @ Lean.Elab.Term.elabIdent @@ -287,7 +287,7 @@ [.] arg : B @ ⟨31, 2⟩-⟨31, 18⟩ : some Nat B.pair : B → A × A @ ⟨31, 6⟩-⟨31, 10⟩ [.] arg.pair : A × A @ ⟨31, 2⟩-⟨31, 18⟩ : some Nat - Prod.fst : {α β : Type} → α × β → α @ ⟨31, 11⟩-⟨31, 14⟩ + @Prod.fst : {α β : Type} → α × β → α @ ⟨31, 11⟩-⟨31, 14⟩ [.] arg.pair.fst : A @ ⟨31, 2⟩-⟨31, 18⟩ : some Nat A.val : A → Nat → Nat @ ⟨31, 15⟩-⟨31, 18⟩ 0 : Nat @ ⟨31, 19⟩-⟨31, 20⟩ @ Lean.Elab.Term.elabNumLit @@ -308,16 +308,16 @@ ===> Prod.mk✝ { val := id } { val := id } ({ val := id }, { val := id }) : A × A @ ⟨34, 10⟩†-⟨34, 39⟩ @ Lean.Elab.Term.elabApp - Prod.mk : {α β : Type} → α → β → α × β @ ⟨34, 10⟩†-⟨34, 40⟩† + @Prod.mk : {α β : Type} → α → β → α × β @ ⟨34, 10⟩†-⟨34, 40⟩† { val := id } : A @ ⟨34, 11⟩-⟨34, 24⟩ @ Lean.Elab.Term.StructInst.elabStructInst id : Nat → Nat @ ⟨34, 20⟩-⟨34, 22⟩ @ Lean.Elab.Term.elabIdent [.] `id : some Nat -> Nat @ ⟨34, 20⟩-⟨34, 22⟩ - id : {α : Type} → α → α @ ⟨34, 20⟩-⟨34, 22⟩ + @id : {α : Type} → α → α @ ⟨34, 20⟩-⟨34, 22⟩ val : Nat → Nat := id @ ⟨34, 13⟩-⟨34, 16⟩ { val := id } : A @ ⟨34, 26⟩-⟨34, 39⟩ @ Lean.Elab.Term.StructInst.elabStructInst id : Nat → Nat @ ⟨34, 35⟩-⟨34, 37⟩ @ Lean.Elab.Term.elabIdent [.] `id : some Nat -> Nat @ ⟨34, 35⟩-⟨34, 37⟩ - id : {α : Type} → α → α @ ⟨34, 35⟩-⟨34, 37⟩ + @id : {α : Type} → α → α @ ⟨34, 35⟩-⟨34, 37⟩ val : Nat → Nat := id @ ⟨34, 28⟩-⟨34, 31⟩ pair : A × A := ({ val := id }, { val := id }) @ ⟨34, 2⟩-⟨34, 6⟩ f5 : Nat → B @ ⟨33, 4⟩-⟨33, 6⟩ diff --git a/tests/lean/interactive/hover.lean.expected.out b/tests/lean/interactive/hover.lean.expected.out index aa25fc0f0d..416cb34bee 100644 --- a/tests/lean/interactive/hover.lean.expected.out +++ b/tests/lean/interactive/hover.lean.expected.out @@ -80,7 +80,7 @@ null {"range": {"start": {"line": 93, "character": 8}, "end": {"line": 93, "character": 10}}, "contents": - {"value": "```lean\nid.{0} : ∀ {α : Prop}, α → α\n```", "kind": "markdown"}} + {"value": "```lean\n@id.{0} : ∀ {α : Prop}, α → α\n```", "kind": "markdown"}} {"textDocument": {"uri": "file://hover.lean"}, "position": {"line": 93, "character": 10}} {"range": diff --git a/tests/lean/openScoped.lean.expected.out b/tests/lean/openScoped.lean.expected.out index 98d19f3dc5..0d2f678226 100644 --- a/tests/lean/openScoped.lean.expected.out +++ b/tests/lean/openScoped.lean.expected.out @@ -1,6 +1,6 @@ openScoped.lean:1:8-1:15: error: unknown identifier 'epsilon' openScoped.lean:4:2-4:24: error: failed to synthesize instance Decidable (f = g) -epsilon : {α : Sort u_1} → [h : Nonempty α] → (α → Prop) → α +@epsilon : {α : Sort u_1} → [h : Nonempty α] → (α → Prop) → α openScoped.lean:15:8-15:15: error: unknown identifier 'epsilon' openScoped.lean:20:8-20:15: error: unknown identifier 'epsilon' diff --git a/tests/lean/pplevel.lean.expected.out b/tests/lean/pplevel.lean.expected.out index e6e05f6c2e..f6e5662cc1 100644 --- a/tests/lean/pplevel.lean.expected.out +++ b/tests/lean/pplevel.lean.expected.out @@ -1,6 +1,6 @@ Type (max u v w) : Type ((max u v w) + 1) Type u : Type (u + 1) -id.{max u v w} : {α : Sort (max u v w)} → α → α +@id.{max u v w} : {α : Sort (max u v w)} → α → α Monad.{max u v, w + 1} : (Type (max u v) → Type (w + 1)) → Type (max ((max u v) + 1) (w + 1)) Type (max (u + 1) w (v + 2)) : Type ((max (u + 1) w (v + 2)) + 1) Type u_1 : Type (u_1 + 1) diff --git a/tests/lean/sizeof.lean.expected.out b/tests/lean/sizeof.lean.expected.out index eaf831bfd4..0a5dc9a442 100644 --- a/tests/lean/sizeof.lean.expected.out +++ b/tests/lean/sizeof.lean.expected.out @@ -7,5 +7,5 @@ 308 310 11 -InfTree.node.sizeOf_spec : ∀ {α : Type u_1} [inst : SizeOf α] (children : Nat → InfTree α), +@InfTree.node.sizeOf_spec : ∀ {α : Type u_1} [inst : SizeOf α] (children : Nat → InfTree α), sizeOf (InfTree.node children) = 1