structure Lean.IR.ToIR.BuilderState : Type

• vars : Std.HashMap FVarId Arg
• joinPoints : Std.HashMap FVarId JoinPointId
• nextId : Nat

@[reducible, inline]

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

Equations

• Lean.IR.ToIR.M = StateRefT' IO.RealWorld Lean.IR.ToIR.BuilderState Lean.CoreM

def Lean.IR.ToIR.M.run {α : Type} (x : M α) : CoreM α

Equations

• x.run = StateRefT'.run' x { }

def Lean.IR.ToIR.getFVarValue (fvarId : FVarId) : M Arg

Equations

• Lean.IR.ToIR.getFVarValue fvarId = do let __do_lift ← get pure (__do_lift.vars.get! fvarId)

def Lean.IR.ToIR.getJoinPointValue (fvarId : FVarId) : M JoinPointId

Equations

• Lean.IR.ToIR.getJoinPointValue fvarId = do let __do_lift ← get pure (__do_lift.joinPoints.get! fvarId)

def Lean.IR.ToIR.bindVar (fvarId : FVarId) : M VarId

Equations

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

def Lean.IR.ToIR.bindJoinPoint (fvarId : FVarId) : M JoinPointId

Equations

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

def Lean.IR.ToIR.bindErased (fvarId : FVarId) : M Unit

Equations

• Lean.IR.ToIR.bindErased fvarId = modify fun (s : Lean.IR.ToIR.BuilderState) => { vars := s.vars.insertIfNew fvarId Lean.IR.Arg.erased, joinPoints := s.joinPoints, nextId := s.nextId }

def Lean.IR.ToIR.addDecl (d : Decl) : M Unit

Equations

• Lean.IR.ToIR.addDecl d = Lean.modifyEnv fun (env : Lean.Environment) => Lean.PersistentEnvExtension.addEntry Lean.IR.declMapExt env d

def Lean.IR.ToIR.lowerLitValue (v : Compiler.LCNF.LitValue) : LitVal × IRType

Equations

• Lean.IR.ToIR.lowerLitValue (Lean.Compiler.LCNF.LitValue.nat n) = (Lean.IR.LitVal.num n, if n < UInt32.size then Lean.IR.IRType.tagged else Lean.IR.IRType.tobject)
• Lean.IR.ToIR.lowerLitValue (Lean.Compiler.LCNF.LitValue.str s) = (Lean.IR.LitVal.str s, Lean.IR.IRType.object)
• Lean.IR.ToIR.lowerLitValue (Lean.Compiler.LCNF.LitValue.uint8 v_2) = (Lean.IR.LitVal.num v_2.toNat, Lean.IR.IRType.uint8)
• Lean.IR.ToIR.lowerLitValue (Lean.Compiler.LCNF.LitValue.uint16 v_2) = (Lean.IR.LitVal.num v_2.toNat, Lean.IR.IRType.uint16)
• Lean.IR.ToIR.lowerLitValue (Lean.Compiler.LCNF.LitValue.uint32 v_2) = (Lean.IR.LitVal.num v_2.toNat, Lean.IR.IRType.uint32)
• Lean.IR.ToIR.lowerLitValue (Lean.Compiler.LCNF.LitValue.uint64 v_2) = (Lean.IR.LitVal.num v_2.toNat, Lean.IR.IRType.uint64)
• Lean.IR.ToIR.lowerLitValue (Lean.Compiler.LCNF.LitValue.usize v_2) = (Lean.IR.LitVal.num v_2.toNat, Lean.IR.IRType.usize)

def Lean.IR.ToIR.lowerArg (a : Compiler.LCNF.Arg Compiler.LCNF.Purity.impure) : M Arg

Equations

• Lean.IR.ToIR.lowerArg (Lean.Compiler.LCNF.Arg.fvar fvarId) = Lean.IR.ToIR.getFVarValue fvarId
• Lean.IR.ToIR.lowerArg Lean.Compiler.LCNF.Arg.erased = pure Lean.IR.Arg.erased

def Lean.IR.ToIR.lowerParam (p : Compiler.LCNF.Param Compiler.LCNF.Purity.impure) : M Param

Equations

• Lean.IR.ToIR.lowerParam p = do let x ← Lean.IR.ToIR.bindVar p.fvarId have ty : Lean.IR.IRType := Lean.IR.toIRType p.type pure { x := x, borrow := p.borrow, ty := ty }

@[inline]

def Lean.IR.ToIR.lowerCtorInfo (i : Compiler.LCNF.CtorInfo) : CtorInfo

Equations

• Lean.IR.ToIR.lowerCtorInfo i = { name := i.name, cidx := i.cidx, size := i.size, usize := i.usize, ssize := i.ssize }

partial def Lean.IR.ToIR.lowerCode (c : Compiler.LCNF.Code Compiler.LCNF.Purity.impure) : M FnBody

partial def Lean.IR.ToIR.lowerLet (decl : Compiler.LCNF.LetDecl Compiler.LCNF.Purity.impure) (k : Compiler.LCNF.Code Compiler.LCNF.Purity.impure) : M FnBody

partial def Lean.IR.ToIR.lowerAlt (a : Compiler.LCNF.Alt Compiler.LCNF.Purity.impure) : M Alt

def Lean.IR.ToIR.lowerDecl (d : Compiler.LCNF.Decl Compiler.LCNF.Purity.impure) : M (Option Decl)

Equations

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

def Lean.IR.toIR (decls : Array (Compiler.LCNF.Decl Compiler.LCNF.Purity.impure)) : CoreM (Array Decl)

Equations

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