def Lean.IR.EmitC.leanMainFn : String

Equations

• Lean.IR.EmitC.leanMainFn = "_lean_main"

structure Lean.IR.EmitC.Context : Type

• env : Environment
• modName : Name
• jpMap : JPParamsMap
• mainFn : FunId
• mainParams : Array Param

@[reducible, inline]

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

Equations

• Lean.IR.EmitC.M = ReaderT Lean.IR.EmitC.Context (EStateM String String)

def Lean.IR.EmitC.getEnv : M Environment

Equations

• Lean.IR.EmitC.getEnv = Lean.IR.EmitC.Context.env <$> read

def Lean.IR.EmitC.getModName : M Name

Equations

• Lean.IR.EmitC.getModName = Lean.IR.EmitC.Context.modName <$> read

def Lean.IR.EmitC.getDecl (n : Name) : M Decl

Equations

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

@[inline]

def Lean.IR.EmitC.emit {α : Type} [ToString α] (a : α) : M Unit

Equations

• Lean.IR.EmitC.emit a = modify fun (out : String) => out ++ toString a

@[inline]

def Lean.IR.EmitC.emitLn {α : Type} [ToString α] (a : α) : M Unit

Equations

• Lean.IR.EmitC.emitLn a = do Lean.IR.EmitC.emit a Lean.IR.EmitC.emit "\n"

def Lean.IR.EmitC.emitLns {α : Type} [ToString α] (as : List α) : M Unit

Equations

• Lean.IR.EmitC.emitLns as = as.forM fun (a : α) => Lean.IR.EmitC.emitLn a

def Lean.IR.EmitC.argToCString (x : Arg) : String

Equations

• Lean.IR.EmitC.argToCString (Lean.IR.Arg.var x_2) = toString x_2
• Lean.IR.EmitC.argToCString x = "lean_box(0)"

def Lean.IR.EmitC.emitArg (x : Arg) : M Unit

Equations

• Lean.IR.EmitC.emitArg x = Lean.IR.EmitC.emit (Lean.IR.EmitC.argToCString x)

def Lean.IR.EmitC.toCType : IRType → String

Equations

• Lean.IR.EmitC.toCType Lean.IR.IRType.float = "double"
• Lean.IR.EmitC.toCType Lean.IR.IRType.float32 = "float"
• Lean.IR.EmitC.toCType Lean.IR.IRType.uint8 = "uint8_t"
• Lean.IR.EmitC.toCType Lean.IR.IRType.uint16 = "uint16_t"
• Lean.IR.EmitC.toCType Lean.IR.IRType.uint32 = "uint32_t"
• Lean.IR.EmitC.toCType Lean.IR.IRType.uint64 = "uint64_t"
• Lean.IR.EmitC.toCType Lean.IR.IRType.usize = "size_t"
• Lean.IR.EmitC.toCType Lean.IR.IRType.object = "lean_object*"
• Lean.IR.EmitC.toCType Lean.IR.IRType.tobject = "lean_object*"
• Lean.IR.EmitC.toCType Lean.IR.IRType.irrelevant = "lean_object*"
• Lean.IR.EmitC.toCType (Lean.IR.IRType.struct leanTypeName types) = panicWithPosWithDecl "Lean.Compiler.IR.EmitC" "Lean.IR.EmitC.toCType" 67 25 "not implemented yet"
• Lean.IR.EmitC.toCType (Lean.IR.IRType.union leanTypeName types) = panicWithPosWithDecl "Lean.Compiler.IR.EmitC" "Lean.IR.EmitC.toCType" 68 25 "not implemented yet"

def Lean.IR.EmitC.throwInvalidExportName {α : Type} (n : Name) : M α

Equations

• Lean.IR.EmitC.throwInvalidExportName n = throw (toString "invalid export name '" ++ toString n ++ toString "'")

def Lean.IR.EmitC.toCName (n : Name) : M String

Equations

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

def Lean.IR.EmitC.emitCName (n : Name) : M Unit

Equations

• Lean.IR.EmitC.emitCName n = Lean.IR.EmitC.toCName n >>= Lean.IR.EmitC.emit

def Lean.IR.EmitC.toCInitName (n : Name) : M String

