Documentation

Lean.Server.InfoUtils

structure String.Range :

Type

start : String.Pos
stop : String.Pos

instance String.instInhabitedRange :

Inhabited String.Range

Equations

String.instInhabitedRange = { default := { start := default, stop := default } }

instance String.instReprRange :

Repr String.Range

Equations

String.instReprRange = { reprPrec := [anonymous] }

def String.Range.contains (r : String.Range) (pos : String.Pos) :

Equations

String.Range.contains r pos = (decide (r.start ≤ pos) && decide (pos < r.stop))

def Lean.Syntax.getRange? (stx : Lean.Syntax) (originalOnly : optParam Bool false) :

Option String.Range

Equations

Lean.Syntax.getRange? stx originalOnly = let _discr := Lean.Syntax.getTailPos? stx originalOnly; match Lean.Syntax.getPos? stx originalOnly, Lean.Syntax.getTailPos? stx originalOnly with | some start, some stop => some { start := start, stop := stop } | x, x_1 => none

def Lean.Elab.InfoTree.deepestNodes {α : Type u_1} (p : Lean.Elab.ContextInfo → Lean.Elab.Info → Std.PersistentArray Lean.Elab.InfoTree → Option α) :

Lean.Elab.InfoTree → List α

Equations

Lean.Elab.InfoTree.deepestNodes p = (fun go => go none) (Lean.Elab.InfoTree.deepestNodes.go p)

partial def Lean.Elab.InfoTree.deepestNodes.go {α : Type u_1} (p : Lean.Elab.ContextInfo → Lean.Elab.Info → Std.PersistentArray Lean.Elab.InfoTree → Option α) (ctx? : Option Lean.Elab.ContextInfo) :

Lean.Elab.InfoTree → List α

def Lean.Elab.InfoTree.foldInfo {α : Type u_1} (f : Lean.Elab.ContextInfo → Lean.Elab.Info → α → α) (init : α) :

Lean.Elab.InfoTree → α

Equations

Lean.Elab.InfoTree.foldInfo f init = (fun go => go none init) (Lean.Elab.InfoTree.foldInfo.go f)

partial def Lean.Elab.InfoTree.foldInfo.go {α : Type u_1} (f : Lean.Elab.ContextInfo → Lean.Elab.Info → α → α) (ctx? : Option Lean.Elab.ContextInfo) (a : α) :

Lean.Elab.InfoTree → α

def Lean.Elab.Info.isTerm :

Lean.Elab.Info → Bool

Equations

Lean.Elab.Info.isTerm x = match x with | Lean.Elab.Info.ofTermInfo x => true | x => false

def Lean.Elab.Info.isCompletion :

Lean.Elab.Info → Bool

Equations

Lean.Elab.Info.isCompletion x = match x with | Lean.Elab.Info.ofCompletionInfo x => true | x => false

def Lean.Elab.InfoTree.getCompletionInfos (infoTree : Lean.Elab.InfoTree) :

Array (Lean.Elab.ContextInfo × Lean.Elab.CompletionInfo)

Equations

Lean.Elab.InfoTree.getCompletionInfos infoTree = Lean.Elab.InfoTree.foldInfo (fun ctx info result => match info with | Lean.Elab.Info.ofCompletionInfo info => Array.push result (ctx, info) | x => result) #[] infoTree

def Lean.Elab.Info.stx :

Lean.Elab.Info → Lean.Syntax

Equations

Lean.Elab.Info.stx x = match x with | Lean.Elab.Info.ofTacticInfo i => i.toElabInfo.stx | Lean.Elab.Info.ofTermInfo i => i.toElabInfo.stx | Lean.Elab.Info.ofCommandInfo i => i.toElabInfo.stx | Lean.Elab.Info.ofMacroExpansionInfo i => i.stx | Lean.Elab.Info.ofFieldInfo i => i.stx | Lean.Elab.Info.ofCompletionInfo i => Lean.Elab.CompletionInfo.stx i

def Lean.Elab.Info.lctx :

Lean.Elab.Info → Lean.LocalContext

Equations

