@[inline]
Equations
- Lean.addAliasEntry s e = match Lean.SMap.find? s e.fst with | none => Lean.SMap.insert s e.fst [e.snd] | some es => if List.elem e.snd es = true then s else Lean.SMap.insert s e.fst (e.snd :: es)
Equations
- Lean.addAlias env a e = Lean.PersistentEnvExtension.addEntry Lean.aliasExtension env (a, e)
Equations
Equations
- Lean.getAliases env a = match Lean.SMap.find? (Lean.SimplePersistentEnvExtension.getState Lean.aliasExtension env) a with | none => [] | some es => es
Equations
- Lean.getRevAliases env e = Lean.SMap.fold (fun as a es => if List.contains es e = true then a :: as else as) [] (Lean.SimplePersistentEnvExtension.getState Lean.aliasExtension env)
def
Lean.ResolveName.resolveGlobalName
(env : Lean.Environment)
(ns : Lean.Name)
(openDecls : List Lean.OpenDecl)
(id : Lean.Name)
:
Equations
- Lean.ResolveName.resolveGlobalName env ns openDecls id = let extractionResult := Lean.extractMacroScopes id; (fun loop => loop extractionResult.name []) (Lean.ResolveName.resolveGlobalName.loop env ns openDecls extractionResult)
def
Lean.ResolveName.resolveGlobalName.loop
(env : Lean.Environment)
(ns : Lean.Name)
(openDecls : List Lean.OpenDecl)
(extractionResult : Lean.MacroScopesView)
(id : Lean.Name)
(projs : List String)
:
Equations
- Lean.ResolveName.resolveGlobalName.loop env ns openDecls extractionResult (Lean.Name.str p s x) projs = let id := Lean.MacroScopesView.review { name := Lean.Name.str p s x, imported := extractionResult.imported, mainModule := extractionResult.mainModule, scopes := extractionResult.scopes }; match Lean.ResolveName.resolveUsingNamespace env id ns with | resolvedIds@h:(x :: x_1) => List.map (fun id => (id, projs)) (List.eraseDups resolvedIds) | [] => match Lean.ResolveName.resolveExact env id with | some newId => [(newId, projs)] | none => let resolvedIds := if Lean.Environment.contains env id = true then [id] else []; let idPrv := Lean.mkPrivateName env id; let resolvedIds := if Lean.Environment.contains env idPrv = true then [idPrv] ++ resolvedIds else resolvedIds; let resolvedIds := Lean.ResolveName.resolveOpenDecls env id openDecls resolvedIds; let resolvedIds := Lean.getAliases env id ++ resolvedIds; match resolvedIds with | x :: x_1 => List.map (fun id => (id, projs)) (List.eraseDups resolvedIds) | [] => Lean.ResolveName.resolveGlobalName.loop env ns openDecls extractionResult p (s :: projs)
- Lean.ResolveName.resolveGlobalName.loop env ns openDecls extractionResult id projs = []
Equations
- Lean.ResolveName.resolveNamespaceUsingScope env n Lean.Name.anonymous = if Lean.Environment.isNamespace env n = true then some n else none
- Lean.ResolveName.resolveNamespaceUsingScope env n (Lean.Name.str p x_1 x_2) = if Lean.Environment.isNamespace env (Lean.Name.str p x_1 x_2 ++ n) = true then some (Lean.Name.str p x_1 x_2 ++ n) else Lean.ResolveName.resolveNamespaceUsingScope env n p
- Lean.ResolveName.resolveNamespaceUsingScope env n x = panicWithPosWithDecl "Lean.ResolveName" "Lean.ResolveName.resolveNamespaceUsingScope" 137 27 "unreachable code has been reached"
Equations
- Lean.ResolveName.resolveNamespaceUsingOpenDecls env n [] = none
- Lean.ResolveName.resolveNamespaceUsingOpenDecls env n (Lean.OpenDecl.simple ns [] :: ds) = if Lean.Environment.isNamespace env (ns ++ n) = true then some (ns ++ n) else Lean.ResolveName.resolveNamespaceUsingOpenDecls env n ds
- Lean.ResolveName.resolveNamespaceUsingOpenDecls env n (x_1 :: ds) = Lean.ResolveName.resolveNamespaceUsingOpenDecls env n ds
def
Lean.ResolveName.resolveNamespace?
(env : Lean.Environment)
(ns : Lean.Name)
(openDecls : List Lean.OpenDecl)
(id : Lean.Name)
:
Equations
- Lean.ResolveName.resolveNamespace? env ns openDecls id = match Lean.ResolveName.resolveNamespaceUsingScope env id ns with | some n => some n | none => match Lean.ResolveName.resolveNamespaceUsingOpenDecls env id openDecls with | some n => some n | none => none
- getCurrNamespace : m Lean.Name
- getOpenDecls : m (List Lean.OpenDecl)
instance
Lean.instMonadResolveName
(m : Type → Type)
(n : Type → Type)
[inst : MonadLift m n]
[inst : Lean.MonadResolveName m]
:
Equations
- Lean.instMonadResolveName m n = { getCurrNamespace := liftM Lean.getCurrNamespace, getOpenDecls := liftM Lean.getOpenDecls }
def
Lean.resolveGlobalName
{m : Type → Type}
[inst : Monad m]
[inst : Lean.MonadResolveName m]
[inst : Lean.MonadEnv m]
(id : Lean.Name)
:
Equations
- Lean.resolveGlobalName id = do let a ← Lean.getEnv let a_1 ← Lean.getCurrNamespace let a_2 ← Lean.getOpenDecls pure (Lean.ResolveName.resolveGlobalName a a_1 a_2 id)
def
Lean.resolveNamespace
{m : Type → Type}
[inst : Monad m]
[inst : Lean.MonadResolveName m]
[inst : Lean.MonadEnv m]
[inst : Lean.MonadError m]
(id : Lean.Name)
:
Equations
- Lean.resolveNamespace id = do let a ← Lean.getEnv let a_1 ← Lean.getCurrNamespace let a_2 ← Lean.getOpenDecls match Lean.ResolveName.resolveNamespace? a a_1 a_2 id with | some ns => pure ns | none => Lean.throwError (Function.comp Lean.MessageData.ofFormat Lean.format (toString "unknown namespace '" ++ toString id ++ toString "'"))
def
Lean.resolveGlobalConstCore
{m : Type → Type}
[inst : Monad m]
[inst : Lean.MonadResolveName m]
[inst : Lean.MonadEnv m]
[inst : Lean.MonadError m]
(n : Lean.Name)
:
Equations
- Lean.resolveGlobalConstCore n = do let cs ← Lean.resolveGlobalName n let cs : List (Lean.Name × List String) := List.filter (fun x => match x with | (x, fieldList) => List.isEmpty fieldList) cs let _do_jp : PUnit → m (List Lean.Name) := fun y => pure (List.map (fun a => a.fst) cs) if List.isEmpty cs = true then do let y ← Lean.throwUnknownConstant n _do_jp y else do let y ← pure PUnit.unit _do_jp y
def
Lean.resolveGlobalConstNoOverloadCore
{m : Type → Type}
[inst : Monad m]
[inst : Lean.MonadResolveName m]
[inst : Lean.MonadEnv m]
[inst : Lean.MonadError m]
(n : Lean.Name)
:
Equations
- Lean.resolveGlobalConstNoOverloadCore n = do let cs ← Lean.resolveGlobalConstCore n match cs with | [c] => pure c | x => Lean.throwError (Function.comp Lean.MessageData.ofFormat Lean.format (toString "ambiguous identifier '" ++ toString (Lean.mkConst n) ++ toString "', possible interpretations: " ++ toString (List.map (fun n => Lean.mkConst n) cs) ++ toString ""))
def
Lean.resolveGlobalConst
{m : Type → Type}
[inst : Monad m]
[inst : Lean.MonadResolveName m]
[inst : Lean.MonadEnv m]
[inst : Lean.MonadError m]
:
Lean.Syntax → m (List Lean.Name)
Equations
- Lean.resolveGlobalConst x = match x with | stx@h:(Lean.Syntax.ident x x_1 n pre) => let pre := List.filterMap (fun x => match x with | (n, fields) => if List.isEmpty fields = true then some n else none) pre; if List.isEmpty pre = true then Lean.withRef stx (Lean.resolveGlobalConstCore n) else pure pre | stx => Lean.throwErrorAt stx (Function.comp Lean.MessageData.ofFormat Lean.format (toString "expected identifier"))
def
Lean.resolveGlobalConstNoOverload
{m : Type → Type}
[inst : Monad m]
[inst : Lean.MonadResolveName m]
[inst : Lean.MonadEnv m]
[inst : Lean.MonadError m]
(id : Lean.Syntax)
:
Equations
- Lean.resolveGlobalConstNoOverload id = do let cs ← Lean.resolveGlobalConst id match cs with | [c] => pure c | x => Lean.throwErrorAt id (Function.comp Lean.MessageData.ofFormat Lean.format (toString "ambiguous identifier '" ++ toString id ++ toString "', possible interpretations: " ++ toString (List.map (fun n => Lean.mkConst n) cs) ++ toString ""))