Equations

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

def Lean.IR.EmitC.emitCInitName (n : Name) : M Unit

Equations

• Lean.IR.EmitC.emitCInitName n = Lean.IR.EmitC.toCInitName n >>= Lean.IR.EmitC.emit

def Lean.IR.EmitC.emitFnDeclAux (decl : Decl) (cppBaseName : String) (isExternal : Bool) : M Unit

Equations

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

def Lean.IR.EmitC.emitFnDecl (decl : Decl) (isExternal : Bool) : M Unit

Equations

• Lean.IR.EmitC.emitFnDecl decl isExternal = do let cppBaseName ← Lean.IR.EmitC.toCName decl.name Lean.IR.EmitC.emitFnDeclAux decl cppBaseName isExternal

def Lean.IR.EmitC.emitExternDeclAux (decl : Decl) (cNameStr : String) : M Unit

Equations

• Lean.IR.EmitC.emitExternDeclAux decl cNameStr = do let env ← Lean.IR.EmitC.getEnv let extC : Bool := Lean.isExternC env decl.name Lean.IR.EmitC.emitFnDeclAux decl cNameStr extC

def Lean.IR.EmitC.emitFnDecls : M Unit

Equations

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

def Lean.IR.EmitC.emitMainFn : M Unit

Equations

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

def Lean.IR.EmitC.hasMainFn : M Bool

Equations

