@[extern lean_get_max_ctor_fields]

opaque Lean.IR.Checker.getMaxCtorFields : Unit → Nat

def Lean.IR.Checker.maxCtorFields : Nat

Equations

• Lean.IR.Checker.maxCtorFields = Lean.IR.Checker.getMaxCtorFields ()

@[extern lean_get_max_ctor_scalars_size]

opaque Lean.IR.Checker.getMaxCtorScalarsSize : Unit → Nat

def Lean.IR.Checker.maxCtorScalarsSize : Nat

Equations

• Lean.IR.Checker.maxCtorScalarsSize = Lean.IR.Checker.getMaxCtorScalarsSize ()

@[extern lean_get_max_ctor_tag]

opaque Lean.IR.Checker.getMaxCtorTag : Unit → Nat

def Lean.IR.Checker.maxCtorTag : Nat

Equations

• Lean.IR.Checker.maxCtorTag = Lean.IR.Checker.getMaxCtorTag ()

@[extern lean_get_usize_size]

opaque Lean.IR.Checker.getUSizeSize : Unit → Nat

def Lean.IR.Checker.usizeSize : Nat

Equations

• Lean.IR.Checker.usizeSize = Lean.IR.Checker.getUSizeSize ()

structure Lean.IR.Checker.CheckerContext : Type

• env : Environment
• localCtx : LocalContext
• decls : Array Decl

structure Lean.IR.Checker.CheckerState : Type

• foundVars : IndexSet

@[reducible, inline]

abbrev Lean.IR.Checker.M (α : Type) : Type

Equations

• Lean.IR.Checker.M = ReaderT Lean.IR.Checker.CheckerContext (ExceptT String (StateT Lean.IR.Checker.CheckerState Id))

def Lean.IR.Checker.markIndex (i : Index) : M Unit

Equations

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

def Lean.IR.Checker.markVar (x : VarId) : M Unit

Equations

• Lean.IR.Checker.markVar x = Lean.IR.Checker.markIndex x.idx

def Lean.IR.Checker.markJP (j : JoinPointId) : M Unit

Equations

• Lean.IR.Checker.markJP j = Lean.IR.Checker.markIndex j.idx

def Lean.IR.Checker.getDecl (c : Name) : M Decl

Equations

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

def Lean.IR.Checker.checkVar (x : VarId) : M Unit

Equations

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

def Lean.IR.Checker.checkJP (j : JoinPointId) : M Unit

Equations

• Lean.IR.Checker.checkJP j = do let ctx ← read if ctx.localCtx.isJP j.idx = true then pure PUnit.unit else throw (toString "unknown join point '" ++ toString j ++ toString "'")

def Lean.IR.Checker.checkArg (a : Arg) : M Unit

Equations

• Lean.IR.Checker.checkArg (Lean.IR.Arg.var x) = Lean.IR.Checker.checkVar x
• Lean.IR.Checker.checkArg a = pure ()

def Lean.IR.Checker.checkArgs (as : Array Arg) : M Unit

Equations

• Lean.IR.Checker.checkArgs as = Array.forM Lean.IR.Checker.checkArg as

@[inline]

def Lean.IR.Checker.checkEqTypes (ty₁ ty₂ : IRType) : M Unit

Equations

• Lean.IR.Checker.checkEqTypes ty₁ ty₂ = if (ty₁ == ty₂) = true then pure PUnit.unit else throw "unexpected type '{ty₁}' != '{ty₂}'"

@[inline]

def Lean.IR.Checker.checkType (ty : IRType) (p : IRType → Bool) (suffix? : Option String := none) : M Unit

Equations

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

def Lean.IR.Checker.checkObjType (ty : IRType) : M Unit

Equations

• Lean.IR.Checker.checkObjType ty = Lean.IR.Checker.checkType ty Lean.IR.IRType.isObj (some "object expected")

def Lean.IR.Checker.checkScalarType (ty : IRType) : M Unit

Equations

• Lean.IR.Checker.checkScalarType ty = Lean.IR.Checker.checkType ty Lean.IR.IRType.isScalar (some "scalar expected")

def Lean.IR.Checker.getType (x : VarId) : M IRType

Equations

• Lean.IR.Checker.getType x = do let ctx ← read match ctx.localCtx.getType x with | some ty => pure ty | none => throw (toString "unknown variable '" ++ toString x ++ toString "'")

@[inline]

