max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

chore: seal EnvExtensionState and EnvExtensionEntry

Browse source
This commit is contained in:
Leonardo de Moura 2020-09-21 11:48:57 -07:00
parent c9e902034d
commit 1f9f12975c
1 changed files with 13 additions and 14 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

27
src/Lean/Environment.lean
View file

@ -11,10 +11,10 @@ import Lean.Util.Path
import Lean.Util.FindExpr
namespace Lean
/- Opaque environment extension state. It is essentially the Lean version of a C `void *` -/
def EnvExtensionState : Type := NonScalar
instance EnvExtensionState.inhabited : Inhabited EnvExtensionState := inferInstanceAs (Inhabited NonScalar)
/- Opaque environment extension state. -/
constant EnvExtensionStateSpec : PointedType.{0} := arbitrary _
def EnvExtensionState : Type := EnvExtensionStateSpec.type
instance EnvExtensionState.inhabited : Inhabited EnvExtensionState := ⟨EnvExtensionStateSpec.val⟩
def ModuleIdx := Nat
@ -241,17 +241,16 @@ structure PersistentEnvExtension (α : Type) (β : Type) (σ : Type) extends Env
(exportEntriesFn : σ → Array α)
(statsFn : σ → Format)
/- Opaque persistent environment extension entry. It is essentially a C `void *`
TODO: mark opaque -/
def EnvExtensionEntry := NonScalar
instance EnvExtensionEntry.inhabited : Inhabited EnvExtensionEntry := inferInstanceAs (Inhabited NonScalar)
/- Opaque persistent environment extension entry. -/
constant EnvExtensionEntrySpec : PointedType.{0} := arbitrary _
def EnvExtensionEntry : Type := EnvExtensionEntrySpec.type
instance EnvExtensionEntry.inhabited : Inhabited EnvExtensionEntry := ⟨EnvExtensionEntrySpec.val⟩
instance PersistentEnvExtensionState.inhabited {α σ} [Inhabited σ] : Inhabited (PersistentEnvExtensionState α σ) :=
⟨{importedEntries := #[], state := arbitrary _ }⟩
instance PersistentEnvExtension.inhabited {α β σ} [Inhabited σ] : Inhabited (PersistentEnvExtension α β σ) :=
⟨{ toEnvExtension := { idx := 0, stateInh := arbitrary _, mkInitial := arbitrary _ },
⟨{ toEnvExtension := arbitrary _,
name := arbitrary _,
addImportedFn := fun _ _ => arbitrary _,
addEntryFn := fun s _ => s,
@ -389,10 +388,10 @@ match env.getModuleIdxFor? n with
end TagDeclarationExtension
/- API for creating extensions in C++.
This API will eventually be deleted. -/
def CPPExtensionState := NonScalar
TODO: delete after we remove legacy code -/
def CPPExtensionState := EnvExtensionState
instance CPPExtensionState.inhabited : Inhabited CPPExtensionState := inferInstanceAs (Inhabited NonScalar)
instance CPPExtensionState.inhabited : Inhabited CPPExtensionState := inferInstanceAs (Inhabited EnvExtensionState)
section
/- It is not safe to use "extract closed term" optimization in the following code because of `unsafeIO`.
@ -420,7 +419,7 @@ end
We will eventually delete this type as soon as we port the remaining Lean 3
legacy code.
TODO: mark opaque -/
TODO: delete after we remove legacy code -/
def Modification := NonScalar
instance Modification.inhabited : Inhabited Modification := inferInstanceAs (Inhabited NonScalar)