• Lean.IR.EmitC.hasMainFn = do let env ← Lean.IR.EmitC.getEnv let decls : List Lean.IR.Decl := Lean.IR.getDecls env pure (decls.any fun (d : Lean.IR.Decl) => d.name == `main)

def Lean.IR.EmitC.emitMainFnIfNeeded : M Unit

Equations

• Lean.IR.EmitC.emitMainFnIfNeeded = do let __do_lift ← Lean.IR.EmitC.hasMainFn if __do_lift = true then Lean.IR.EmitC.emitMainFn else pure PUnit.unit

def Lean.IR.EmitC.emitFileHeader : M Unit

Equations

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

def Lean.IR.EmitC.emitFileFooter : M Unit

Equations

• Lean.IR.EmitC.emitFileFooter = Lean.IR.EmitC.emitLns ["#ifdef __cplusplus", "}", "#endif"]

def Lean.IR.EmitC.throwUnknownVar {α : Type} (x : VarId) : M α

Equations

• Lean.IR.EmitC.throwUnknownVar x = throw (toString "unknown variable '" ++ toString x ++ toString "'")

def Lean.IR.EmitC.getJPParams (j : JoinPointId) : M (Array Param)

Equations

• Lean.IR.EmitC.getJPParams j = do let ctx ← read match ctx.jpMap[j]? with | some ps => pure ps | none => throw "unknown join point"

def Lean.IR.EmitC.declareVar (x : VarId) (t : IRType) : M Unit

Equations

• Lean.IR.EmitC.declareVar x t = do Lean.IR.EmitC.emit (Lean.IR.EmitC.toCType t) Lean.IR.EmitC.emit " " Lean.IR.EmitC.emit x Lean.IR.EmitC.emit "; "

def Lean.IR.EmitC.declareParams (ps : Array Param) : M Unit

Equations

• Lean.IR.EmitC.declareParams ps = Array.forM (fun (p : Lean.IR.Param) => Lean.IR.EmitC.declareVar p.x p.ty) ps

partial def Lean.IR.EmitC.declareVars : FnBody → Bool → M Bool

def Lean.IR.EmitC.emitTag (x : VarId) (xType : IRType) : M Unit

Equations

• Lean.IR.EmitC.emitTag x xType = if xType.isObj = true then do Lean.IR.EmitC.emit "lean_obj_tag(" Lean.IR.EmitC.emit x Lean.IR.EmitC.emit ")" else Lean.IR.EmitC.emit x

def Lean.IR.EmitC.isIf (alts : Array Alt) : Option (Nat × FnBody × FnBody)

Equations

• Lean.IR.EmitC.isIf alts = if h : alts.size ≠ 2 then none else match alts[0] with | Lean.IR.Alt.ctor c b => some (c.cidx, b, alts[1].body) | x => none

def Lean.IR.EmitC.emitInc (x : VarId) (n : Nat) (checkRef : Bool) : M Unit

Equations

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

def Lean.IR.EmitC.emitDec (x : VarId) (n : Nat) (checkRef : Bool) : M Unit

Equations

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

def Lean.IR.EmitC.emitDel (x : VarId) : M Unit

Equations

• Lean.IR.EmitC.emitDel x = do Lean.IR.EmitC.emit "lean_free_object(" Lean.IR.EmitC.emit x Lean.IR.EmitC.emitLn ");"

def Lean.IR.EmitC.emitSetTag (x : VarId) (i : Nat) : M Unit

Equations

• Lean.IR.EmitC.emitSetTag x i = do Lean.IR.EmitC.emit "lean_ctor_set_tag(" Lean.IR.EmitC.emit x Lean.IR.EmitC.emit ", " Lean.IR.EmitC.emit i Lean.IR.EmitC.emitLn ");"

def Lean.IR.EmitC.emitSet (x : VarId) (i : Nat) (y : Arg) : M Unit

Equations

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

def Lean.IR.EmitC.emitOffset (n offset : Nat) : M Unit

Equations

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

def Lean.IR.EmitC.emitUSet (x : VarId) (n : Nat) (y : VarId) : M Unit

Equations

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

def Lean.IR.EmitC.emitSSet (x : VarId) (n offset : Nat) (y : VarId) (t : IRType) : M Unit

Equations

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

def Lean.IR.EmitC.emitJmp (j : JoinPointId) (xs : Array Arg) : M Unit

Equations

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

def Lean.IR.EmitC.emitLhs (z : VarId) : M Unit

Equations

• Lean.IR.EmitC.emitLhs z = do Lean.IR.EmitC.emit z Lean.IR.EmitC.emit " = "

def Lean.IR.EmitC.emitArgs (ys : Array Arg) : M Unit

Equations

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

def Lean.IR.EmitC.emitCtorScalarSize (usize ssize : Nat) : M Unit

Equations

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

def Lean.IR.EmitC.emitAllocCtor (c : CtorInfo) : M Unit

Equations

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

def Lean.IR.EmitC.emitCtorSetArgs (z : VarId) (ys : Array Arg) : M Unit

Equations

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

def Lean.IR.EmitC.emitCtor (z : VarId) (c : CtorInfo) (ys : Array Arg) : M Unit

Equations

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

def Lean.IR.EmitC.emitReset (z : VarId) (n : Nat) (x : VarId) : M Unit

Equations

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

def Lean.IR.EmitC.emitReuse (z x : VarId) (c : CtorInfo) (updtHeader : Bool) (ys : Array Arg) : M Unit

Equations

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

def Lean.IR.EmitC.emitProj (z : VarId) (i : Nat) (x : VarId) : M Unit

Equations

• Lean.IR.EmitC.emitProj z i x = do Lean.IR.EmitC.emitLhs z Lean.IR.EmitC.emit "lean_ctor_get(" Lean.IR.EmitC.emit x Lean.IR.EmitC.emit ", " Lean.IR.EmitC.emit i Lean.IR.EmitC.emitLn ");"

def Lean.IR.EmitC.emitUProj (z : VarId) (i : Nat) (x : VarId) : M Unit

Equations

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

def Lean.IR.EmitC.emitSProj (z : VarId) (t : IRType) (n offset : Nat) (x : VarId) : M Unit

Equations

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

def Lean.IR.EmitC.toStringArgs (ys : Array Arg) : List String

Equations

• Lean.IR.EmitC.toStringArgs ys = List.map Lean.IR.EmitC.argToCString ys.toList

def Lean.IR.EmitC.emitSimpleExternalCall (f : String) (ps : Array Param) (ys : Array Arg) : M Unit

Equations

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

def Lean.IR.EmitC.emitExternCall (f : FunId) (ps : Array Param) (extData : ExternAttrData) (ys : Array Arg) : M Unit

Equations

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

def Lean.IR.EmitC.emitFullApp (z : VarId) (f : FunId) (ys : Array Arg) : M Unit

Equations

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

def Lean.IR.EmitC.emitPartialApp (z : VarId) (f : FunId) (ys : Array Arg) : M Unit

Equations

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

def Lean.IR.EmitC.emitApp (z f : VarId) (ys : Array Arg) : M Unit

Equations

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

def Lean.IR.EmitC.emitBoxFn (xType : IRType) : M Unit

Equations

• Lean.IR.EmitC.emitBoxFn Lean.IR.IRType.usize = Lean.IR.EmitC.emit "lean_box_usize"
• Lean.IR.EmitC.emitBoxFn Lean.IR.IRType.uint32 = Lean.IR.EmitC.emit "lean_box_uint32"
• Lean.IR.EmitC.emitBoxFn Lean.IR.IRType.uint64 = Lean.IR.EmitC.emit "lean_box_uint64"
• Lean.IR.EmitC.emitBoxFn Lean.IR.IRType.float = Lean.IR.EmitC.emit "lean_box_float"
• Lean.IR.EmitC.emitBoxFn Lean.IR.IRType.float32 = Lean.IR.EmitC.emit "lean_box_float32"
• Lean.IR.EmitC.emitBoxFn xType = Lean.IR.EmitC.emit "lean_box"

def Lean.IR.EmitC.emitBox (z x : VarId) (xType : IRType) : M Unit

Equations

• Lean.IR.EmitC.emitBox z x xType = do Lean.IR.EmitC.emitLhs z Lean.IR.EmitC.emitBoxFn xType Lean.IR.EmitC.emit "(" Lean.IR.EmitC.emit x Lean.IR.EmitC.emitLn ");"

def Lean.IR.EmitC.emitUnbox (z : VarId) (t : IRType) (x : VarId) : M Unit

Equations

• Lean.IR.EmitC.emitUnbox z t x = do Lean.IR.EmitC.emitLhs z Lean.IR.EmitC.emit (Lean.IR.getUnboxOpName t) Lean.IR.EmitC.emit "(" Lean.IR.EmitC.emit x Lean.IR.EmitC.emitLn ");"

def Lean.IR.EmitC.emitIsShared (z x : VarId) : M Unit

Equations

• Lean.IR.EmitC.emitIsShared z x = do Lean.IR.EmitC.emitLhs z Lean.IR.EmitC.emit "!lean_is_exclusive(" Lean.IR.EmitC.emit x Lean.IR.EmitC.emitLn ");"

def Lean.IR.EmitC.toHexDigit (c : Nat) : String

Equations

• Lean.IR.EmitC.toHexDigit c = String.singleton c.digitChar

def Lean.IR.EmitC.quoteString (s : String) : String

Equations

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

def Lean.IR.EmitC.emitNumLit (t : IRType) (v : Nat) : M Unit

Equations

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

def Lean.IR.EmitC.emitLit (z : VarId) (t : IRType) (v : LitVal) : M Unit

Equations

• One or more equations did not get rendered due to their size.
• Lean.IR.EmitC.emitLit z t (Lean.IR.LitVal.num v_2) = do Lean.IR.EmitC.emitLhs z Lean.IR.EmitC.emitNumLit t v_2 Lean.IR.EmitC.emitLn ";"

def Lean.IR.EmitC.emitVDecl (z : VarId) (t : IRType) (v : Expr) : M Unit

Equations

• Lean.IR.EmitC.emitVDecl z t (Lean.IR.Expr.ctor c ys) = Lean.IR.EmitC.emitCtor z c ys
• Lean.IR.EmitC.emitVDecl z t (Lean.IR.Expr.reset n x) = Lean.IR.EmitC.emitReset z n x
• Lean.IR.EmitC.emitVDecl z t (Lean.IR.Expr.reuse x c u ys) = Lean.IR.EmitC.emitReuse z x c u ys
• Lean.IR.EmitC.emitVDecl z t (Lean.IR.Expr.proj i x) = Lean.IR.EmitC.emitProj z i x
• Lean.IR.EmitC.emitVDecl z t (Lean.IR.Expr.uproj i x) = Lean.IR.EmitC.emitUProj z i x
• Lean.IR.EmitC.emitVDecl z t (Lean.IR.Expr.sproj n o x) = Lean.IR.EmitC.emitSProj z t n o x
• Lean.IR.EmitC.emitVDecl z t (Lean.IR.Expr.fap c ys) = Lean.IR.EmitC.emitFullApp z c ys
• Lean.IR.EmitC.emitVDecl z t (Lean.IR.Expr.pap c ys) = Lean.IR.EmitC.emitPartialApp z c ys
• Lean.IR.EmitC.emitVDecl z t (Lean.IR.Expr.ap x ys) = Lean.IR.EmitC.emitApp z x ys
• Lean.IR.EmitC.emitVDecl z t (Lean.IR.Expr.box t_1 x) = Lean.IR.EmitC.emitBox z x t_1
• Lean.IR.EmitC.emitVDecl z t (Lean.IR.Expr.unbox x) = Lean.IR.EmitC.emitUnbox z t x
• Lean.IR.EmitC.emitVDecl z t (Lean.IR.Expr.isShared x) = Lean.IR.EmitC.emitIsShared z x
• Lean.IR.EmitC.emitVDecl z t (Lean.IR.Expr.lit v_2) = Lean.IR.EmitC.emitLit z t v_2

def Lean.IR.EmitC.isTailCall (x : VarId) (v : Expr) (b : FnBody) : M Bool

Equations

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

def Lean.IR.EmitC.paramEqArg (p : Param) (x : Arg) : Bool

Equations

• Lean.IR.EmitC.paramEqArg p (Lean.IR.Arg.var x_2) = (p.x == x_2)
• Lean.IR.EmitC.paramEqArg p x = false

def Lean.IR.EmitC.overwriteParam (ps : Array Param) (ys : Array Arg) : Bool

Given [p_0, ..., p_{n-1}], [y_0, ..., y_{n-1}], representing the assignments

p_0 := y_0,
...
p_{n-1} := y_{n-1}

Return true iff we have (i, j) where j > i, and y_j == p_i. That is, we have

      p_i := y_i,
      ...
      p_j := p_i, -- p_i was overwritten above

Equations

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

def Lean.IR.EmitC.emitTailCall (v : Expr) : M Unit

Equations

• One or more equations did not get rendered due to their size.
• Lean.IR.EmitC.emitTailCall v = throw "bug at emitTailCall"

partial def Lean.IR.EmitC.emitIf (x : VarId) (xType : IRType) (tag : Nat) (t e : FnBody) : M Unit

partial def Lean.IR.EmitC.emitCase (x : VarId) (xType : IRType) (alts : Array Alt) : M Unit

partial def Lean.IR.EmitC.emitBlock (b : FnBody) : M Unit

partial def Lean.IR.EmitC.emitJPs : FnBody → M Unit

partial def Lean.IR.EmitC.emitFnBody (b : FnBody) : M Unit

def Lean.IR.EmitC.emitDeclAux (d : Decl) : M Unit

Equations

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

def Lean.IR.EmitC.emitDecl (d : Decl) : M Unit

Equations

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

def Lean.IR.EmitC.emitFns : M Unit

Equations

• Lean.IR.EmitC.emitFns = do let env ← Lean.IR.EmitC.getEnv let decls : List Lean.IR.Decl := Lean.IR.getDecls env decls.reverse.forM Lean.IR.EmitC.emitDecl

def Lean.IR.EmitC.emitMarkPersistent (d : Decl) (n : Name) : M Unit

Equations

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

def Lean.IR.EmitC.emitDeclInit (d : Decl) : M Unit

Equations

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

def Lean.IR.EmitC.emitInitFn : M Unit

Equations

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

def Lean.IR.EmitC.main : M Unit

Equations

• Lean.IR.EmitC.main = do Lean.IR.EmitC.emitFileHeader Lean.IR.EmitC.emitFnDecls Lean.IR.EmitC.emitFns Lean.IR.EmitC.emitInitFn Lean.IR.EmitC.emitMainFnIfNeeded Lean.IR.EmitC.emitFileFooter

@[export lean_ir_emit_c]

def Lean.IR.emitC (env : Environment) (modName : Name) : Except String String

Equations

• Lean.IR.emitC env modName = match (Lean.IR.EmitC.main { env := env, modName := modName }).run "" with | EStateM.Result.ok a s => Except.ok s | EStateM.Result.error err a => Except.error err