Documentation

Lean.Compiler.IR.EmitC

source
def Lean.IR.EmitC.leanMainFn :
String
Equations
source
structure Lean.IR.EmitC.Context :
Type
source
@[reducible, inline]
abbrev Lean.IR.EmitC.M (α : Type) :
Type
Equations
source
def Lean.IR.EmitC.getEnv :
M Environment
Equations
source
def Lean.IR.EmitC.getModName :
M Name
Equations
source
def Lean.IR.EmitC.getDecl (n : Name) :
M Decl
Equations
  • One or more equations did not get rendered due to their size.
source
@[inline]
def Lean.IR.EmitC.emit {α : Type} [ToString α] (a : α) :
M Unit
Equations
source
@[inline]
def Lean.IR.EmitC.emitLn {α : Type} [ToString α] (a : α) :
M Unit
Equations
source
def Lean.IR.EmitC.emitLns {α : Type} [ToString α] (as : List α) :
M Unit
Equations
source
def Lean.IR.EmitC.argToCString (x : Arg) :
String
Equations
source
def Lean.IR.EmitC.emitArg (x : Arg) :
M Unit
Equations
source
def Lean.IR.EmitC.toCType :
IRType → String
Equations
source
def Lean.IR.EmitC.throwInvalidExportName {α : Type} (n : Name) :
M α
Equations
source
def Lean.IR.EmitC.toCName (n : Name) :
M String
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.IR.EmitC.emitCName (n : Name) :
M Unit
Equations
source
def Lean.IR.EmitC.toCInitName (n : Name) :
M String
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.IR.EmitC.emitCInitName (n : Name) :
M Unit
Equations
source
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.
source
def Lean.IR.EmitC.emitFnDecl (decl : Decl) (isExternal : Bool) :
M Unit
Equations
source
def Lean.IR.EmitC.emitExternDeclAux (decl : Decl) (cNameStr : String) :
M Unit
Equations
source
def Lean.IR.EmitC.emitFnDecls :
M Unit
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.IR.EmitC.emitMainFn :
M Unit
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.IR.EmitC.hasMainFn :
M Bool
Equations
source
def Lean.IR.EmitC.emitMainFnIfNeeded :
M Unit
Equations
source
def Lean.IR.EmitC.emitFileHeader :
M Unit
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.IR.EmitC.emitFileFooter :
M Unit
Equations
source
def Lean.IR.EmitC.throwUnknownVar {α : Type} (x : VarId) :
M α
Equations
source
def Lean.IR.EmitC.getJPParams (j : JoinPointId) :
M (Array Param)
Equations
source
def Lean.IR.EmitC.declareVar (x : VarId) (t : IRType) :
M Unit
Equations
source
def Lean.IR.EmitC.declareParams (ps : Array Param) :
M Unit
Equations
source
partial def Lean.IR.EmitC.declareVars :
FnBody → Bool → M Bool
source
def Lean.IR.EmitC.emitTag (x : VarId) (xType : IRType) :
M Unit
Equations
source
def Lean.IR.EmitC.isIf (alts : Array Alt) :
Option (Nat × FnBody × FnBody)
Equations
source
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.
source
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.
source
def Lean.IR.EmitC.emitDel (x : VarId) :
M Unit
Equations
source
def Lean.IR.EmitC.emitSetTag (x : VarId) (i : Nat) :
M Unit
Equations
source
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.
source
def Lean.IR.EmitC.emitOffset (n offset : Nat) :
M Unit
Equations
  • One or more equations did not get rendered due to their size.
source
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.
source
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.
source
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.
source
def Lean.IR.EmitC.emitLhs (z : VarId) :
M Unit
Equations
source
def Lean.IR.EmitC.emitArgs (ys : Array Arg) :
M Unit
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.IR.EmitC.emitCtorScalarSize (usize ssize : Nat) :
M Unit
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.IR.EmitC.emitAllocCtor (c : CtorInfo) :
M Unit
Equations
  • One or more equations did not get rendered due to their size.
source
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.
source
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.
source
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.
source
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.
source
def Lean.IR.EmitC.emitProj (z : VarId) (i : Nat) (x : VarId) :
M Unit
Equations
source
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.
source
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.
source
def Lean.IR.EmitC.toStringArgs (ys : Array Arg) :
List String
Equations
source
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.
source
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.
source
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.
source
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.
source
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.
source
def Lean.IR.EmitC.emitBoxFn (xType : IRType) :
M Unit
Equations
source
def Lean.IR.EmitC.emitBox (z x : VarId) (xType : IRType) :
M Unit
Equations
source
def Lean.IR.EmitC.emitUnbox (z : VarId) (t : IRType) (x : VarId) :
M Unit
Equations
source
def Lean.IR.EmitC.emitIsShared (z x : VarId) :
M Unit
Equations
source
def Lean.IR.EmitC.toHexDigit (c : Nat) :
String
Equations
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 : IRType) (v : Nat) :
M Unit
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.IR.EmitC.emitLit (z : VarId) (t : IRType) (v : LitVal) :
M Unit
Equations
source
def Lean.IR.EmitC.emitVDecl (z : VarId) (t : IRType) (v : Expr) :
M Unit
Equations
source
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.
source
def Lean.IR.EmitC.paramEqArg (p : Param) (x : Arg) :
Bool
Equations
source
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.
source
def Lean.IR.EmitC.emitTailCall (v : Expr) :
M Unit
Equations
source
partial def Lean.IR.EmitC.emitIf (x : VarId) (xType : IRType) (tag : Nat) (t e : FnBody) :
M Unit
source
partial def Lean.IR.EmitC.emitCase (x : VarId) (xType : IRType) (alts : Array Alt) :
M Unit
source
partial def Lean.IR.EmitC.emitBlock (b : FnBody) :
M Unit
source
partial def Lean.IR.EmitC.emitJPs :
FnBody → M Unit
source
partial def Lean.IR.EmitC.emitFnBody (b : FnBody) :
M Unit
source
def Lean.IR.EmitC.emitDeclAux (d : Decl) :
M Unit
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.IR.EmitC.emitDecl (d : Decl) :
M Unit
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.IR.EmitC.emitFns :
M Unit
Equations
source
def Lean.IR.EmitC.emitMarkPersistent (d : Decl) (n : Name) :
M Unit
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.IR.EmitC.emitDeclInit (d : Decl) :
M Unit
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.IR.EmitC.emitInitFn :
M Unit
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.IR.EmitC.main :
M Unit
Equations
source
@[export lean_ir_emit_c]
def Lean.IR.emitC (env : Environment) (modName : Name) :
Except String String
Equations