Lean.Compiler.IR.Checker

Lean.IR.Checker.markIndex i = do let s ← get let _do_jp : PUnit → Lean.IR.Checker.M Unit := fun y => modify fun s => { foundVars := Std.RBTree.insert s.foundVars i } if Std.RBTree.contains s.foundVars i = true then do let y ← throw (toString "variable / joinpoint index " ++ toString i ++ toString " has already been used") _do_jp y else do let y ← pure PUnit.unit _do_jp y

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

Lean.IR.Checker.getDecl c = do let ctx ← read match Lean.IR.findEnvDecl' ctx.env c ctx.decls with | none => throw (toString "unknown declaration '" ++ toString c ++ toString "'") | some d => pure d

source

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

Lean.IR.Checker.M Unit

Equations

Lean.IR.Checker.checkVar x = do let ctx ← read if (Lean.IR.LocalContext.isLocalVar ctx.localCtx x.idx || Lean.IR.LocalContext.isParam ctx.localCtx x.idx) = true then pure PUnit.unit else throw (toString "unknown variable '" ++ toString x ++ toString "'")

source

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

Lean.IR.Checker.M Unit

Equations

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

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 | other => 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"

source

@[inline]

def Lean.IR.Checker.checkType (ty : Lean.IR.IRType) (p : Lean.IR.IRType → Bool) :

Lean.IR.Checker.M Unit

Equations

Lean.IR.Checker.checkType ty p = if p ty = true then pure PUnit.unit else throw (toString "unexpected type '" ++ toString ty ++ toString "'")

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

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

source

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

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

Equations

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

source

@[inline]

def Lean.IR.Checker.checkVarType (x : Lean.IR.VarId) (p : Lean.IR.IRType → Bool) :

Lean.IR.Checker.M Unit

Equations

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

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

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

source

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

Lean.IR.Checker.M Unit

Equations

Lean.IR.Checker.checkFullApp c ys = do let decl ← Lean.IR.Checker.getDecl c let _do_jp : PUnit → Lean.IR.Checker.M Unit := fun y => Lean.IR.Checker.checkArgs ys if (Array.size ys == Array.size (Lean.IR.Decl.params decl)) = true then do let y ← pure PUnit.unit _do_jp y else do let y ← throw (toString "incorrect number of arguments to '" ++ toString c ++ toString "', " ++ toString (Array.size ys) ++ toString " provided, " ++ toString (Array.size (Lean.IR.Decl.params decl)) ++ toString " expected") _do_jp y

source

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

Lean.IR.Checker.M Unit

Equations

Lean.IR.Checker.checkPartialApp c ys = do let decl ← Lean.IR.Checker.getDecl c let _do_jp : PUnit → Lean.IR.Checker.M Unit := fun y => Lean.IR.Checker.checkArgs ys if Array.size ys < Array.size (Lean.IR.Decl.params decl) then do let y ← pure PUnit.unit _do_jp y else do let y ← throw (toString "too many arguments too partial application '" ++ toString c ++ toString "', num. args: " ++ toString (Array.size ys) ++ toString ", arity: " ++ toString (Array.size (Lean.IR.Decl.params decl)) ++ toString "") _do_jp y

source

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

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

Equations

