source
@[extern lean_get_max_ctor_fields]
opaque Lean.IR.Checker.getMaxCtorFields :
Unit → Nat
source
def Lean.IR.Checker.maxCtorFields :
Nat
Equations

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

Instances For

source
@[extern lean_get_max_ctor_scalars_size]
opaque Lean.IR.Checker.getMaxCtorScalarsSize :
Unit → Nat
source
def Lean.IR.Checker.maxCtorScalarsSize :
Nat
Equations

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

Instances For

source
@[extern lean_get_max_ctor_tag]
opaque Lean.IR.Checker.getMaxCtorTag :
Unit → Nat
source
def Lean.IR.Checker.maxCtorTag :
Nat
Equations

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

Instances For

source
@[extern lean_get_usize_size]
opaque Lean.IR.Checker.getUSizeSize :
Unit → Nat
source
def Lean.IR.Checker.usizeSize :
Nat
Equations

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

Instances For

source
structure Lean.IR.Checker.CheckerContext :
Type

- localCtx : LocalContext
- currentDecl : Decl
- decls : Array Decl

Instances For

source
structure Lean.IR.Checker.CheckerState :
Type

- foundVars : IndexSet

Instances For

source
@[reducible, inline]
abbrev Lean.IR.Checker.M (α : Type) :
Type
Equations

- Lean.IR.Checker.M = ReaderT Lean.IR.Checker.CheckerContext (StateRefT' IO.RealWorld Lean.IR.Checker.CheckerState Lean.IR.CompilerM)

Instances For

source
def Lean.IR.Checker.throwCheckerError {α : Type} (msg : String) :
M α
Equations

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

Instances For

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

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

Instances For

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

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

Instances For

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

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

Instances For

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

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

Instances For

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

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

Instances For

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

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

Instances For

source
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 Lean.IR.Arg.erased = pure ()

Instances For

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

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

Instances For

source
@[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 Lean.IR.Checker.throwCheckerError "unexpected type '{ty₁}' != '{ty₂}'"

Instances For

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

Instances For

source
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")

Instances For

source
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")

Instances For

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

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

Instances For

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

Instances For

source
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")

Instances For

source
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")

Instances For

source
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.

Instances For

source
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.

Instances For

source
def Lean.IR.Checker.checkExpr (ty : IRType) (e : 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) = do Lean.IR.Checker.checkPartialApp f ys Lean.IR.Checker.checkObjType ty
- Lean.IR.Checker.checkExpr ty (Lean.IR.Expr.ap x ys) = do Lean.IR.Checker.checkObjVar x Lean.IR.Checker.checkArgs ys Lean.IR.Checker.checkObjType ty
- 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) = do Lean.IR.Checker.checkObjVar x Lean.IR.Checker.checkObjType ty
- Lean.IR.Checker.checkExpr ty (Lean.IR.Expr.reuse x i updtHeader ys) = do Lean.IR.Checker.checkObjVar x Lean.IR.Checker.checkArgs ys Lean.IR.Checker.checkObjType ty
- Lean.IR.Checker.checkExpr ty (Lean.IR.Expr.box xty x) = do Lean.IR.Checker.checkObjType ty Lean.IR.Checker.checkScalarVar x Lean.IR.Checker.checkVarType x fun (x : Lean.IR.IRType) => x == xty
- Lean.IR.Checker.checkExpr ty (Lean.IR.Expr.unbox x) = do Lean.IR.Checker.checkScalarType ty Lean.IR.Checker.checkObjVar x
- Lean.IR.Checker.checkExpr ty (Lean.IR.Expr.uproj i x) = do Lean.IR.Checker.checkObjVar x Lean.IR.Checker.checkType ty fun (x : Lean.IR.IRType) => x == Lean.IR.IRType.usize
- Lean.IR.Checker.checkExpr ty (Lean.IR.Expr.sproj n offset x) = do Lean.IR.Checker.checkObjVar x Lean.IR.Checker.checkScalarType ty
- Lean.IR.Checker.checkExpr ty (Lean.IR.Expr.isShared x) = do Lean.IR.Checker.checkObjVar x Lean.IR.Checker.checkType ty fun (x : Lean.IR.IRType) => x == 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 ()

Instances For

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

Instances For

source
partial def Lean.IR.Checker.checkFnBody (fnBody : FnBody) :
M Unit
source
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 ())

Instances For

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

- Lean.IR.checkDecl decls decl = (Lean.IR.Checker.checkDecl decl { currentDecl := decl, decls := decls }).run' { }

Instances For

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

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

Instances For