Lean.Elab.Info.lctx x = match x with | Lean.Elab.Info.ofTermInfo i => i.lctx | Lean.Elab.Info.ofFieldInfo i => i.lctx | x => Lean.LocalContext.empty

def Lean.Elab.Info.pos? (i : Lean.Elab.Info) :

Option String.Pos

Equations

Lean.Elab.Info.pos? i = Lean.Syntax.getPos? (Lean.Elab.Info.stx i) true

def Lean.Elab.Info.tailPos? (i : Lean.Elab.Info) :

Option String.Pos

Equations

Lean.Elab.Info.tailPos? i = Lean.Syntax.getTailPos? (Lean.Elab.Info.stx i) true

def Lean.Elab.Info.range? (i : Lean.Elab.Info) :

Option String.Range

Equations

Lean.Elab.Info.range? i = Lean.Syntax.getRange? (Lean.Elab.Info.stx i) true

def Lean.Elab.Info.contains (i : Lean.Elab.Info) (pos : String.Pos) :

Equations

Lean.Elab.Info.contains i pos = Option.any (fun a => String.Range.contains a pos) (Lean.Elab.Info.range? i)

def Lean.Elab.Info.size? (i : Lean.Elab.Info) :

Equations

Lean.Elab.Info.size? i = OptionM.run do let pos ← Lean.Elab.Info.pos? i let tailPos ← Lean.Elab.Info.tailPos? i pure (tailPos - pos)

def Lean.Elab.Info.isSmaller (i₁ : Lean.Elab.Info) (i₂ : Lean.Elab.Info) :

Equations

Lean.Elab.Info.isSmaller i₁ i₂ = let _discr := Lean.Elab.Info.pos? i₂; match Lean.Elab.Info.size? i₁, Lean.Elab.Info.pos? i₂ with | some sz₁, some sz₂ => decide (sz₁ < sz₂) | some x, none => true | x, x_1 => false

def Lean.Elab.Info.occursBefore? (i : Lean.Elab.Info) (hoverPos : String.Pos) :

Equations

Lean.Elab.Info.occursBefore? i hoverPos = OptionM.run do let tailPos ← Lean.Elab.Info.tailPos? i guard (tailPos ≤ hoverPos) pure (hoverPos - tailPos)

def Lean.Elab.Info.occursInside? (i : Lean.Elab.Info) (hoverPos : String.Pos) :

Equations

Lean.Elab.Info.occursInside? i hoverPos = OptionM.run do let headPos ← Lean.Elab.Info.pos? i let tailPos ← Lean.Elab.Info.tailPos? i guard ((decide (headPos ≤ hoverPos) && decide (hoverPos < tailPos)) = true) pure (hoverPos - headPos)

def Lean.Elab.InfoTree.smallestInfo? (p : Lean.Elab.Info → Bool) (t : Lean.Elab.InfoTree) :

Option (Lean.Elab.ContextInfo × Lean.Elab.Info)

Equations

Lean.Elab.InfoTree.smallestInfo? p t = let ts := Lean.Elab.InfoTree.deepestNodes (fun ctx i x => if p i = true then some (ctx, i) else none) t; let infos := List.map (fun x => match x with | (ci, i) => let diff := Option.get! (Lean.Elab.Info.tailPos? i) - Option.get! (Lean.Elab.Info.pos? i); (diff, ci, i)) ts; Option.map (fun x => match x with | (x, ci, i) => (ci, i)) (Array.getMax? (List.toArray infos) fun a b => decide (a.fst > b.fst))

def Lean.Elab.InfoTree.hoverableInfoAt? (t : Lean.Elab.InfoTree) (hoverPos : String.Pos) :

Option (Lean.Elab.ContextInfo × Lean.Elab.Info)

Equations

