From 4e292be6febee52168f06a333865f6304bd5f1c0 Mon Sep 17 00:00:00 2001 From: Kyle Miller Date: Thu, 24 Oct 2024 15:56:47 -0700 Subject: [PATCH] chore: review delaborators, make sure they respond to `pp.explicit` (#5830) Rule: if an expression contains an implicit argument that the delaborator would omit, only use the delaborator if `pp.explicit` is false. --- .../PrettyPrinter/Delaborator/Builtins.lean | 19 +++++++++++-------- tests/lean/delabOverApp.lean.expected.out | 2 +- tests/lean/run/delabProjectionApp.lean | 4 ++-- .../rwWithSynthesizeBug.lean.expected.out | 4 ++-- 4 files changed, 16 insertions(+), 13 deletions(-) diff --git a/src/Lean/PrettyPrinter/Delaborator/Builtins.lean b/src/Lean/PrettyPrinter/Delaborator/Builtins.lean index 68051e96ea3a..aa13f8f2c5cb 100644 --- a/src/Lean/PrettyPrinter/Delaborator/Builtins.lean +++ b/src/Lean/PrettyPrinter/Delaborator/Builtins.lean @@ -1014,7 +1014,7 @@ Delaborates an `OfNat.ofNat` literal. `@OfNat.ofNat _ n _` ~> `n`. -/ @[builtin_delab app.OfNat.ofNat] -def delabOfNat : Delab := whenPPOption getPPCoercions <| withOverApp 3 do +def delabOfNat : Delab := whenNotPPOption getPPExplicit <| whenPPOption getPPCoercions <| withOverApp 3 do delabOfNatCore (showType := (← getPPOption getPPNumericTypes)) /-- @@ -1022,7 +1022,7 @@ Delaborates the negative of an `OfNat.ofNat` literal. `-@OfNat.ofNat _ n _` ~> `-n` -/ @[builtin_delab app.Neg.neg] -def delabNeg : Delab := whenPPOption getPPCoercions do +def delabNeg : Delab := whenNotPPOption getPPExplicit <| whenPPOption getPPCoercions do delabNegIntCore (showType := (← getPPOption getPPNumericTypes)) /-- @@ -1031,12 +1031,12 @@ Delaborates a rational number literal. and `-@OfNat.ofNat _ n _ / @OfNat.ofNat _ m` ~> `-n / m` -/ @[builtin_delab app.HDiv.hDiv] -def delabHDiv : Delab := whenPPOption getPPCoercions do +def delabHDiv : Delab := whenNotPPOption getPPExplicit <| whenPPOption getPPCoercions do delabDivRatCore (showType := (← getPPOption getPPNumericTypes)) -- `@OfDecimal.ofDecimal _ _ m s e` ~> `m*10^(sign * e)` where `sign == 1` if `s = false` and `sign = -1` if `s = true` @[builtin_delab app.OfScientific.ofScientific] -def delabOfScientific : Delab := whenPPOption getPPCoercions <| withOverApp 5 do +def delabOfScientific : Delab := whenNotPPOption getPPExplicit <| whenPPOption getPPCoercions <| withOverApp 5 do let expr ← getExpr guard <| expr.getAppNumArgs == 5 let .lit (.natVal m) ← pure (expr.getArg! 2) | failure @@ -1080,6 +1080,9 @@ def coeDelaborator : Delab := whenPPOption getPPCoercions do let e ← getExpr let .const declName _ := e.getAppFn | failure let some info ← Meta.getCoeFnInfo? declName | failure + if (← getPPOption getPPExplicit) && info.coercee != 0 then + -- Approximation: the only implicit arguments come before the coercee + failure let n := e.getAppNumArgs withOverApp info.numArgs do match info.type with @@ -1092,7 +1095,7 @@ def coeDelaborator : Delab := whenPPOption getPPCoercions do | .coeSort => `(↥$(← withNaryArg info.coercee delab)) @[builtin_delab app.dite] -def delabDIte : Delab := whenPPOption getPPNotation <| withOverApp 5 do +def delabDIte : Delab := whenNotPPOption getPPExplicit <| whenPPOption getPPNotation <| withOverApp 5 do -- Note: we keep this as a delaborator for now because it actually accesses the expression. guard $ (← getExpr).getAppNumArgs == 5 let c ← withAppFn $ withAppFn $ withAppFn $ withAppArg delab @@ -1109,7 +1112,7 @@ where return (← delab, h.getId) @[builtin_delab app.cond] -def delabCond : Delab := whenPPOption getPPNotation <| withOverApp 4 do +def delabCond : Delab := whenNotPPOption getPPExplicit <| whenPPOption getPPNotation <| withOverApp 4 do guard $ (← getExpr).getAppNumArgs == 4 let c ← withAppFn $ withAppFn $ withAppArg delab let t ← withAppFn $ withAppArg delab @@ -1129,7 +1132,7 @@ def delabNamedPattern : Delab := do `($x:ident@$h:ident:$p:term) -- Sigma and PSigma delaborators -def delabSigmaCore (sigma : Bool) : Delab := whenPPOption getPPNotation do +def delabSigmaCore (sigma : Bool) : Delab := whenNotPPOption getPPExplicit <| whenPPOption getPPNotation do guard $ (← getExpr).getAppNumArgs == 2 guard $ (← getExpr).appArg!.isLambda withAppArg do @@ -1209,7 +1212,7 @@ partial def delabDoElems : DelabM (List Syntax) := do prependAndRec x : DelabM _ := List.cons <$> x <*> delabDoElems @[builtin_delab app.Bind.bind] -def delabDo : Delab := whenPPOption getPPNotation do +def delabDo : Delab := whenNotPPOption getPPExplicit <| whenPPOption getPPNotation do guard <| (← getExpr).isAppOfArity ``Bind.bind 6 let elems ← delabDoElems let items ← elems.toArray.mapM (`(doSeqItem|$(·):doElem)) diff --git a/tests/lean/delabOverApp.lean.expected.out b/tests/lean/delabOverApp.lean.expected.out index 43157f618050..db68ae147eee 100644 --- a/tests/lean/delabOverApp.lean.expected.out +++ b/tests/lean/delabOverApp.lean.expected.out @@ -3,4 +3,4 @@ f +' g : Nat → Nat f * g : Nat → Nat (f * g) 1 : Nat mul f g : Nat → Nat -mul f g 1 : Nat +mul f g (@OfNat.ofNat Nat 1 (instOfNatNat 1)) : Nat diff --git a/tests/lean/run/delabProjectionApp.lean b/tests/lean/run/delabProjectionApp.lean index 3e4ec1b0eb9e..abf5b90df4c3 100644 --- a/tests/lean/run/delabProjectionApp.lean +++ b/tests/lean/run/delabProjectionApp.lean @@ -97,9 +97,9 @@ set_option pp.explicit true #guard_msgs in #check x.val /-- info: y.val : Nat -/ #guard_msgs in #check y.val -/-- info: (@Fin''.toFin0 5 z).val : Nat -/ +/-- info: (@Fin''.toFin0 (@OfNat.ofNat Nat 5 (instOfNatNat 5)) z).val : Nat -/ #guard_msgs in #check z.val -/-- info: (@D.toA 5 d).x : Nat -/ +/-- info: (@D.toA (@OfNat.ofNat Nat 5 (instOfNatNat 5)) d).x : Nat -/ #guard_msgs in #check d.x end diff --git a/tests/lean/rwWithSynthesizeBug.lean.expected.out b/tests/lean/rwWithSynthesizeBug.lean.expected.out index 346fb27aae7b..4174cef80c4a 100644 --- a/tests/lean/rwWithSynthesizeBug.lean.expected.out +++ b/tests/lean/rwWithSynthesizeBug.lean.expected.out @@ -1,4 +1,4 @@ rwWithSynthesizeBug.lean:36:18-39:15: error: unsolved goals -inst : Bar Nat := @Bar.mk Nat 0 -h : @w Nat (@f Nat inst 5) +inst : Bar Nat := @Bar.mk Nat (@OfNat.ofNat Nat 0 (instOfNatNat 0)) +h : @w Nat (@f Nat inst (@OfNat.ofNat Nat 5 (instOfNatNat 5))) ⊢ True