Lean.CoreM

Lean.Core.instInhabitedState = { default := { env := default, nextMacroScope := default, ngen := default, traceState := default, cache := default, messages := default } }

source

structure Lean.Core.Context:

Type

fileName : String
fileMap : Lean.FileMap
options : Lean.Options
currRecDepth : Nat
maxRecDepth : Nat
ref : Lean.Syntax
currNamespace : Lean.Name
openDecls : List Lean.OpenDecl
initHeartbeats : Nat
maxHeartbeats : Nat
currMacroScope : Lean.MacroScope

Context for the CoreM monad.

source

@[inline]

abbrev Lean.Core.CoreM (α : Type) :

Type

CoreM is a monad for manipulating the Lean environment. It is the base monad for MetaM. The main features it provides are:

name generator state
environment state
Lean options context
the current open namespace

Equations

Lean.CoreM = ReaderT Lean.Core.Context (StateRefT' IO.RealWorld Lean.Core.State (EIO Lean.Exception))

source

instance Lean.Core.instMonadCoreM:

Monad Lean.CoreM

Equations

Lean.Core.instMonadCoreM = let i := inferInstanceAs (Monad Lean.CoreM); Monad.mk

source

instance Lean.Core.instInhabitedCoreM {α : Type} :

Inhabited (Lean.CoreM α)

Equations

Lean.Core.instInhabitedCoreM = { default := fun x x => throw default }

source

instance Lean.Core.instMonadRefCoreM:

Lean.MonadRef Lean.CoreM

Equations

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

source

instance Lean.Core.instMonadEnvCoreM:

Lean.MonadEnv Lean.CoreM

Equations

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

source

instance Lean.Core.instMonadOptionsCoreM:

Lean.MonadOptions Lean.CoreM

Equations

Lean.Core.instMonadOptionsCoreM = { getOptions := do let a ← read pure a.options }

source

instance Lean.Core.instMonadWithOptionsCoreM:

Lean.MonadWithOptions Lean.CoreM

Equations

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

source

instance Lean.Core.instAddMessageContextCoreM:

Lean.AddMessageContext Lean.CoreM

Equations

Lean.Core.instAddMessageContextCoreM = { addMessageContext := Lean.addMessageContextPartial }

source

instance Lean.Core.instMonadNameGeneratorCoreM:

Lean.MonadNameGenerator Lean.CoreM

Equations

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

source

instance Lean.Core.instMonadRecDepthCoreM:

Lean.MonadRecDepth Lean.CoreM

Equations

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

source

instance Lean.Core.instMonadResolveNameCoreM:

Lean.MonadResolveName Lean.CoreM

Equations

Lean.Core.instMonadResolveNameCoreM = { getCurrNamespace := do let a ← read pure a.currNamespace, getOpenDecls := do let a ← read pure a.openDecls }

source

def Lean.Core.withFreshMacroScope {α : Type} (x : Lean.CoreM α) :

Lean.CoreM α

Equations

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

source

instance Lean.Core.instMonadQuotationCoreM:

Lean.MonadQuotation Lean.CoreM

Equations

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

source

@[inline]

def Lean.Core.modifyCache (f : Lean.Core.Cache → Lean.Core.Cache) :

Lean.CoreM Unit

Equations

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

source

@[inline]

def Lean.Core.modifyInstLevelTypeCache (f : Lean.Core.InstantiateLevelCache → Lean.Core.InstantiateLevelCache) :

Lean.CoreM Unit

Equations

Lean.Core.modifyInstLevelTypeCache f = Lean.Core.modifyCache fun x => match x with | { instLevelType := c₁, instLevelValue := c₂ } => { instLevelType := f c₁, instLevelValue := c₂ }

source

@[inline]

def Lean.Core.modifyInstLevelValueCache (f : Lean.Core.InstantiateLevelCache → Lean.Core.InstantiateLevelCache) :

Lean.CoreM Unit

Equations

Lean.Core.modifyInstLevelValueCache f = Lean.Core.modifyCache fun x => match x with | { instLevelType := c₁, instLevelValue := c₂ } => { instLevelType := c₁, instLevelValue := f c₂ }

source

def Lean.Core.instantiateTypeLevelParams (c : Lean.ConstantInfo) (us : List Lean.Level) :

Lean.CoreM Lean.Expr

Equations

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

source

def Lean.Core.instantiateValueLevelParams (c : Lean.ConstantInfo) (us : List Lean.Level) :

Lean.CoreM Lean.Expr

Equations

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

source

@[inline]

def Lean.Core.liftIOCore {α : Type} (x : IO α) :

Lean.CoreM α

Equations

Lean.Core.liftIOCore x = do let ref ← Lean.getRef liftM (IO.toEIO (fun err => Lean.Exception.error ref (Function.comp Lean.MessageData.ofFormat Lean.format (toString err))) x)

source

instance Lean.Core.instMonadLiftIOCoreM:

MonadLift IO Lean.CoreM

Equations

Lean.Core.instMonadLiftIOCoreM = { monadLift := fun {α} => Lean.Core.liftIOCore }

source

instance Lean.Core.instMonadTraceCoreM:

Lean.MonadTrace Lean.CoreM

Equations

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

source

def Lean.Core.restore (b : Lean.Core.State) :

Lean.CoreM Unit

Restore backtrackable parts of the state.

Equations

Lean.Core.restore b = modify fun s => { env := b.env, nextMacroScope := s.nextMacroScope, ngen := s.ngen, traceState := s.traceState, cache := s.cache, messages := b.messages }

source

def Lean.Core.mkFreshUserName (n : Lean.Name) :

Lean.CoreM Lean.Name

Equations

Lean.mkFreshUserName n = Lean.Core.mkFreshNameImp n

source

@[inline]

def Lean.Core.CoreM.run {α : Type} (x : Lean.CoreM α) (ctx : Lean.Core.Context) (s : Lean.Core.State) :

EIO Lean.Exception (α × Lean.Core.State)

Equations

Lean.Core.CoreM.run x ctx s = StateRefT'.run (x ctx) s

source

@[inline]

def Lean.Core.CoreM.run' {α : Type} (x : Lean.CoreM α) (ctx : Lean.Core.Context) (s : Lean.Core.State) :

EIO Lean.Exception α

Equations

Lean.Core.CoreM.run' x ctx s = Prod.fst <$> Lean.Core.CoreM.run x ctx s

source

@[inline]

def Lean.Core.CoreM.toIO {α : Type} (x : Lean.CoreM α) (ctx : Lean.Core.Context) (s : Lean.Core.State) :

IO (α × Lean.Core.State)

Equations

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

source

instance Lean.Core.instMetaEvalCoreM {α : Type} [inst : Lean.MetaEval α] :

Lean.MetaEval (Lean.CoreM α)

Equations

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

source

def Lean.Core.withIncRecDepth {m : Type → Type u_1} {α : Type} [inst : Monad m] [inst : MonadControlT Lean.CoreM m] (x : m α) :

m α

Equations

Lean.Core.withIncRecDepth x = controlAt Lean.CoreM fun runInBase => Lean.withIncRecDepth (runInBase x)

source

def Lean.Core.throwMaxHeartbeat (moduleName : Lean.Name) (optionName : Lean.Name) (max : Nat) :

Lean.CoreM Unit

Equations

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

source

def Lean.Core.checkMaxHeartbeatsCore (moduleName : String) (optionName : Lean.Name) (max : Nat) :

Lean.CoreM Unit

Equations

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

source

def Lean.Core.checkMaxHeartbeats (moduleName : String) :

Lean.CoreM Unit

Equations

Lean.checkMaxHeartbeats moduleName = do let a ← read Lean.Core.checkMaxHeartbeatsCore moduleName `maxHeartbeats a.maxHeartbeats

source

def Lean.Core.withCurrHeartbeats {m : Type → Type u_1} {α : Type} [inst : Monad m] [inst : MonadControlT Lean.CoreM m] (x : m α) :

m α

Equations

Lean.withCurrHeartbeats x = controlAt Lean.CoreM fun runInBase => Lean.Core.withCurrHeartbeatsImp (runInBase x)

source

def Lean.Core.setMessageLog (messages : Lean.MessageLog) :

Lean.CoreM Unit

Equations

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

source

def Lean.Core.resetMessageLog:

Lean.CoreM Unit

Equations

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

source

def Lean.Core.getMessageLog:

Lean.CoreM Lean.MessageLog

Equations

Lean.Core.getMessageLog = do let a ← get pure a.messages

source

instance Lean.Core.instMonadLogCoreM:

Lean.MonadLog Lean.CoreM

Equations

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

source

@[inline]

def Lean.catchInternalId {m : Type u_1 → Type u_2} {α : Type u_1} [inst : Monad m] [inst : MonadExcept Lean.Exception m] (id : Lean.InternalExceptionId) (x : m α) (h : Lean.Exception → m α) :

m α

Equations

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

source

@[inline]

def Lean.catchInternalIds {m : Type u_1 → Type u_2} {α : Type u_1} [inst : Monad m] [inst : MonadExcept Lean.Exception m] (ids : List Lean.InternalExceptionId) (x : m α) (h : Lean.Exception → m α) :

m α

Equations

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

source

def Lean.Exception.isMaxHeartbeat (ex : Lean.Exception) :

Bool

Return true if ex was generated by throwMaxHeartbeat. This function is a bit hackish. The heartbeat exception should probably be an internal exception. We used a similar hack at Exception.isMaxRecDepth

Equations

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