Lean.Compiler.IR.EmitC

source

def Lean.IR.EmitC.leanMainFn:

String

Equations

Lean.IR.EmitC.leanMainFn = "_lean_main"

source

structure Lean.IR.EmitC.Context:

Type

env : Lean.Environment
modName : Lean.Name
jpMap : Lean.IR.JPParamsMap
mainFn : Lean.IR.FunId
mainParams : Array Lean.IR.Param

source

@[inline]

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

Type

Equations

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

source

def Lean.IR.EmitC.getEnv:

Lean.IR.EmitC.M Lean.Environment

Equations

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

source

def Lean.IR.EmitC.getModName:

Lean.IR.EmitC.M Lean.Name

Equations

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

source

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

Lean.IR.EmitC.M Lean.IR.Decl

Equations

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

source

@[inline]

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

Lean.IR.EmitC.M Unit

Equations

Lean.IR.EmitC.emit a = modify fun out => out ++ toString a

source

@[inline]

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

Lean.IR.EmitC.M Unit

Equations

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

source

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

Lean.IR.EmitC.M Unit

Equations

Lean.IR.EmitC.emitLns as = List.forM as fun a => Lean.IR.EmitC.emitLn a

source

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

String

Equations

Lean.IR.EmitC.argToCString x = match x with | Lean.IR.Arg.var x => toString x | x => "lean_box(0)"

source

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

Lean.IR.EmitC.M Unit

Equations

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

source

def Lean.IR.EmitC.toCType:

Lean.IR.IRType → String

Equations

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

source

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

Lean.IR.EmitC.M α

Equations

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

source

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

Lean.IR.EmitC.M String

Equations

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

source

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

Lean.IR.EmitC.M Unit

Equations

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

source

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

Lean.IR.EmitC.M String

Equations

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

source

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

Lean.IR.EmitC.M Unit

Equations

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

source

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

Lean.IR.EmitC.M Unit

Equations

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

source

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

Lean.IR.EmitC.M Unit

Equations

Lean.IR.EmitC.emitFnDecl decl isExternal = do let cppBaseName ← Lean.IR.EmitC.toCName (Lean.IR.Decl.name decl) Lean.IR.EmitC.emitFnDeclAux decl cppBaseName isExternal

source

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

Lean.IR.EmitC.M Unit

Equations

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

source

def Lean.IR.EmitC.emitFnDecls:

Lean.IR.EmitC.M Unit

Equations

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

source

def Lean.IR.EmitC.emitMainFn:

Lean.IR.EmitC.M Unit

Equations

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

source

def Lean.IR.EmitC.hasMainFn:

Lean.IR.EmitC.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 (List.any decls fun d => Lean.IR.Decl.name d == `main)

source

def Lean.IR.EmitC.emitMainFnIfNeeded:

Lean.IR.EmitC.M Unit

Equations

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

source

def Lean.IR.EmitC.emitFileHeader:

Lean.IR.EmitC.M Unit

Equations

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

source

def Lean.IR.EmitC.emitFileFooter:

Lean.IR.EmitC.M Unit

Equations

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

source

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

Lean.IR.EmitC.M α

Equations

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

source

def Lean.IR.EmitC.getJPParams (j : Lean.IR.JoinPointId) :

Lean.IR.EmitC.M (Array Lean.IR.Param)

Equations

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

source

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

Lean.IR.EmitC.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 " "

source

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

Lean.IR.EmitC.M Unit

Equations

Lean.IR.EmitC.declareParams ps = Array.forM (fun p => Lean.IR.EmitC.declareVar p.x p.ty) ps 0 (Array.size ps)

source

partial def Lean.IR.EmitC.declareVars:

Lean.IR.FnBody → Bool → Lean.IR.EmitC.M Bool

source

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

Lean.IR.EmitC.M Unit

Equations

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

source

def Lean.IR.EmitC.isIf (alts : Array Lean.IR.Alt) :

Option (Nat × Lean.IR.FnBody × Lean.IR.FnBody)

Equations

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

source

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

Lean.IR.EmitC.M Unit

Equations

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

source

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

Lean.IR.EmitC.M Unit

Equations

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

source

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

Lean.IR.EmitC.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 ");"

source

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

Lean.IR.EmitC.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 ");"

source

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

Lean.IR.EmitC.M Unit

Equations

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

source

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

Lean.IR.EmitC.M Unit

Equations

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

source

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

Lean.IR.EmitC.M Unit

Equations

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

source

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

Lean.IR.EmitC.M Unit

Equations

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

source

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

Lean.IR.EmitC.M Unit

Equations

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

source

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

Lean.IR.EmitC.M Unit

Equations

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

source

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

Lean.IR.EmitC.M Unit

Equations

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

source

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

Lean.IR.EmitC.M Unit

Equations

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

source

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

Lean.IR.EmitC.M Unit

Equations

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

source

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

Lean.IR.EmitC.M Unit

Equations

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

source

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

Lean.IR.EmitC.M Unit

Equations

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

source

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

Lean.IR.EmitC.M Unit

Equations

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

source

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

Lean.IR.EmitC.M Unit

Equations

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

source

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

Lean.IR.EmitC.M Unit

Equations

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

source

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

Lean.IR.EmitC.M Unit

Equations

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

source

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

Lean.IR.EmitC.M Unit

Equations

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

source

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

List String

Equations

Lean.IR.EmitC.toStringArgs ys = List.map Lean.IR.EmitC.argToCString (Array.toList ys)

source

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

Lean.IR.EmitC.M Unit

Equations

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

source

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

Lean.IR.EmitC.M Unit

Equations

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

source

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

Lean.IR.EmitC.M Unit

Equations

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

source

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

Lean.IR.EmitC.M Unit

Equations

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

source

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

Lean.IR.EmitC.M Unit

Equations

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

source

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

Lean.IR.EmitC.M Unit

Equations

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

source

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

Lean.IR.EmitC.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 ");"

source

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

Lean.IR.EmitC.M Unit

Equations

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

source

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

Lean.IR.EmitC.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 ");"

source

def Lean.IR.EmitC.emitIsTaggedPtr (z : Lean.IR.VarId) (x : Lean.IR.VarId) :

Lean.IR.EmitC.M Unit

Equations

Lean.IR.EmitC.emitIsTaggedPtr z x = do Lean.IR.EmitC.emitLhs z Lean.IR.EmitC.emit "!lean_is_scalar(" Lean.IR.EmitC.emit x Lean.IR.EmitC.emitLn ");"

source

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

String

Equations

Lean.IR.EmitC.toHexDigit c = String.singleton (Nat.digitChar c)

source

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

String

Equations

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

source

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

Lean.IR.EmitC.M Unit

Equations

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

source

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

Lean.IR.EmitC.M Unit

Equations

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

source

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

Lean.IR.EmitC.M Unit

Equations

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

source

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

Lean.IR.EmitC.M Bool

Equations

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

source

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

Bool

Equations

Lean.IR.EmitC.paramEqArg p x = match x with | Lean.IR.Arg.var x => p.x == x | x => false

source

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

Bool

Equations

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

source

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

Lean.IR.EmitC.M Unit

Equations

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

source

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

Lean.IR.EmitC.M Unit

source

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

Lean.IR.EmitC.M Unit

source

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

Lean.IR.EmitC.M Unit

source

partial def Lean.IR.EmitC.emitJPs:

Lean.IR.FnBody → Lean.IR.EmitC.M Unit

source

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

Lean.IR.EmitC.M Unit

source

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

Lean.IR.EmitC.M Unit

Equations

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

source

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

Lean.IR.EmitC.M Unit

Equations

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

source

def Lean.IR.EmitC.emitFns:

Lean.IR.EmitC.M Unit

Equations

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

source

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

Lean.IR.EmitC.M Unit

Equations

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

source

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

Lean.IR.EmitC.M Unit

Equations

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

source

def Lean.IR.EmitC.emitInitFn:

Lean.IR.EmitC.M Unit

Equations

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

source

def Lean.IR.EmitC.main:

Lean.IR.EmitC.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

source

@[export lean_ir_emit_c]

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

Except String String

Equations

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