Lean.ResolveName

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 = []

source

def Lean.ResolveName.resolveNamespaceUsingScope (env : Lean.Environment) (n : Lean.Name) :

Lean.Name → Option Lean.Name

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"

source

def Lean.ResolveName.resolveNamespaceUsingOpenDecls (env : Lean.Environment) (n : Lean.Name) :

List Lean.OpenDecl → Option Lean.Name

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

source

def Lean.ResolveName.resolveNamespace? (env : Lean.Environment) (ns : Lean.Name) (openDecls : List Lean.OpenDecl) (id : Lean.Name) :

Option 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

source

class Lean.MonadResolveName (m : Type → Type) :

Type

getCurrNamespace : m Lean.Name
getOpenDecls : m (List Lean.OpenDecl)

Instances

source

instance Lean.instMonadResolveName (m : Type → Type) (n : Type → Type) [inst : MonadLift m n] [inst : Lean.MonadResolveName m] :

Lean.MonadResolveName n

Equations

Lean.instMonadResolveName m n = { getCurrNamespace := liftM Lean.getCurrNamespace, getOpenDecls := liftM Lean.getOpenDecls }

source

def Lean.resolveGlobalName {m : Type → Type} [inst : Monad m] [inst : Lean.MonadResolveName m] [inst : Lean.MonadEnv m] (id : Lean.Name) :

m (List (Lean.Name × List String))

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)

source

def Lean.resolveNamespace {m : Type → Type} [inst : Monad m] [inst : Lean.MonadResolveName m] [inst : Lean.MonadEnv m] [inst : Lean.MonadError m] (id : Lean.Name) :

m 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 "'"))

source

def Lean.resolveGlobalConstCore {m : Type → Type} [inst : Monad m] [inst : Lean.MonadResolveName m] [inst : Lean.MonadEnv m] [inst : Lean.MonadError m] (n : Lean.Name) :

m (List 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

source

def Lean.resolveGlobalConstNoOverloadCore {m : Type → Type} [inst : Monad m] [inst : Lean.MonadResolveName m] [inst : Lean.MonadEnv m] [inst : Lean.MonadError m] (n : Lean.Name) :

m 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 ""))

source

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"))

source

def Lean.resolveGlobalConstNoOverload {m : Type → Type} [inst : Monad m] [inst : Lean.MonadResolveName m] [inst : Lean.MonadEnv m] [inst : Lean.MonadError m] (id : Lean.Syntax) :

m Lean.Name

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 ""))