Lean.Elab.InfoTree

source

structure Lean.Elab.ContextInfo :

Type

env : Lean.Environment
fileMap : Lean.FileMap
mctx : Lean.MetavarContext
options : Lean.Options
currNamespace : Lean.Name
openDecls : List Lean.OpenDecl

source

instance Lean.Elab.instInhabitedContextInfo :

Inhabited Lean.Elab.ContextInfo

Equations

Lean.Elab.instInhabitedContextInfo = { default := { env := default, fileMap := default, mctx := default, options := default, currNamespace := default, openDecls := default } }

source

structure Lean.Elab.ElabInfo :

Type

elaborator : Lean.Name
stx : Lean.Syntax

source

instance Lean.Elab.instInhabitedElabInfo :

Inhabited Lean.Elab.ElabInfo

Equations

Lean.Elab.instInhabitedElabInfo = { default := { elaborator := default, stx := default } }

source

structure Lean.Elab.TermInfo extends Lean.Elab.ElabInfo :

Type

lctx : Lean.LocalContext
expectedType? : Option Lean.Expr
expr : Lean.Expr
isBinder : Bool

source

instance Lean.Elab.instInhabitedTermInfo :

Inhabited Lean.Elab.TermInfo

Equations

Lean.Elab.instInhabitedTermInfo = { default := { toElabInfo := default, lctx := default, expectedType? := default, expr := default, isBinder := default } }

source

structure Lean.Elab.CommandInfo extends Lean.Elab.ElabInfo :

Type

source

instance Lean.Elab.instInhabitedCommandInfo :

Inhabited Lean.Elab.CommandInfo

Equations

Lean.Elab.instInhabitedCommandInfo = { default := { toElabInfo := default } }

source

inductive Lean.Elab.CompletionInfo :

Type

dot: Lean.Elab.TermInfo → Option Lean.Syntax → Option Lean.Expr → Lean.Elab.CompletionInfo
id: Lean.Syntax → Lean.Name → Bool → Lean.LocalContext → Option Lean.Expr → Lean.Elab.CompletionInfo
namespaceId: Lean.Syntax → Lean.Elab.CompletionInfo
option: Lean.Syntax → Lean.Elab.CompletionInfo
endSection: Lean.Syntax → List String → Lean.Elab.CompletionInfo
tactic: Lean.Syntax → List Lean.MVarId → Lean.Elab.CompletionInfo

source

def Lean.Elab.CompletionInfo.stx :

Lean.Elab.CompletionInfo → Lean.Syntax

Equations

Lean.Elab.CompletionInfo.stx x = match x with | Lean.Elab.CompletionInfo.dot i x x_1 => i.toElabInfo.stx | Lean.Elab.CompletionInfo.id stx x x_1 x_2 x_3 => stx | Lean.Elab.CompletionInfo.namespaceId stx => stx | Lean.Elab.CompletionInfo.option stx => stx | Lean.Elab.CompletionInfo.endSection stx x => stx | Lean.Elab.CompletionInfo.tactic stx x => stx

source

structure Lean.Elab.FieldInfo :

Type

projName : Lean.Name
fieldName : Lean.Name
lctx : Lean.LocalContext
val : Lean.Expr
stx : Lean.Syntax

source

instance Lean.Elab.instInhabitedFieldInfo :

Inhabited Lean.Elab.FieldInfo

Equations

Lean.Elab.instInhabitedFieldInfo = { default := { projName := default, fieldName := default, lctx := default, val := default, stx := default } }

source

structure Lean.Elab.TacticInfo extends Lean.Elab.ElabInfo :

Type

mctxBefore : Lean.MetavarContext
goalsBefore : List Lean.MVarId
mctxAfter : Lean.MetavarContext
goalsAfter : List Lean.MVarId

source

instance Lean.Elab.instInhabitedTacticInfo :

Inhabited Lean.Elab.TacticInfo

Equations

