From ab52480b696cda41abb91ab9559aa6f00f1636ea Mon Sep 17 00:00:00 2001 From: Joscha Date: Thu, 6 Jan 2022 16:32:53 +0100 Subject: [PATCH] fix: implement suggestions --- src/Lean/Data/Lsp/Basic.lean | 7 +------ src/Lean/Data/Lsp/Internal.lean | 9 ++++----- src/Lean/Elab/Frontend.lean | 10 +++++----- src/Lean/Server/FileWorker.lean | 4 +--- src/Lean/Server/References.lean | 16 ++++++++-------- src/Lean/Server/Watchdog.lean | 2 +- 6 files changed, 20 insertions(+), 28 deletions(-) diff --git a/src/Lean/Data/Lsp/Basic.lean b/src/Lean/Data/Lsp/Basic.lean index 81a9f650cd..779080ceb6 100644 --- a/src/Lean/Data/Lsp/Basic.lean +++ b/src/Lean/Data/Lsp/Basic.lean @@ -31,16 +31,11 @@ offsets. For diagnostics, one-based `Lean.Position`s are used internally. structure Position where line : Nat character : Nat - deriving Inhabited, BEq, Hashable, ToJson, FromJson + deriving Inhabited, BEq, Ord, Hashable, ToJson, FromJson instance : ToString Position := ⟨fun p => "(" ++ toString p.line ++ ", " ++ toString p.character ++ ")"⟩ -instance : Ord Position where - compare a b := match compare a.line b.line with - | Ordering.eq => compare a.character b.character - | o => o - instance : LT Position := ltOfOrd instance : LE Position := leOfOrd diff --git a/src/Lean/Data/Lsp/Internal.lean b/src/Lean/Data/Lsp/Internal.lean index 1be31d644e..38af7342ec 100644 --- a/src/Lean/Data/Lsp/Internal.lean +++ b/src/Lean/Data/Lsp/Internal.lean @@ -32,17 +32,16 @@ def toString : RefIdent → String def fromString (s : String) : Except String RefIdent := do let sPrefix := s.take 2 let sName := s.drop 2 - let mk ← match sPrefix with - | "c:" => RefIdent.const - | "f:" => fun n => RefIdent.fvar <| FVarId.mk n - | _ => throw "string must start with 'c:' or 'f:'" -- See `FromJson Name` let name ← match sName with | "[anonymous]" => Name.anonymous | _ => match Syntax.decodeNameLit ("`" ++ sName) with | some n => n | none => throw s!"expected a Name, got {sName}" - mk name + match sPrefix with + | "c:" => RefIdent.const name + | "f:" => RefIdent.fvar <| FVarId.mk name + | _ => throw "string must start with 'c:' or 'f:'" end RefIdent diff --git a/src/Lean/Elab/Frontend.lean b/src/Lean/Elab/Frontend.lean index d7417b2b60..4381a0e199 100644 --- a/src/Lean/Elab/Frontend.lean +++ b/src/Lean/Elab/Frontend.lean @@ -101,7 +101,7 @@ def runFrontend (fileName : String) (mainModuleName : Name) (trustLevel : UInt32 := 0) - (ileanFileName: Option String := none) + (ileanFileName? : Option String := none) : IO (Environment × Bool) := do let inputCtx := Parser.mkInputContext input fileName let (header, parserState, messages) ← Parser.parseHeader inputCtx @@ -109,16 +109,16 @@ def runFrontend let env := env.setMainModule mainModuleName let mut commandState := Command.mkState env messages opts - if ileanFileName.isSome then + if ileanFileName?.isSome then -- Collect InfoTrees so we can later extract and export their info to the ilean file - commandState := { commandState with infoState := { commandState.infoState with enabled := true }} + commandState := { commandState with infoState.enabled := true } let s ← IO.processCommands inputCtx parserState commandState for msg in s.commandState.messages.toList do IO.print (← msg.toString (includeEndPos := getPrintMessageEndPos opts)) - if let some ileanFileName := ileanFileName then - let trees := s.commandState.infoState.trees.toList + if let some ileanFileName := ileanFileName? then + let trees := s.commandState.infoState.trees.toArray let references := Lean.Server.findModuleRefs inputCtx.fileMap trees (localVars := false) let ilean := { module := mainModuleName, references : Lean.Server.Ilean } IO.FS.writeFile ileanFileName $ toString $ toJson ilean diff --git a/src/Lean/Server/FileWorker.lean b/src/Lean/Server/FileWorker.lean index 37e86e9f46..0f85fe8463 100644 --- a/src/Lean/Server/FileWorker.lean +++ b/src/Lean/Server/FileWorker.lean @@ -70,9 +70,7 @@ section Elab snaps : List Snapshot private def AsyncElabState.lastSnap (s : AsyncElabState) : Snapshot := - match s.snaps.getLast? with - | some snap => snap - | none => s.headerSnap + s.snaps.getLastD s.headerSnap abbrev AsyncElabM := StateT AsyncElabState $ ExceptT ElabTaskError IO diff --git a/src/Lean/Server/References.lean b/src/Lean/Server/References.lean index a31166980c..544f57740c 100644 --- a/src/Lean/Server/References.lean +++ b/src/Lean/Server/References.lean @@ -46,9 +46,9 @@ def contains (self : RefInfo) (pos : Lsp.Position) : Bool := Id.run do if contains range pos then return true false - where - contains (range : Lsp.Range) (pos : Lsp.Position) : Bool := - range.start <= pos && pos < range.end +where + contains (range : Lsp.Range) (pos : Lsp.Position) : Bool := + range.start <= pos && pos < range.end end Lean.Lsp.RefInfo @@ -141,10 +141,10 @@ def combineFvars (refs : Array Reference) : Array Reference := Id.run do | { ident := ident@(RefIdent.fvar _), range, isDeclaration := false } => refs.push { ident := applyIdMap idMap ident, range, isDeclaration := false } | _ => refs.push ref - where - applyIdMap : HashMap FVarId FVarId → RefIdent → RefIdent - | m, RefIdent.fvar id => RefIdent.fvar <| m.findD id id - | _, ident => ident +where + applyIdMap : HashMap FVarId FVarId → RefIdent → RefIdent + | m, RefIdent.fvar id => RefIdent.fvar <| m.findD id id + | _, ident => ident def findModuleRefs (text : FileMap) (trees : List InfoTree) (localVars : Bool := true) : ModuleRefs := Id.run do @@ -194,7 +194,7 @@ def findAt? (self : References) (module : Name) (pos : Lsp.Position) : Option Re return refs.findAt? pos none -def referingTo (self : References) (ident : RefIdent) (srcSearchPath : SearchPath) +def referringTo (self : References) (ident : RefIdent) (srcSearchPath : SearchPath) (includeDefinition : Bool := true) : IO (Array Location) := do let mut result := #[] for (module, refs) in self.allRefs.toList do diff --git a/src/Lean/Server/Watchdog.lean b/src/Lean/Server/Watchdog.lean index 491ab0a83f..f7627ceaa1 100644 --- a/src/Lean/Server/Watchdog.lean +++ b/src/Lean/Server/Watchdog.lean @@ -359,7 +359,7 @@ def handleReference (p : ReferenceParams) : ServerM (Array Location) := do if let some module ← searchModuleNameOfFileName path srcSearchPath then let references ← (← read).references.get if let some ident := references.findAt? module p.position then - return ← references.referingTo ident srcSearchPath p.context.includeDeclaration + return ← references.referringTo ident srcSearchPath p.context.includeDeclaration #[] end RequestHandling