Lean.Environment

Lean.instInhabitedEnvironmentHeader = { default := { trustLevel := default, quotInit := default, mainModule := default, imports := default, regions := default, moduleNames := default, moduleData := default } }

source

structure Lean.Environment :

Type

const2ModIdx : Std.HashMap Lean.Name Lean.ModuleIdx
constants : Lean.ConstMap
extensions : Array Lean.EnvExtensionState
header : Lean.EnvironmentHeader

source

instance Lean.instInhabitedEnvironment :

Inhabited Lean.Environment

Equations

Lean.instInhabitedEnvironment = { default := { const2ModIdx := default, constants := default, extensions := default, header := default } }

source

def Lean.Environment.addAux (env : Lean.Environment) (cinfo : Lean.ConstantInfo) :

Lean.Environment

Equations

Lean.Environment.addAux env cinfo = { const2ModIdx := env.const2ModIdx, constants := Lean.SMap.insert env.constants (Lean.ConstantInfo.name cinfo) cinfo, extensions := env.extensions, header := env.header }

source

def Lean.Environment.find? (env : Lean.Environment) (n : Lean.Name) :

Option Lean.ConstantInfo

Equations

Lean.Environment.find? env n = Lean.SMap.find?' env.constants n

source

def Lean.Environment.contains (env : Lean.Environment) (n : Lean.Name) :

Bool

Equations

Lean.Environment.contains env n = Lean.SMap.contains env.constants n

source

def Lean.Environment.imports (env : Lean.Environment) :

Array Lean.Import

Equations

Lean.Environment.imports env = env.header.imports

source

def Lean.Environment.allImportedModuleNames (env : Lean.Environment) :

Array Lean.Name

Equations

Lean.Environment.allImportedModuleNames env = env.header.moduleNames

source

def Lean.Environment.setMainModule (env : Lean.Environment) (m : Lean.Name) :

Lean.Environment

Equations

Lean.Environment.setMainModule env m = { const2ModIdx := env.const2ModIdx, constants := env.constants, extensions := env.extensions, header := let src := env.header; { trustLevel := src.trustLevel, quotInit := src.quotInit, mainModule := m, imports := src.imports, regions := src.regions, moduleNames := src.moduleNames, moduleData := src.moduleData } }

source

def Lean.Environment.mainModule (env : Lean.Environment) :

Lean.Name

Equations

Lean.Environment.mainModule env = env.header.mainModule

source

def Lean.Environment.getModuleIdxFor? (env : Lean.Environment) (declName : Lean.Name) :

Option Lean.ModuleIdx

Equations

Lean.Environment.getModuleIdxFor? env declName = Std.HashMap.find? env.const2ModIdx declName

source

def Lean.Environment.isConstructor (env : Lean.Environment) (declName : Lean.Name) :

Bool

Equations

Lean.Environment.isConstructor env declName = match Lean.Environment.find? env declName with | some (Lean.ConstantInfo.ctorInfo x) => true | x => false

source

def Lean.Environment.getModuleIdx? (env : Lean.Environment) (moduleName : Lean.Name) :

Option Lean.ModuleIdx

Equations

Lean.Environment.getModuleIdx? env moduleName = Array.findIdx? env.header.moduleNames fun a => a == moduleName

source

inductive Lean.KernelException :

Type

unknownConstant: Lean.Environment → Lean.Name → Lean.KernelException
alreadyDeclared: Lean.Environment → Lean.Name → Lean.KernelException
declTypeMismatch: Lean.Environment → Lean.Declaration → Lean.Expr → Lean.KernelException
declHasMVars: Lean.Environment → Lean.Name → Lean.Expr → Lean.KernelException
declHasFVars: Lean.Environment → Lean.Name → Lean.Expr → Lean.KernelException
funExpected: Lean.Environment → Lean.LocalContext → Lean.Expr → Lean.KernelException
typeExpected: Lean.Environment → Lean.LocalContext → Lean.Expr → Lean.KernelException
letTypeMismatch: Lean.Environment → Lean.LocalContext → Lean.Name → Lean.Expr → Lean.Expr → Lean.KernelException
exprTypeMismatch: Lean.Environment → Lean.LocalContext → Lean.Expr → Lean.Expr → Lean.KernelException
appTypeMismatch: Lean.Environment → Lean.LocalContext → Lean.Expr → Lean.Expr → Lean.Expr → Lean.KernelException
invalidProj: Lean.Environment → Lean.LocalContext → Lean.Expr → Lean.KernelException
other: String → Lean.KernelException

source

@[extern lean_add_decl]

constant Lean.Environment.addDecl (env : Lean.Environment) (decl : Lean.Declaration) :

Except Lean.KernelException Lean.Environment

source

@[extern lean_compile_decl]

constant Lean.Environment.compileDecl (env : Lean.Environment) (opt : Lean.Options) (decl : Lean.Declaration) :

Except Lean.KernelException Lean.Environment

source

def Lean.Environment.addAndCompile (env : Lean.Environment) (opt : Lean.Options) (decl : Lean.Declaration) :

Except Lean.KernelException Lean.Environment

Equations

Lean.Environment.addAndCompile env opt decl = do let env ← Lean.Environment.addDecl env decl Lean.Environment.compileDecl env opt decl

source

structure Lean.EnvExtensionInterface :

