130 lines
5.9 KiB
Text
130 lines
5.9 KiB
Text
import init.lean init.lean.parser.syntax
|
||
|
||
namespace Lean
|
||
/-- An extension of the State held by an `environment` object. The new State
|
||
holds objects of Type `entryTy`, which optionally are persisted to the
|
||
.olean file and collected when loading imports. Objects can be retrieved
|
||
using an appropriate `stateTy` data structure, which is computed on-demand. -/
|
||
constant EnvironmentExtension (entryTy stateTy : Type) : Type := Unit
|
||
|
||
namespace EnvironmentExtension
|
||
variable {entryTy stateTy : Type}
|
||
/-- Register a new environment extension. The Result should usually be bound to
|
||
a top-Level definition, after which it can be used to access and modify the
|
||
extension State. -/
|
||
@[extern "lean_environment_ext_register"] constant register
|
||
/- A unique String used for identifying persisted data of this extension. If
|
||
this key has already been used, the Lean process will halt with an error.
|
||
If the key is `none`, data of this extension will not be persisted, i.e. is
|
||
local to the current file. -/
|
||
(key : Option String)
|
||
/- initial cache value -/
|
||
(emptyState : stateTy)
|
||
/- Add an entry to the cache. `init` is `True` while building the initial
|
||
cache from the loaded imports, in which case the input cache may assumed to
|
||
be unshared and amenable to destructive updates. -/
|
||
(addEntry : Π (init : Bool), environment → stateTy → entryTy → stateTy) :
|
||
IO (EnvironmentExtension entryTy stateTy) := default _
|
||
|
||
variable {entryTy' stateTy' : Type}
|
||
|
||
/- Register a dependency between two environment extensions.
|
||
That is, whenever an entry `e` is added to `fromExt`,
|
||
Lean also adds an entry `convertEntry e` to `toExt`. -/
|
||
@[extern "lean_environment_ext_register_dep"] constant registerDep
|
||
(fromExt : EnvironmentExtension entryTy stateTy)
|
||
(toExt : EnvironmentExtension entryTy' stateTy')
|
||
(convertEntry : entryTy → entryTy')
|
||
: IO Unit := default _
|
||
|
||
@[extern "lean_environment_ext_add_entry"] constant addEntry (ext : EnvironmentExtension entryTy stateTy) (entry : entryTy) : environment → environment := id
|
||
|
||
--constant getModuleEntries (ext : EnvironmentExtension entryTy stateTy) (mod : ModID) : IO (Array entryTy)
|
||
|
||
/-- Retrieve the State of an environment extension. -/
|
||
@[extern "lean_environment_ext_get_state"] constant getState [Inhabited stateTy] : EnvironmentExtension entryTy stateTy → environment → stateTy := default _
|
||
end EnvironmentExtension
|
||
|
||
structure ScopedEnvironmentExtension.Scope (entryTy stateTy : Type) :=
|
||
(state : stateTy)
|
||
(localEntries : List entryTy)
|
||
|
||
def ScopedEnvironmentExtension (entryTy stateTy : Type) :=
|
||
EnvironmentExtension (Bool × entryTy) (List (ScopedEnvironmentExtension.Scope entryTy stateTy))
|
||
|
||
namespace ScopedEnvironmentExtension
|
||
structure Info :=
|
||
(pushScope popScope : environment → environment)
|
||
|
||
def scopedExtsRef.init : IO (IO.Ref (List Info)) := IO.mkRef []
|
||
@[init scopedExtsRef.init] private constant scopedExtsRef : IO.Ref (List Info) := default _
|
||
def scopedExts : IO (List Info) := scopedExtsRef.get
|
||
|
||
variable {entryTy stateTy : Type}
|
||
|
||
def register (key : Option String) (emptyState : stateTy)
|
||
(addEntry : Π (init : Bool), environment → stateTy → entryTy → stateTy)
|
||
: IO (ScopedEnvironmentExtension entryTy stateTy) :=
|
||
EnvironmentExtension.register key [{state := emptyState, localEntries := []}] $
|
||
λ init env st ⟨persistent, e⟩,
|
||
if persistent then st.map (λ scope, {scope with state := addEntry init env scope.state e})
|
||
else match st with
|
||
| ⟨st, es⟩::scopes := ⟨st, e::es⟩::scopes
|
||
| [] := []
|
||
|
||
def addEntry (ext : ScopedEnvironmentExtension entryTy stateTy) (persistent : Bool) (entry : entryTy) (env : environment) : environment :=
|
||
EnvironmentExtension.addEntry ext (persistent, entry) env
|
||
|
||
def pushScope (env : environment) : IO environment := do
|
||
exts ← scopedExts,
|
||
pure $ exts.foldr Info.pushScope env
|
||
|
||
def popScope (env : environment) : IO environment := do
|
||
exts ← scopedExts,
|
||
pure $ exts.foldr Info.popScope env
|
||
end ScopedEnvironmentExtension
|
||
|
||
/-- A datum as used by `AttributeExtension`. -/
|
||
structure AttributeEntry :=
|
||
(decl : Name)
|
||
(args : Parser.Syntax)
|
||
|
||
/-- The Result of registering an attribute in the global State. -/
|
||
structure AttributeExtension (stateTy : Type) :=
|
||
-- global and local attribute entries as well as "active" scoped entries
|
||
(activeExt : ScopedEnvironmentExtension AttributeEntry stateTy)
|
||
-- all scoped entries
|
||
(scopedExt : EnvironmentExtension AttributeEntry (List AttributeEntry))
|
||
|
||
/-- `cacheTy`-oblivious attribute data available to the Elaborator. -/
|
||
structure AttributeInfo :=
|
||
(attr : Name)
|
||
(addActiveEntry (persistent : Bool) : AttributeEntry → environment → environment)
|
||
(scopedExt : EnvironmentExtension AttributeEntry (List AttributeEntry))
|
||
|
||
namespace AttributeInfo
|
||
def addScopedEntry (attr : AttributeInfo) : AttributeEntry → environment → environment := attr.scopedExt.addEntry
|
||
def activateScopedEntries (attr : AttributeInfo) (declOpen : Name → Bool) (env : environment) : environment :=
|
||
((attr.scopedExt.getState env).filter (λ e : AttributeEntry, declOpen e.decl)).foldr (attr.addActiveEntry true) env
|
||
end AttributeInfo
|
||
|
||
def attributesRef.init : IO (IO.Ref (List AttributeInfo)) := IO.mkRef []
|
||
@[init attributesRef.init] private constant attributesRef : IO.Ref (List AttributeInfo) := default _
|
||
/-- The List of all attributes registered by `attributeExt.register`. -/
|
||
def attributes : IO (List AttributeInfo) := attributesRef.get
|
||
|
||
namespace AttributeExtension
|
||
variable {stateTy : Type}
|
||
|
||
def register (attr : Name) (emptyState : stateTy)
|
||
(addEntry : Π (init : Bool), environment → stateTy → AttributeEntry → stateTy)
|
||
: IO (AttributeExtension stateTy) := do
|
||
ext ← AttributeExtension.mk
|
||
<$> ScopedEnvironmentExtension.register (toString attr) emptyState addEntry
|
||
<*> EnvironmentExtension.register (some $ toString $ attr ++ `scoped) [] (λ _ _ entries e, e::entries),
|
||
attributesRef.modify $ λ attrs, {attr := attr,
|
||
addActiveEntry := ext.activeExt.addEntry,
|
||
scopedExt := ext.scopedExt}::attrs,
|
||
pure ext
|
||
end AttributeExtension
|
||
end Lean
|