Lean.Compiler.IR.Checker

source

@[extern c inline "lean_box(LEAN_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 ()

source

@[extern c inline "lean_box(LEAN_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 ()

source

@[extern c inline "lean_box(sizeof(size_t))"]

opaque Lean.IR.Checker.getUSizeSize:

Unit → Nat

source

def Lean.IR.Checker.usizeSize:

Nat

Equations

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

source

structure Lean.IR.Checker.CheckerContext:

Type

source

structure Lean.IR.Checker.CheckerState:

Type

foundVars : Lean.IR.IndexSet

source

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

source

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

Lean.IR.Checker.M Unit

Equations

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

source

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

Lean.IR.Checker.M Unit

Equations

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

source

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

Lean.IR.Checker.M Unit

Equations

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

source

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

Lean.IR.Checker.M Lean.IR.Decl

Equations

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

source

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

Lean.IR.Checker.M Unit

Equations

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

source

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

Lean.IR.Checker.M Unit

Equations

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

source

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

Lean.IR.Checker.M Unit

Equations

Lean.IR.Checker.checkArg a = match a with | Lean.IR.Arg.var x => Lean.IR.Checker.checkVar x | x => pure ()

source

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

Lean.IR.Checker.M Unit

Equations

Lean.IR.Checker.checkArgs as = Array.forM Lean.IR.Checker.checkArg as 0 (Array.size as)

source

@[inline]

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

Lean.IR.Checker.M Unit

Equations

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

source

@[inline]

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

Lean.IR.Checker.M Unit

Equations

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

source

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

Lean.IR.Checker.M Unit

Equations

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

source

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

Lean.IR.Checker.M Unit

Equations

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

source

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

Lean.IR.Checker.M Lean.IR.IRType

Equations

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

source

@[inline]

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

Lean.IR.Checker.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?

source

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

Lean.IR.Checker.M Unit

Equations

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

source

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

Lean.IR.Checker.M Unit

Equations

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

source

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

Lean.IR.Checker.M Unit

Equations

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

source

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

Lean.IR.Checker.M Unit

Equations

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

source

def Lean.IR.Checker.checkExpr (ty : Lean.IR.IRType) :

Lean.IR.Expr → Lean.IR.Checker.M Unit

Equations

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

source

@[inline]

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

Lean.IR.Checker.M Unit

Equations

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

source

partial def Lean.IR.Checker.checkFnBody:

Lean.IR.FnBody → Lean.IR.Checker.M Unit

source

def Lean.IR.Checker.checkDecl:

Lean.IR.Decl → Lean.IR.Checker.M Unit

Equations

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

source

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

Lean.IR.CompilerM Unit

Equations

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

source

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

Lean.IR.CompilerM Unit

Equations

Lean.IR.checkDecls decls = Array.forM (Lean.IR.checkDecl decls) decls 0 (Array.size decls)