phc/lean4game
6
1
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity

allow for empty lines in editor

Browse Source
This commit is contained in:
Jon Eugster
2024-02-07 12:50:39 +01:00
parent 6aebb8993f
commit 538f74004c
1 changed files with 71 additions and 109 deletions
Download Patch File Download Diff File Expand all files Collapse all files
server/GameServer/RpcHandlers.lean
+71 -109
View File
@@ -1,5 +1,6 @@
import GameServer.EnvExtensions
import GameServer.InteractiveGoal
import Std.Data.Array.Init.Basic
open Lean
open Server
@@ -133,53 +134,15 @@ 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
out := out.push {
message := .text "level completed with warnings. 🎭"
range := {
start := pos
«end» := pos
}
severity? := Lsp.DiagnosticSeverity.information }
else
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! 🎉"
range := {
@@ -187,7 +150,17 @@ def addCompletionDiagnostics (diag : Array InteractiveDiagnostic) (goals : Array
«end» := pos
}
severity? := Lsp.DiagnosticSeverity.information }
else if goals.size < prevGoalCount then
else if completedWithWarnings then
out := out.push {
message := .text "level completed with warnings… 🎭"
range := {
start := pos
«end» := pos
}
severity? := Lsp.DiagnosticSeverity.information }
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 (· ++ ·) []⟩
let goalsAtPos : Array InteractiveGoalWithHints := ⟨goalsAtPos'.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)
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