From f5531c2a11b0a9a027cba43a6d46429e00fd1601 Mon Sep 17 00:00:00 2001 From: Wojciech Nawrocki Date: Sun, 18 Dec 2022 02:47:54 -0500 Subject: [PATCH] feat: add context and term data to goals --- .../Server/FileWorker/RequestHandling.lean | 4 +- .../Server/FileWorker/WidgetRequests.lean | 38 +++--- src/Lean/Widget/Basic.lean | 6 +- src/Lean/Widget/Diff.lean | 6 +- src/Lean/Widget/InteractiveCode.lean | 9 +- src/Lean/Widget/InteractiveGoal.lean | 127 +++++++++--------- 6 files changed, 100 insertions(+), 90 deletions(-) diff --git a/src/Lean/Server/FileWorker/RequestHandling.lean b/src/Lean/Server/FileWorker/RequestHandling.lean index e51efebda0..1e211516be 100644 --- a/src/Lean/Server/FileWorker/RequestHandling.lean +++ b/src/Lean/Server/FileWorker/RequestHandling.lean @@ -222,7 +222,7 @@ def getInteractiveTermGoal (p : Lsp.PlainTermGoalParams) let goal ← ci.runMetaM lctx' do Widget.goalToInteractive (← Meta.mkFreshExprMVar ty).mvarId! let range := if let some r := i.range? then r.toLspRange text else ⟨p.position, p.position⟩ - return some { goal with range } + return some { goal with range, term := ⟨ti⟩ } else return none @@ -230,7 +230,7 @@ def handlePlainTermGoal (p : PlainTermGoalParams) : RequestM (RequestTask (Option PlainTermGoal)) := do let t ← getInteractiveTermGoal p return t.map <| Except.map <| Option.map fun goal => - { goal := toString goal.toInteractiveGoal.pretty + { goal := toString goal.pretty range := goal.range } diff --git a/src/Lean/Server/FileWorker/WidgetRequests.lean b/src/Lean/Server/FileWorker/WidgetRequests.lean index 1978923009..1e5b8e2d24 100644 --- a/src/Lean/Server/FileWorker/WidgetRequests.lean +++ b/src/Lean/Server/FileWorker/WidgetRequests.lean @@ -46,25 +46,25 @@ The intended usage of this is for the infoview to pass the `InfoWithCtx` which was stored for a particular `SubexprInfo` tag in a `TaggedText` generated with `ppExprTagged`. -/ def makePopup : WithRpcRef InfoWithCtx → RequestM (RequestTask InfoPopup) - | ⟨i⟩ => RequestM.asTask do - i.ctx.runMetaM i.info.lctx do - let type? ← match (← i.info.type?) with - | some type => some <$> ppExprTagged type - | none => pure none - let exprExplicit? ← match i.info with - | Elab.Info.ofTermInfo ti => - let ti ← ppExprTagged ti.expr (explicit := true) - -- remove top-level expression highlight - pure <| some <| match ti with - | .tag _ tt => tt - | tt => tt - | Elab.Info.ofFieldInfo fi => pure <| some <| TaggedText.text fi.fieldName.toString - | _ => pure none - return { - type := type? - exprExplicit := exprExplicit? - doc := ← i.info.docString? : InfoPopup - } + | ⟨i⟩ => RequestM.asTask do + i.ctx.runMetaM i.info.lctx do + let type? ← match (← i.info.type?) with + | some type => some <$> ppExprTagged type + | none => pure none + let exprExplicit? ← match i.info with + | Elab.Info.ofTermInfo ti => + let ti ← ppExprTagged ti.expr (explicit := true) + -- remove top-level expression highlight + pure <| some <| match ti with + | .tag _ tt => tt + | tt => tt + | Elab.Info.ofFieldInfo fi => pure <| some <| TaggedText.text fi.fieldName.toString + | _ => pure none + return { + type := type? + exprExplicit := exprExplicit? + doc := ← i.info.docString? : InfoPopup + } builtin_initialize registerBuiltinRpcProcedure diff --git a/src/Lean/Widget/Basic.lean b/src/Lean/Widget/Basic.lean index 65ff340185..c56178d323 100644 --- a/src/Lean/Widget/Basic.lean +++ b/src/Lean/Widget/Basic.lean @@ -14,13 +14,17 @@ This is the input to the RPC call `Lean.Widget.InteractiveDiagnostics.infoToInte The purpose of `InfoWithCtx` is to carry over information about delaborated `Info` nodes in a `CodeWithInfos`, and the associated pretty-printing functionality is purpose-specific to showing the contents of infoview popups. --/ + +NOTE: This type is for internal use in the infoview. It should not be used in user widgets. -/ structure InfoWithCtx where ctx : Elab.ContextInfo info : Elab.Info deriving TypeName deriving instance TypeName for MessageData +deriving instance TypeName for LocalContext +deriving instance TypeName for Elab.ContextInfo +deriving instance TypeName for Elab.TermInfo instance : ToJson FVarId := ⟨fun f => toJson f.name⟩ instance : ToJson MVarId := ⟨fun f => toJson f.name⟩ diff --git a/src/Lean/Widget/Diff.lean b/src/Lean/Widget/Diff.lean index 15ff3d74c3..55c6823660 100644 --- a/src/Lean/Widget/Diff.lean +++ b/src/Lean/Widget/Diff.lean @@ -238,8 +238,7 @@ def diffInteractiveGoal (useAfter : Bool) (g₀ : MVarId) (i₁ : InteractiveGoa let lctx₀ := md₀.lctx |>.sanitizeNames.run' {options := (← getOptions)} let hs₁ ← diffHypotheses useAfter lctx₀ i₁.hyps let i₁ := {i₁ with hyps := hs₁} - let some g₁ := i₁.mvarId? - | throwError "Expected InteractiveGoal to have an mvarId" + let g₁ := i₁.mvarId let t₀ ← instantiateMVars <|← inferType (Expr.mvar g₀) let some md₁ := (← getMCtx).findDecl? g₁ | throwError "Unknown goal {g₁}" @@ -265,8 +264,7 @@ def diffInteractiveGoals (useAfter : Bool) (info : Elab.TacticInfo) (igs₁ : In | some xs => xs.contains after | none => false let goals ← igs₁.goals.mapM (fun ig₁ => do - let some g₁ := ig₁.mvarId? - | throwError "error: goal not found" + let g₁ := ig₁.mvarId withGoalCtx (g₁ : MVarId) (fun _lctx₁ _md₁ => do -- if the goal is present on the previous version then continue if goals₀.any (fun g₀ => g₀ == g₁) then diff --git a/src/Lean/Widget/InteractiveCode.lean b/src/Lean/Widget/InteractiveCode.lean index f7a6162320..de70d7e495 100644 --- a/src/Lean/Widget/InteractiveCode.lean +++ b/src/Lean/Widget/InteractiveCode.lean @@ -29,12 +29,13 @@ inductive DiffTag where structure SubexprInfo where /-- The `Elab.Info` node with the semantics of this part of the output. -/ info : WithRpcRef InfoWithCtx - /-- The position of this subexpression within the top-level expression. - See `Lean.SubExpr`. -/ + /-- The position of this subexpression within the top-level expression. See `Lean.SubExpr`. -/ subexprPos : Lean.SubExpr.Pos -- TODO(WN): add fields for semantic highlighting -- kind : Lsp.SymbolKind - /-- Ask the renderer to highlight this node in the given color. -/ + /-- In certain situations such as when goal states change between positions in a tactic-mode proof, + we can show subexpression-level diffs between two expressions. This field asks the renderer to + display the subexpression as in a diff view (e.g. red/green like `git diff`). -/ diffStatus? : Option DiffTag := none deriving RpcEncodable @@ -53,7 +54,7 @@ def CodeWithInfos.pretty (tt : CodeWithInfos) := tt.stripTags def SubexprInfo.withDiffTag (tag : DiffTag) (c : SubexprInfo) : SubexprInfo := - {c with diffStatus? := some tag } + { c with diffStatus? := some tag } /-- Tags pretty-printed code with infos from the delaborator. -/ partial def tagCodeInfos (ctx : Elab.ContextInfo) (infos : SubExpr.PosMap Elab.Info) (tt : TaggedText (Nat × Nat)) diff --git a/src/Lean/Widget/InteractiveGoal.lean b/src/Lean/Widget/InteractiveGoal.lean index aa6fabe948..1e4f0dbf39 100644 --- a/src/Lean/Widget/InteractiveGoal.lean +++ b/src/Lean/Widget/InteractiveGoal.lean @@ -8,16 +8,16 @@ import Lean.Meta.PPGoal import Lean.Widget.InteractiveCode import Lean.Data.Lsp.Extra -/-! RPC procedures for retrieving tactic and term goals with embedded `CodeWithInfos`. -/ +/-! Functionality related to tactic-mode and term-mode goals with embedded `CodeWithInfos`. -/ namespace Lean.Widget open Server -/-- In the infoview, if multiple hypotheses `h₁`, `h₂` have the same type `α`, they are rendered as `h₁ h₂ : α`. -We call this a 'hypothesis bundle'. -/ +/-- In the infoview, if multiple hypotheses `h₁`, `h₂` have the same type `α`, they are rendered +as `h₁ h₂ : α`. We call this a 'hypothesis bundle'. We use `none` instead of `some false` for +booleans to save space in the json encoding. -/ structure InteractiveHypothesisBundle where - /-- The user-friendly name for each hypothesis. - If anonymous then the name is inaccessible and hidden. -/ + /-- The user-friendly name for each hypothesis. -/ names : Array Name /-- The ids for each variable. Should have the same length as `names`. -/ fvarIds : Array FVarId @@ -25,42 +25,53 @@ structure InteractiveHypothesisBundle where /-- The value, in the case the hypothesis is a `let`-binder. -/ val? : Option CodeWithInfos := none /-- The hypothesis is a typeclass instance. -/ - isInstance : Bool + isInstance? : Option Bool := none /-- The hypothesis is a type. -/ - isType : Bool + isType? : Option Bool := none /-- If true, the hypothesis was not present on the previous tactic state. - Uses `none` instead of `some false` to save space in the json encoding. -/ + Only present in tactic-mode goals. -/ isInserted? : Option Bool := none /-- If true, the hypothesis will be removed in the next tactic state. - Uses `none` instead of `some false` to save space in the json encoding. -/ - isRemoved? : Option Bool := none - deriving Inhabited, RpcEncodable - -structure InteractiveGoal where - hyps : Array InteractiveHypothesisBundle - type : CodeWithInfos - userName? : Option String - goalPrefix : String - /-- Identifies the goal (ie with the unique - name of the MVar that it is a goal for.) - This is none when we are showing a term goal. -/ - mvarId? : Option MVarId := none - /-- If true, the goal was not present on the previous tactic state. - Uses `none` instead of `some false` to save space in the json encoding. -/ - isInserted?: Option Bool := none - /-- If true, the goal will be removed on the next tactic state. - Uses `none` instead of `some false` to save space in the json encoding. -/ + Only present in tactic-mode goals. -/ isRemoved? : Option Bool := none deriving Inhabited, RpcEncodable -namespace InteractiveGoal +/-- The shared parts of interactive term-mode and tactic-mode goals. -/ +structure InteractiveGoalCore where + hyps : Array InteractiveHypothesisBundle + /-- The target type. -/ + type : CodeWithInfos + /-- Metavariable context that the goal is well-typed in. -/ + ctx : WithRpcRef Elab.ContextInfo + deriving Inhabited -private def addLine (fmt : Format) : Format := - if fmt.isNil then fmt else fmt ++ Format.line +/-- An interactive tactic-mode goal. -/ +structure InteractiveGoal extends InteractiveGoalCore where + /-- The name `foo` in `case foo`, if any. -/ + userName? : Option String + /-- The symbol to display before the target type. Usually `⊢` but `conv` goals use `∣` + and it could be extended. -/ + goalPrefix : String + /-- Identifies the goal (ie with the unique name of the MVar that it is a goal for.) -/ + mvarId : MVarId + /-- If true, the goal was not present on the previous tactic state. -/ + isInserted? : Option Bool := none + /-- If true, the goal will be removed on the next tactic state. -/ + isRemoved? : Option Bool := none + deriving Inhabited, RpcEncodable -def pretty (g : InteractiveGoal) : Format := Id.run do +/-- An interactive term-mode goal. -/ +structure InteractiveTermGoal extends InteractiveGoalCore where + /-- Syntactic range of the term. -/ + range : Lsp.Range + /-- Information about the term whose type is the term-mode goal. -/ + term : WithRpcRef Elab.TermInfo + deriving Inhabited, RpcEncodable + +def InteractiveGoalCore.pretty (g : InteractiveGoalCore) (userName? : Option String) + (goalPrefix : String) : Format := Id.run do let indent := 2 -- Use option - let mut ret := match g.userName? with + let mut ret := match userName? with | some userName => f!"case {userName}" | none => Format.nil for hyp in g.hyps do @@ -80,23 +91,16 @@ def pretty (g : InteractiveGoal) : Format := Id.run do | none => ret := ret ++ Format.group f!"{names} :{Format.nest indent (Format.line ++ hyp.type.stripTags)}" ret := addLine ret - ret ++ f!"{g.goalPrefix}{Format.nest indent g.type.stripTags}" + ret ++ f!"{goalPrefix}{Format.nest indent g.type.stripTags}" +where + addLine (fmt : Format) : Format := + if fmt.isNil then fmt else fmt ++ Format.line + +def InteractiveGoal.pretty (g : InteractiveGoal) : Format := + g.toInteractiveGoalCore.pretty g.userName? g.goalPrefix -end InteractiveGoal - -/-- This is everything needed to render an interactive term goal in the infoview. -/ -structure InteractiveTermGoal where - hyps : Array InteractiveHypothesisBundle - type : CodeWithInfos - range : Lsp.Range - deriving Inhabited, RpcEncodable - -namespace InteractiveTermGoal - -def toInteractiveGoal (g : InteractiveTermGoal) : InteractiveGoal := - { g with userName? := none, goalPrefix := "⊢ " } - -end InteractiveTermGoal +def InteractiveTermGoal.pretty (g : InteractiveTermGoal) : Format := + g.toInteractiveGoalCore.pretty none "" structure InteractiveGoals where goals : Array InteractiveGoal @@ -109,18 +113,21 @@ instance : Append InteractiveGoals := ⟨InteractiveGoals.append⟩ instance : EmptyCollection InteractiveGoals := ⟨{goals := #[]}⟩ open Meta in -def addInteractiveHypothesisBundle (hyps : Array InteractiveHypothesisBundle) (ids : Array (Name × FVarId)) (type : Expr) (value? : Option Expr := none) : MetaM (Array InteractiveHypothesisBundle) := do +/-- Extend an array of hypothesis bundles with another bundle. -/ +def addInteractiveHypothesisBundle (hyps : Array InteractiveHypothesisBundle) + (ids : Array (Name × FVarId)) (type : Expr) (value? : Option Expr := none) : + MetaM (Array InteractiveHypothesisBundle) := do if ids.size == 0 then throwError "Can only add a nonzero number of ids as an InteractiveHypothesisBundle." let fvarIds := ids.map Prod.snd let names := ids.map Prod.fst return hyps.push { - names := names - fvarIds := fvarIds - type := (← ppExprTagged type) - val? := (← value?.mapM ppExprTagged) - isInstance := (← isClass? type).isSome - isType := (← instantiateMVars type).isSort + names + fvarIds + type := (← ppExprTagged type) + val? := (← value?.mapM ppExprTagged) + isInstance? := if (← isClass? type).isSome then true else none + isType? := if (← instantiateMVars type).isSort then true else none } open Meta in @@ -132,7 +139,6 @@ def withGoalCtx (goal : MVarId) (action : LocalContext → MetavarDecl → n α) let lctx := mvarDecl.lctx |>.sanitizeNames.run' {options := (← getOptions)} withLCtx lctx mvarDecl.localInstances (action lctx mvarDecl) - open Meta in /-- A variant of `Meta.ppGoal` which preserves subexpression information for interactivity. -/ def goalToInteractive (mvarId : MVarId) : MetaM InteractiveGoal := do @@ -180,11 +186,12 @@ def goalToInteractive (mvarId : MVarId) : MetaM InteractiveGoal := do | Name.anonymous => none | name => some <| toString name.eraseMacroScopes return { - hyps, - type := goalFmt, - userName?, - goalPrefix := getGoalPrefix mvarDecl, - mvarId? := some mvarId + hyps + type := goalFmt + ctx := ⟨← Elab.ContextInfo.save⟩ + userName? + goalPrefix := getGoalPrefix mvarDecl + mvarId } end Lean.Widget