Lean.Environment.replay

replay env constantMap will "replay" all the constants in constantMap : HashMap Name ConstantInfo into env, sending each declaration to the kernel for checking.

replay does not send constructors or recursors in constantMap to the kernel, but rather checks that they are identical to constructors or recursors generated in the environment after replaying any inductive definitions occurring in constantMap.

replay can be used either as:

• a verifier for an Environment, by sending everything to the kernel, or
• a mechanism to safely transfer constants from one Environment to another.

structure Lean.Environment.Replay.Context : Type

• newConstants : Std.HashMap Lake.Name Lean.ConstantInfo

structure Lean.Environment.Replay.State : Type

• env : Lean.Environment
• remaining : Lean.NameSet
• pending : Lean.NameSet
• postponedConstructors : Lean.NameSet
• postponedRecursors : Lean.NameSet

@[reducible, inline]

abbrev Lean.Environment.Replay.M (α : Type) : Type

Equations

• Lean.Environment.Replay.M = ReaderT Lean.Environment.Replay.Context (StateRefT' IO.RealWorld Lean.Environment.Replay.State IO)

def Lean.Environment.Replay.isTodo (name : Lake.Name) : Lean.Environment.Replay.M Bool

Check if a Name still needs processing. If so, move it from remaining to pending.

Equations

• One or more equations did not get rendered due to their size.

def Lean.Environment.Replay.throwKernelException (ex : Lean.KernelException) : Lean.Environment.Replay.M Unit

Use the current Environment to throw a KernelException.

Equations

• One or more equations did not get rendered due to their size.

def Lean.Environment.Replay.addDecl (d : Lean.Declaration) : Lean.Environment.Replay.M Unit

Add a declaration, possibly throwing a KernelException.

Equations

• One or more equations did not get rendered due to their size.

partial def Lean.Environment.Replay.replayConstant (name : Lake.Name) : Lean.Environment.Replay.M Unit

Check if a Name still needs to be processed (i.e. is in remaining).

If so, recursively replay any constants it refers to, to ensure we add declarations in the right order.

The construct the Declaration from its stored ConstantInfo, and add it to the environment.

partial def Lean.Environment.Replay.replayConstants (names : Lean.NameSet) : Lean.Environment.Replay.M Unit

Replay a set of constants one at a time.

def Lean.Environment.Replay.checkPostponedConstructors : Lean.Environment.Replay.M Unit

Check that all postponed constructors are identical to those generated when we replayed the inductives.

Equations

• One or more equations did not get rendered due to their size.

def Lean.Environment.Replay.checkPostponedRecursors : Lean.Environment.Replay.M Unit

Check that all postponed recursors are identical to those generated when we replayed the inductives.

Equations

• One or more equations did not get rendered due to their size.

def Lean.Environment.replay (newConstants : Std.HashMap Lake.Name Lean.ConstantInfo) (env : Lean.Environment) : IO Lean.Environment

"Replay" some constants into an Environment, sending them to the kernel for checking.

Throws a IO.userError if the kernel rejects a constant, or if there are malformed recursors or constructors for inductive types.

Equations

• One or more equations did not get rendered due to their size.