Lean.Elab.instInhabitedTacticInfo = { default := { toElabInfo := default, mctxBefore := default, goalsBefore := default, mctxAfter := default, goalsAfter := default } }

source

structure Lean.Elab.MacroExpansionInfo :

Type

lctx : Lean.LocalContext
stx : Lean.Syntax
output : Lean.Syntax

source

instance Lean.Elab.instInhabitedMacroExpansionInfo :

Inhabited Lean.Elab.MacroExpansionInfo

Equations

Lean.Elab.instInhabitedMacroExpansionInfo = { default := { lctx := default, stx := default, output := default } }

source

inductive Lean.Elab.Info :

Type

ofTacticInfo: Lean.Elab.TacticInfo → Lean.Elab.Info
ofTermInfo: Lean.Elab.TermInfo → Lean.Elab.Info
ofCommandInfo: Lean.Elab.CommandInfo → Lean.Elab.Info
ofMacroExpansionInfo: Lean.Elab.MacroExpansionInfo → Lean.Elab.Info
ofFieldInfo: Lean.Elab.FieldInfo → Lean.Elab.Info
ofCompletionInfo: Lean.Elab.CompletionInfo → Lean.Elab.Info

source

instance Lean.Elab.instInhabitedInfo :

Inhabited Lean.Elab.Info

Equations

Lean.Elab.instInhabitedInfo = { default := Lean.Elab.Info.ofTacticInfo default }

source

inductive Lean.Elab.InfoTree :

Type

context: Lean.Elab.ContextInfo → Lean.Elab.InfoTree → Lean.Elab.InfoTree
node: Lean.Elab.Info → Std.PersistentArray Lean.Elab.InfoTree → Lean.Elab.InfoTree
ofJson: Lean.Json → Lean.Elab.InfoTree
hole: Lean.MVarId → Lean.Elab.InfoTree

source

instance Lean.Elab.instInhabitedInfoTree :

Inhabited Lean.Elab.InfoTree

Equations

Lean.Elab.instInhabitedInfoTree = { default := Lean.Elab.InfoTree.node default default }

source

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

Option Lean.Elab.Info

source

structure Lean.Elab.InfoState :

Type

enabled : Bool
assignment : Std.PersistentHashMap Lean.MVarId Lean.Elab.InfoTree
trees : Std.PersistentArray Lean.Elab.InfoTree

source

instance Lean.Elab.instInhabitedInfoState :

Inhabited Lean.Elab.InfoState

Equations

Lean.Elab.instInhabitedInfoState = { default := { enabled := default, assignment := default, trees := default } }

source

class Lean.Elab.MonadInfoTree (m : Type → Type) :

Type

getInfoState : m Lean.Elab.InfoState
modifyInfoState : (Lean.Elab.InfoState → Lean.Elab.InfoState) → m Unit

Instances

source

instance Lean.Elab.instMonadInfoTree {m : Type → Type} {n : Type → Type} [inst : MonadLift m n] [inst : Lean.Elab.MonadInfoTree m] :

Lean.Elab.MonadInfoTree n

Equations

Lean.Elab.instMonadInfoTree = { getInfoState := liftM Lean.Elab.getInfoState, modifyInfoState := fun f => liftM (Lean.Elab.modifyInfoState f) }

source

partial def Lean.Elab.InfoTree.substitute (tree : Lean.Elab.InfoTree) (assignment : Std.PersistentHashMap Lean.MVarId Lean.Elab.InfoTree) :

Lean.Elab.InfoTree

source

def Lean.Elab.ContextInfo.runMetaM {α : Type} (info : Lean.Elab.ContextInfo) (lctx : Lean.LocalContext) (x : Lean.MetaM α) :

IO α

Equations

