From d8c31fb8576a7a5a3e51cdbe177a06e2dfb77d5f Mon Sep 17 00:00:00 2001 From: Kyle Miller Date: Fri, 8 Nov 2024 08:57:54 -0800 Subject: [PATCH 1/2] fix: avoid delaborating with field notation if object is a metavariable This PR prevents `Nat.succ ?_` from pretty printing as `?_.succ`, which should make `apply?` be more usable. Closes #5993 --- .../PrettyPrinter/Delaborator/Builtins.lean | 9 ++++-- tests/lean/run/5993.lean | 32 +++++++++++++++++++ 2 files changed, 38 insertions(+), 3 deletions(-) create mode 100644 tests/lean/run/5993.lean diff --git a/src/Lean/PrettyPrinter/Delaborator/Builtins.lean b/src/Lean/PrettyPrinter/Delaborator/Builtins.lean index 277078e464cd..b81d51419922 100644 --- a/src/Lean/PrettyPrinter/Delaborator/Builtins.lean +++ b/src/Lean/PrettyPrinter/Delaborator/Builtins.lean @@ -245,13 +245,16 @@ def appFieldNotationCandidate? : DelabM (Option (Nat × Name)) := do | return none unless idx < e.getAppNumArgs do return none /- - There are some kinds of expressions that cause issues with field notation, - so we prevent using it in these cases. - For example, `2.succ` is not parseable. + There are some kinds of expressions that cause issues with field notation, so we prevent using it in these cases. -/ let obj := e.getArg! idx + -- `(2).fn` is unlikely to elaborate. if obj.isRawNatLit || obj.isAppOfArity ``OfNat.ofNat 3 || obj.isAppOfArity ``OfScientific.ofScientific 5 then return none + -- `(?m).fn` is unlikely to elaborate. https://github.com/leanprover/lean4/issues/5993 + -- We also exclude metavariable applications (these are delayed assignments for example) + if obj.getAppFn.isMVar then + return none return (idx, field) /-- diff --git a/tests/lean/run/5993.lean b/tests/lean/run/5993.lean new file mode 100644 index 000000000000..b96ec4337006 --- /dev/null +++ b/tests/lean/run/5993.lean @@ -0,0 +1,32 @@ +/-! +# Avoid delaborating with field notation if object is a metavariable application. + +https://github.com/leanprover/lean4/issues/5993 +-/ + +set_option pp.mvars false + +/-! +No field notation notation here. Used to print `refine ?_.succ` and `refine ?_.snd`. +-/ + +/-- +info: Try this: refine Nat.succ ?_ +--- +info: Try this: refine Prod.snd ?_ +-/ +#guard_msgs in +example : Nat := by + show_term refine Nat.succ ?_ + show_term refine Prod.snd (α := Int) ?_ + exact default + +/-! +No field notation even under binders. (That is, be aware of delayed assignment metavariables.) +-/ + +/-- info: Try this: refine fun x => Nat.succ ?_ -/ +#guard_msgs in +example : Nat → Nat := by + show_term refine fun _ => Nat.succ ?_ + exact default From f7342cb3af9b07326837c16eae87449b6dc518ff Mon Sep 17 00:00:00 2001 From: Kyle Miller Date: Fri, 8 Nov 2024 09:05:07 -0800 Subject: [PATCH 2/2] fix tests --- tests/lean/474.lean.expected.out | 2 +- tests/lean/rewrite.lean.expected.out | 2 +- tests/lean/run/meta2.lean | 4 ++-- tests/lean/run/scopedunifhint.lean | 10 +++++----- 4 files changed, 9 insertions(+), 9 deletions(-) diff --git a/tests/lean/474.lean.expected.out b/tests/lean/474.lean.expected.out index b656f5c6b1f3..0bb9fb7d338d 100644 --- a/tests/lean/474.lean.expected.out +++ b/tests/lean/474.lean.expected.out @@ -3,6 +3,6 @@ y.add y fun y_1 => y.add y_1 fun y => Nat.add FREE y fun (y : Nat) => Nat.add y y -?m.add y +Nat.add ?m y Nat.add (?m #0) #0 fun y => (y.add y).add y diff --git a/tests/lean/rewrite.lean.expected.out b/tests/lean/rewrite.lean.expected.out index d848327ad72e..8757fb8cede2 100644 --- a/tests/lean/rewrite.lean.expected.out +++ b/tests/lean/rewrite.lean.expected.out @@ -2,7 +2,7 @@ as bs : List α ⊢ as ++ bs ++ bs = as ++ (bs ++ bs) rewrite.lean:18:20-18:29: error: tactic 'rewrite' failed, did not find instance of the pattern in the target expression - ?as.reverse.reverse + (List.reverse ?as).reverse α : Type u_1 as bs : List α ⊢ as ++ [] ++ [] ++ bs ++ bs = as ++ (bs ++ bs) diff --git a/tests/lean/run/meta2.lean b/tests/lean/run/meta2.lean index 26b9130d7cfe..c2096ce305bb 100644 --- a/tests/lean/run/meta2.lean +++ b/tests/lean/run/meta2.lean @@ -597,8 +597,8 @@ withLocalDeclD `x nat $ fun x => do /-- info: [Meta.debug] ----- tst30 ----- -[Meta.debug] (?_ x).succ -[Meta.debug] ?_.succ +[Meta.debug] Nat.succ (?_ x) +[Meta.debug] Nat.succ ?_ [Meta.debug] fun x => ?_ -/ #guard_msgs in diff --git a/tests/lean/run/scopedunifhint.lean b/tests/lean/run/scopedunifhint.lean index bb8fdd5c9a2e..09125d2521fb 100644 --- a/tests/lean/run/scopedunifhint.lean +++ b/tests/lean/run/scopedunifhint.lean @@ -35,7 +35,7 @@ argument has type Nat : Type but is expected to have type - ?_.α : Type _ + Magma.α ?_ : Type _ -/ #guard_msgs in #check mul x x -- Error: unification hint is not active @@ -48,7 +48,7 @@ argument has type Nat × Nat : Type but is expected to have type - ?_.α : Type _ + Magma.α ?_ : Type _ -/ #guard_msgs in #check mul (x, x) (x, x) -- Error: no unification hint @@ -63,7 +63,7 @@ argument has type Nat : Type but is expected to have type - ?_.α : Type _ + Magma.α ?_ : Type _ -/ #guard_msgs in #check x*x -- Error: unification hint is not active @@ -81,7 +81,7 @@ argument has type Nat × Nat : Type but is expected to have type - ?_.α : Type _ + Magma.α ?_ : Type _ -/ #guard_msgs in #check mul (x, x) (x, x) -- still error @@ -109,7 +109,7 @@ argument has type Nat × Nat : Type but is expected to have type - ?_.α : Type _ + Magma.α ?_ : Type _ -/ #guard_msgs in #check (x, x) * (x, x) -- error, local hint is not active after end of section anymore