Equations
- Lean.IR.EmitC.leanMainFn = "_lean_main"
Instances For
- env : Lean.Environment
- modName : Lake.Name
- jpMap : Lean.IR.JPParamsMap
- mainFn : Lean.IR.FunId
- mainParams : Array Lean.IR.Param
Instances For
@[reducible, inline]
Equations
Instances For
Equations
Instances For
Equations
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[inline]
Instances For
@[inline]
Equations
- Lean.IR.EmitC.emitLn a = do Lean.IR.EmitC.emit a Lean.IR.EmitC.emit "\n"
Instances For
Equations
- Lean.IR.EmitC.emitLns as = as.forM fun (a : α) => Lean.IR.EmitC.emitLn a
Instances For
Equations
- Lean.IR.EmitC.argToCString x = match x with | Lean.IR.Arg.var x => toString x | x => "lean_box(0)"
Instances For
Equations
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- Lean.IR.EmitC.emitCName n = Lean.IR.EmitC.toCName n >>= Lean.IR.EmitC.emit
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- Lean.IR.EmitC.emitCInitName n = Lean.IR.EmitC.toCInitName n >>= Lean.IR.EmitC.emit
Instances For
Equations
- Lean.IR.EmitC.shouldExport n = !`Lean.Compiler.LCNF.isPrefixOf n
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- Lean.IR.EmitC.emitFnDecl decl isExternal = do let cppBaseName ← Lean.IR.EmitC.toCName decl.name Lean.IR.EmitC.emitFnDeclAux decl cppBaseName isExternal
Instances For
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
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
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)
Instances For
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
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
Instances For
Equations
- Lean.IR.EmitC.getJPParams j = do let ctx ← read match Lean.HashMap.find? ctx.jpMap j with | some ps => pure ps | none => throw "unknown join point"
Instances For
Equations
Instances For
Equations
- Lean.IR.EmitC.declareParams ps = Array.forM (fun (p : Lean.IR.Param) => Lean.IR.EmitC.declareVar p.x p.ty) ps 0
Instances For
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
Instances For
Equations
- Lean.IR.EmitC.isIf alts = if (alts.size != 2) = true then none else match alts[0]! with | Lean.IR.AltCore.ctor c b => some (c.cidx, b, Lean.IR.AltCore.body alts[1]!) | x => none
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- Lean.IR.EmitC.emitDel x = do Lean.IR.EmitC.emit "lean_free_object(" Lean.IR.EmitC.emit x Lean.IR.EmitC.emitLn ");"
Instances For
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 ");"
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
def
Lean.IR.EmitC.emitSSet
(x : Lean.IR.VarId)
(n : Nat)
(offset : Nat)
(y : Lean.IR.VarId)
(t : Lean.IR.IRType)
:
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- Lean.IR.EmitC.emitLhs z = do Lean.IR.EmitC.emit z Lean.IR.EmitC.emit " = "
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
def
Lean.IR.EmitC.emitReuse
(z : Lean.IR.VarId)
(x : Lean.IR.VarId)
(c : Lean.IR.CtorInfo)
(updtHeader : Bool)
(ys : Array Lean.IR.Arg)
:
Equations
- One or more equations did not get rendered due to their size.
Instances For
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 ");"
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
def
Lean.IR.EmitC.emitSProj
(z : Lean.IR.VarId)
(t : Lean.IR.IRType)
(n : Nat)
(offset : Nat)
(x : Lean.IR.VarId)
:
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- Lean.IR.EmitC.toStringArgs ys = List.map Lean.IR.EmitC.argToCString ys.toList
Instances For
def
Lean.IR.EmitC.emitSimpleExternalCall
(f : String)
(ps : Array Lean.IR.Param)
(ys : Array Lean.IR.Arg)
:
Equations
- One or more equations did not get rendered due to their size.
Instances For
def
Lean.IR.EmitC.emitExternCall
(f : Lean.IR.FunId)
(ps : Array Lean.IR.Param)
(extData : Lean.ExternAttrData)
(ys : Array Lean.IR.Arg)
:
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
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 ");"
Instances For
Equations
Instances For
Equations
- Lean.IR.EmitC.toHexDigit c = String.singleton c.digitChar
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- Lean.IR.EmitC.paramEqArg p x = match x with | Lean.IR.Arg.var x => p.x == x | x => false
Instances For
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
- Lean.IR.EmitC.overwriteParam ps ys = let n := ps.size; Nat.any (fun (i : Nat) => let p := ps[i]!; Prod.anyI (fun (j : Nat) => Lean.IR.EmitC.paramEqArg p ys[j]!) (i + 1, n)) n
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
partial def
Lean.IR.EmitC.emitIf
(x : Lean.IR.VarId)
(xType : Lean.IR.IRType)
(tag : Nat)
(t : Lean.IR.FnBody)
(e : Lean.IR.FnBody)
:
partial def
Lean.IR.EmitC.emitCase
(x : Lean.IR.VarId)
(xType : Lean.IR.IRType)
(alts : Array Lean.IR.Alt)
:
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
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
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[export lean_ir_emit_c]
Equations
- One or more equations did not get rendered due to their size.