Lean.IR.Checker.checkExpr ty x = match x with | Lean.IR.Expr.pap f ys => SeqRight.seqRight (Lean.IR.Checker.checkPartialApp f ys) fun x => Lean.IR.Checker.checkObjType ty | Lean.IR.Expr.ap x ys => SeqRight.seqRight (Lean.IR.Checker.checkObjVar x) fun x => Lean.IR.Checker.checkArgs ys | Lean.IR.Expr.fap f ys => Lean.IR.Checker.checkFullApp f ys | Lean.IR.Expr.ctor c ys => let _do_jp := fun y => let _do_jp := fun y => if (!Lean.IR.IRType.isStruct ty && !Lean.IR.IRType.isUnion ty && Lean.IR.CtorInfo.isRef c) = true then SeqRight.seqRight (Lean.IR.Checker.checkObjType ty) fun x => Lean.IR.Checker.checkArgs ys else pure PUnit.unit; if c.ssize + c.usize * Lean.IR.Checker.usizeSize > Lean.IR.Checker.maxCtorScalarsSize then do let y ← throw (toString "constructor '" ++ toString c.name ++ toString "' has too many scalar fields") _do_jp y else do let y ← pure PUnit.unit _do_jp y; if c.size > Lean.IR.Checker.maxCtorFields then do let y ← throw (toString "constructor '" ++ toString c.name ++ toString "' has too many fields") _do_jp y else do let y ← pure PUnit.unit _do_jp y | Lean.IR.Expr.reset x x_1 => SeqRight.seqRight (Lean.IR.Checker.checkObjVar x_1) fun x => Lean.IR.Checker.checkObjType ty | Lean.IR.Expr.reuse x i u ys => SeqRight.seqRight (SeqRight.seqRight (Lean.IR.Checker.checkObjVar x) fun x => Lean.IR.Checker.checkArgs ys) fun x => Lean.IR.Checker.checkObjType ty | Lean.IR.Expr.box xty x => SeqRight.seqRight (SeqRight.seqRight (Lean.IR.Checker.checkObjType ty) fun x_1 => Lean.IR.Checker.checkScalarVar x) fun x_1 => Lean.IR.Checker.checkVarType x fun t => t == xty | Lean.IR.Expr.unbox x => SeqRight.seqRight (Lean.IR.Checker.checkScalarType ty) fun x_1 => Lean.IR.Checker.checkObjVar x | Lean.IR.Expr.proj i x => do let xType ← Lean.IR.Checker.getType x match xType with | Lean.IR.IRType.object => Lean.IR.Checker.checkObjType ty | Lean.IR.IRType.tobject => Lean.IR.Checker.checkObjType ty | Lean.IR.IRType.struct x tys => if h : i < Array.size tys then Lean.IR.Checker.checkEqTypes (Array.get tys { val := i, isLt := h }) ty else throw "invalid proj index" | Lean.IR.IRType.union x tys => if h : i < Array.size tys then Lean.IR.Checker.checkEqTypes (Array.get tys { val := i, isLt := h }) ty else throw "invalid proj index" | other => throw (toString "unexpected IR type '" ++ toString xType ++ toString "'") | Lean.IR.Expr.uproj x x_1 => SeqRight.seqRight (Lean.IR.Checker.checkObjVar x_1) fun x => Lean.IR.Checker.checkType ty fun t => t == Lean.IR.IRType.usize | Lean.IR.Expr.sproj x x_1 x_2 => SeqRight.seqRight (Lean.IR.Checker.checkObjVar x_2) fun x => Lean.IR.Checker.checkScalarType ty | Lean.IR.Expr.isShared x => SeqRight.seqRight (Lean.IR.Checker.checkObjVar x) fun x => Lean.IR.Checker.checkType ty fun t => t == Lean.IR.IRType.uint8 | Lean.IR.Expr.isTaggedPtr x => SeqRight.seqRight (Lean.IR.Checker.checkObjVar x) fun x => Lean.IR.Checker.checkType ty fun t => t == Lean.IR.IRType.uint8 | Lean.IR.Expr.lit (Lean.IR.LitVal.str x) => Lean.IR.Checker.checkObjType ty | Lean.IR.Expr.lit x => pure ()

source

@[inline]

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

Lean.IR.Checker.M Unit

Equations

Lean.IR.Checker.withParams ps k = do let ctx ← read let localCtx ← Array.foldlM (fun ctx p => do Lean.IR.Checker.markVar p.x pure (Lean.IR.LocalContext.addParam ctx p)) ctx.localCtx ps 0 (Array.size ps) withReader (fun x => { env := ctx.env, localCtx := localCtx, decls := ctx.decls }) k

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

Lean.IR.Checker.checkDecl x = match x with | Lean.IR.Decl.fdecl x xs x_1 b x_2 => Lean.IR.Checker.withParams xs (Lean.IR.Checker.checkFnBody b) | Lean.IR.Decl.extern x xs x_1 x_2 => Lean.IR.Checker.withParams xs (pure ())

source

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

Lean.IR.CompilerM Unit

Equations

Lean.IR.checkDecl decls decl = do let env ← Lean.IR.getEnv match StateT.run' (Lean.IR.Checker.checkDecl decl { env := env, localCtx := ∅, decls := decls }) { foundVars := ∅ } with | Except.error msg => throw (toString "IR check failed at '" ++ toString (Lean.IR.Decl.name decl) ++ toString "', error: " ++ toString msg ++ toString "") | other => pure ()

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)