Lean.Elab.InfoTree.hoverableInfoAt? t hoverPos = Id.run (let res := Lean.Elab.InfoTree.smallestInfo? (fun i => Id.run (let _do_jp := fun y => pure false; if ((match i with | Lean.Elab.Info.ofFieldInfo x => true | x => false) || Option.isSome (Lean.Elab.Info.toElabInfo? i)) = true then pure (Lean.Elab.Info.contains i hoverPos) else do let y ← pure PUnit.unit _do_jp y)) t; let _do_jp := fun y => res; match res with | some (x, Lean.Elab.Info.ofTermInfo ti) => if Lean.Expr.isSyntheticSorry ti.expr = true then pure none else do let y ← pure PUnit.unit _do_jp y | x => do let y ← pure PUnit.unit _do_jp y)

def Lean.Elab.Info.type? (i : Lean.Elab.Info) :

Lean.MetaM (Option Lean.Expr)

Equations

Lean.Elab.Info.type? i = match i with | Lean.Elab.Info.ofTermInfo ti => Lean.Internal.coeM (Lean.Meta.inferType ti.expr) | Lean.Elab.Info.ofFieldInfo fi => Lean.Internal.coeM (Lean.Meta.inferType fi.val) | x => pure none

def Lean.Elab.Info.docString? (i : Lean.Elab.Info) :

Lean.MetaM (Option String)

Equations

Lean.Elab.Info.docString? i = do let env ← Lean.getEnv let _do_jp : PUnit → Lean.MetaM (Option String) := fun y => let _do_jp := fun y => let _do_jp := fun y => pure none; match Lean.Elab.Info.toElabInfo? i with | some ei => do let a ← liftM (Lean.findDocString? env ei.elaborator) <||> liftM (Lean.findDocString? env (Lean.Syntax.getKind ei.stx)) pure a | x => do let y ← pure PUnit.unit _do_jp y; match i with | Lean.Elab.Info.ofFieldInfo fi => do let a ← liftM (Lean.findDocString? env fi.projName) pure a | x => do let y ← pure PUnit.unit _do_jp y match i with | Lean.Elab.Info.ofTermInfo ti => match Lean.Expr.constName? ti.expr with | some n => do let a ← liftM (Lean.findDocString? env n) pure a | x => do let y ← pure PUnit.unit _do_jp y | x => do let y ← pure PUnit.unit _do_jp y

def Lean.Elab.Info.fmtHover? (ci : Lean.Elab.ContextInfo) (i : Lean.Elab.Info) :

IO (Option Lean.Format)

Equations

