|
| 1 | +/- |
| 2 | +Copyright (c) 2026 Lean FRO. All rights reserved. |
| 3 | +Released under Apache 2.0 license as described in the file LICENSE. |
| 4 | +
|
| 5 | +Authors: Wojciech Nawrocki, Leonardo de Moura, Sebastian Ullrich |
| 6 | +-/ |
| 7 | +module |
| 8 | + |
| 9 | +prelude |
| 10 | +public import Lean.Elab.InfoTree.Types |
| 11 | +import Init.Data.Format.Macro |
| 12 | +import Init.Data.Range.Polymorphic.Stream |
| 13 | +import Init.Task |
| 14 | +import Lean.Syntax |
| 15 | + |
| 16 | +public section |
| 17 | + |
| 18 | +namespace Lean.Elab |
| 19 | + |
| 20 | +/-- |
| 21 | +Merges the `inner` partial context into the `outer` context s.t. fields of the `inner` context |
| 22 | +overwrite fields of the `outer` context. Panics if the invariant described in the documentation |
| 23 | +for `PartialContextInfo` is violated. |
| 24 | +
|
| 25 | +When traversing an `InfoTree`, this function should be used to combine the context of outer |
| 26 | +nodes with the partial context of their subtrees. This ensures that the traversal has the context |
| 27 | +from the inner node to the root node of the `InfoTree` available, with partial contexts of |
| 28 | +inner nodes taking priority over contexts of outer nodes. |
| 29 | +-/ |
| 30 | +def PartialContextInfo.mergeIntoOuter? |
| 31 | + : (inner : PartialContextInfo) → (outer? : Option ContextInfo) → Option ContextInfo |
| 32 | + | .commandCtx info, none => |
| 33 | + some { info with } |
| 34 | + | .parentDeclCtx _, none => |
| 35 | + panic! "Unexpected incomplete InfoTree context info." |
| 36 | + | .autoImplicitCtx _, none => |
| 37 | + panic! "Unexpected incomplete InfoTree context info." |
| 38 | + | .commandCtx innerInfo, some outer => |
| 39 | + some { outer with toCommandContextInfo := { innerInfo with cmdEnv? := outer.cmdEnv? <|> innerInfo.cmdEnv? } } |
| 40 | + | .parentDeclCtx innerParentDecl, some outer => |
| 41 | + some { outer with parentDecl? := innerParentDecl } |
| 42 | + | .autoImplicitCtx innerAutoImplicits, some outer => |
| 43 | + some { outer with autoImplicits := innerAutoImplicits } |
| 44 | + |
| 45 | +def CompletionInfo.stx : CompletionInfo → Syntax |
| 46 | + | dot i .. => i.stx |
| 47 | + | id stx .. => stx |
| 48 | + | dotId stx .. => stx |
| 49 | + | fieldId stx .. => stx |
| 50 | + | namespaceId stx => stx |
| 51 | + | option stx => stx |
| 52 | + | errorName stx .. => stx |
| 53 | + | endSection stx .. => stx |
| 54 | + | tactic stx .. => stx |
| 55 | + |
| 56 | +/-- |
| 57 | +Obtains the `LocalContext` from this `CompletionInfo` if available and yields an empty context |
| 58 | +otherwise. |
| 59 | +-/ |
| 60 | +def CompletionInfo.lctx : CompletionInfo → LocalContext |
| 61 | + | dot i .. => i.lctx |
| 62 | + | id _ _ _ lctx .. => lctx |
| 63 | + | dotId _ _ lctx .. => lctx |
| 64 | + | fieldId _ _ lctx .. => lctx |
| 65 | + | _ => .empty |
| 66 | + |
| 67 | +partial def InfoTree.findInfo? (p : Info → Bool) (t : InfoTree) : Option Info := |
| 68 | + match t with |
| 69 | + | context _ t => findInfo? p t |
| 70 | + | node i ts => |
| 71 | + if p i then |
| 72 | + some i |
| 73 | + else |
| 74 | + ts.findSome? (findInfo? p) |
| 75 | + | _ => none |
| 76 | + |
| 77 | +/-- Instantiate the holes on the given `tree` with the assignment table. |
| 78 | +(analogous to instantiating the metavariables in an expression) -/ |
| 79 | +partial def InfoTree.substitute (tree : InfoTree) (assignment : PersistentHashMap MVarId InfoTree) : InfoTree := |
| 80 | + match tree with |
| 81 | + | node i c => node i <| c.map (substitute · assignment) |
| 82 | + | context i t => context i (substitute t assignment) |
| 83 | + | hole id => match assignment.find? id with |
| 84 | + | none => hole id |
| 85 | + | some tree => substitute tree assignment |
| 86 | + |
| 87 | +/-- Applies `s.lazyAssignment` to `s.trees`, asynchronously. -/ |
| 88 | +def InfoState.substituteLazy (s : InfoState) : Task InfoState := |
| 89 | + Task.mapList (tasks := s.lazyAssignment.toList.map (·.2)) fun _ => { s with |
| 90 | + trees := s.trees.map (·.substitute <| s.lazyAssignment.map (·.get)) |
| 91 | + lazyAssignment := {} |
| 92 | + } |
| 93 | + |
| 94 | +def Info.toElabInfo? : Info → Option ElabInfo |
| 95 | + | ofTacticInfo i => some i.toElabInfo |
| 96 | + | ofTermInfo i => some i.toElabInfo |
| 97 | + | ofPartialTermInfo i => some i.toElabInfo |
| 98 | + | ofCommandInfo i => some i.toElabInfo |
| 99 | + | ofMacroExpansionInfo _ => none |
| 100 | + | ofOptionInfo _ => none |
| 101 | + | ofErrorNameInfo _ => none |
| 102 | + | ofFieldInfo _ => none |
| 103 | + | ofCompletionInfo _ => none |
| 104 | + | ofUserWidgetInfo _ => none |
| 105 | + | ofCustomInfo _ => none |
| 106 | + | ofFVarAliasInfo _ => none |
| 107 | + | ofFieldRedeclInfo _ => none |
| 108 | + | ofDelabTermInfo i => some i.toElabInfo |
| 109 | + | ofChoiceInfo i => some i.toElabInfo |
| 110 | + | ofDocInfo i => some i.toElabInfo |
| 111 | + | ofDocElabInfo i => some i.toElabInfo |
| 112 | + |
| 113 | +/-- |
| 114 | + Helper function for propagating the tactic metavariable context to its children nodes. |
| 115 | + We need this function because we preserve `TacticInfo` nodes during backtracking *and* their |
| 116 | + children. Moreover, we backtrack the metavariable context to undo metavariable assignments. |
| 117 | + `TacticInfo` nodes save the metavariable context before/after the tactic application, and |
| 118 | + can be pretty printed without any extra information. This is not the case for `TermInfo` nodes. |
| 119 | + Without this function, the formatting method would often fail when processing `TermInfo` nodes |
| 120 | + that are children of `TacticInfo` nodes that have been preserved during backtracking. |
| 121 | + Saving the metavariable context at `TermInfo` nodes is also not a good option because |
| 122 | + at `TermInfo` creation time, the metavariable context often miss information, e.g., |
| 123 | + a TC problem has not been resolved, a postponed subterm has not been elaborated, etc. |
| 124 | +
|
| 125 | + See `Term.SavedState.restore`. |
| 126 | +-/ |
| 127 | +def Info.updateContext? : Option ContextInfo → Info → Option ContextInfo |
| 128 | + | some ctx, ofTacticInfo i => some { ctx with mctx := i.mctxAfter } |
| 129 | + | ctx?, _ => ctx? |
| 130 | + |
| 131 | +def Info.stx : Info → Syntax |
| 132 | + | ofTacticInfo i => i.stx |
| 133 | + | ofTermInfo i => i.stx |
| 134 | + | ofPartialTermInfo i => i.stx |
| 135 | + | ofCommandInfo i => i.stx |
| 136 | + | ofMacroExpansionInfo i => i.stx |
| 137 | + | ofOptionInfo i => i.stx |
| 138 | + | ofErrorNameInfo i => i.stx |
| 139 | + | ofFieldInfo i => i.stx |
| 140 | + | ofCompletionInfo i => i.stx |
| 141 | + | ofCustomInfo i => i.stx |
| 142 | + | ofUserWidgetInfo i => i.stx |
| 143 | + | ofFVarAliasInfo _ => .missing |
| 144 | + | ofFieldRedeclInfo i => i.stx |
| 145 | + | ofDelabTermInfo i => i.stx |
| 146 | + | ofChoiceInfo i => i.stx |
| 147 | + | ofDocInfo i => i.stx |
| 148 | + | ofDocElabInfo i => i.stx |
| 149 | + |
| 150 | +private def CompletionInfo.setStx (stx : Syntax) : CompletionInfo → CompletionInfo |
| 151 | + | dot i e? => .dot { i with stx } e? |
| 152 | + | id _ n dd lctx e? => .id stx n dd lctx e? |
| 153 | + | dotId _ n lctx e? => .dotId stx n lctx e? |
| 154 | + | fieldId _ n? lctx s => .fieldId stx n? lctx s |
| 155 | + | namespaceId _ => .namespaceId stx |
| 156 | + | option _ => .option stx |
| 157 | + | errorName _ pid => .errorName stx pid |
| 158 | + | endSection _ n? dd ns => .endSection stx n? dd ns |
| 159 | + | tactic _ => .tactic stx |
| 160 | + |
| 161 | +private def Info.setStx (stx : Syntax) : Info → Info |
| 162 | + | ofTacticInfo i => ofTacticInfo { i with stx } |
| 163 | + | ofTermInfo i => ofTermInfo { i with stx } |
| 164 | + | ofPartialTermInfo i => ofPartialTermInfo { i with stx } |
| 165 | + | ofCommandInfo i => ofCommandInfo { i with stx } |
| 166 | + | ofMacroExpansionInfo i => ofMacroExpansionInfo { i with stx } |
| 167 | + | ofOptionInfo i => ofOptionInfo { i with stx } |
| 168 | + | ofErrorNameInfo i => ofErrorNameInfo { i with stx } |
| 169 | + | ofFieldInfo i => ofFieldInfo { i with stx } |
| 170 | + | ofCompletionInfo i => ofCompletionInfo (i.setStx stx) |
| 171 | + | ofCustomInfo i => ofCustomInfo { i with stx } |
| 172 | + | ofUserWidgetInfo i => ofUserWidgetInfo { i with stx } |
| 173 | + | ofFVarAliasInfo i => ofFVarAliasInfo i |
| 174 | + | ofFieldRedeclInfo i => ofFieldRedeclInfo { i with stx } |
| 175 | + | ofDelabTermInfo i => ofDelabTermInfo { i with stx } |
| 176 | + | ofChoiceInfo i => ofChoiceInfo { i with stx } |
| 177 | + | ofDocInfo i => ofDocInfo { i with stx } |
| 178 | + | ofDocElabInfo i => ofDocElabInfo { i with stx } |
| 179 | + |
| 180 | +/-- |
| 181 | +Adds the given trailing substring to all adjacent syntax in the info tree if any, otherwise returns |
| 182 | +`none`. |
| 183 | +-/ |
| 184 | +partial def InfoTree.addTrailing? (trailing : Substring.Raw) : Elab.InfoTree → Option Elab.InfoTree |
| 185 | + | .context i t => t.addTrailing? trailing |>.map (.context i) |
| 186 | + | .node info children => Id.run do |
| 187 | + let stx? := info.stx.addTrailing? trailing |
| 188 | + -- NOTE: we need to visit the children even if `stx` was not actually changed as info trees are |
| 189 | + -- not necessarily properly nested regarding syntax ranges! |
| 190 | + let childTrailing := (stx?.getD info.stx).getTrailing?.getD trailing |
| 191 | + let mut changed := false |
| 192 | + let mut newChildren := children |
| 193 | + for c in children, i in 0...* do |
| 194 | + if let some c' := c.addTrailing? childTrailing then |
| 195 | + changed := true |
| 196 | + newChildren := newChildren.set i c' |
| 197 | + if stx?.isNone && !changed then |
| 198 | + return none |
| 199 | + let info := match stx? with |
| 200 | + | some stx => info.setStx stx |
| 201 | + | none => info |
| 202 | + return some (.node info newChildren) |
| 203 | + | .hole _ => none |
| 204 | + |
| 205 | +/-- Adds the given trailing substring to all adjacent syntax in the info tree. -/ |
| 206 | +def InfoTree.addTrailing (trailing : Substring.Raw) (t : Elab.InfoTree) : Elab.InfoTree := |
| 207 | + t.addTrailing? trailing |>.getD t |
0 commit comments