-
Notifications
You must be signed in to change notification settings - Fork 11
/
Extension.lean
51 lines (41 loc) · 2.02 KB
/
Extension.lean
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
/-
Copyright (c) 2022 Mac Malone. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Mac Malone
-/
import Lean.Environment
open Lean
namespace Alloy
/-- Unsafe implementation of `findOrRegisterPersistentExtension`. -/
unsafe def unsafeFindOrRegisterPersistentExtension {α β σ : Type} [Inhabited σ]
(name : Name) (register : Name → IO (PersistentEnvExtension α β σ)) : IO (PersistentEnvExtension α β σ) := do
let pExts ← persistentEnvExtensionsRef.get
match pExts.find? (·.name == name) with
| some ext => unsafeCast ext
| none => register name
/--
Find the already registered persistent extension with the given name
or register one using the provided function.
We need this because otherwise persistent extensions will encounter a clash
between their precompiled (via `precompileModules`) version loaded as a shared
library (via `--load-dynlib`) and their interpreted version imported via olean.
-/
@[implemented_by unsafeFindOrRegisterPersistentExtension]
opaque findOrRegisterPersistentExtension {α β σ : Type} [Inhabited σ]
(name : Name) (register : Name → IO (PersistentEnvExtension α β σ)) : IO (PersistentEnvExtension α β σ)
/-- Persistent environment extension for storing a single serializable value per module. -/
def ModuleEnvExtension (σ : Type) := PersistentEnvExtension σ σ σ
def registerModuleEnvExtension [Inhabited σ] (mkInitial : IO σ) (name : Name) : IO (ModuleEnvExtension σ) :=
registerPersistentEnvExtension {
name := name
mkInitial := pure default
addImportedFn := fun _ _ => mkInitial
addEntryFn := fun s _ => s
exportEntriesFn := fun s => #[s]
}
namespace ModuleEnvExtension
instance [Inhabited σ] : Inhabited (ModuleEnvExtension σ) :=
inferInstanceAs (Inhabited (PersistentEnvExtension ..))
def find? [Inhabited σ] (ext : ModuleEnvExtension σ) (env : Environment) (mod : Name) : Option σ :=
env.getModuleIdx? mod >>= fun idx => (ext.getModuleEntries env idx)[0]?
end ModuleEnvExtension