Lean.Server.Completion

Lean.Server.Completion.matchNamespace ns nsFragment danglingDot = if danglingDot = true then nsFragment != ns && Lean.Name.isPrefixOf nsFragment ns else match ns, nsFragment with | Lean.Name.str p₁ s₁ x, Lean.Name.str p₂ s₂ x_1 => p₁ == p₂ && String.isPrefixOf s₂ s₁ | x, x_1 => false

source

def Lean.Server.Completion.completeNamespaces (ctx : Lean.Elab.ContextInfo) (id : Lean.Name) (danglingDot : Bool) :

Lean.Server.Completion.M Unit

Equations

Lean.Server.Completion.completeNamespaces ctx id danglingDot = do let env ← Lean.getEnv let add : Lean.Name → Lean.Name → Lean.Server.Completion.M Unit := fun ns ns' => if danglingDot = true then Lean.Server.Completion.addNamespaceCompletionItem (Lean.Name.replacePrefix ns (ns' ++ id) Lean.Name.anonymous) else Lean.Server.Completion.addNamespaceCompletionItem (Lean.Name.replacePrefix ns ns' Lean.Name.anonymous) Lean.SSet.forM (Lean.Environment.getNamespaceSet env) fun ns => if (Lean.Name.isInternal ns || Lean.Environment.contains env ns) = true then pure PUnit.unit else do let r ← let col := ctx.openDecls; forIn col { fst := none, snd := PUnit.unit } fun openDecl r => let r := r.snd; match openDecl with | Lean.OpenDecl.simple ns' except => if Lean.Server.Completion.matchNamespace ns (ns' ++ id) danglingDot = true then do add ns ns' pure (ForInStep.done { fst := some (), snd := PUnit.unit }) else do pure PUnit.unit pure (ForInStep.yield { fst := none, snd := PUnit.unit }) | x => do pure () pure (ForInStep.yield { fst := none, snd := PUnit.unit }) let x : PUnit := r.snd let _do_jp : PUnit → Lean.Server.Completion.M PUnit := fun y => (fun visitNamespaces => visitNamespaces ctx.currNamespace) (Lean.Server.Completion.completeNamespaces.visitNamespaces id danglingDot add ns) match r.fst with | none => do let y ← pure PUnit.unit _do_jp y | some a => pure a

source

def Lean.Server.Completion.completeNamespaces.visitNamespaces (id : Lean.Name) (danglingDot : Bool) (add : Lean.Name → Lean.Name → Lean.Server.Completion.M Unit) (ns : Lean.Name) (ns' : Lean.Name) :

Lean.Server.Completion.M Unit

Equations

Lean.Server.Completion.completeNamespaces.visitNamespaces id danglingDot add ns (Lean.Name.str p x x_1) = if Lean.Server.Completion.matchNamespace ns (Lean.Name.str p x x_1 ++ id) danglingDot = true then add ns (Lean.Name.str p x x_1) else Lean.Server.Completion.completeNamespaces.visitNamespaces id danglingDot add ns p
Lean.Server.Completion.completeNamespaces.visitNamespaces id danglingDot add ns ns' = if Lean.Server.Completion.matchNamespace ns (ns' ++ id) danglingDot = true then add ns ns' else pure ()

source

def Lean.Server.Completion.find? (fileMap : Lean.FileMap) (hoverPos : String.Pos) (infoTree : Lean.Elab.InfoTree) (caps : Lean.Lsp.ClientCapabilities) :

IO (Option Lean.Lsp.CompletionList)

Equations

Lean.Server.Completion.find? fileMap hoverPos infoTree caps = (fun choose => let x := Lean.FileMap.toPosition fileMap hoverPos; match x with | { line := hoverLine, column := x } => match Lean.Elab.InfoTree.foldInfo (choose fileMap hoverLine) none infoTree with | some (hoverInfo, ctx, Lean.Elab.Info.ofCompletionInfo info) => match info with | Lean.Elab.CompletionInfo.dot info x expectedType? => Lean.Server.Completion.dotCompletion ctx info hoverInfo expectedType? | Lean.Elab.CompletionInfo.id stx id danglingDot lctx expectedType? => Lean.Server.Completion.idCompletion ctx lctx id hoverInfo danglingDot expectedType? | Lean.Elab.CompletionInfo.option stx => Lean.Server.Completion.optionCompletion ctx stx caps | Lean.Elab.CompletionInfo.tactic x x_1 => Lean.Server.Completion.tacticCompletion ctx | x => pure none | x => pure none) (Lean.Server.Completion.find?.choose hoverPos)

source

def Lean.Server.Completion.find?.choose (hoverPos : String.Pos) (fileMap : Lean.FileMap) (hoverLine : Nat) (ctx : Lean.Elab.ContextInfo) (info : Lean.Elab.Info) (best? : Option (Lean.Server.Completion.HoverInfo × Lean.Elab.ContextInfo × Lean.Elab.Info)) :

Option (Lean.Server.Completion.HoverInfo × Lean.Elab.ContextInfo × Lean.Elab.Info)

Equations

Lean.Server.Completion.find?.choose hoverPos fileMap hoverLine ctx info best? = if (!Lean.Elab.Info.isCompletion info) = true then best? else if Option.isSome (Lean.Elab.Info.occursInside? info hoverPos) = true then let headPos := Option.get! (Lean.Elab.Info.pos? info); let x := Lean.FileMap.toPosition fileMap headPos; match x with | { line := headPosLine, column := x } => let x := Lean.FileMap.toPosition fileMap (Option.get! (Lean.Elab.Info.tailPos? info)); match x with | { line := tailPosLine, column := x } => if (headPosLine != hoverLine || headPosLine != tailPosLine) = true then best? else match best? with | none => some (Lean.Server.Completion.HoverInfo.inside (hoverPos - headPos), ctx, info) | some (Lean.Server.Completion.HoverInfo.after, x, x_1) => some (Lean.Server.Completion.HoverInfo.inside (hoverPos - headPos), ctx, info) | some (x, x_1, best) => if Lean.Elab.Info.isSmaller info best = true then some (Lean.Server.Completion.HoverInfo.inside (hoverPos - headPos), ctx, info) else best? else match best? with | some (Lean.Server.Completion.HoverInfo.inside x, x_1, x_2) => best? | x => match Lean.Elab.Info.occursBefore? info hoverPos with | some d => let pos := Option.get! (Lean.Elab.Info.tailPos? info); let x := Lean.FileMap.toPosition fileMap pos; match x with | { line := line, column := x } => if (line != hoverLine) = true then best? else match best? with | none => some (Lean.Server.Completion.HoverInfo.after, ctx, info) | some (x, x_1, best) => let dBest := Option.get! (Lean.Elab.Info.occursBefore? best hoverPos); if (decide (d < dBest) || d == dBest && Lean.Elab.Info.isSmaller info best) = true then some (Lean.Server.Completion.HoverInfo.after, ctx, info) else best? | x => best?