From 538f74004c0fb340f08c4cfa7e193888857fd102 Mon Sep 17 00:00:00 2001 From: Jon Eugster Date: Wed, 7 Feb 2024 12:41:21 +0100 Subject: [PATCH] allow for empty lines in editor --- server/GameServer/RpcHandlers.lean | 170 +++++++++++------------------ 1 file changed, 66 insertions(+), 104 deletions(-) diff --git a/server/GameServer/RpcHandlers.lean b/server/GameServer/RpcHandlers.lean index 8069b65..61d46c8 100644 --- a/server/GameServer/RpcHandlers.lean +++ b/server/GameServer/RpcHandlers.lean @@ -1,5 +1,6 @@ import GameServer.EnvExtensions import GameServer.InteractiveGoal +import Std.Data.Array.Init.Basic open Lean open Server @@ -133,61 +134,33 @@ def findHints (goal : MVarId) (m : DocumentMeta) (initParams : Lsp.InitializePar return none return hints -/-- Get the line that ends in `pos`. Note that `pos` is expected to be the -position of a `\n` but this is not enforced. -/ -def _root_.Lean.FileMap.getLineBefore (fmap : FileMap) (pos : String.Pos) : String := Id.run do - match fmap.positions.findIdx? (· == pos) with - | none => - panic s!"Position {pos} is not a newline character in " ++ - s!"the following string: '{fmap.source}'!" - | some 0 => - -- the first entry of `positions` is always `0` - return "" - | some (i + 1) => - let line : Substring := ⟨fmap.source, fmap.positions.get! i, pos⟩ - return line.toString - -/-- Returns the `List` without the last element. -/ -def _root_.List.dropBack {α : Type _} : List α → List α -| [] => [] -| _ :: [] => [] -| x :: xs => x :: xs.dropBack - -/-- Trim empty lines from the file and add a single newline. -/ -def _root_.Lean.FileMap.trim (fmap : FileMap) : FileMap := - let str := match fmap.source.trim with - | "" => "" - | s => s ++ "\n" - FileMap.ofString str - -/-- Returns the `Array` without the last element. -/ -def _root_.Array.dropBack {α : Type _} (a : Array α) : Array α := ⟨a.data.dropBack⟩ - +-- TODO: no need to have `RequestM`, just anything where `mut` works /-- Add custom diagnostics about whether the level is completed. -/ -def addCompletionDiagnostics (diag : Array InteractiveDiagnostic) (goals : Array InteractiveGoalWithHints) - (pos : Lsp.Position) (prevGoalCount : Nat) : RequestM <| Array InteractiveDiagnostic := do - let mut out : Array InteractiveDiagnostic := diag - - if goals.size == 0 then - if diag.any (·.severity? == some .error) then - pure () - else if diag.any (·.severity? == some .warning) then +def completionDiagnostics (goalCount : Nat) (prevGoalCount : Nat) (completed : Bool) + (completedWithWarnings : Bool) (pos : Lsp.Position) + (startDiags : Array InteractiveDiagnostic := #[]) : + RequestM <| Array InteractiveDiagnostic := do + let mut out : Array InteractiveDiagnostic := startDiags + if goalCount == 0 then + if completed then out := out.push { - message := .text "level completed with warnings. 🎭" + message := .text "level completed! 🎉" range := { start := pos «end» := pos } severity? := Lsp.DiagnosticSeverity.information } - else + else if completedWithWarnings then out := out.push { - message := .text "level completed! 🎉" + message := .text "level completed with warnings… 🎭" range := { start := pos «end» := pos } severity? := Lsp.DiagnosticSeverity.information } - else if goals.size < prevGoalCount then + else + pure () + else if goalCount < prevGoalCount then out := out.push { message := .text "intermediate goal solved! 🎉" range := { @@ -196,19 +169,13 @@ def addCompletionDiagnostics (diag : Array InteractiveDiagnostic) (goals : Array } severity? := Lsp.DiagnosticSeverity.information } - - return out - -- diagsAtPos := if goalsAtPos.size < intermediateGoalCount then - -- diagsAtPos.push { - -- message := .text "intermediate goal solved 🎉" - -- range := { - -- start := lspPosAt - -- «end» := lspPosAt - -- } - -- severity? := Lsp.DiagnosticSeverity.information - -- } - -- else diagsAtPos + +def filterUnsolvedGoal (a : Array InteractiveDiagnostic) : + Array InteractiveDiagnostic := + a.filter (fun d => match d.message with + | .append ⟨(.text x) :: _⟩ => x != "unsolved goals" + | _ => true) /-- Request that returns the goals at the end of each line of the tactic proof plus the diagnostics (i.e. warnings/errors) for the proof. @@ -216,7 +183,7 @@ plus the diagnostics (i.e. warnings/errors) for the proof. def getProofState (_ : Lsp.PlainGoalParams) : RequestM (RequestTask (Option ProofState)) := do let doc ← readDoc let rc ← readThe RequestContext - let text := doc.meta.text.trim + let text := doc.meta.text -- BUG: trimming here is a problem, since the snap might already be evaluated before -- the trimming and then the positions don't match anymore :(( @@ -237,18 +204,46 @@ def getProofState (_ : Lsp.PlainGoalParams) : RequestM (RequestTask (Option Proo -- Answer: The last snap only copied the diags from the end of this snap let mut diag : Array InteractiveDiagnostic := snap.interactiveDiags.toArray + -- Level is completed if there are no errrors or warnings + let completedWithWarnings : Bool := ¬ diag.any (·.severity? == some .error) + let completed : Bool := completedWithWarnings ∧ ¬ diag.any (·.severity? == some .warning) + let mut intermediateGoalCount := 0 + -- only the positions that have non-whitespace characters since the last position + -- should add a new proof step. + let positionsWithSource : Array (String.Pos × String) := + text.positions.zipWithIndex.filterMap ( + fun (pos, i) => match i with + | 0 => some (pos, "") + | i' + 1 => + let source : String := Substring.toString ⟨text.source, text.positions.get! i', pos⟩ + if source.trim.length == 0 then + none + else + some (pos, source)) + -- Drop the last position as we ensured that there is always a newline at the end - for pos in text.positions.dropBack do - -- iterate over all newlines in the proof and get the goals and hints at each position - -- TODO: we drop the last position because we always have a newline. Would be better - -- to trim newlines instead before submitting! - let source := text.getLineBefore pos + for ((pos, source), i) in positionsWithSource.zipWithIndex do + -- iterate over all steps in the proof and get the goals and hints at each position + + -- diags are labeled in Lsp-positions, which differ from the lean-internal + -- positions by `1`. + let lspPosAt := text.utf8PosToLspPos pos + + let mut diagsAtPos : Array InteractiveDiagnostic := filterUnsolvedGoal <| + -- `+1` for getting the errors after the line. + match i with + | 0 => + -- `lspPosAt` is `(0, 0)` + diag.filter (fun d => d.range.start == lspPosAt ) + | i' + 1 => + diag.filter (fun d => + ((text.utf8PosToLspPos <| (positionsWithSource.get! i').1) ≤ d.range.start) ∧ + d.range.start < lspPosAt ) if let goalsAtResult@(_ :: _) := snap.infoTree.goalsAt? doc.meta.text pos then - pure () - let goalAtPos : List <| List InteractiveGoalWithHints ← goalsAtResult.mapM + let goalsAtPos' : List <| List InteractiveGoalWithHints ← goalsAtResult.mapM fun { ctxInfo := ci, tacticInfo := tacticInfo, useAfter := useAfter, .. } => do -- TODO: What does this function body do? -- let ciAfter := { ci with mctx := ti.mctxAfter } @@ -275,58 +270,24 @@ def getProofState (_ : Lsp.PlainGoalParams) : RequestM (RequestTask (Option Proo -- return goals -- ) return interactiveGoals - let goalsAtPos : Array InteractiveGoalWithHints := ⟨goalAtPos.foldl (· ++ ·) []⟩ - - -- diags are labeled in Lsp-positions, which differ from the lean-internal - -- positions by `1`. - let lspPosAt := text.utf8PosToLspPos pos - - let mut diagsAtPos : Array InteractiveDiagnostic := - -- `+1` for getting the errors after the line. - diag.filter (·.range.start.line + 1 == lspPosAt.line) + let goalsAtPos : Array InteractiveGoalWithHints := ⟨goalsAtPos'.foldl (· ++ ·) []⟩ - diagsAtPos ← addCompletionDiagnostics diagsAtPos goalsAtPos lspPosAt intermediateGoalCount + diagsAtPos ← completionDiagnostics goalsAtPos.size intermediateGoalCount + completed completedWithWarnings lspPosAt diagsAtPos intermediateGoalCount := goalsAtPos.size steps := steps.push ⟨goalsAtPos, source, diagsAtPos, lspPosAt.line, lspPosAt.character⟩ else -- No goals present - steps := steps.push default - - - - -- // if (goals.length && goalCount > goals.length) { - -- // messages.unshift({ - -- // range: { - -- // start: { - -- // line: i-1, - -- // character: 0, - -- // }, - -- // end: { - -- // line: i-1, - -- // character: 0, - -- // }}, - -- // severity: DiagnosticSeverity.Information, - -- // message: { - -- // text: 'intermediate goal solved 🎉' - -- // } - -- // }) - -- // } - - -- Level is completed if there are no errrors or warnings - - let completedWithWarnings : Bool := ¬ diag.any (·.severity? == some .error) - let completed : Bool := completedWithWarnings ∧ ¬ diag.any (·.severity? == some .warning) + steps := steps.push ⟨#[], source, diagsAtPos, lspPosAt.line, none⟩ -- Filter out the "unsolved goals" message - diag := diag.filter (fun d => match d.message with - | .append ⟨(.text x) :: _⟩ => x != "unsolved goals" - | _ => true) + diag := filterUnsolvedGoal diag - let lastPos := text.utf8PosToLspPos text.positions.back + let lastPos := text.utf8PosToLspPos positionsWithSource.back.1 let remainingDiags : Array InteractiveDiagnostic := - diag.filter (fun d => d.range.start.line >= lastPos.line) + diag.filter (fun d => lastPos ≤ d.range.start) return some { steps := steps, @@ -338,9 +299,10 @@ def getProofState (_ : Lsp.PlainGoalParams) : RequestM (RequestTask (Option Proo open RequestM in +-- The editor apparently uses this def getInteractiveGoals (p : Lsp.PlainGoalParams) : RequestM (RequestTask (Option <| InteractiveGoals)) := do let doc ← readDoc - let rc ← readThe RequestContext + -- let rc ← readThe RequestContext let text := doc.meta.text let hoverPos := text.lspPosToUtf8Pos p.position -- TODO: I couldn't find a good condition to find the correct snap. So we are looking