- global: {α : Type} → α → Lean.ScopedEnvExtension.Entry α
- scoped: {α : Type} → Lean.Name → α → Lean.ScopedEnvExtension.Entry α
- state : σ
- activeScopes : Lean.NameSet
- map : Lean.SMap Lean.Name (Std.PArray β)
instance
Lean.ScopedEnvExtension.instInhabitedScopedEntries
:
{a : Type} → Inhabited (Lean.ScopedEnvExtension.ScopedEntries a)
Equations
- Lean.ScopedEnvExtension.instInhabitedScopedEntries = { default := { map := default } }
- stateStack : List (Lean.ScopedEnvExtension.State σ)
- scopedEntries : Lean.ScopedEnvExtension.ScopedEntries β
- newEntries : List (Lean.ScopedEnvExtension.Entry α)
instance
Lean.ScopedEnvExtension.instInhabitedStateStack
:
{a a_1 a_2 : Type} → Inhabited (Lean.ScopedEnvExtension.StateStack a a_1 a_2)
Equations
- Lean.ScopedEnvExtension.instInhabitedStateStack = { default := { stateStack := default, scopedEntries := default, newEntries := default } }
- name : Lean.Name
- mkInitial : IO σ
- ofOLeanEntry : σ → α → Lean.ImportM β
- toOLeanEntry : β → α
- addEntry : σ → β → σ
- finalizeImport : σ → σ
instance
Lean.ScopedEnvExtension.instInhabitedDescr
{α : Type}
{β : Type}
{σ : Type}
[inst : Inhabited α]
:
Equations
- Lean.ScopedEnvExtension.instInhabitedDescr = { default := { name := default, mkInitial := default, ofOLeanEntry := default, toOLeanEntry := default, addEntry := fun s x => s, finalizeImport := id } }
def
Lean.ScopedEnvExtension.mkInitial
{α : Type}
{β : Type}
{σ : Type}
(descr : Lean.ScopedEnvExtension.Descr α β σ)
:
IO (Lean.ScopedEnvExtension.StateStack α β σ)
Equations
- Lean.ScopedEnvExtension.mkInitial descr = do let a ← descr.mkInitial pure { stateStack := [{ state := a, activeScopes := ∅ }], scopedEntries := { map := { stage₁ := true, map₁ := ∅, map₂ := { root := Std.PersistentHashMap.Node.entries Std.PersistentHashMap.mkEmptyEntriesArray, size := 0 } } }, newEntries := [] }
def
Lean.ScopedEnvExtension.ScopedEntries.insert
{β : Type}
(scopedEntries : Lean.ScopedEnvExtension.ScopedEntries β)
(ns : Lean.Name)
(b : β)
:
Equations
- Lean.ScopedEnvExtension.ScopedEntries.insert scopedEntries ns b = match Lean.SMap.find? scopedEntries.map ns with | none => { map := Lean.SMap.insert scopedEntries.map ns (Std.PersistentArray.push { root := Std.PersistentArrayNode.node (Array.mkEmpty (USize.toNat Std.PersistentArray.branching)), tail := Array.mkEmpty (USize.toNat Std.PersistentArray.branching), size := 0, shift := Std.PersistentArray.initShift, tailOff := 0 } b) } | some bs => { map := Lean.SMap.insert scopedEntries.map ns (Std.PersistentArray.push bs b) }
def
Lean.ScopedEnvExtension.addImportedFn
{α : Type}
{β : Type}
{σ : Type}
(descr : Lean.ScopedEnvExtension.Descr α β σ)
(as : Array (Array (Lean.ScopedEnvExtension.Entry α)))
:
Equations
- Lean.ScopedEnvExtension.addImportedFn descr as = do let s ← liftM descr.mkInitial let scopedEntries : Lean.ScopedEnvExtension.ScopedEntries β := { map := { stage₁ := true, map₁ := ∅, map₂ := { root := Std.PersistentHashMap.Node.entries Std.PersistentHashMap.mkEmptyEntriesArray, size := 0 } } } let r ← forIn as { fst := s, snd := scopedEntries } fun a r => let s := r.fst; let scopedEntries := r.snd; do let r ← forIn a { fst := s, snd := scopedEntries } fun e r => let s := r.fst; let scopedEntries := r.snd; match e with | Lean.ScopedEnvExtension.Entry.global a => do let b ← Lean.ScopedEnvExtension.Descr.ofOLeanEntry descr s a let s : σ := Lean.ScopedEnvExtension.Descr.addEntry descr s b pure PUnit.unit pure (ForInStep.yield { fst := s, snd := scopedEntries }) | Lean.ScopedEnvExtension.Entry.scoped ns a => do let b ← Lean.ScopedEnvExtension.Descr.ofOLeanEntry descr s a let scopedEntries : Lean.ScopedEnvExtension.ScopedEntries β := Lean.ScopedEnvExtension.ScopedEntries.insert scopedEntries ns b pure PUnit.unit pure (ForInStep.yield { fst := s, snd := scopedEntries }) let x : MProd σ (Lean.ScopedEnvExtension.ScopedEntries β) := r match x with | { fst := s, snd := scopedEntries } => do pure PUnit.unit pure (ForInStep.yield { fst := s, snd := scopedEntries }) let x : MProd σ (Lean.ScopedEnvExtension.ScopedEntries β) := r match x with | { fst := s, snd := scopedEntries } => let s := Lean.ScopedEnvExtension.Descr.finalizeImport descr s; pure { stateStack := [{ state := s, activeScopes := ∅ }], scopedEntries := scopedEntries, newEntries := [] }
def
Lean.ScopedEnvExtension.addEntryFn
{α : Type}
{β : Type}
{σ : Type}
(descr : Lean.ScopedEnvExtension.Descr α β σ)
(s : Lean.ScopedEnvExtension.StateStack α β σ)
(e : Lean.ScopedEnvExtension.Entry β)
:
Equations
- Lean.ScopedEnvExtension.addEntryFn descr s e = match s with | { stateStack := stateStack, scopedEntries := scopedEntries, newEntries := newEntries } => match e with | Lean.ScopedEnvExtension.Entry.global b => { stateStack := List.map (fun s => { state := Lean.ScopedEnvExtension.Descr.addEntry descr s.state b, activeScopes := s.activeScopes }) stateStack, scopedEntries := scopedEntries, newEntries := Lean.ScopedEnvExtension.Entry.global (Lean.ScopedEnvExtension.Descr.toOLeanEntry descr b) :: newEntries } | Lean.ScopedEnvExtension.Entry.scoped ns b => { stateStack := List.map (fun s => if Lean.NameSet.contains s.activeScopes ns = true then { state := Lean.ScopedEnvExtension.Descr.addEntry descr s.state b, activeScopes := s.activeScopes } else s) stateStack, scopedEntries := Lean.ScopedEnvExtension.ScopedEntries.insert scopedEntries ns b, newEntries := Lean.ScopedEnvExtension.Entry.scoped ns (Lean.ScopedEnvExtension.Descr.toOLeanEntry descr b) :: newEntries }
def
Lean.ScopedEnvExtension.exportEntriesFn
{α : Type}
{β : Type}
{σ : Type}
(s : Lean.ScopedEnvExtension.StateStack α β σ)
:
Equations
- Lean.ScopedEnvExtension.exportEntriesFn s = Array.reverse (List.toArray s.newEntries)
- descr : Lean.ScopedEnvExtension.Descr α β σ
- ext : Lean.PersistentEnvExtension (Lean.ScopedEnvExtension.Entry α) (Lean.ScopedEnvExtension.Entry β) (Lean.ScopedEnvExtension.StateStack α β σ)
instance
Lean.instInhabitedScopedEnvExtension
:
{a : Type} → [inst : Inhabited a] → {a_1 a_2 : Type} → Inhabited (Lean.ScopedEnvExtension a a_1 a_2)
Equations
- Lean.instInhabitedScopedEnvExtension = { default := { descr := default, ext := default } }
unsafe def
Lean.registerScopedEnvExtensionUnsafe
{α : Type}
{β : Type}
{σ : Type}
(descr : Lean.ScopedEnvExtension.Descr α β σ)
:
IO (Lean.ScopedEnvExtension α β σ)
Equations
- Lean.registerScopedEnvExtensionUnsafe descr = do let ext ← Lean.registerPersistentEnvExtension { name := descr.name, mkInitial := Lean.ScopedEnvExtension.mkInitial descr, addImportedFn := Lean.ScopedEnvExtension.addImportedFn descr, addEntryFn := Lean.ScopedEnvExtension.addEntryFn descr, exportEntriesFn := Lean.ScopedEnvExtension.exportEntriesFn, statsFn := fun s => Lean.format "number of local entries: " ++ Lean.format (List.length s.newEntries) } let ext : Lean.ScopedEnvExtension α β σ := { descr := descr, ext := ext } ST.Ref.modify Lean.scopedEnvExtensionsRef fun exts => Array.push exts (unsafeCast ext) pure ext
@[implementedBy Lean.registerScopedEnvExtensionUnsafe]
constant
Lean.registerScopedEnvExtension
{α : Type}
{β : Type}
{σ : Type}
(descr : Lean.ScopedEnvExtension.Descr α β σ)
:
IO (Lean.ScopedEnvExtension α β σ)
def
Lean.ScopedEnvExtension.pushScope
{α : Type}
{β : Type}
{σ : Type}
(ext : Lean.ScopedEnvExtension α β σ)
(env : Lean.Environment)
:
Equations
- Lean.ScopedEnvExtension.pushScope ext env = let s := Lean.PersistentEnvExtension.getState ext.ext env; match s.stateStack with | [] => env | state :: stack => Lean.PersistentEnvExtension.setState ext.ext env { stateStack := state :: state :: stack, scopedEntries := s.scopedEntries, newEntries := s.newEntries }
def
Lean.ScopedEnvExtension.popScope
{α : Type}
{β : Type}
{σ : Type}
(ext : Lean.ScopedEnvExtension α β σ)
(env : Lean.Environment)
:
Equations
- Lean.ScopedEnvExtension.popScope ext env = let s := Lean.PersistentEnvExtension.getState ext.ext env; match s.stateStack with | state₁ :: state₂ :: stack => Lean.PersistentEnvExtension.setState ext.ext env { stateStack := state₂ :: stack, scopedEntries := s.scopedEntries, newEntries := s.newEntries } | x => env
def
Lean.ScopedEnvExtension.addEntry
{α : Type}
{β : Type}
{σ : Type}
(ext : Lean.ScopedEnvExtension α β σ)
(env : Lean.Environment)
(b : β)
:
Equations
- Lean.ScopedEnvExtension.addEntry ext env b = Lean.PersistentEnvExtension.addEntry ext.ext env (Lean.ScopedEnvExtension.Entry.global b)
def
Lean.ScopedEnvExtension.addScopedEntry
{α : Type}
{β : Type}
{σ : Type}
(ext : Lean.ScopedEnvExtension α β σ)
(env : Lean.Environment)
(namespaceName : Lean.Name)
(b : β)
:
Equations
- Lean.ScopedEnvExtension.addScopedEntry ext env namespaceName b = Lean.PersistentEnvExtension.addEntry ext.ext env (Lean.ScopedEnvExtension.Entry.scoped namespaceName b)
def
Lean.ScopedEnvExtension.addLocalEntry
{α : Type}
{β : Type}
{σ : Type}
(ext : Lean.ScopedEnvExtension α β σ)
(env : Lean.Environment)
(b : β)
:
Equations
- Lean.ScopedEnvExtension.addLocalEntry ext env b = let s := Lean.PersistentEnvExtension.getState ext.ext env; match s.stateStack with | [] => env | top :: states => let top := { state := Lean.ScopedEnvExtension.Descr.addEntry ext.descr top.state b, activeScopes := top.activeScopes }; Lean.PersistentEnvExtension.setState ext.ext env { stateStack := top :: states, scopedEntries := s.scopedEntries, newEntries := s.newEntries }
def
Lean.ScopedEnvExtension.add
{m : Type → Type}
{α : Type}
{β : Type}
{σ : Type}
[inst : Monad m]
[inst : Lean.MonadResolveName m]
[inst : Lean.MonadEnv m]
(ext : Lean.ScopedEnvExtension α β σ)
(b : β)
(kind : optParam Lean.AttributeKind Lean.AttributeKind.global)
:
m Unit
Equations
- Lean.ScopedEnvExtension.add ext b kind = match kind with | Lean.AttributeKind.global => Lean.modifyEnv fun a => Lean.ScopedEnvExtension.addEntry ext a b | Lean.AttributeKind.local => Lean.modifyEnv fun a => Lean.ScopedEnvExtension.addLocalEntry ext a b | Lean.AttributeKind.scoped => do let a ← Lean.getCurrNamespace Lean.modifyEnv fun a_1 => Lean.ScopedEnvExtension.addScopedEntry ext a_1 a b
def
Lean.ScopedEnvExtension.getState
{σ : Type}
{α : Type}
{β : Type}
[inst : Inhabited σ]
(ext : Lean.ScopedEnvExtension α β σ)
(env : Lean.Environment)
:
σ
Equations
- Lean.ScopedEnvExtension.getState ext env = match (Lean.PersistentEnvExtension.getState ext.ext env).stateStack with | top :: x => top.state | x => panicWithPosWithDecl "Lean.ScopedEnvExtension" "Lean.ScopedEnvExtension.getState" 157 16 "unreachable code has been reached"
def
Lean.ScopedEnvExtension.activateScoped
{α : Type}
{β : Type}
{σ : Type}
(ext : Lean.ScopedEnvExtension α β σ)
(env : Lean.Environment)
(namespaceName : Lean.Name)
:
Equations
- Lean.ScopedEnvExtension.activateScoped ext env namespaceName = let s := Lean.PersistentEnvExtension.getState ext.ext env; match s.stateStack with | top :: stack => if Lean.NameSet.contains top.activeScopes namespaceName = true then env else let activeScopes := Lean.NameSet.insert top.activeScopes namespaceName; let top := match Lean.SMap.find? s.scopedEntries.map namespaceName with | none => { state := top.state, activeScopes := activeScopes } | some bs => Id.run (let state := top.state; do let r ← forIn bs state fun b r => let state := r; let state := Lean.ScopedEnvExtension.Descr.addEntry ext.descr state b; do pure PUnit.unit pure (ForInStep.yield state) let x : σ := r let state : σ := x { state := state, activeScopes := activeScopes }); Lean.PersistentEnvExtension.setState ext.ext env { stateStack := top :: stack, scopedEntries := s.scopedEntries, newEntries := s.newEntries } | x => env
def
Lean.ScopedEnvExtension.modifyState
{α : Type}
{β : Type}
{σ : Type}
(ext : Lean.ScopedEnvExtension α β σ)
(env : Lean.Environment)
(f : σ → σ)
:
Equations
- Lean.ScopedEnvExtension.modifyState ext env f = let s := Lean.PersistentEnvExtension.getState ext.ext env; match s.stateStack with | top :: stack => Lean.PersistentEnvExtension.setState ext.ext env { stateStack := { state := f top.state, activeScopes := top.activeScopes } :: stack, scopedEntries := s.scopedEntries, newEntries := s.newEntries } | x => env
def
Lean.pushScope
{m : Type → Type}
[inst : Monad m]
[inst : Lean.MonadEnv m]
[inst : MonadLiftT (ST IO.RealWorld) m]
:
m Unit
Equations
- Lean.pushScope = do let a ← ST.Ref.get Lean.scopedEnvExtensionsRef let r ← let col := a; forIn col PUnit.unit fun ext r => do Lean.modifyEnv (Lean.ScopedEnvExtension.pushScope ext) pure (ForInStep.yield PUnit.unit) let x : PUnit := r pure PUnit.unit
def
Lean.popScope
{m : Type → Type}
[inst : Monad m]
[inst : Lean.MonadEnv m]
[inst : MonadLiftT (ST IO.RealWorld) m]
:
m Unit
Equations
- Lean.popScope = do let a ← ST.Ref.get Lean.scopedEnvExtensionsRef let r ← let col := a; forIn col PUnit.unit fun ext r => do Lean.modifyEnv (Lean.ScopedEnvExtension.popScope ext) pure (ForInStep.yield PUnit.unit) let x : PUnit := r pure PUnit.unit
def
Lean.activateScoped
{m : Type → Type}
[inst : Monad m]
[inst : Lean.MonadEnv m]
[inst : MonadLiftT (ST IO.RealWorld) m]
(namespaceName : Lean.Name)
:
m Unit
Equations
- Lean.activateScoped namespaceName = do let a ← ST.Ref.get Lean.scopedEnvExtensionsRef let r ← let col := a; forIn col PUnit.unit fun ext r => do Lean.modifyEnv fun a => Lean.ScopedEnvExtension.activateScoped ext a namespaceName pure (ForInStep.yield PUnit.unit) let x : PUnit := r pure PUnit.unit
@[inline]
Equations
- name : Lean.Name
- addEntry : σ → α → σ
- initial : σ
- finalizeImport : σ → σ
def
Lean.registerSimpleScopedEnvExtension
{α : Type}
{σ : Type}
(descr : Lean.SimpleScopedEnvExtension.Descr α σ)
:
Equations
- Lean.registerSimpleScopedEnvExtension descr = Lean.registerScopedEnvExtension { name := descr.name, mkInitial := pure descr.initial, ofOLeanEntry := fun s a => pure a, toOLeanEntry := id, addEntry := descr.addEntry, finalizeImport := descr.finalizeImport }