def Lean.IR.Checker.checkVarType (x : VarId) (p : IRType → Bool) (suffix? : Option String := none) : M Unit

Equations

• Lean.IR.Checker.checkVarType x p suffix? = do let ty ← Lean.IR.Checker.getType x Lean.IR.Checker.checkType ty p suffix?

def Lean.IR.Checker.checkObjVar (x : VarId) : M Unit

Equations

• Lean.IR.Checker.checkObjVar x = Lean.IR.Checker.checkVarType x Lean.IR.IRType.isObj (some "object expected")

def Lean.IR.Checker.checkScalarVar (x : VarId) : M Unit

Equations

• Lean.IR.Checker.checkScalarVar x = Lean.IR.Checker.checkVarType x Lean.IR.IRType.isScalar (some "scalar expected")

def Lean.IR.Checker.checkFullApp (c : FunId) (ys : Array Arg) : M Unit

Equations

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

def Lean.IR.Checker.checkPartialApp (c : FunId) (ys : Array Arg) : M Unit

Equations

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

def Lean.IR.Checker.checkExpr (ty : IRType) : Expr → M Unit

Equations

• One or more equations did not get rendered due to their size.
• Lean.IR.Checker.checkExpr ty (Lean.IR.Expr.pap f ys) = Lean.IR.Checker.checkPartialApp f ys *> Lean.IR.Checker.checkObjType ty
• Lean.IR.Checker.checkExpr ty (Lean.IR.Expr.ap x_1 ys) = Lean.IR.Checker.checkObjVar x_1 *> Lean.IR.Checker.checkArgs ys
• Lean.IR.Checker.checkExpr ty (Lean.IR.Expr.fap f ys) = Lean.IR.Checker.checkFullApp f ys
• Lean.IR.Checker.checkExpr ty (Lean.IR.Expr.reset n x_1) = Lean.IR.Checker.checkObjVar x_1 *> Lean.IR.Checker.checkObjType ty
• Lean.IR.Checker.checkExpr ty (Lean.IR.Expr.reuse x_1 i updtHeader ys) = Lean.IR.Checker.checkObjVar x_1 *> Lean.IR.Checker.checkArgs ys *> Lean.IR.Checker.checkObjType ty
• Lean.IR.Checker.checkExpr ty (Lean.IR.Expr.unbox x_1) = Lean.IR.Checker.checkScalarType ty *> Lean.IR.Checker.checkObjVar x_1
• Lean.IR.Checker.checkExpr ty (Lean.IR.Expr.uproj i x_1) = Lean.IR.Checker.checkObjVar x_1 *> Lean.IR.Checker.checkType ty fun (t : Lean.IR.IRType) => t == Lean.IR.IRType.usize
• Lean.IR.Checker.checkExpr ty (Lean.IR.Expr.sproj n offset x_1) = Lean.IR.Checker.checkObjVar x_1 *> Lean.IR.Checker.checkScalarType ty
• Lean.IR.Checker.checkExpr ty (Lean.IR.Expr.isShared x_1) = Lean.IR.Checker.checkObjVar x_1 *> Lean.IR.Checker.checkType ty fun (t : Lean.IR.IRType) => t == Lean.IR.IRType.uint8
• Lean.IR.Checker.checkExpr ty (Lean.IR.Expr.lit (Lean.IR.LitVal.str v)) = Lean.IR.Checker.checkObjType ty
• Lean.IR.Checker.checkExpr ty (Lean.IR.Expr.lit v) = pure ()

@[inline]

def Lean.IR.Checker.withParams (ps : Array Param) (k : M Unit) : M Unit

Equations

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

partial def Lean.IR.Checker.checkFnBody : FnBody → M Unit

def Lean.IR.Checker.checkDecl : Decl → M Unit

Equations

• Lean.IR.Checker.checkDecl (Lean.IR.Decl.fdecl f xs type b info) = Lean.IR.Checker.withParams xs (Lean.IR.Checker.checkFnBody b)
• Lean.IR.Checker.checkDecl (Lean.IR.Decl.extern f xs type ext) = Lean.IR.Checker.withParams xs (pure ())

def Lean.IR.checkDecl (decls : Array Decl) (decl : Decl) : CompilerM Unit

Equations

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

def Lean.IR.checkDecls (decls : Array Decl) : CompilerM Unit

Equations

• Lean.IR.checkDecls decls = Array.forM (Lean.IR.checkDecl decls) decls