| /- | |
| Copyright (c) 2021 Microsoft Corporation. All rights reserved. | |
| Released under Apache 2.0 license as described in the file LICENSE. | |
| Authors: Leonardo de Moura | |
| -/ | |
| prelude | |
| import Lean.Data.DeclarationRange | |
| import Lean.MonadEnv | |
| /-! | |
| # Environment extension for declaration ranges | |
| -/ | |
| namespace Lean | |
| builtin_initialize builtinDeclRanges : IO.Ref (NameMap DeclarationRanges) ← IO.mkRef {} | |
| builtin_initialize declRangeExt : MapDeclarationExtension DeclarationRanges ← mkMapDeclarationExtension | |
| def addBuiltinDeclarationRanges (declName : Name) (declRanges : DeclarationRanges) : IO Unit := | |
| builtinDeclRanges.modify (·.insert declName declRanges) | |
| def addDeclarationRanges [Monad m] [MonadEnv m] (declName : Name) (declRanges : DeclarationRanges) : m Unit := do | |
| unless declRangeExt.contains (← getEnv) declName do | |
| modifyEnv fun env => declRangeExt.insert env declName declRanges | |
| def findDeclarationRangesCore? [Monad m] [MonadEnv m] (declName : Name) : m (Option DeclarationRanges) := | |
| return declRangeExt.find? (← getEnv) declName | |
| def findDeclarationRanges? [Monad m] [MonadEnv m] [MonadLiftT BaseIO m] (declName : Name) : m (Option DeclarationRanges) := do | |
| let env ← getEnv | |
| let ranges ← if isAuxRecursor env declName || isNoConfusion env declName || (← isRec declName) then | |
| findDeclarationRangesCore? declName.getPrefix | |
| else | |
| findDeclarationRangesCore? declName | |
| match ranges with | |
| | none => return (← builtinDeclRanges.get (m := BaseIO)).find? declName | |
| | some _ => return ranges | |
| end Lean |