source
@[reducible, inline]
abbrev Lean.Compiler.LCNF.ScopeM (α : Type) :
Type

A general abstraction for the idea of a scope in the compiler.

Equations

- Lean.Compiler.LCNF.ScopeM = StateRefT' IO.RealWorld Lean.FVarIdSet Lean.Compiler.LCNF.CompilerM

Instances For

source
def Lean.Compiler.LCNF.ScopeM.getScope :
ScopeM FVarIdSet
Equations

- Lean.Compiler.LCNF.ScopeM.getScope = get

Instances For

source
def Lean.Compiler.LCNF.ScopeM.setScope (newScope : FVarIdSet) :
ScopeM Unit
Equations

- Lean.Compiler.LCNF.ScopeM.setScope newScope = set newScope

Instances For

source
def Lean.Compiler.LCNF.ScopeM.clearScope :
ScopeM Unit
Equations

- Lean.Compiler.LCNF.ScopeM.clearScope = Lean.Compiler.LCNF.ScopeM.setScope ∅

Instances For

source
def Lean.Compiler.LCNF.ScopeM.withBackTrackingScope {m : Type → Type u_1} {α : Type} [MonadLiftT ScopeM m] [Monad m] [MonadFinally m] (x : m α) :
m α

Execute `x` but recover the previous scope after doing so.

Equations

- Lean.Compiler.LCNF.ScopeM.withBackTrackingScope x = do let scope ← liftM Lean.Compiler.LCNF.ScopeM.getScope tryFinally x (liftM (Lean.Compiler.LCNF.ScopeM.setScope scope))

Instances For

source
def Lean.Compiler.LCNF.ScopeM.withNewScope {m : Type → Type u_1} {α : Type} [MonadLiftT ScopeM m] [Monad m] [MonadFinally m] (x : m α) :
m α

Clear the current scope for the monadic action `x`, afterwards continuing with the old one.

Equations

- Lean.Compiler.LCNF.ScopeM.withNewScope x = Lean.Compiler.LCNF.ScopeM.withBackTrackingScope do liftM Lean.Compiler.LCNF.ScopeM.clearScope x

Instances For

source
def Lean.Compiler.LCNF.ScopeM.isInScope (fvarId : FVarId) :
ScopeM Bool

Check whether `fvarId` is in the current scope, that is, was declared within the current `fun` declaration that is being processed.

Equations

- Lean.Compiler.LCNF.ScopeM.isInScope fvarId = do let scope ← Lean.Compiler.LCNF.ScopeM.getScope pure (Std.TreeSet.contains scope fvarId)

Instances For

source
def Lean.Compiler.LCNF.ScopeM.addToScope (fvarId : FVarId) :
ScopeM Unit

Add a new `FVarId` to the current scope.

Equations

- Lean.Compiler.LCNF.ScopeM.addToScope fvarId = modify fun (scope : Lean.FVarIdSet) => scope.insert fvarId

Instances For