structure Lean.Compiler.LCNF.Check.Context : Type

• Join points that are in scope.

  jps : Lean.FVarIdSet

• Variables and local functions in scope

  vars : Lean.FVarIdSet

structure Lean.Compiler.LCNF.Check.State : Type

• All free variables found

  all : Lean.FVarIdHashSet

@[inline]

abbrev Lean.Compiler.LCNF.Check.CheckM (α : Type) : Type

Equations

• Lean.Compiler.LCNF.Check.CheckM = ReaderT Lean.Compiler.LCNF.Check.Context (StateRefT' IO.RealWorld Lean.Compiler.LCNF.Check.State Lean.Compiler.LCNF.InferType.InferTypeM)

def Lean.Compiler.LCNF.Check.checkFVar (fvarId : Lean.FVarId) : Lean.Compiler.LCNF.Check.CheckM Unit

Equations

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

def Lean.Compiler.LCNF.Check.checkAppArgs (f : Lean.Expr) (args : Array Lean.Expr) : Lean.Compiler.LCNF.Check.CheckM Unit

Equations

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

def Lean.Compiler.LCNF.Check.checkApp (f : Lean.Expr) (args : Array Lean.Expr) : Lean.Compiler.LCNF.Check.CheckM Unit

Equations

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

def Lean.Compiler.LCNF.Check.checkExpr (e : Lean.Expr) : Lean.Compiler.LCNF.Check.CheckM Unit

Equations

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

def Lean.Compiler.LCNF.Check.checkJpInScope (jp : Lean.FVarId) : Lean.Compiler.LCNF.Check.CheckM Unit

Equations

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

def Lean.Compiler.LCNF.Check.checkParam (param : Lean.Compiler.LCNF.Param) : Lean.Compiler.LCNF.Check.CheckM Unit

Equations

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

def Lean.Compiler.LCNF.Check.checkParams (params : Array Lean.Compiler.LCNF.Param) : Lean.Compiler.LCNF.Check.CheckM Unit

Equations

• Lean.Compiler.LCNF.Check.checkParams params = Array.forM Lean.Compiler.LCNF.Check.checkParam params 0 (Array.size params)

def Lean.Compiler.LCNF.Check.checkLetDecl (letDecl : Lean.Compiler.LCNF.LetDecl) : Lean.Compiler.LCNF.Check.CheckM Unit

Equations

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

def Lean.Compiler.LCNF.Check.addFVarId (fvarId : Lean.FVarId) : Lean.Compiler.LCNF.Check.CheckM Unit

Equations

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

@[inline]

def Lean.Compiler.LCNF.Check.withFVarId {α : Type} (fvarId : Lean.FVarId) (x : Lean.Compiler.LCNF.Check.CheckM α) : Lean.Compiler.LCNF.Check.CheckM α

Equations

• Lean.Compiler.LCNF.Check.withFVarId fvarId x = do Lean.Compiler.LCNF.Check.addFVarId fvarId withReader (fun ctx => { jps := ctx.jps, vars := Lean.RBTree.insert ctx.vars fvarId }) x

@[inline]

def Lean.Compiler.LCNF.Check.withJp {α : Type} (fvarId : Lean.FVarId) (x : Lean.Compiler.LCNF.Check.CheckM α) : Lean.Compiler.LCNF.Check.CheckM α

Equations

• Lean.Compiler.LCNF.Check.withJp fvarId x = do Lean.Compiler.LCNF.Check.addFVarId fvarId withReader (fun ctx => { jps := Lean.RBTree.insert ctx.jps fvarId, vars := ctx.vars }) x

@[inline]

def Lean.Compiler.LCNF.Check.withParams {α : Type} (params : Array Lean.Compiler.LCNF.Param) (x : Lean.Compiler.LCNF.Check.CheckM α) : Lean.Compiler.LCNF.Check.CheckM α

Equations

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

partial def Lean.Compiler.LCNF.Check.checkFunDeclCore (declName : Lean.Name) (type : Lean.Expr) (params : Array Lean.Compiler.LCNF.Param) (value : Lean.Compiler.LCNF.Code) : Lean.Compiler.LCNF.Check.CheckM Unit

partial def Lean.Compiler.LCNF.Check.checkFunDecl (funDecl : Lean.Compiler.LCNF.FunDecl) : Lean.Compiler.LCNF.Check.CheckM Unit

partial def Lean.Compiler.LCNF.Check.checkCases (c : Lean.Compiler.LCNF.Cases) : Lean.Compiler.LCNF.Check.CheckM Lean.Expr

partial def Lean.Compiler.LCNF.Check.check (code : Lean.Compiler.LCNF.Code) : Lean.Compiler.LCNF.Check.CheckM Lean.Expr

def Lean.Compiler.LCNF.Check.run {α : Type} (x : Lean.Compiler.LCNF.Check.CheckM α) : Lean.Compiler.LCNF.CompilerM α

Equations

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

def Lean.Compiler.LCNF.Decl.check (decl : Lean.Compiler.LCNF.Decl) : Lean.Compiler.LCNF.CompilerM Unit

Equations

• Lean.Compiler.LCNF.Decl.check decl = Lean.Compiler.LCNF.Check.run (Lean.Compiler.LCNF.Check.checkFunDeclCore decl.name decl.type decl.params decl.value)

def Lean.Compiler.LCNF.checkDeadLocalDecls (decls : Array Lean.Compiler.LCNF.Decl) : Lean.Compiler.LCNF.CompilerM Unit

Check whether every local declaration in the local context is used in one of given decls.

Equations

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

def Lean.Compiler.LCNF.checkDeadLocalDecls.visitFVar (fvarId : Lean.FVarId) : StateM Lean.FVarIdHashSet Unit

Equations

• Lean.Compiler.LCNF.checkDeadLocalDecls.visitFVar fvarId = modify fun a => Lean.HashSet.insert a fvarId

def Lean.Compiler.LCNF.checkDeadLocalDecls.visitParam (param : Lean.Compiler.LCNF.Param) : StateM Lean.FVarIdHashSet Unit

Equations

• Lean.Compiler.LCNF.checkDeadLocalDecls.visitParam param = Lean.Compiler.LCNF.checkDeadLocalDecls.visitFVar param.fvarId

def Lean.Compiler.LCNF.checkDeadLocalDecls.visitParams (params : Array Lean.Compiler.LCNF.Param) : StateM Lean.FVarIdHashSet Unit

Equations

• Lean.Compiler.LCNF.checkDeadLocalDecls.visitParams params = Array.forM Lean.Compiler.LCNF.checkDeadLocalDecls.visitParam params 0 (Array.size params)

partial def Lean.Compiler.LCNF.checkDeadLocalDecls.visitCode (code : Lean.Compiler.LCNF.Code) : StateM Lean.FVarIdHashSet Unit

def Lean.Compiler.LCNF.checkDeadLocalDecls.visitDecl (decl : Lean.Compiler.LCNF.Decl) : StateM Lean.FVarIdHashSet Unit

Equations

• Lean.Compiler.LCNF.checkDeadLocalDecls.visitDecl decl = do Lean.Compiler.LCNF.checkDeadLocalDecls.visitParams decl.params Lean.Compiler.LCNF.checkDeadLocalDecls.visitCode decl.value

def Lean.Compiler.LCNF.checkDeadLocalDecls.visitDecls (decls : Array Lean.Compiler.LCNF.Decl) : StateM Lean.FVarIdHashSet Unit

Equations

• Lean.Compiler.LCNF.checkDeadLocalDecls.visitDecls decls = Array.forM Lean.Compiler.LCNF.checkDeadLocalDecls.visitDecl decls 0 (Array.size decls)