Lean.CoreM

Lean.Core.instMonadRefCoreM = { getRef := do let a ← read pure a.ref, withRef := fun {α} ref x => withReader (fun ctx => { options := ctx.options, currRecDepth := ctx.currRecDepth, maxRecDepth := ctx.maxRecDepth, ref := ref, currNamespace := ctx.currNamespace, openDecls := ctx.openDecls, initHeartbeats := ctx.initHeartbeats, maxHeartbeats := ctx.maxHeartbeats }) x }

source

instance Lean.Core.instMonadEnvCoreM :

Lean.MonadEnv Lean.CoreM

Equations

Lean.Core.instMonadEnvCoreM = { getEnv := do let a ← get pure a.env, modifyEnv := fun f => modify fun s => { env := f s.env, nextMacroScope := s.nextMacroScope, ngen := s.ngen, traceState := s.traceState } }

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

Lean.Core.instMonadWithOptionsCoreM = { withOptions := fun {α} f x => withReader (fun ctx => { options := f ctx.options, currRecDepth := ctx.currRecDepth, maxRecDepth := ctx.maxRecDepth, ref := ctx.ref, currNamespace := ctx.currNamespace, openDecls := ctx.openDecls, initHeartbeats := ctx.initHeartbeats, maxHeartbeats := ctx.maxHeartbeats }) x }

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

Lean.Core.instMonadNameGeneratorCoreM = { getNGen := do let a ← get pure a.ngen, setNGen := fun ngen => modify fun s => { env := s.env, nextMacroScope := s.nextMacroScope, ngen := ngen, traceState := s.traceState } }

source

instance Lean.Core.instMonadRecDepthCoreM :

Lean.MonadRecDepth Lean.CoreM

Equations

Lean.Core.instMonadRecDepthCoreM = { withRecDepth := fun {α} d x => withReader (fun ctx => { options := ctx.options, currRecDepth := d, maxRecDepth := ctx.maxRecDepth, ref := ctx.ref, currNamespace := ctx.currNamespace, openDecls := ctx.openDecls, initHeartbeats := ctx.initHeartbeats, maxHeartbeats := ctx.maxHeartbeats }) x, getRecDepth := do let a ← read pure a.currRecDepth, getMaxRecDepth := do let a ← read pure a.maxRecDepth }

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

@[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

Lean.Core.instMonadTraceCoreM = { modifyTraceState := fun f => modify fun s => { env := s.env, nextMacroScope := s.nextMacroScope, ngen := s.ngen, traceState := f s.traceState }, getTraceState := do let a ← get pure a.traceState }

source

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

Lean.CoreM Unit

Equations

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

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

Lean.Core.CoreM.toIO x ctx s = do let a ← liftM IO.getNumHeartbeats let a ← EIO.toIO' (Lean.Core.CoreM.run x { options := ctx.options, currRecDepth := ctx.currRecDepth, maxRecDepth := ctx.maxRecDepth, ref := ctx.ref, currNamespace := ctx.currNamespace, openDecls := ctx.openDecls, initHeartbeats := a, maxHeartbeats := ctx.maxHeartbeats } s) match a with | Except.error (Lean.Exception.error x msg) => do let a ← Lean.MessageData.toString msg throw (IO.userError a) | Except.error (Lean.Exception.internal id x) => throw (IO.userError ("internal exception #" ++ toString id.idx)) | Except.ok a => pure a

source

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

Lean.MetaEval (Lean.CoreM α)

Equations

Lean.Core.instMetaEvalCoreM = { eval := fun env opts x x_1 => let x := tryFinally x Lean.printTraces; do let discr ← Lean.Core.CoreM.toIO x { options := opts, currRecDepth := 0, maxRecDepth := Lean.Option.get opts Lean.maxRecDepth, ref := Lean.Syntax.missing, currNamespace := Lean.Name.anonymous, openDecls := [], initHeartbeats := 0, maxHeartbeats := Lean.Core.getMaxHeartbeats opts } { env := env, nextMacroScope := Lean.firstFrontendMacroScope + 1, ngen := { namePrefix := `_uniq, idx := 1 }, traceState := { enabled := true, traces := { root := Std.PersistentArrayNode.node (Array.mkEmpty (USize.toNat Std.PersistentArray.branching)), tail := Array.mkEmpty (USize.toNat Std.PersistentArray.branching), size := 0, shift := Std.PersistentArray.initShift, tailOff := 0 } } } let x : α × Lean.Core.State := discr match x with | (a, s) => Lean.MetaEval.eval s.env opts a true }

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.checkMaxHeartbeatsCore (moduleName : String) (optionName : Lean.Name) (max : Nat) :

Lean.CoreM Unit

Equations

Lean.Core.checkMaxHeartbeatsCore moduleName optionName max = if (max == 0) = true then pure PUnit.unit else do let numHeartbeats ← liftM IO.getNumHeartbeats let a ← read if numHeartbeats - a.initHeartbeats > max then Lean.throwError (Lean.toMessageData "(deterministic) timeout at '" ++ Lean.toMessageData moduleName ++ Lean.toMessageData "', maximum number of heartbeats (" ++ Lean.toMessageData (max / 1000) ++ Lean.toMessageData ") has been reached (use 'set_option " ++ Lean.toMessageData optionName ++ Lean.toMessageData " ' to set the limit)") else pure PUnit.unit

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

@[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

Lean.catchInternalId id x h = tryCatch x fun ex => match ex with | Lean.Exception.error x x_1 => throw ex | Lean.Exception.internal id' x => if (id == id') = true then h ex else throw ex

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

Lean.catchInternalIds ids x h = tryCatch x fun ex => match ex with | Lean.Exception.error x x_1 => throw ex | Lean.Exception.internal id x => if List.contains ids id = true then h ex else throw ex