From 4d077214f9cfc52db875a98aa753ce49a7b395f8 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sat, 9 Apr 2022 15:26:56 -0700 Subject: [PATCH] feat: jump to definition for `match` pattern variables --- src/Lean/Elab/Match.lean | 32 +++++++++++++------ .../1018unknowMVarIssue.lean.expected.out | 8 ++--- tests/lean/infoTree.lean.expected.out | 5 +-- .../interactive/discrsIssue.lean.expected.out | 3 +- 4 files changed, 31 insertions(+), 17 deletions(-) diff --git a/src/Lean/Elab/Match.lean b/src/Lean/Elab/Match.lean index 3f169351d4..c802fac250 100644 --- a/src/Lean/Elab/Match.lean +++ b/src/Lean/Elab/Match.lean @@ -605,16 +605,30 @@ where /-- Save pattern information in the info tree, and remove `patternWithRef?` annotations. -/ -def savePatternInfo (p : Expr) : TermElabM Expr := - withReader (fun ctx => { ctx with inPattern := false }) do - let post (e : Expr) : TermElabM TransformStep := do - if let some (stx, e) := patternWithRef? e then - -- TODO: track whether we are inside of an inaccessible, and set `isBinder` - addTermInfo' stx e - return .done e +partial def savePatternInfo (p : Expr) : TermElabM Expr := + go p |>.run false +where + /- The `Bool` context is true iff we are inside of an "inaccessible" pattern. -/ + go (p : Expr) : ReaderT Bool TermElabM Expr := do + match p with + | .forallE n d b bi => withLocalDecl n b.binderInfo (← go d) fun x => do mkForallFVars #[x] (← go (b.instantiate1 x)) + | .lam n d b bi => withLocalDecl n b.binderInfo (← go d) fun x => do mkLambdaFVars #[x] (← go (b.instantiate1 x)) + | .letE n t v b .. => withLetDecl n (← go t) (← go v) fun x => do mkLetFVars #[x] (← go (b.instantiate1 x)) + | .app f a _ => return mkApp (← go f) (← go a) + | .proj _ _ b _ => return p.updateProj! (← go b) + | .mdata k b _ => + if inaccessible? p |>.isSome then + return mkMData k (← withReader (fun _ => false) (go b)) + else if let some (stx, p) := patternWithRef? p then + let p ← go p + if p.isFVar && !(← read) then + /- If `p` is a free variable and we are not inside of an "inaccessible" pattern, this `p` is a binder. -/ + addTermInfo stx p (isBinder := true) + else + addTermInfo stx p else - return .done e - transform p (post := post) + return mkMData k (← go b) + | _ => return p /-- Main method for `withDepElimPatterns`. diff --git a/tests/lean/1018unknowMVarIssue.lean.expected.out b/tests/lean/1018unknowMVarIssue.lean.expected.out index 6a1e77597d..6a3239357b 100644 --- a/tests/lean/1018unknowMVarIssue.lean.expected.out +++ b/tests/lean/1018unknowMVarIssue.lean.expected.out @@ -46,11 +46,11 @@ a : α @Fam2.any : {α : Type} → Fam2 α α @ ⟨9, 4⟩-⟨9, 12⟩ a : α @ ⟨8, 2⟩†-⟨10, 19⟩† [.] `Fam2.any : some Fam2 ([mdata _patWithRef: [mdata _inaccessible:1 [mdata _patWithRef: ?_uniq.652]]]) ([mdata _patWithRef: [mdata _inaccessible:1 [mdata _patWithRef: ?_uniq.653]]]) @ ⟨9, 4⟩-⟨9, 12⟩ - α : Type @ ⟨8, 2⟩†-⟨10, 19⟩† + α (isBinder := true) : Type @ ⟨8, 2⟩†-⟨10, 19⟩† α : Type @ ⟨8, 2⟩†-⟨10, 19⟩† α : Type @ ⟨9, 4⟩†-⟨9, 12⟩† Fam2.any : Fam2 α α @ ⟨9, 4⟩†-⟨9, 12⟩† - a : α @ ⟨8, 2⟩†-⟨10, 19⟩† + a (isBinder := true) : α @ ⟨8, 2⟩†-⟨10, 19⟩† ?m x α a : α @ ⟨9, 18⟩-⟨9, 19⟩ @ Lean.Elab.Term.elabHole [.] `Fam2.nat : none @ ⟨10, 4⟩-⟨10, 12⟩ Fam2.nat : Nat → Fam2 Nat Nat @ ⟨10, 4⟩-⟨10, 12⟩ @@ -59,9 +59,9 @@ a : α [.] `Fam2.nat : some Fam2 ([mdata _patWithRef: [mdata _inaccessible:1 [mdata _patWithRef: ?_uniq.684]]]) ([mdata _patWithRef: [mdata _inaccessible:1 [mdata _patWithRef: ?_uniq.685]]]) @ ⟨10, 4⟩-⟨10, 12⟩ Nat : Type @ ⟨8, 2⟩†-⟨10, 19⟩† Nat : Type @ ⟨8, 2⟩†-⟨10, 19⟩† - n : Nat @ ⟨10, 13⟩-⟨10, 14⟩ + n (isBinder := true) : Nat @ ⟨10, 13⟩-⟨10, 14⟩ Fam2.nat n : Fam2 Nat Nat @ ⟨10, 4⟩†-⟨10, 14⟩ - a : Nat @ ⟨8, 2⟩†-⟨10, 19⟩† + a (isBinder := true) : Nat @ ⟨8, 2⟩†-⟨10, 19⟩† n : Nat @ ⟨10, 18⟩-⟨10, 19⟩ @ Lean.Elab.Term.elabIdent n : Nat @ ⟨10, 18⟩-⟨10, 19⟩ @_example (isBinder := true) : {α β : Type} → α → Fam2 α β → β @ ⟨7, 0⟩-⟨7, 7⟩ diff --git a/tests/lean/infoTree.lean.expected.out b/tests/lean/infoTree.lean.expected.out index d8ad8e7d94..1bd111a2fa 100644 --- a/tests/lean/infoTree.lean.expected.out +++ b/tests/lean/infoTree.lean.expected.out @@ -216,8 +216,9 @@ [.] `z : none @ ⟨23, 9⟩-⟨23, 10⟩ [.] `w : none @ ⟨23, 12⟩-⟨23, 13⟩ Nat : Type @ ⟨23, 4⟩†-⟨23, 13⟩† - z : Nat @ ⟨23, 9⟩-⟨23, 10⟩ - w : Nat @ ⟨23, 12⟩-⟨23, 13⟩ + Nat : Type @ ⟨23, 4⟩†-⟨23, 13⟩† + z (isBinder := true) : Nat @ ⟨23, 9⟩-⟨23, 10⟩ + w (isBinder := true) : Nat @ ⟨23, 12⟩-⟨23, 13⟩ (z, w) : Nat × Nat @ ⟨23, 4⟩†-⟨23, 13⟩ let z1 := z + w; z + z1 : Nat @ ⟨24, 4⟩-⟨25, 10⟩ @ Lean.Elab.Term.elabLetDecl diff --git a/tests/lean/interactive/discrsIssue.lean.expected.out b/tests/lean/interactive/discrsIssue.lean.expected.out index 49fc6a0e4f..b09821e1e0 100644 --- a/tests/lean/interactive/discrsIssue.lean.expected.out +++ b/tests/lean/interactive/discrsIssue.lean.expected.out @@ -2,5 +2,4 @@ "position": {"line": 32, "character": 18}} {"range": {"start": {"line": 32, "character": 18}, "end": {"line": 32, "character": 20}}, - "goal": - "e a b : Expr\nh₁ : HasType a Ty.nat\nh₂ : HasType b Ty.nat\n⊢ HasType a Ty.nat"} + "goal": "e a b : Expr\nh₁ : HasType a Ty.nat\n⊢ HasType a Ty.nat"}