Lean.Elab.Info.fmtHover? ci i = (fun fmtTerm? isAtomicFormat => Lean.Elab.ContextInfo.runMetaM ci (Lean.Elab.Info.lctx i) (let fmts := #[]; do let r ← tryCatch (do let a ← fmtTerm? match a with | some f => let fmts := Array.push fmts f; do let y ← pure PUnit.unit pure { fst := y, snd := fmts } | x => do let y ← pure PUnit.unit pure { fst := y, snd := fmts }) fun x => do let y ← pure () pure { fst := y, snd := fmts } let x : Array Lean.Format := r.snd let fmts : Array Lean.Format := x pure r.fst let a ← Lean.Elab.Info.docString? i let _do_jp : Array Lean.Format → PUnit → Lean.MetaM (Option Lean.Format) := fun fmts y => if Array.isEmpty fmts = true then pure none else pure (some (Lean.Format.joinSep (Array.toList fmts) (Lean.format "\n***\n"))) match a with | some m => let fmts := Array.push fmts (Std.Format.text m); do let y ← pure PUnit.unit _do_jp fmts y | x => do let y ← pure PUnit.unit _do_jp fmts y)) (Lean.Elab.Info.fmtHover?.fmtTerm? i) Lean.Elab.Info.fmtHover?.isAtomicFormat

def Lean.Elab.Info.fmtHover?.fmtTerm? (i : Lean.Elab.Info) :

Lean.MetaM (Option Lean.Format)

Equations

Lean.Elab.Info.fmtHover?.fmtTerm? i = match i with | Lean.Elab.Info.ofTermInfo ti => let _do_jp := fun y => do let tp ← Lean.Meta.inferType ti.expr let eFmt ← Lean.withOptions (fun a => (fun a => Lean.Option.set a Lean.pp.universes true) (Lean.Option.set a Lean.pp.fullNames true)) (Lean.Meta.ppExpr ti.expr) let tpFmt ← Lean.Meta.ppExpr tp let fmt : Lean.Format := if (Lean.Expr.isConst ti.expr || Lean.Elab.Info.fmtHover?.isAtomicFormat eFmt) = true then Lean.format "" ++ Lean.format eFmt ++ Lean.format " : " ++ Lean.format tpFmt ++ Lean.format "" else Lean.format "" ++ Lean.format tpFmt ++ Lean.format "" pure (some (Lean.format "```lean\n" ++ Lean.format fmt ++ Lean.format "\n```")); if Lean.Expr.isSort ti.expr = true then pure none else do let y ← pure PUnit.unit _do_jp y | Lean.Elab.Info.ofFieldInfo fi => do let tp ← Lean.Meta.inferType fi.val let tpFmt ← Lean.Meta.ppExpr tp pure (some (Lean.format "```lean\n" ++ Lean.format fi.fieldName ++ Lean.format " : " ++ Lean.format tpFmt ++ Lean.format "\n```")) | x => pure none

structure Lean.Elab.GoalsAtResult :

Type

ctxInfo : Lean.Elab.ContextInfo
tacticInfo : Lean.Elab.TacticInfo
useAfter : Bool

def Lean.Elab.InfoTree.goalsAt? (text : Lean.FileMap) (t : Lean.Elab.InfoTree) (hoverPos : String.Pos) :

List Lean.Elab.GoalsAtResult

Equations

Lean.Elab.InfoTree.goalsAt? text t hoverPos = (fun hasNestedTactic => Id.run (Lean.Elab.InfoTree.deepestNodes (fun x x_1 x_2 => match x, x_1, x_2 with | ctx, i@h:(Lean.Elab.Info.ofTacticInfo ti), cs => OptionM.run (match (Lean.Elab.Info.pos? i, Lean.Elab.Info.tailPos? i) with | (some pos, some tailPos) => let trailSize := Lean.Syntax.getTrailingSize (Lean.Elab.Info.stx i); let atEOF := tailPos + trailSize == String.bsize text.source; do guard (pos ≤ hoverPos ∧ (decide (hoverPos < tailPos + trailSize) || atEOF) = true) pure { ctxInfo := ctx, tacticInfo := ti, useAfter := decide (hoverPos > pos) && (decide (hoverPos ≥ tailPos) || !Std.PersistentArray.any cs (hasNestedTactic pos tailPos)) } | x => failure) | x, x_3, x_4 => none) t)) Lean.Elab.InfoTree.goalsAt?.hasNestedTactic

partial def Lean.Elab.InfoTree.goalsAt?.hasNestedTactic (pos : String.Pos) (tailPos : String.Pos) :

Lean.Elab.InfoTree → Bool

def Lean.Elab.InfoTree.termGoalAt? (t : Lean.Elab.InfoTree) (hoverPos : String.Pos) :

Option (Lean.Elab.ContextInfo × Lean.Elab.Info)

Equations

Lean.Elab.InfoTree.termGoalAt? t hoverPos = (fun getHeadFnPos? => let headFns := Lean.Elab.InfoTree.foldInfo (fun ctx i headFns => match getHeadFnPos? (Lean.Elab.Info.stx i) with | some pos => Std.HashSet.insert headFns pos | x => headFns) ∅ t; Lean.Elab.InfoTree.smallestInfo? (fun i => Id.run (let _do_jp := fun y => false; if Lean.Elab.Info.contains i hoverPos = true then match i with | Lean.Elab.Info.ofTermInfo ti => pure (!Lean.Syntax.isIdent ti.toElabInfo.stx || !Std.HashSet.contains headFns (Option.get! (Lean.Elab.Info.pos? i))) | x => do let y ← pure PUnit.unit _do_jp y else do let y ← pure PUnit.unit _do_jp y)) t) Lean.Elab.InfoTree.termGoalAt?.getHeadFnPos?

partial def Lean.Elab.InfoTree.termGoalAt?.getHeadFnPos? (s : Lean.Syntax) (foundArgs : optParam Bool false) :

Option String.Pos