Type 1

ext : Type → Type
inhabitedExt : {σ : Type} → Inhabited σ → Inhabited (ext σ)
registerExt : {σ : Type} → IO σ → IO (ext σ)
setState : {σ : Type} → ext σ → Lean.Environment → σ → Lean.Environment
modifyState : {σ : Type} → ext σ → Lean.Environment → (σ → σ) → Lean.Environment
getState : {σ : Type} → [inst : Inhabited σ] → ext σ → Lean.Environment → σ
mkInitialExtStates : IO (Array Lean.EnvExtensionState)
ensureExtensionsSize : Lean.Environment → IO Lean.Environment

source

instance Lean.instInhabitedEnvExtensionInterface :

Inhabited Lean.EnvExtensionInterface

Equations

Lean.instInhabitedEnvExtensionInterface = { default := { ext := id, inhabitedExt := fun {σ} => id, registerExt := fun {σ} mk => mk, setState := fun {σ} x env x => env, modifyState := fun {σ} x env x => env, getState := fun {σ} [Inhabited σ] ext x => ext, mkInitialExtStates := pure #[], ensureExtensionsSize := fun env => pure env } }

source

structure Lean.EnvExtensionInterfaceUnsafe.Ext (σ : Type) :

Type

idx : Nat
mkInitial : IO σ

source

instance Lean.EnvExtensionInterfaceUnsafe.instInhabitedExt :

{a : Type} → Inhabited (Lean.EnvExtensionInterfaceUnsafe.Ext a)

Equations

Lean.EnvExtensionInterfaceUnsafe.instInhabitedExt = { default := { idx := default, mkInitial := default } }

source

def Lean.EnvExtensionInterfaceUnsafe.ensureExtensionsArraySize (env : Lean.Environment) :

IO Lean.Environment

Equations

Lean.EnvExtensionInterfaceUnsafe.ensureExtensionsArraySize env = (fun loop => loop (Array.size env.extensions) env) Lean.EnvExtensionInterfaceUnsafe.ensureExtensionsArraySize.loop

source

partial def Lean.EnvExtensionInterfaceUnsafe.ensureExtensionsArraySize.loop (i : Nat) (env : Lean.Environment) :

IO Lean.Environment

source

unsafe def Lean.EnvExtensionInterfaceUnsafe.setState {σ : Type} (ext : Lean.EnvExtensionInterfaceUnsafe.Ext σ) (env : Lean.Environment) (s : σ) :

Lean.Environment

Equations

Lean.EnvExtensionInterfaceUnsafe.setState ext env s = if h : ext.idx < Array.size env.extensions then { const2ModIdx := env.const2ModIdx, constants := env.constants, extensions := Array.set env.extensions { val := ext.idx, isLt := h } (unsafeCast s), header := env.header } else panicWithPosWithDecl "Lean.Environment" "Lean.EnvExtensionInterfaceUnsafe.setState" 219 4 Lean.EnvExtensionInterfaceUnsafe.invalidExtMsg

source

@[inline]

unsafe def Lean.EnvExtensionInterfaceUnsafe.modifyState {σ : Type} (ext : Lean.EnvExtensionInterfaceUnsafe.Ext σ) (env : Lean.Environment) (f : σ → σ) :

Lean.Environment

Equations

Lean.EnvExtensionInterfaceUnsafe.modifyState ext env f = if ext.idx < Array.size env.extensions then { const2ModIdx := env.const2ModIdx, constants := env.constants, extensions := Array.modify env.extensions ext.idx fun s => let s := unsafeCast s; let s := f s; unsafeCast s, header := env.header } else panicWithPosWithDecl "Lean.Environment" "Lean.EnvExtensionInterfaceUnsafe.modifyState" 229 4 Lean.EnvExtensionInterfaceUnsafe.invalidExtMsg

source

unsafe def Lean.EnvExtensionInterfaceUnsafe.getState {σ : Type} [inst : Inhabited σ] (ext : Lean.EnvExtensionInterfaceUnsafe.Ext σ) (env : Lean.Environment) :

σ

Equations

Lean.EnvExtensionInterfaceUnsafe.getState ext env = if h : ext.idx < Array.size env.extensions then let s := Array.get env.extensions { val := ext.idx, isLt := h }; unsafeCast s else panicWithPosWithDecl "Lean.Environment" "Lean.EnvExtensionInterfaceUnsafe.getState" 236 4 Lean.EnvExtensionInterfaceUnsafe.invalidExtMsg

source

unsafe def Lean.EnvExtensionInterfaceUnsafe.registerExt {σ : Type} (mkInitial : IO σ) :

IO (Lean.EnvExtensionInterfaceUnsafe.Ext σ)

Equations

Lean.EnvExtensionInterfaceUnsafe.registerExt mkInitial = do let a ← Lean.initializing let _do_jp : PUnit → IO (Lean.EnvExtensionInterfaceUnsafe.Ext σ) := fun y => do let exts ← ST.Ref.get Lean.EnvExtensionInterfaceUnsafe.envExtensionsRef let idx : Nat := Array.size exts let ext : Lean.EnvExtensionInterfaceUnsafe.Ext σ := { idx := idx, mkInitial := mkInitial } ST.Ref.modify Lean.EnvExtensionInterfaceUnsafe.envExtensionsRef fun exts => Array.push exts (unsafeCast ext) pure ext if a = true then do let y ← pure PUnit.unit _do_jp y else do let y ← throw (IO.userError "failed to register environment, extensions can only be registered during initialization") _do_jp y

source

def Lean.EnvExtensionInterfaceUnsafe.mkInitialExtStates :

IO (Array Lean.EnvExtensionState)

Equations

Lean.EnvExtensionInterfaceUnsafe.mkInitialExtStates = do let exts ← ST.Ref.get Lean.EnvExtensionInterfaceUnsafe.envExtensionsRef Array.mapM (fun ext => ext.mkInitial) exts

source

unsafe def Lean.EnvExtensionInterfaceUnsafe.imp :

Lean.EnvExtensionInterface

Equations

Lean.EnvExtensionInterfaceUnsafe.imp = { ext := Lean.EnvExtensionInterfaceUnsafe.Ext, inhabitedExt := fun {σ} x => { default := default }, registerExt := fun {σ} => Lean.EnvExtensionInterfaceUnsafe.registerExt, setState := fun {σ} => Lean.EnvExtensionInterfaceUnsafe.setState, modifyState := fun {σ} => Lean.EnvExtensionInterfaceUnsafe.modifyState, getState := fun {σ} [Inhabited σ] => Lean.EnvExtensionInterfaceUnsafe.getState, mkInitialExtStates := Lean.EnvExtensionInterfaceUnsafe.mkInitialExtStates, ensureExtensionsSize := Lean.EnvExtensionInterfaceUnsafe.ensureExtensionsArraySize }

source

@[implementedBy Lean.EnvExtensionInterfaceUnsafe.imp]

constant Lean.EnvExtensionInterfaceImp :

Lean.EnvExtensionInterface

source

noncomputable def Lean.EnvExtension (σ : Type) :

Type

Equations

Lean.EnvExtension σ = Lean.EnvExtensionInterface.ext Lean.EnvExtensionInterfaceImp σ

source

instance Lean.EnvExtension.instInhabitedEnvExtension {σ : Type} [s : Inhabited σ] :

Inhabited (Lean.EnvExtension σ)

Equations

Lean.EnvExtension.instInhabitedEnvExtension = Lean.EnvExtensionInterface.inhabitedExt Lean.EnvExtensionInterfaceImp s

source

def Lean.EnvExtension.setState {σ : Type} (ext : Lean.EnvExtension σ) (env : Lean.Environment) (s : σ) :

Lean.Environment

Equations

Lean.EnvExtension.setState ext env s = Lean.EnvExtensionInterface.setState Lean.EnvExtensionInterfaceImp ext env s

source

def Lean.EnvExtension.modifyState {σ : Type} (ext : Lean.EnvExtension σ) (env : Lean.Environment) (f : σ → σ) :

Lean.Environment

Equations

Lean.EnvExtension.modifyState ext env f = Lean.EnvExtensionInterface.modifyState Lean.EnvExtensionInterfaceImp ext env f

source

def Lean.EnvExtension.getState {σ : Type} [inst : Inhabited σ] (ext : Lean.EnvExtension σ) (env : Lean.Environment) :

σ

Equations

Lean.EnvExtension.getState ext env = Lean.EnvExtensionInterface.getState Lean.EnvExtensionInterfaceImp ext env

source

def Lean.registerEnvExtension {σ : Type} (mkInitial : IO σ) :

IO (Lean.EnvExtension σ)

Equations

Lean.registerEnvExtension mkInitial = Lean.EnvExtensionInterface.registerExt Lean.EnvExtensionInterfaceImp mkInitial

source

def Lean.mkEmptyEnvironment (trustLevel : optParam UInt32 0) :

IO Lean.Environment

Equations

Lean.mkEmptyEnvironment trustLevel = do let initializing ← liftM IO.initializing let _do_jp : PUnit → IO Lean.Environment := fun y => do let exts ← Lean.mkInitialExtensionStates pure { const2ModIdx := ∅, constants := { stage₁ := true, map₁ := ∅, map₂ := { root := Std.PersistentHashMap.Node.entries Std.PersistentHashMap.mkEmptyEntriesArray, size := 0 } }, extensions := exts, header := { trustLevel := trustLevel, quotInit := false, mainModule := default, imports := #[], regions := #[], moduleNames := #[], moduleData := #[] } } if initializing = true then do let y ← throw (IO.userError "environment objects cannot be created during initialization") _do_jp y else do let y ← pure PUnit.unit _do_jp y

source

structure Lean.PersistentEnvExtensionState (α : Type) (σ : Type) :

Type

importedEntries : Array (Array α)
state : σ

source

structure Lean.ImportM.Context :

Type

env : Lean.Environment
opts : Lean.Options

source

@[inline]

abbrev Lean.ImportM (α : Type) :

Type

Equations

Lean.ImportM = ReaderT Lean.ImportM.Context IO

source

structure Lean.PersistentEnvExtension (α : Type) (β : Type) (σ : Type) :

Type

toEnvExtension : Lean.EnvExtension (Lean.PersistentEnvExtensionState α σ)
name : Lean.Name
addImportedFn : Array (Array α) → Lean.ImportM σ
addEntryFn : σ → β → σ
exportEntriesFn : σ → Array α
statsFn : σ → Lean.Format

source

instance Lean.instInhabitedPersistentEnvExtensionState {α : Type} {σ : Type} [inst : Inhabited σ] :

Inhabited (Lean.PersistentEnvExtensionState α σ)

Equations

Lean.instInhabitedPersistentEnvExtensionState = { default := { importedEntries := #[], state := default } }

source

instance Lean.instInhabitedPersistentEnvExtension {α : Type} {β : Type} {σ : Type} [inst : Inhabited σ] :

Inhabited (Lean.PersistentEnvExtension α β σ)

Equations

Lean.instInhabitedPersistentEnvExtension = { default := { toEnvExtension := default, name := default, addImportedFn := fun x => default, addEntryFn := fun s x => s, exportEntriesFn := fun x => #[], statsFn := fun x => Lean.Format.nil } }

source

def Lean.PersistentEnvExtension.getModuleEntries {α : Type} {β : Type} {σ : Type} [inst : Inhabited σ] (ext : Lean.PersistentEnvExtension α β σ) (env : Lean.Environment) (m : Lean.ModuleIdx) :

Array α

Equations

Lean.PersistentEnvExtension.getModuleEntries ext env m = Array.get! (Lean.EnvExtension.getState ext.toEnvExtension env).importedEntries m

source

def Lean.PersistentEnvExtension.addEntry {α : Type} {β : Type} {σ : Type} (ext : Lean.PersistentEnvExtension α β σ) (env : Lean.Environment) (b : β) :

Lean.Environment

Equations

Lean.PersistentEnvExtension.addEntry ext env b = Lean.EnvExtension.modifyState ext.toEnvExtension env fun s => let state := Lean.PersistentEnvExtension.addEntryFn ext s.state b; { importedEntries := s.importedEntries, state := state }

source

def Lean.PersistentEnvExtension.getState {α : Type} {β : Type} {σ : Type} [inst : Inhabited σ] (ext : Lean.PersistentEnvExtension α β σ) (env : Lean.Environment) :

σ

Equations

Lean.PersistentEnvExtension.getState ext env = (Lean.EnvExtension.getState ext.toEnvExtension env).state

source

def Lean.PersistentEnvExtension.setState {α : Type} {β : Type} {σ : Type} (ext : Lean.PersistentEnvExtension α β σ) (env : Lean.Environment) (s : σ) :

Lean.Environment

Equations

Lean.PersistentEnvExtension.setState ext env s = Lean.EnvExtension.modifyState ext.toEnvExtension env fun ps => { importedEntries := ps.importedEntries, state := s }

source

def Lean.PersistentEnvExtension.modifyState {α : Type} {β : Type} {σ : Type} (ext : Lean.PersistentEnvExtension α β σ) (env : Lean.Environment) (f : σ → σ) :

Lean.Environment

Equations

Lean.PersistentEnvExtension.modifyState ext env f = Lean.EnvExtension.modifyState ext.toEnvExtension env fun ps => { importedEntries := ps.importedEntries, state := f ps.state }

source

constant Lean.persistentEnvExtensionsRef :

IO.Ref (Array (Lean.PersistentEnvExtension Lean.EnvExtensionEntry Lean.EnvExtensionEntry Lean.EnvExtensionState))

source

structure Lean.PersistentEnvExtensionDescr (α : Type) (β : Type) (σ : Type) :

Type

name : Lean.Name
mkInitial : IO σ
addImportedFn : Array (Array α) → Lean.ImportM σ
addEntryFn : σ → β → σ
exportEntriesFn : σ → Array α
statsFn : σ → Lean.Format

source

unsafe def Lean.registerPersistentEnvExtensionUnsafe {α : Type} {β : Type} {σ : Type} [inst : Inhabited σ] (descr : Lean.PersistentEnvExtensionDescr α β σ) :

IO (Lean.PersistentEnvExtension α β σ)

Equations

Lean.registerPersistentEnvExtensionUnsafe descr = do let pExts ← ST.Ref.get Lean.persistentEnvExtensionsRef let _do_jp : PUnit → IO (Lean.PersistentEnvExtension α β σ) := fun y => do let ext ← Lean.registerEnvExtension do let initial ← descr.mkInitial let s : Lean.PersistentEnvExtensionState α σ := { importedEntries := #[], state := initial } pure s let pExt : Lean.PersistentEnvExtension α β σ := { toEnvExtension := ext, name := descr.name, addImportedFn := descr.addImportedFn, addEntryFn := descr.addEntryFn, exportEntriesFn := descr.exportEntriesFn, statsFn := descr.statsFn } ST.Ref.modify Lean.persistentEnvExtensionsRef fun pExts => Array.push pExts (unsafeCast pExt) pure pExt if Array.any pExts (fun ext => ext.name == descr.name) 0 (Array.size pExts) = true then do let y ← throw (IO.userError (toString "invalid environment extension, '" ++ toString descr.name ++ toString "' has already been used")) _do_jp y else do let y ← pure PUnit.unit _do_jp y

source

@[implementedBy Lean.registerPersistentEnvExtensionUnsafe]

constant Lean.registerPersistentEnvExtension {α : Type} {β : Type} {σ : Type} [inst : Inhabited σ] (descr : Lean.PersistentEnvExtensionDescr α β σ) :

IO (Lean.PersistentEnvExtension α β σ)

source

noncomputable def Lean.SimplePersistentEnvExtension (α : Type) (σ : Type) :

Type

Equations

Lean.SimplePersistentEnvExtension α σ = Lean.PersistentEnvExtension α α (List α × σ)

source

@[specialize]

def Lean.mkStateFromImportedEntries {α : Type} {σ : Type} (addEntryFn : σ → α → σ) (initState : σ) (as : Array (Array α)) :

σ

Equations

Lean.mkStateFromImportedEntries addEntryFn initState as = Array.foldl (fun r es => Array.foldl (fun r e => addEntryFn r e) r es 0 (Array.size es)) initState as 0 (Array.size as)

source

structure Lean.SimplePersistentEnvExtensionDescr (α : Type) (σ : Type) :

Type

name : Lean.Name
addEntryFn : σ → α → σ
addImportedFn : Array (Array α) → σ
toArrayFn : List α → Array α

source

def Lean.registerSimplePersistentEnvExtension {α : Type} {σ : Type} [inst : Inhabited σ] (descr : Lean.SimplePersistentEnvExtensionDescr α σ) :

IO (Lean.SimplePersistentEnvExtension α σ)

Equations

Lean.registerSimplePersistentEnvExtension descr = Lean.registerPersistentEnvExtension { name := descr.name, mkInitial := pure ([], Lean.SimplePersistentEnvExtensionDescr.addImportedFn descr #[]), addImportedFn := fun as => pure ([], Lean.SimplePersistentEnvExtensionDescr.addImportedFn descr as), addEntryFn := fun s e => match s with | (entries, s) => (e :: entries, Lean.SimplePersistentEnvExtensionDescr.addEntryFn descr s e), exportEntriesFn := fun s => Lean.SimplePersistentEnvExtensionDescr.toArrayFn descr (List.reverse s.fst), statsFn := fun s => Lean.format "number of local entries: " ++ Lean.format (List.length s.fst) }

source

instance Lean.SimplePersistentEnvExtension.instInhabitedSimplePersistentEnvExtension {α : Type} {σ : Type} [inst : Inhabited σ] :

Inhabited (Lean.SimplePersistentEnvExtension α σ)

Equations

Lean.SimplePersistentEnvExtension.instInhabitedSimplePersistentEnvExtension = inferInstanceAs (Inhabited (Lean.PersistentEnvExtension α α (List α × σ)))

source

def Lean.SimplePersistentEnvExtension.getEntries {α : Type} {σ : Type} [inst : Inhabited σ] (ext : Lean.SimplePersistentEnvExtension α σ) (env : Lean.Environment) :

List α

Equations

Lean.SimplePersistentEnvExtension.getEntries ext env = (Lean.PersistentEnvExtension.getState ext env).fst

source

def Lean.SimplePersistentEnvExtension.getState {α : Type} {σ : Type} [inst : Inhabited σ] (ext : Lean.SimplePersistentEnvExtension α σ) (env : Lean.Environment) :

σ

Equations

Lean.SimplePersistentEnvExtension.getState ext env = (Lean.PersistentEnvExtension.getState ext env).snd

source

def Lean.SimplePersistentEnvExtension.setState {α : Type} {σ : Type} (ext : Lean.SimplePersistentEnvExtension α σ) (env : Lean.Environment) (s : σ) :

Lean.Environment

Equations

Lean.SimplePersistentEnvExtension.setState ext env s = Lean.PersistentEnvExtension.modifyState ext env fun x => match x with | (entries, x) => (entries, s)

source

def Lean.SimplePersistentEnvExtension.modifyState {α : Type} {σ : Type} (ext : Lean.SimplePersistentEnvExtension α σ) (env : Lean.Environment) (f : σ → σ) :

Lean.Environment

Equations

Lean.SimplePersistentEnvExtension.modifyState ext env f = Lean.PersistentEnvExtension.modifyState ext env fun x => match x with | (entries, s) => (entries, f s)

source

noncomputable def Lean.TagDeclarationExtension :

Type

Equations

Lean.TagDeclarationExtension = Lean.SimplePersistentEnvExtension Lean.Name Lean.NameSet

source

def Lean.mkTagDeclarationExtension (name : Lean.Name) :

IO Lean.TagDeclarationExtension

Equations

Lean.mkTagDeclarationExtension name = Lean.registerSimplePersistentEnvExtension { name := name, addEntryFn := fun s n => Lean.NameSet.insert s n, addImportedFn := fun as => ∅, toArrayFn := fun es => Array.qsort (List.toArray es) Lean.Name.quickLt 0 (Array.size (List.toArray es) - 1) }

source

instance Lean.TagDeclarationExtension.instInhabitedTagDeclarationExtension :

Inhabited Lean.TagDeclarationExtension

Equations

Lean.TagDeclarationExtension.instInhabitedTagDeclarationExtension = inferInstanceAs (Inhabited (Lean.SimplePersistentEnvExtension Lean.Name Lean.NameSet))

source

def Lean.TagDeclarationExtension.tag (ext : Lean.TagDeclarationExtension) (env : Lean.Environment) (n : Lean.Name) :

Lean.Environment

Equations

Lean.TagDeclarationExtension.tag ext env n = Lean.PersistentEnvExtension.addEntry ext env n

source

def Lean.TagDeclarationExtension.isTagged (ext : Lean.TagDeclarationExtension) (env : Lean.Environment) (n : Lean.Name) :

Bool

Equations

Lean.TagDeclarationExtension.isTagged ext env n = match Lean.Environment.getModuleIdxFor? env n with | some modIdx => Array.binSearchContains (Lean.PersistentEnvExtension.getModuleEntries ext env modIdx) n Lean.Name.quickLt 0 (Array.size (Lean.PersistentEnvExtension.getModuleEntries ext env modIdx) - 1) | none => Lean.NameSet.contains (Lean.SimplePersistentEnvExtension.getState ext env) n

source

noncomputable def Lean.MapDeclarationExtension (α : Type) :

Type

Equations

Lean.MapDeclarationExtension α = Lean.SimplePersistentEnvExtension (Lean.Name × α) (Lean.NameMap α)

source

def Lean.mkMapDeclarationExtension {α : Type} [inst : Inhabited α] (name : Lean.Name) :

IO (Lean.MapDeclarationExtension α)

Equations

Lean.mkMapDeclarationExtension name = Lean.registerSimplePersistentEnvExtension { name := name, addEntryFn := fun s n => Lean.NameMap.insert s n.fst n.snd, addImportedFn := fun as => ∅, toArrayFn := fun es => Array.qsort (List.toArray es) (fun a b => Lean.Name.quickLt a.fst b.fst) 0 (Array.size (List.toArray es) - 1) }

source

instance Lean.MapDeclarationExtension.instInhabitedMapDeclarationExtension {α : Type} :

Inhabited (Lean.MapDeclarationExtension α)

Equations

Lean.MapDeclarationExtension.instInhabitedMapDeclarationExtension = inferInstanceAs (Inhabited (Lean.SimplePersistentEnvExtension (Lean.Name × α) (Lean.NameMap α)))

source

def Lean.MapDeclarationExtension.insert {α : Type} (ext : Lean.MapDeclarationExtension α) (env : Lean.Environment) (declName : Lean.Name) (val : α) :

Lean.Environment

Equations

Lean.MapDeclarationExtension.insert ext env declName val = Lean.PersistentEnvExtension.addEntry ext env (declName, val)

source

def Lean.MapDeclarationExtension.find? {α : Type} [inst : Inhabited α] (ext : Lean.MapDeclarationExtension α) (env : Lean.Environment) (declName : Lean.Name) :

Option α

Equations

Lean.MapDeclarationExtension.find? ext env declName = match Lean.Environment.getModuleIdxFor? env declName with | some modIdx => match Array.binSearch (Lean.PersistentEnvExtension.getModuleEntries ext env modIdx) (declName, default) (fun a b => Lean.Name.quickLt a.fst b.fst) 0 (Array.size (Lean.PersistentEnvExtension.getModuleEntries ext env modIdx) - 1) with | some e => some e.snd | none => none | none => Lean.NameMap.find? (Lean.SimplePersistentEnvExtension.getState ext env) declName

source

def Lean.MapDeclarationExtension.contains {α : Type} [inst : Inhabited α] (ext : Lean.MapDeclarationExtension α) (env : Lean.Environment) (declName : Lean.Name) :

Bool

Equations

Lean.MapDeclarationExtension.contains ext env declName = match Lean.Environment.getModuleIdxFor? env declName with | some modIdx => Array.binSearchContains (Lean.PersistentEnvExtension.getModuleEntries ext env modIdx) (declName, default) (fun a b => Lean.Name.quickLt a.fst b.fst) 0 (Array.size (Lean.PersistentEnvExtension.getModuleEntries ext env modIdx) - 1) | none => Lean.NameMap.contains (Lean.SimplePersistentEnvExtension.getState ext env) declName

source

@[extern lean_save_module_data]

constant Lean.saveModuleData (fname : System.FilePath) (mod : Lean.Name) (data : Lean.ModuleData) :

IO Unit

source

@[extern lean_read_module_data]

constant Lean.readModuleData (fname : System.FilePath) :

IO (Lean.ModuleData × Lean.CompactedRegion)

source

@[noinline]

unsafe def Lean.Environment.freeRegions (env : Lean.Environment) :

IO Unit

Equations

Lean.Environment.freeRegions env = Array.forM Lean.CompactedRegion.free env.header.regions 0 (Array.size env.header.regions)

source

def Lean.mkModuleData (env : Lean.Environment) :

IO Lean.ModuleData

Equations

Lean.mkModuleData env = do let pExts ← ST.Ref.get Lean.persistentEnvExtensionsRef let entries : Array (Lean.Name × Array Lean.EnvExtensionEntry) := Nat.fold (fun i result => let state := Lean.PersistentEnvExtension.getState (Array.get! pExts i) env; let exportEntriesFn := (Array.get! pExts i).exportEntriesFn; let extName := (Array.get! pExts i).name; Array.push result (extName, exportEntriesFn state)) (Array.size pExts) #[] pure { imports := env.header.imports, constants := Lean.SMap.foldStage2 (fun cs x c => Array.push cs c) #[] env.constants, entries := entries }

source

def Lean.writeModule (env : Lean.Environment) (fname : System.FilePath) :

IO Unit

Equations

Lean.writeModule env fname = do let a ← Lean.mkModuleData env Lean.saveModuleData fname (Lean.Environment.mainModule env) a

source

@[extern 2lean_update_env_attributes]

constant Lean.updateEnvAttributes :

Lean.Environment → IO Lean.Environment

source

@[extern 1lean_get_num_attributes]

constant Lean.getNumBuiltiAttributes :

IO Nat

source

structure Lean.ImportState :

Type

moduleNameSet : Lean.NameSet
moduleNames : Array Lean.Name
moduleData : Array Lean.ModuleData
regions : Array Lean.CompactedRegion

source

def Lean.importModules (imports : List Lean.Import) (opts : Lean.Options) (trustLevel : optParam UInt32 0) :

IO Lean.Environment

Equations

Lean.importModules imports opts trustLevel = (fun importMods => Lean.profileitIO "import" opts (Lean.withImporting do let discr ← StateRefT'.run (importMods imports) { moduleNameSet := ∅, moduleNames := #[], moduleData := #[], regions := #[] } let x : Unit × Lean.ImportState := discr match x with | (x, s) => let numConsts := 0; do let r ← let col := s.moduleData; forIn col numConsts fun mod r => let numConsts := r; let numConsts := numConsts + Array.size mod.constants; do pure PUnit.unit pure (ForInStep.yield numConsts) let x : Nat := r let numConsts : Nat := x let modIdx : Nat := 0 let const2ModIdx : Std.HashMap Lean.Name Lean.ModuleIdx := Std.mkHashMap numConsts let constantMap : Std.HashMap Lean.Name Lean.ConstantInfo := Std.mkHashMap numConsts let r ← let col := s.moduleData; forIn col { fst := constantMap, snd := { fst := modIdx, snd := const2ModIdx } } fun mod r => let constantMap := r.fst; let x := r.snd; let modIdx := x.fst; let const2ModIdx := x.snd; do let r ← let col := mod.constants; forIn col { fst := constantMap, snd := const2ModIdx } fun cinfo r => let constantMap := r.fst; let const2ModIdx := r.snd; let const2ModIdx := Std.HashMap.insert const2ModIdx (Lean.ConstantInfo.name cinfo) modIdx; match Std.HashMap.insert' constantMap (Lean.ConstantInfo.name cinfo) cinfo with | (constantMap', replaced) => let constantMap := constantMap'; if replaced = true then do throw (IO.userError (toString "import failed, environment already contains '" ++ toString (Lean.ConstantInfo.name cinfo) ++ toString "'")) pure (ForInStep.yield { fst := constantMap, snd := const2ModIdx }) else do pure PUnit.unit pure (ForInStep.yield { fst := constantMap, snd := const2ModIdx }) let x : MProd (Std.HashMap Lean.Name Lean.ConstantInfo) (Std.HashMap Lean.Name Lean.ModuleIdx) := r match x with | { fst := constantMap, snd := const2ModIdx } => let modIdx := modIdx + 1; do pure PUnit.unit pure (ForInStep.yield { fst := constantMap, snd := { fst := modIdx, snd := const2ModIdx } }) let x : MProd (Std.HashMap Lean.Name Lean.ConstantInfo) (MProd Nat (Std.HashMap Lean.Name Lean.ModuleIdx)) := r match x with | { fst := constantMap, snd := { fst := modIdx, snd := const2ModIdx } } => let constants := Lean.SMap.fromHashMap constantMap false; do let exts ← Lean.mkInitialExtensionStates let env : Lean.Environment := { const2ModIdx := const2ModIdx, constants := constants, extensions := exts, header := { trustLevel := trustLevel, quotInit := !List.isEmpty imports, mainModule := default, imports := List.toArray imports, regions := s.regions, moduleNames := s.moduleNames, moduleData := s.moduleData } } let env ← Lean.setImportedEntries env s.moduleData 0 let env ← Lean.finalizePersistentExtensions env s.moduleData opts pure env)) Lean.importModules.importMods

source

partial def Lean.importModules.importMods :

List Lean.Import → StateRefT' IO.RealWorld Lean.ImportState IO Unit

source

unsafe def Lean.withImportModules {α : Type} (imports : List Lean.Import) (opts : Lean.Options) (trustLevel : optParam UInt32 0) (x : Lean.Environment → IO α) :

IO α

Equations

Lean.withImportModules imports opts trustLevel x = do let env ← Lean.importModules imports opts trustLevel tryFinally (x env) (Lean.Environment.freeRegions env)

source

constant Lean.namespacesExt :

Lean.SimplePersistentEnvExtension Lean.Name Lean.NameSSet

source

def Lean.Environment.registerNamespace (env : Lean.Environment) (n : Lean.Name) :

Lean.Environment

Equations

Lean.Environment.registerNamespace env n = if Lean.NameSSet.contains (Lean.SimplePersistentEnvExtension.getState Lean.namespacesExt env) n = true then env else Lean.PersistentEnvExtension.addEntry Lean.namespacesExt env n

source

def Lean.Environment.isNamespace (env : Lean.Environment) (n : Lean.Name) :

Bool

Equations

Lean.Environment.isNamespace env n = Lean.NameSSet.contains (Lean.SimplePersistentEnvExtension.getState Lean.namespacesExt env) n

source

def Lean.Environment.getNamespaceSet (env : Lean.Environment) :

Lean.NameSSet

Equations

Lean.Environment.getNamespaceSet env = Lean.SimplePersistentEnvExtension.getState Lean.namespacesExt env

source

def Lean.Environment.add (env : Lean.Environment) (cinfo : Lean.ConstantInfo) :

Lean.Environment

Equations

Lean.Environment.add env cinfo = let env := Lean.Environment.registerNamePrefixes env (Lean.ConstantInfo.name cinfo); Lean.Environment.addAux env cinfo

source

def Lean.Environment.displayStats (env : Lean.Environment) :

IO Unit

Equations

Lean.Environment.displayStats env = do let pExtDescrs ← ST.Ref.get Lean.persistentEnvExtensionsRef IO.println ("direct imports: " ++ toString env.header.imports) IO.println ("number of imported modules: " ++ toString (Array.size env.header.regions)) IO.println ("number of memory-mapped modules: " ++ toString (Array.size (Array.filter (fun a => Lean.CompactedRegion.isMemoryMapped a) env.header.regions 0 (Array.size env.header.regions)))) IO.println ("number of consts: " ++ toString (Lean.SMap.size env.constants)) IO.println ("number of imported consts: " ++ toString (Lean.SMap.stageSizes env.constants).fst) IO.println ("number of local consts: " ++ toString (Lean.SMap.stageSizes env.constants).snd) IO.println ("number of buckets for imported consts: " ++ toString (Lean.SMap.numBuckets env.constants)) IO.println ("trust level: " ++ toString env.header.trustLevel) IO.println ("number of extensions: " ++ toString (Array.size env.extensions)) Array.forM (fun extDescr => do IO.println ("extension '" ++ toString extDescr.name ++ "'") let s : Lean.PersistentEnvExtensionState Lean.EnvExtensionEntry Lean.EnvExtensionState := Lean.EnvExtension.getState extDescr.toEnvExtension env let fmt : Lean.Format := Lean.PersistentEnvExtension.statsFn extDescr s.state let _do_jp : PUnit → IO Unit := fun y => IO.println (" number of imported entries: " ++ toString (Array.foldl (fun sum es => sum + Array.size es) 0 s.importedEntries 0 (Array.size s.importedEntries))) if Std.Format.isNil fmt = true then do let y ← pure PUnit.unit _do_jp y else do let y ← IO.println (" " ++ toString (Lean.Format.nest 2 (Lean.PersistentEnvExtension.statsFn extDescr s.state))) _do_jp y) pExtDescrs 0 (Array.size pExtDescrs)

source

@[extern lean_eval_const]

unsafe constant Lean.Environment.evalConst (α : Type u_1) (env : Lean.Environment) (opts : Lean.Options) (constName : Lean.Name) :

Except String α

source

unsafe def Lean.Environment.evalConstCheck (α : Type) (env : Lean.Environment) (opts : Lean.Options) (typeName : Lean.Name) (constName : Lean.Name) :

ExceptT String Id α

Equations

Lean.Environment.evalConstCheck α env opts typeName constName = match Lean.Environment.find? env constName with | none => throw ("unknown constant '" ++ toString constName ++ "'") | some info => match Lean.ConstantInfo.type info with | Lean.Expr.const c x x_1 => if (c != typeName) = true then Lean.Environment.throwUnexpectedType typeName constName else Lean.Environment.evalConst α env opts constName | x => Lean.Environment.throwUnexpectedType typeName constName

source

def Lean.Environment.hasUnsafe (env : Lean.Environment) (e : Lean.Expr) :

Bool

Equations

Lean.Environment.hasUnsafe env e = let c? := Lean.Expr.find? (fun e => match e with | Lean.Expr.const c x x_1 => match Lean.Environment.find? env c with | some cinfo => Lean.ConstantInfo.isUnsafe cinfo | none => false | x => false) e; Option.isSome c?

source

@[extern lean_kernel_is_def_eq]

constant Lean.Kernel.isDefEq (env : Lean.Environment) (lctx : Lean.LocalContext) (a : Lean.Expr) (b : Lean.Expr) :

Bool

source

@[extern lean_kernel_whnf]

constant Lean.Kernel.whnf (env : Lean.Environment) (lctx : Lean.LocalContext) (a : Lean.Expr) :

Lean.Expr

source

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

Type

getEnv : m Lean.Environment
modifyEnv : (Lean.Environment → Lean.Environment) → m Unit

Instances

source

instance Lean.instMonadEnv (m : Type → Type) (n : Type → Type) [inst : MonadLift m n] [inst : Lean.MonadEnv m] :

Lean.MonadEnv n

Equations

Lean.instMonadEnv m n = { getEnv := liftM Lean.getEnv, modifyEnv := fun f => liftM (Lean.modifyEnv f) }

source

def Lean.mkBaseNameFor (env : Lean.Environment) (declName : Lean.Name) (elemSuffix : Lean.Name) (suffix : Lean.Name) :

Lean.Name

Equations

Lean.mkBaseNameFor env declName elemSuffix suffix = (fun go => if (!Lean.Environment.contains env (declName ++ elemSuffix)) = true then declName else go 1) (Lean.mkBaseNameFor.go env declName elemSuffix suffix)

source

partial def Lean.mkBaseNameFor.go (env : Lean.Environment) (declName : Lean.Name) (elemSuffix : Lean.Name) (suffix : Lean.Name) (idx : Nat) :

Lean.Name