Lean.Elab.ContextInfo.runMetaM info lctx x = let x := Lean.Meta.MetaM.run x { config := { foApprox := false, ctxApprox := false, quasiPatternApprox := false, constApprox := false, isDefEqStuckEx := false, transparency := Lean.Meta.TransparencyMode.default, zetaNonDep := true, trackZeta := false, unificationHints := true, proofIrrelevance := true, assignSyntheticOpaque := false, ignoreLevelMVarDepth := true, offsetCnstrs := true, etaStruct := true }, lctx := lctx, localInstances := #[], defEqCtx? := none, synthPendingDepth := 0, canUnfold? := none } { mctx := info.mctx, cache := { inferType := { root := Std.PersistentHashMap.Node.entries Std.PersistentHashMap.mkEmptyEntriesArray, size := 0 }, funInfo := { root := Std.PersistentHashMap.Node.entries Std.PersistentHashMap.mkEmptyEntriesArray, size := 0 }, synthInstance := { root := Std.PersistentHashMap.Node.entries Std.PersistentHashMap.mkEmptyEntriesArray, size := 0 }, whnfDefault := { root := Std.PersistentHashMap.Node.entries Std.PersistentHashMap.mkEmptyEntriesArray, size := 0 }, whnfAll := { root := Std.PersistentHashMap.Node.entries Std.PersistentHashMap.mkEmptyEntriesArray, size := 0 }, defEqDefault := { root := Std.PersistentHashMap.Node.entries Std.PersistentHashMap.mkEmptyEntriesArray, size := 0 }, defEqAll := { root := Std.PersistentHashMap.Node.entries Std.PersistentHashMap.mkEmptyEntriesArray, size := 0 } }, zetaFVarIds := ∅, postponed := { root := Std.PersistentArrayNode.node (Array.mkEmpty (USize.toNat Std.PersistentArray.branching)), tail := Array.mkEmpty (USize.toNat Std.PersistentArray.branching), size := 0, shift := Std.PersistentArray.initShift, tailOff := 0 } }; do let discr ← Lean.Core.CoreM.toIO x { options := info.options, currRecDepth := 0, maxRecDepth := 1000, ref := Lean.Syntax.missing, currNamespace := info.currNamespace, openDecls := info.openDecls, initHeartbeats := 0, maxHeartbeats := Lean.Core.getMaxHeartbeats info.options } { env := info.env, nextMacroScope := Lean.firstFrontendMacroScope + 1, ngen := { namePrefix := `_uniq, idx := 1 }, traceState := { enabled := true, traces := { root := Std.PersistentArrayNode.node (Array.mkEmpty (USize.toNat Std.PersistentArray.branching)), tail := Array.mkEmpty (USize.toNat Std.PersistentArray.branching), size := 0, shift := Std.PersistentArray.initShift, tailOff := 0 } } } let x : (α × Lean.Meta.State) × Lean.Core.State := discr match x with | ((a, x), x_1) => pure a

source

def Lean.Elab.ContextInfo.toPPContext (info : Lean.Elab.ContextInfo) (lctx : Lean.LocalContext) :

Lean.PPContext

Equations

Lean.Elab.ContextInfo.toPPContext info lctx = { env := info.env, mctx := info.mctx, lctx := lctx, opts := info.options, currNamespace := info.currNamespace, openDecls := info.openDecls }

source

def Lean.Elab.ContextInfo.ppSyntax (info : Lean.Elab.ContextInfo) (lctx : Lean.LocalContext) (stx : Lean.Syntax) :

IO Lean.Format

Equations

Lean.Elab.ContextInfo.ppSyntax info lctx stx = Lean.ppTerm (Lean.Elab.ContextInfo.toPPContext info lctx) stx

source

def Lean.Elab.TermInfo.runMetaM {α : Type} (info : Lean.Elab.TermInfo) (ctx : Lean.Elab.ContextInfo) (x : Lean.MetaM α) :

IO α

Equations

Lean.Elab.TermInfo.runMetaM info ctx x = Lean.Elab.ContextInfo.runMetaM ctx info.lctx x

source

def Lean.Elab.TermInfo.format (ctx : Lean.Elab.ContextInfo) (info : Lean.Elab.TermInfo) :

IO Lean.Format

Equations

Lean.Elab.TermInfo.format ctx info = Lean.Elab.TermInfo.runMetaM info ctx (let _do_jp := fun ty => do let a ← Lean.Meta.ppExpr info.expr pure (Lean.format "" ++ Lean.format a ++ Lean.format " " ++ Lean.format (if info.isBinder = true then "(isBinder := true) " else "") ++ Lean.format ": " ++ Lean.format ty ++ Lean.format " @ " ++ Lean.format (Lean.Elab.formatElabInfo ctx info.toElabInfo) ++ Lean.format ""); do let y ← tryCatch (do let a ← Lean.Meta.inferType info.expr Lean.Meta.ppExpr a) fun x => pure (Std.Format.text "") _do_jp y)

source

def Lean.Elab.CompletionInfo.format (ctx : Lean.Elab.ContextInfo) (info : Lean.Elab.CompletionInfo) :

IO Lean.Format

Equations

Lean.Elab.CompletionInfo.format ctx info = match info with | Lean.Elab.CompletionInfo.dot i x expectedType? => do let a ← Lean.Elab.TermInfo.format ctx i pure (Lean.format "[.] " ++ Lean.format a ++ Lean.format " : " ++ Lean.format expectedType? ++ Lean.format "") | Lean.Elab.CompletionInfo.id stx x x_1 lctx expectedType? => Lean.Elab.ContextInfo.runMetaM ctx lctx (pure (Lean.format "[.] " ++ Lean.format stx ++ Lean.format " : " ++ Lean.format expectedType? ++ Lean.format " @ " ++ Lean.format (Lean.Elab.formatStxRange ctx (Lean.Elab.CompletionInfo.stx info)) ++ Lean.format "")) | x => pure (Lean.format "[.] " ++ Lean.format (Lean.Elab.CompletionInfo.stx info) ++ Lean.format " @ " ++ Lean.format (Lean.Elab.formatStxRange ctx (Lean.Elab.CompletionInfo.stx info)) ++ Lean.format "")

source

def Lean.Elab.CommandInfo.format (ctx : Lean.Elab.ContextInfo) (info : Lean.Elab.CommandInfo) :

IO Lean.Format

Equations

Lean.Elab.CommandInfo.format ctx info = pure (Lean.format "command @ " ++ Lean.format (Lean.Elab.formatElabInfo ctx info.toElabInfo) ++ Lean.format "")

source

def Lean.Elab.FieldInfo.format (ctx : Lean.Elab.ContextInfo) (info : Lean.Elab.FieldInfo) :

IO Lean.Format

Equations

Lean.Elab.FieldInfo.format ctx info = Lean.Elab.ContextInfo.runMetaM ctx info.lctx do let a ← Lean.Meta.inferType info.val let a ← Lean.Meta.ppExpr a let a_1 ← Lean.Meta.ppExpr info.val pure (Lean.format "" ++ Lean.format info.fieldName ++ Lean.format " : " ++ Lean.format a ++ Lean.format " := " ++ Lean.format a_1 ++ Lean.format " @ " ++ Lean.format (Lean.Elab.formatStxRange ctx info.stx) ++ Lean.format "")

source

def Lean.Elab.ContextInfo.ppGoals (ctx : Lean.Elab.ContextInfo) (goals : List Lean.MVarId) :

IO Lean.Format

Equations

Lean.Elab.ContextInfo.ppGoals ctx goals = if List.isEmpty goals = true then pure (Std.Format.text "no goals") else Lean.Elab.ContextInfo.runMetaM ctx { fvarIdToDecl := { root := Std.PersistentHashMap.Node.entries Std.PersistentHashMap.mkEmptyEntriesArray, size := 0 }, decls := { root := Std.PersistentArrayNode.node (Array.mkEmpty (USize.toNat Std.PersistentArray.branching)), tail := Array.mkEmpty (USize.toNat Std.PersistentArray.branching), size := 0, shift := Std.PersistentArray.initShift, tailOff := 0 } } do let a ← List.mapM (fun a => Lean.Meta.ppGoal a) goals pure (Std.Format.prefixJoin (Std.Format.text "\n") a)

source

def Lean.Elab.TacticInfo.format (ctx : Lean.Elab.ContextInfo) (info : Lean.Elab.TacticInfo) :

IO Lean.Format

Equations

Lean.Elab.TacticInfo.format ctx info = let ctxB := { env := ctx.env, fileMap := ctx.fileMap, mctx := info.mctxBefore, options := ctx.options, currNamespace := ctx.currNamespace, openDecls := ctx.openDecls }; let ctxA := { env := ctx.env, fileMap := ctx.fileMap, mctx := info.mctxAfter, options := ctx.options, currNamespace := ctx.currNamespace, openDecls := ctx.openDecls }; do let goalsBefore ← Lean.Elab.ContextInfo.ppGoals ctxB info.goalsBefore let goalsAfter ← Lean.Elab.ContextInfo.ppGoals ctxA info.goalsAfter pure (Lean.format "Tactic @ " ++ Lean.format (Lean.Elab.formatElabInfo ctx info.toElabInfo) ++ Lean.format "\n" ++ Lean.format info.toElabInfo.stx ++ Lean.format "\nbefore " ++ Lean.format goalsBefore ++ Lean.format "\nafter " ++ Lean.format goalsAfter ++ Lean.format "")

source

def Lean.Elab.MacroExpansionInfo.format (ctx : Lean.Elab.ContextInfo) (info : Lean.Elab.MacroExpansionInfo) :

IO Lean.Format

Equations

Lean.Elab.MacroExpansionInfo.format ctx info = do let stx ← Lean.Elab.ContextInfo.ppSyntax ctx info.lctx info.stx let output ← Lean.Elab.ContextInfo.ppSyntax ctx info.lctx info.output pure (Lean.format "Macro expansion\n" ++ Lean.format stx ++ Lean.format "\n===>\n" ++ Lean.format output ++ Lean.format "")

source

def Lean.Elab.Info.format (ctx : Lean.Elab.ContextInfo) :

Lean.Elab.Info → IO Lean.Format

Equations

Lean.Elab.Info.format ctx x = match x with | Lean.Elab.Info.ofTacticInfo i => Lean.Elab.TacticInfo.format ctx i | Lean.Elab.Info.ofTermInfo i => Lean.Elab.TermInfo.format ctx i | Lean.Elab.Info.ofCommandInfo i => Lean.Elab.CommandInfo.format ctx i | Lean.Elab.Info.ofMacroExpansionInfo i => Lean.Elab.MacroExpansionInfo.format ctx i | Lean.Elab.Info.ofFieldInfo i => Lean.Elab.FieldInfo.format ctx i | Lean.Elab.Info.ofCompletionInfo i => Lean.Elab.CompletionInfo.format ctx i

source

def Lean.Elab.Info.toElabInfo? :

Lean.Elab.Info → Option Lean.Elab.ElabInfo

Equations

Lean.Elab.Info.toElabInfo? x = match x with | Lean.Elab.Info.ofTacticInfo i => some i.toElabInfo | Lean.Elab.Info.ofTermInfo i => some i.toElabInfo | Lean.Elab.Info.ofCommandInfo i => some i.toElabInfo | Lean.Elab.Info.ofMacroExpansionInfo i => none | Lean.Elab.Info.ofFieldInfo i => none | Lean.Elab.Info.ofCompletionInfo i => none

source

def Lean.Elab.Info.updateContext? :

Option Lean.Elab.ContextInfo → Lean.Elab.Info → Option Lean.Elab.ContextInfo

Equations

Lean.Elab.Info.updateContext? x x = match x, x with | some ctx, Lean.Elab.Info.ofTacticInfo i => some { env := ctx.env, fileMap := ctx.fileMap, mctx := i.mctxAfter, options := ctx.options, currNamespace := ctx.currNamespace, openDecls := ctx.openDecls } | ctx?, x => ctx?

source

partial def Lean.Elab.InfoTree.format (tree : Lean.Elab.InfoTree) (ctx? : optParam (Option Lean.Elab.ContextInfo) none) :

IO Lean.Format

source

def Lean.Elab.getResetInfoTrees {m : Type → Type} [inst : Monad m] [inst : Lean.Elab.MonadInfoTree m] :

m (Std.PersistentArray Lean.Elab.InfoTree)

Equations

Lean.Elab.getResetInfoTrees = do let a ← Lean.Elab.getInfoState let trees : Std.PersistentArray Lean.Elab.InfoTree := a.trees Lean.Elab.modifyInfoTrees fun x => { root := Std.PersistentArrayNode.node (Array.mkEmpty (USize.toNat Std.PersistentArray.branching)), tail := Array.mkEmpty (USize.toNat Std.PersistentArray.branching), size := 0, shift := Std.PersistentArray.initShift, tailOff := 0 } pure trees

source

def Lean.Elab.pushInfoTree {m : Type → Type} [inst : Monad m] [inst : Lean.Elab.MonadInfoTree m] (t : Lean.Elab.InfoTree) :

m Unit

Equations

Lean.Elab.pushInfoTree t = do let a ← Lean.Elab.getInfoState if a.enabled = true then Lean.Elab.modifyInfoTrees fun ts => Std.PersistentArray.push ts t else pure PUnit.unit

source

def Lean.Elab.pushInfoLeaf {m : Type → Type} [inst : Monad m] [inst : Lean.Elab.MonadInfoTree m] (t : Lean.Elab.Info) :

m Unit

Equations

Lean.Elab.pushInfoLeaf t = do let a ← Lean.Elab.getInfoState if a.enabled = true then Lean.Elab.pushInfoTree (Lean.Elab.InfoTree.node t { root := Std.PersistentArrayNode.node (Array.mkEmpty (USize.toNat Std.PersistentArray.branching)), tail := Array.mkEmpty (USize.toNat Std.PersistentArray.branching), size := 0, shift := Std.PersistentArray.initShift, tailOff := 0 }) else pure PUnit.unit

source

def Lean.Elab.addCompletionInfo {m : Type → Type} [inst : Monad m] [inst : Lean.Elab.MonadInfoTree m] (info : Lean.Elab.CompletionInfo) :

m Unit

Equations

Lean.Elab.addCompletionInfo info = Lean.Elab.pushInfoLeaf (Lean.Elab.Info.ofCompletionInfo info)

source

def Lean.Elab.resolveGlobalConstNoOverloadWithInfo {m : Type → Type} [inst : Monad m] [inst : Lean.Elab.MonadInfoTree m] [inst : Lean.MonadResolveName m] [inst : Lean.MonadEnv m] [inst : Lean.MonadError m] (id : Lean.Syntax) (expectedType? : optParam (Option Lean.Expr) none) :

m Lean.Name

Equations

Lean.Elab.resolveGlobalConstNoOverloadWithInfo id expectedType? = do let n ← Lean.resolveGlobalConstNoOverload id let a ← Lean.Elab.getInfoState let _do_jp : Unit → m Lean.Name := fun y => pure n if a.enabled = true then do let a ← Lean.mkConstWithLevelParams n let y ← Lean.Elab.pushInfoLeaf (Lean.Elab.Info.ofTermInfo { toElabInfo := { elaborator := Lean.Name.anonymous, stx := id }, lctx := Lean.LocalContext.empty, expectedType? := expectedType?, expr := a, isBinder := false }) _do_jp y else do let y ← pure PUnit.unit _do_jp y

source

def Lean.Elab.resolveGlobalConstWithInfos {m : Type → Type} [inst : Monad m] [inst : Lean.Elab.MonadInfoTree m] [inst : Lean.MonadResolveName m] [inst : Lean.MonadEnv m] [inst : Lean.MonadError m] (id : Lean.Syntax) (expectedType? : optParam (Option Lean.Expr) none) :

m (List Lean.Name)

Equations

Lean.Elab.resolveGlobalConstWithInfos id expectedType? = do let ns ← Lean.resolveGlobalConst id let a ← Lean.Elab.getInfoState let _do_jp : PUnit → m (List Lean.Name) := fun y => pure ns if a.enabled = true then do let r ← forIn ns PUnit.unit fun n r => do let a ← Lean.mkConstWithLevelParams n Lean.Elab.pushInfoLeaf (Lean.Elab.Info.ofTermInfo { toElabInfo := { elaborator := Lean.Name.anonymous, stx := id }, lctx := Lean.LocalContext.empty, expectedType? := expectedType?, expr := a, isBinder := false }) pure (ForInStep.yield PUnit.unit) let x : PUnit := r let y ← pure PUnit.unit _do_jp y else do let y ← pure PUnit.unit _do_jp y

source

def Lean.Elab.withInfoContext' {m : Type → Type} [inst : Monad m] [inst : Lean.Elab.MonadInfoTree m] {α : Type} [inst : MonadFinally m] (x : m α) (mkInfo : α → m (Lean.Elab.Info ⊕ Lean.MVarId)) :

m α

Equations

Lean.Elab.withInfoContext' x mkInfo = do let a ← Lean.Elab.getInfoState if a.enabled = true then do let treesSaved ← Lean.Elab.getResetInfoTrees Prod.fst <$> tryFinally' x fun a? => match a? with | none => Lean.Elab.modifyInfoTrees fun x => treesSaved | some a => do let info ← mkInfo a Lean.Elab.modifyInfoTrees fun trees => match info with | Sum.inl info => Std.PersistentArray.push treesSaved (Lean.Elab.InfoTree.node info trees) | Sum.inr mvaId => Std.PersistentArray.push treesSaved (Lean.Elab.InfoTree.hole mvaId) else x

source

def Lean.Elab.withInfoTreeContext {m : Type → Type} [inst : Monad m] [inst : Lean.Elab.MonadInfoTree m] {α : Type} [inst : MonadFinally m] (x : m α) (mkInfoTree : Std.PersistentArray Lean.Elab.InfoTree → m Lean.Elab.InfoTree) :

m α

Equations

Lean.Elab.withInfoTreeContext x mkInfoTree = do let a ← Lean.Elab.getInfoState if a.enabled = true then do let treesSaved ← Lean.Elab.getResetInfoTrees Prod.fst <$> tryFinally' x fun x => do let st ← Lean.Elab.getInfoState let tree ← mkInfoTree st.trees Lean.Elab.modifyInfoTrees fun x => Std.PersistentArray.push treesSaved tree else x

source

@[inline]

def Lean.Elab.withInfoContext {m : Type → Type} [inst : Monad m] [inst : Lean.Elab.MonadInfoTree m] {α : Type} [inst : MonadFinally m] (x : m α) (mkInfo : m Lean.Elab.Info) :

m α

Equations

Lean.Elab.withInfoContext x mkInfo = Lean.Elab.withInfoTreeContext x fun trees => do let a ← mkInfo pure (Lean.Elab.InfoTree.node a trees)

source

def Lean.Elab.withSaveInfoContext {m : Type → Type} [inst : Monad m] [inst : Lean.Elab.MonadInfoTree m] {α : Type} [inst : MonadFinally m] [inst : Lean.MonadEnv m] [inst : Lean.MonadOptions m] [inst : Lean.MonadMCtx m] [inst : Lean.MonadResolveName m] [inst : Lean.MonadFileMap m] (x : m α) :

m α

Equations

Lean.Elab.withSaveInfoContext x = do let a ← Lean.Elab.getInfoState if a.enabled = true then do let treesSaved ← Lean.Elab.getResetInfoTrees Prod.fst <$> tryFinally' x fun x => do let st ← Lean.Elab.getInfoState let trees ← Std.PersistentArray.mapM (fun tree => let tree := Lean.Elab.InfoTree.substitute tree st.assignment; do let a ← Lean.getEnv let a_1 ← Lean.getFileMap let a_2 ← Lean.getMCtx let a_3 ← Lean.getCurrNamespace let a_4 ← Lean.getOpenDecls let a_5 ← Lean.getOptions pure (Lean.Elab.InfoTree.context { env := a, fileMap := a_1, mctx := a_2, options := a_5, currNamespace := a_3, openDecls := a_4 } tree)) st.trees Lean.Elab.modifyInfoTrees fun x => treesSaved ++ trees else x

source

def Lean.Elab.getInfoHoleIdAssignment? {m : Type → Type} [inst : Monad m] [inst : Lean.Elab.MonadInfoTree m] (mvarId : Lean.MVarId) :

m (Option Lean.Elab.InfoTree)

Equations

Lean.Elab.getInfoHoleIdAssignment? mvarId = do let a ← Lean.Elab.getInfoState pure (Std.PersistentHashMap.getOp a.assignment mvarId)

source

def Lean.Elab.assignInfoHoleId {m : Type → Type} [inst : Monad m] [inst : Lean.Elab.MonadInfoTree m] (mvarId : Lean.MVarId) (infoTree : Lean.Elab.InfoTree) :

m Unit

Equations

Lean.Elab.assignInfoHoleId mvarId infoTree = do let a ← Lean.Elab.getInfoHoleIdAssignment? mvarId if Option.isNone a = true then Lean.Elab.modifyInfoState fun s => { enabled := s.enabled, assignment := Std.PersistentHashMap.insert s.assignment mvarId infoTree, trees := s.trees } else panicWithPosWithDecl "Lean.Elab.InfoTree" "Lean.Elab.assignInfoHoleId" 341 2 ("assertion violation: " ++ "( a ).isNone\n ")

source

def Lean.Elab.withMacroExpansionInfo {m : Type → Type} {α : Type} [inst : MonadFinally m] [inst : Monad m] [inst : Lean.Elab.MonadInfoTree m] [inst : Lean.MonadLCtx m] (stx : Lean.Syntax) (output : Lean.Syntax) (x : m α) :

m α

Equations

Lean.Elab.withMacroExpansionInfo stx output x = let mkInfo := do let a ← Lean.getLCtx pure (Lean.Elab.Info.ofMacroExpansionInfo { lctx := a, stx := stx, output := output }); Lean.Elab.withInfoContext x mkInfo

source

@[inline]

def Lean.Elab.withInfoHole {m : Type → Type} {α : Type} [inst : MonadFinally m] [inst : Monad m] [inst : Lean.Elab.MonadInfoTree m] (mvarId : Lean.MVarId) (x : m α) :

m α

Equations

Lean.Elab.withInfoHole mvarId x = do let a ← Lean.Elab.getInfoState if a.enabled = true then do let treesSaved ← Lean.Elab.getResetInfoTrees Prod.fst <$> tryFinally' x fun a? => Lean.Elab.modifyInfoState fun s => if s.trees.size > 0 then { enabled := s.enabled, assignment := Std.PersistentHashMap.insert s.assignment mvarId (Std.PersistentArray.getOp s.trees (s.trees.size - 1)), trees := treesSaved } else { enabled := s.enabled, assignment := s.assignment, trees := treesSaved } else x

source

def Lean.Elab.enableInfoTree {m : Type → Type} [inst : Lean.Elab.MonadInfoTree m] (flag : optParam Bool true) :

m Unit

Equations

Lean.Elab.enableInfoTree flag = Lean.Elab.modifyInfoState fun s => { enabled := flag, assignment := s.assignment, trees := s.trees }

source

def Lean.Elab.getInfoTrees {m : Type → Type} [inst : Lean.Elab.MonadInfoTree m] [inst : Monad m] :

m (Std.PersistentArray Lean.Elab.InfoTree)

Equations

Lean.Elab.getInfoTrees = do let a ← Lean.Elab.getInfoState pure a.trees