From 8863761401845e8aa2be9e5cef7640d09e0cc3c1 Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Sat, 1 May 2021 23:26:31 +0200 Subject: [PATCH] feat: show initial state for tactic combinators by default --- src/Lean/Elab/SyntheticMVars.lean | 10 +---- src/Lean/Elab/Tactic/Basic.lean | 33 +++++++++-------- src/Lean/Server/FileWorker.lean | 4 +- src/Lean/Server/InfoUtils.lean | 37 +++++++++++++------ tests/lean/infoTree.lean.expected.out | 8 +++- tests/lean/interactive/plainGoal.lean | 4 +- .../interactive/plainGoal.lean.expected.out | 6 ++- 7 files changed, 62 insertions(+), 40 deletions(-) diff --git a/src/Lean/Elab/SyntheticMVars.lean b/src/Lean/Elab/SyntheticMVars.lean index e0b69aaa6a..7c07cff814 100644 --- a/src/Lean/Elab/SyntheticMVars.lean +++ b/src/Lean/Elab/SyntheticMVars.lean @@ -8,7 +8,7 @@ import Lean.Elab.Term import Lean.Elab.Tactic.Basic namespace Lean.Elab.Term -open Tactic (TacticM evalTactic getUnsolvedGoals mkTacticInfo) +open Tactic (TacticM evalTactic getUnsolvedGoals withTacticInfoContext) open Meta /-- Auxiliary function used to implement `synthesizeSyntheticMVars`. -/ @@ -211,13 +211,7 @@ mutual modifyThe Meta.State fun s => { s with mctx := s.mctx.instantiateMVarDeclMVars mvarId } let remainingGoals ← withInfoHole mvarId <| liftTacticElabM mvarId do - let mctxBefore ← getMCtx - -- NOTE: we need an outer node as `withInfoHole` discards all trees but the last one - withInfoContext (do - -- push separate leaf for `by` so we show the initial state on the whole token - pushInfoLeaf (← mkTacticInfo mctxBefore [mvarId] byTk) - evalTactic code) - (mkTacticInfo mctxBefore [mvarId] tacticCode) + withTacticInfoContext tacticCode (evalTactic code) getUnsolvedGoals unless remainingGoals.isEmpty do reportUnsolvedGoals remainingGoals diff --git a/src/Lean/Elab/Tactic/Basic.lean b/src/Lean/Elab/Tactic/Basic.lean index c12a9661d6..4083fda6f3 100644 --- a/src/Lean/Elab/Tactic/Basic.lean +++ b/src/Lean/Elab/Tactic/Basic.lean @@ -95,6 +95,20 @@ private def evalTacticUsing (s : SavedState) (stx : Syntax) (tactics : List Tact def getGoals : TacticM (List MVarId) := return (← get).goals +def mkTacticInfo (mctxBefore : MetavarContext) (goalsBefore : List MVarId) (stx : Syntax) : TacticM Info := + return Info.ofTacticInfo { + mctxBefore := mctxBefore + goalsBefore := goalsBefore + stx := stx + mctxAfter := (← getMCtx) + goalsAfter := (← getGoals) + } + +@[inline] def withTacticInfoContext (stx : Syntax) (x : TacticM α) : TacticM α := do + let mctxBefore ← getMCtx + let goalsBefore ← getGoals + withInfoContext x (mkTacticInfo mctxBefore goalsBefore stx) + mutual partial def expandTacticMacroFns (stx : Syntax) (macros : List Macro) : TacticM Unit := @@ -132,19 +146,8 @@ mutual | none => expandTacticMacro stx | _ => throwError "unexpected command" - partial def mkTacticInfo (mctxBefore : MetavarContext) (goalsBefore : List MVarId) (stx : Syntax) : TacticM Info := - return Info.ofTacticInfo { - mctxBefore := mctxBefore - goalsBefore := goalsBefore - stx := stx - mctxAfter := (← getMCtx) - goalsAfter := (← getGoals) - } - - partial def evalTactic (stx : Syntax) : TacticM Unit := do - let mctxBefore ← getMCtx - let goalsBefore ← getGoals - withInfoContext (evalTacticAux stx) (mkTacticInfo mctxBefore goalsBefore stx) + partial def evalTactic (stx : Syntax) : TacticM Unit := + withTacticInfoContext stx (evalTacticAux stx) end @@ -155,9 +158,7 @@ end -/ def saveTacticInfoForToken (stx : Syntax) : TacticM Unit := do unless stx.getPos?.isNone do - let mctxBefore ← getMCtx - let goalsBefore ← getGoals - withInfoContext (pure ()) (mkTacticInfo mctxBefore goalsBefore stx) + withTacticInfoContext stx (pure ()) /- Elaborate `x` with `stx` on the macro stack -/ @[inline] diff --git a/src/Lean/Server/FileWorker.lean b/src/Lean/Server/FileWorker.lean index 6b01e900c7..a36f15f9fb 100644 --- a/src/Lean/Server/FileWorker.lean +++ b/src/Lean/Server/FileWorker.lean @@ -609,10 +609,10 @@ section RequestHandling if let (some pos, some tailPos) := (stx.getPos?, stx.getTailPos?) then for t in (← read).infoState.trees do for ti in t.deepestNodes (fun - | _, i@(Elab.Info.ofTermInfo ti) => match i.pos? with + | _, i@(Elab.Info.ofTermInfo ti), _ => match i.pos? with | some ipos => if pos <= ipos && ipos < tailPos then some ti else none | _ => none - | _, _ => none) do + | _, _, _ => none) do match ti.expr with | Expr.fvar .. => addToken ti.stx SemanticTokenType.variable | _ => if ti.stx.getPos?.get! > pos then addToken ti.stx SemanticTokenType.property diff --git a/src/Lean/Server/InfoUtils.lean b/src/Lean/Server/InfoUtils.lean index 0340ab40f3..1e3f97d0bf 100644 --- a/src/Lean/Server/InfoUtils.lean +++ b/src/Lean/Server/InfoUtils.lean @@ -13,17 +13,16 @@ namespace Lean.Elab /-- For every branch, find the deepest node in that branch matching `p` with a surrounding context (the innermost one) and return all of them. -/ -partial def InfoTree.deepestNodes (p : ContextInfo → Info → Option α) : InfoTree → List α := +partial def InfoTree.deepestNodes (p : ContextInfo → Info → Std.PersistentArray InfoTree → Option α) : InfoTree → List α := go none where go ctx? | context ctx t => go ctx t | n@(node i cs) => - let cs := cs.toList - let ccs := cs.map (go <| i.updateContext? ctx?) - let cs := ccs.join - if !cs.isEmpty then cs + let ccs := cs.toList.map (go <| i.updateContext? ctx?) + let cs' := ccs.join + if !cs'.isEmpty then cs' else match ctx? with - | some ctx => match p ctx i with + | some ctx => match p ctx i cs with | some a => [a] | _ => [] | _ => [] @@ -86,7 +85,7 @@ def Info.occursBefore? (i : Info) (hoverPos : String.Pos) : Option Nat := Option return hoverPos - tailPos def InfoTree.smallestInfo? (p : Info → Bool) (t : InfoTree) : Option (ContextInfo × Info) := - let ts := t.deepestNodes fun ctx i => if p i then some (ctx, i) else none + let ts := t.deepestNodes fun ctx i _ => if p i then some (ctx, i) else none let infos := ts.map fun (ci, i) => let diff := i.tailPos?.get! - i.pos?.get! @@ -160,18 +159,34 @@ structure GoalsAtResult where - None of the `children` can provide satisfy the condition above. That is, for composite tactics such as `induction`, we always give preference for information stored in nested (children) tactics. - Moreover, we instruct the LSP server to use the state after the tactic execution if hoverPos >= endPos + Moreover, we instruct the LSP server to use the state after the tactic execution if hoverPos >= endPos *and* + there is no nested tactic info (i.e. it is a leaf tactic; tactic combinators should decide for themselves + where to show intermediate/final states) -/ partial def InfoTree.goalsAt? (t : InfoTree) (hoverPos : String.Pos) : List GoalsAtResult := do t.deepestNodes fun - | ctx, i@(Info.ofTacticInfo ti) => OptionM.run do + | ctx, i@(Info.ofTacticInfo ti), cs => OptionM.run do let (some pos, some tailPos) ← pure (i.pos?, i.tailPos?) | failure let trailSize := i.stx.getTrailingSize -- NOTE: include position just after tactic, i.e. when the cursor is still adjacent -- (even when `trailSize == 0`, which is the case at EOF) guard <| pos ≤ hoverPos ∧ hoverPos < tailPos + Nat.max 1 trailSize - return { ctxInfo := ctx, tacticInfo := ti, useAfter := hoverPos > pos } - | _, _ => none + return { ctxInfo := ctx, tacticInfo := ti, useAfter := + hoverPos > pos && !cs.any (hasNestedTactic pos tailPos) } + | _, _, _ => none +where + hasNestedTactic (pos tailPos) : InfoTree → Bool + | InfoTree.node (Info.ofTacticInfo ti) cs => do + if let `(by $t) := ti.stx then + return false -- ignore term-nested proofs such as in `simp [show p by ...]` + if let (some pos', some tailPos') := (ti.stx.getPos?, ti.stx.getTailPos?) then + -- ignore nested infos of the same tactic, e.g. from expansion + if (pos', tailPos') != (pos, tailPos) then + return true + cs.any (hasNestedTactic pos tailPos) + | InfoTree.node (Info.ofMacroExpansionInfo _) cs => + cs.any (hasNestedTactic pos tailPos) + | _ => false end Lean.Elab diff --git a/tests/lean/infoTree.lean.expected.out b/tests/lean/infoTree.lean.expected.out index 805d36e573..168478c3db 100644 --- a/tests/lean/infoTree.lean.expected.out +++ b/tests/lean/infoTree.lean.expected.out @@ -81,7 +81,7 @@ y : Nat @ ⟨18, 8⟩-⟨18, 9⟩ Bool : Type @ ⟨18, 10⟩-⟨18, 11⟩ b : Bool @ ⟨18, 10⟩-⟨18, 11⟩ - Tactic @ ⟨19, 4⟩-⟨19, 8⟩ + Tactic @ ⟨18, 15⟩-⟨19, 8⟩ before x y : Nat b : Bool @@ -99,6 +99,12 @@ b : Bool ⊢ x + 0 = x after no goals + Tactic @ ⟨19, 4⟩-⟨19, 8⟩ + before + x y : Nat + b : Bool + ⊢ x + 0 = x + after no goals [Elab.info] command @ ⟨21, 0⟩-⟨25, 10⟩ Nat → Nat → Bool → Nat : Type @ ⟨21, 9⟩-⟨21, 39⟩ Nat : Type @ ⟨21, 16⟩-⟨21, 19⟩ diff --git a/tests/lean/interactive/plainGoal.lean b/tests/lean/interactive/plainGoal.lean index ed64ea6bf2..732305480b 100644 --- a/tests/lean/interactive/plainGoal.lean +++ b/tests/lean/interactive/plainGoal.lean @@ -4,7 +4,9 @@ example : α → α := by intro a --^ $/lean/plainGoal --^ $/lean/plainGoal - apply a + --v $/lean/plainGoal + focus + apply a example : α → α := by --^ $/lean/plainGoal diff --git a/tests/lean/interactive/plainGoal.lean.expected.out b/tests/lean/interactive/plainGoal.lean.expected.out index b41d6529b5..77f9dc0513 100644 --- a/tests/lean/interactive/plainGoal.lean.expected.out +++ b/tests/lean/interactive/plainGoal.lean.expected.out @@ -15,6 +15,10 @@ {"rendered": "```lean\nα : Sort ?u\na : α\n⊢ α\n```", "goals": ["α : Sort ?u\na : α\n⊢ α"]} {"textDocument": {"uri": "file://plainGoal.lean"}, - "position": {"line": 8, "character": 20}} + "position": {"line": 7, "character": 3}} +{"rendered": "```lean\nα : Sort ?u\na : α\n⊢ α\n```", + "goals": ["α : Sort ?u\na : α\n⊢ α"]} +{"textDocument": {"uri": "file://plainGoal.lean"}, + "position": {"line": 10, "character": 20}} {"rendered": "```lean\nα : Sort ?u\n⊢ α → α\n```", "goals": ["α : Sort ?u\n⊢ α → α"]}