- env : Lean.Environment
- modName : Lean.Name
- jpMap : Lean.IR.JPParamsMap
- mainFn : Lean.IR.FunId
- mainParams : Array Lean.IR.Param
@[inline]
Equations
Equations
Equations
Equations
- Lean.IR.EmitC.getDecl n = do let env ← Lean.IR.EmitC.getEnv match Lean.IR.findEnvDecl env n with | some d => pure d | none => throw (toString "unknown declaration '" ++ toString n ++ toString "'")
@[inline]
Equations
- Lean.IR.EmitC.emit a = modify fun out => out ++ toString a
@[inline]
Equations
- Lean.IR.EmitC.emitLn a = do Lean.IR.EmitC.emit a Lean.IR.EmitC.emit "\n"
Equations
- Lean.IR.EmitC.emitLns as = List.forM as fun a => Lean.IR.EmitC.emitLn a
Equations
- Lean.IR.EmitC.argToCString x = match x with | Lean.IR.Arg.var x => toString x | x => "lean_box(0)"
Equations
Equations
- Lean.IR.EmitC.toCType x = match x with | Lean.IR.IRType.float => "double" | Lean.IR.IRType.uint8 => "uint8_t" | Lean.IR.IRType.uint16 => "uint16_t" | Lean.IR.IRType.uint32 => "uint32_t" | Lean.IR.IRType.uint64 => "uint64_t" | Lean.IR.IRType.usize => "size_t" | Lean.IR.IRType.object => "lean_object*" | Lean.IR.IRType.tobject => "lean_object*" | Lean.IR.IRType.irrelevant => "lean_object*" | Lean.IR.IRType.struct x x_1 => panicWithPosWithDecl "Lean.Compiler.IR.EmitC" "Lean.IR.EmitC.toCType" 65 25 "not implemented yet" | Lean.IR.IRType.union x x_1 => panicWithPosWithDecl "Lean.Compiler.IR.EmitC" "Lean.IR.EmitC.toCType" 66 25 "not implemented yet"
Equations
- Lean.IR.EmitC.toCName n = do let env ← Lean.IR.EmitC.getEnv match Lean.getExportNameFor env n with | some (Lean.Name.str Lean.Name.anonymous s x) => pure s | some x => Lean.IR.EmitC.throwInvalidExportName n | none => if (n == `main) = true then pure Lean.IR.EmitC.leanMainFn else pure (Lean.Name.mangle n)
Equations
- Lean.IR.EmitC.emitCName n = Lean.IR.EmitC.toCName n >>= Lean.IR.EmitC.emit
Equations
- Lean.IR.EmitC.toCInitName n = do let env ← Lean.IR.EmitC.getEnv match Lean.getExportNameFor env n with | some (Lean.Name.str Lean.Name.anonymous s x) => pure ("_init_" ++ s) | some x => Lean.IR.EmitC.throwInvalidExportName n | none => pure ("_init_" ++ Lean.Name.mangle n)
Equations
- Lean.IR.EmitC.emitCInitName n = Lean.IR.EmitC.toCInitName n >>= Lean.IR.EmitC.emit
Equations
- Lean.IR.EmitC.emitFnDeclAux decl cppBaseName isExternal = let ps := Lean.IR.Decl.params decl; do let env ← Lean.IR.EmitC.getEnv let _do_jp : Unit → Lean.IR.EmitC.M Unit := fun y => do Lean.IR.EmitC.emit (Lean.IR.EmitC.toCType (Lean.IR.Decl.resultType decl) ++ " " ++ cppBaseName) let _do_jp : PUnit → Lean.IR.EmitC.M Unit := fun y => Lean.IR.EmitC.emitLn ";" if Array.isEmpty ps = true then do let y ← pure PUnit.unit _do_jp y else do Lean.IR.EmitC.emit "(" let ps : Array Lean.IR.Param := if Lean.isExternC env (Lean.IR.Decl.name decl) = true then Array.filter (fun p => !Lean.IR.IRType.isIrrelevant p.ty) ps 0 (Array.size ps) else ps let _do_jp : Unit → Lean.IR.EmitC.M Unit := fun y => do let y ← Lean.IR.EmitC.emit ")" _do_jp y if (decide (Array.size ps > Lean.closureMaxArgs) && Lean.IR.ExplicitBoxing.isBoxedName (Lean.IR.Decl.name decl)) = true then do let y ← Lean.IR.EmitC.emit "lean_object**" _do_jp y else do let y ← Nat.forM (Array.size ps) fun i => let _do_jp := fun y => Lean.IR.EmitC.emit (Lean.IR.EmitC.toCType (Array.getOp ps i).ty); if i > 0 then do let y ← Lean.IR.EmitC.emit ", " _do_jp y else do let y ← pure PUnit.unit _do_jp y _do_jp y if Array.isEmpty ps = true then if Lean.isClosedTermName env (Lean.IR.Decl.name decl) = true then do let y ← Lean.IR.EmitC.emit "static " _do_jp y else if isExternal = true then do let y ← Lean.IR.EmitC.emit "extern " _do_jp y else do let y ← Lean.IR.EmitC.emit "LEAN_EXPORT " _do_jp y else if (!isExternal) = true then do let y ← Lean.IR.EmitC.emit "LEAN_EXPORT " _do_jp y else do let y ← pure PUnit.unit _do_jp y
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
Equations
- Lean.IR.EmitC.emitExternDeclAux decl cNameStr = let cName := Lean.Name.mkSimple 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
Equations
- Lean.IR.EmitC.emitFnDecls = do let env ← Lean.IR.EmitC.getEnv let decls : List Lean.IR.Decl := Lean.IR.getDecls env let modDecls : Lean.NameSet := List.foldl (fun s d => Lean.NameSet.insert s (Lean.IR.Decl.name d)) ∅ decls let usedDecls : Lean.NameSet := List.foldl (fun s d => Lean.IR.collectUsedDecls env d (Lean.NameSet.insert s (Lean.IR.Decl.name d))) ∅ decls let usedDecls : List Lean.Name := Std.RBTree.toList usedDecls List.forM usedDecls fun n => do let decl ← Lean.IR.EmitC.getDecl n match Lean.getExternNameFor env `c (Lean.IR.Decl.name decl) with | some cName => Lean.IR.EmitC.emitExternDeclAux decl cName | none => Lean.IR.EmitC.emitFnDecl decl !Lean.NameSet.contains modDecls n
Equations
-
Lean.IR.EmitC.emitMainFn = do
let d ← Lean.IR.EmitC.getDecl `main
match d with
| Lean.IR.Decl.fdecl f xs t b x =>
let _do_jp := fun y => do
let env ← Lean.IR.EmitC.getEnv
let usesLeanAPI : Bool := Lean.IR.usesModuleFrom env `Lean
let _do_jp : Unit → Lean.IR.EmitC.M Unit := fun y => do
Lean.IR.EmitC.emitLn
"\n #if defined(WIN32) || defined(_WIN32)\n #include
\n #endif\n\n int main(int argc, char ** argv) {\n #if defined(WIN32) || defined(_WIN32)\n SetErrorMode(SEM_FAILCRITICALERRORS);\n #endif\n lean_object* in; lean_object* res;" let _do_jp : Unit → Lean.IR.EmitC.M Unit := fun y => do let modName ← Lean.IR.EmitC.getModName Lean.IR.EmitC.emitLn "lean_set_panic_messages(false);" Lean.IR.EmitC.emitLn ("res = " ++ Lean.mkModuleInitializationFunctionName modName ++ "(1 /* builtin */, lean_io_mk_world());") Lean.IR.EmitC.emitLn "lean_set_panic_messages(true);" Lean.IR.EmitC.emitLns ["lean_io_mark_end_initialization();", "if (lean_io_result_is_ok(res)) {", "lean_dec_ref(res);", "lean_init_task_manager();"] let _do_jp : Unit → Lean.IR.EmitC.M Unit := fun y => do Lean.IR.EmitC.emitLn "}" let retTy : Lean.Expr := Lean.Expr.getForallBody (Lean.ConstantInfo.type (Option.get! (Lean.Environment.find? env `main))) let retTy : Lean.Expr := Lean.Expr.appArg! retTy Lean.IR.EmitC.emitLns ["lean_finalize_task_manager();", "if (lean_io_result_is_ok(res)) {", " int ret = " ++ if (Lean.Expr.constName? retTy == some `UInt32) = true then "lean_unbox_uint32(lean_io_result_get_value(res));" else "0;", " lean_dec_ref(res);", " return ret;", "} else {", " lean_io_result_show_error(res);", " lean_dec_ref(res);", " return 1;", "}"] Lean.IR.EmitC.emitLn "}" if (Array.size xs == 2) = true then do Lean.IR.EmitC.emitLns ["in = lean_box(0);", "int i = argc;", "while (i > 1) {", " lean_object* n;", " i--;", " n = lean_alloc_ctor(1,2,0); lean_ctor_set(n, 0, lean_mk_string(argv[i])); lean_ctor_set(n, 1, in);", " in = n;", "}"] let y ← Lean.IR.EmitC.emitLn ("res = " ++ Lean.IR.EmitC.leanMainFn ++ "(in, lean_io_mk_world());") _do_jp y else do let y ← Lean.IR.EmitC.emitLn ("res = " ++ Lean.IR.EmitC.leanMainFn ++ "(lean_io_mk_world());") _do_jp y if usesLeanAPI = true then do let y ← Lean.IR.EmitC.emitLn "lean_initialize();" _do_jp y else do let y ← Lean.IR.EmitC.emitLn "lean_initialize_runtime_module();" _do_jp y if usesLeanAPI = true then do let y ← Lean.IR.EmitC.emitLn "void lean_initialize();" _do_jp y else do let y ← Lean.IR.EmitC.emitLn "void lean_initialize_runtime_module();" _do_jp y; if (Array.size xs == 2 || Array.size xs == 1) = true then do let y ← pure PUnit.unit _do_jp y else do let y ← throw "invalid main function, incorrect arity when generating code" _do_jp y | other => throw "function declaration expected"
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)
Equations
- Lean.IR.EmitC.emitMainFnIfNeeded = do let a ← Lean.IR.EmitC.hasMainFn if a = true then Lean.IR.EmitC.emitMainFn else pure PUnit.unit
Equations
-
Lean.IR.EmitC.emitFileHeader = do
let env ← Lean.IR.EmitC.getEnv
let modName ← Lean.IR.EmitC.getModName
Lean.IR.EmitC.emitLn "// Lean compiler output"
Lean.IR.EmitC.emitLn ("// Module: " ++ toString modName)
Lean.IR.EmitC.emit "// Imports:"
Array.forM (fun m => Lean.IR.EmitC.emit (" " ++ toString m)) (Lean.Environment.imports env) 0
(Array.size (Lean.Environment.imports env))
Lean.IR.EmitC.emitLn ""
Lean.IR.EmitC.emitLn "#include
" Lean.IR.EmitC.emitLns ["#if defined(__clang__)", "#pragma clang diagnostic ignored \"-Wunused-parameter\"", "#pragma clang diagnostic ignored \"-Wunused-label\"", "#elif defined(__GNUC__) && !defined(__CLANG__)", "#pragma GCC diagnostic ignored \"-Wunused-parameter\"", "#pragma GCC diagnostic ignored \"-Wunused-label\"", "#pragma GCC diagnostic ignored \"-Wunused-but-set-variable\"", "#endif", "#ifdef __cplusplus", "extern \"C\" {", "#endif"]
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"
Equations
Equations
- Lean.IR.EmitC.declareParams ps = Array.forM (fun p => Lean.IR.EmitC.declareVar p.x p.ty) ps 0 (Array.size ps)
Equations
- Lean.IR.EmitC.emitTag x xType = if Lean.IR.IRType.isObj xType = 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
Equations
- Lean.IR.EmitC.isIf alts = if (Array.size alts != 2) = true then none else match Array.getOp alts 0 with | Lean.IR.AltCore.ctor c b => some (c.cidx, b, Lean.IR.AltCore.body (Array.getOp alts 1)) | x => none
Equations
- Lean.IR.EmitC.emitInc x n checkRef = do Lean.IR.EmitC.emit (if checkRef = true then if (n == 1) = true then "lean_inc" else "lean_inc_n" else if (n == 1) = true then "lean_inc_ref" else "lean_inc_ref_n") Lean.IR.EmitC.emit "(" Lean.IR.EmitC.emit x let _do_jp : Unit → Lean.IR.EmitC.M Unit := fun y => Lean.IR.EmitC.emitLn ");" if (n != 1) = true then do Lean.IR.EmitC.emit ", " let y ← Lean.IR.EmitC.emit n _do_jp y else do let y ← pure PUnit.unit _do_jp y
Equations
- Lean.IR.EmitC.emitDec x n checkRef = do Lean.IR.EmitC.emit (if checkRef = true then "lean_dec" else "lean_dec_ref") Lean.IR.EmitC.emit "(" Lean.IR.EmitC.emit x let _do_jp : Unit → Lean.IR.EmitC.M Unit := fun y => Lean.IR.EmitC.emitLn ");" if (n != 1) = true then do Lean.IR.EmitC.emit ", " let y ← Lean.IR.EmitC.emit n _do_jp y else do let y ← pure PUnit.unit _do_jp y
Equations
- Lean.IR.EmitC.emitDel x = do Lean.IR.EmitC.emit "lean_free_object(" Lean.IR.EmitC.emit x Lean.IR.EmitC.emitLn ");"
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 ");"
Equations
- Lean.IR.EmitC.emitSet x i y = do Lean.IR.EmitC.emit "lean_ctor_set(" Lean.IR.EmitC.emit x Lean.IR.EmitC.emit ", " Lean.IR.EmitC.emit i Lean.IR.EmitC.emit ", " Lean.IR.EmitC.emitArg y Lean.IR.EmitC.emitLn ");"
Equations
- Lean.IR.EmitC.emitOffset n offset = if n > 0 then do Lean.IR.EmitC.emit "sizeof(void*)*" Lean.IR.EmitC.emit n if offset > 0 then do Lean.IR.EmitC.emit " + " Lean.IR.EmitC.emit offset else pure PUnit.unit else Lean.IR.EmitC.emit offset
Equations
- Lean.IR.EmitC.emitUSet x n y = do Lean.IR.EmitC.emit "lean_ctor_set_usize(" Lean.IR.EmitC.emit x Lean.IR.EmitC.emit ", " Lean.IR.EmitC.emit n Lean.IR.EmitC.emit ", " Lean.IR.EmitC.emit y Lean.IR.EmitC.emitLn ");"
def
Lean.IR.EmitC.emitSSet
(x : Lean.IR.VarId)
(n : Nat)
(offset : Nat)
(y : Lean.IR.VarId)
(t : Lean.IR.IRType)
:
Equations
- Lean.IR.EmitC.emitSSet x n offset y t = let _do_jp := fun y => do Lean.IR.EmitC.emit "(" Lean.IR.EmitC.emit x Lean.IR.EmitC.emit ", " Lean.IR.EmitC.emitOffset n offset Lean.IR.EmitC.emit ", " Lean.IR.EmitC.emit y Lean.IR.EmitC.emitLn ");"; match t with | Lean.IR.IRType.float => do let y ← Lean.IR.EmitC.emit "lean_ctor_set_float" _do_jp y | Lean.IR.IRType.uint8 => do let y ← Lean.IR.EmitC.emit "lean_ctor_set_uint8" _do_jp y | Lean.IR.IRType.uint16 => do let y ← Lean.IR.EmitC.emit "lean_ctor_set_uint16" _do_jp y | Lean.IR.IRType.uint32 => do let y ← Lean.IR.EmitC.emit "lean_ctor_set_uint32" _do_jp y | Lean.IR.IRType.uint64 => do let y ← Lean.IR.EmitC.emit "lean_ctor_set_uint64" _do_jp y | x => do let y ← throw "invalid instruction" _do_jp y
Equations
- Lean.IR.EmitC.emitJmp j xs = do let ps ← Lean.IR.EmitC.getJPParams j let _do_jp : PUnit → Lean.IR.EmitC.M Unit := fun y => do Nat.forM (Array.size xs) fun i => let p := Array.getOp ps i; let x := Array.getOp xs i; do Lean.IR.EmitC.emit p.x Lean.IR.EmitC.emit " = " Lean.IR.EmitC.emitArg x Lean.IR.EmitC.emitLn ";" Lean.IR.EmitC.emit "goto " Lean.IR.EmitC.emit j Lean.IR.EmitC.emitLn ";" if (Array.size xs == Array.size ps) = true then do let y ← pure PUnit.unit _do_jp y else do let y ← throw "invalid goto" _do_jp y
Equations
- Lean.IR.EmitC.emitLhs z = do Lean.IR.EmitC.emit z Lean.IR.EmitC.emit " = "
Equations
- Lean.IR.EmitC.emitArgs ys = Nat.forM (Array.size ys) fun i => let _do_jp := fun y => Lean.IR.EmitC.emitArg (Array.getOp ys i); if i > 0 then do let y ← Lean.IR.EmitC.emit ", " _do_jp y else do let y ← pure PUnit.unit _do_jp y
Equations
- Lean.IR.EmitC.emitCtorScalarSize usize ssize = if (usize == 0) = true then Lean.IR.EmitC.emit ssize else if (ssize == 0) = true then do Lean.IR.EmitC.emit "sizeof(size_t)*" Lean.IR.EmitC.emit usize else do Lean.IR.EmitC.emit "sizeof(size_t)*" Lean.IR.EmitC.emit usize Lean.IR.EmitC.emit " + " Lean.IR.EmitC.emit ssize
Equations
- Lean.IR.EmitC.emitAllocCtor c = do Lean.IR.EmitC.emit "lean_alloc_ctor(" Lean.IR.EmitC.emit c.cidx Lean.IR.EmitC.emit ", " Lean.IR.EmitC.emit c.size Lean.IR.EmitC.emit ", " Lean.IR.EmitC.emitCtorScalarSize c.usize c.ssize Lean.IR.EmitC.emitLn ");"
Equations
- Lean.IR.EmitC.emitCtorSetArgs z ys = Nat.forM (Array.size ys) fun i => do Lean.IR.EmitC.emit "lean_ctor_set(" Lean.IR.EmitC.emit z Lean.IR.EmitC.emit ", " Lean.IR.EmitC.emit i Lean.IR.EmitC.emit ", " Lean.IR.EmitC.emitArg (Array.getOp ys i) Lean.IR.EmitC.emitLn ");"
Equations
- Lean.IR.EmitC.emitCtor z c ys = do Lean.IR.EmitC.emitLhs z if (c.size == 0 && c.usize == 0 && c.ssize == 0) = true then do Lean.IR.EmitC.emit "lean_box(" Lean.IR.EmitC.emit c.cidx Lean.IR.EmitC.emitLn ");" else do Lean.IR.EmitC.emitAllocCtor c Lean.IR.EmitC.emitCtorSetArgs z ys
Equations
- Lean.IR.EmitC.emitReset z n x = do Lean.IR.EmitC.emit "if (lean_is_exclusive(" Lean.IR.EmitC.emit x Lean.IR.EmitC.emitLn ")) {" Nat.forM n fun i => do Lean.IR.EmitC.emit " lean_ctor_release(" Lean.IR.EmitC.emit x Lean.IR.EmitC.emit ", " Lean.IR.EmitC.emit i Lean.IR.EmitC.emitLn ");" Lean.IR.EmitC.emit " " Lean.IR.EmitC.emitLhs z Lean.IR.EmitC.emit x Lean.IR.EmitC.emitLn ";" Lean.IR.EmitC.emitLn "} else {" Lean.IR.EmitC.emit " lean_dec_ref(" Lean.IR.EmitC.emit x Lean.IR.EmitC.emitLn ");" Lean.IR.EmitC.emit " " Lean.IR.EmitC.emitLhs z Lean.IR.EmitC.emitLn "lean_box(0);" Lean.IR.EmitC.emitLn "}"
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
- Lean.IR.EmitC.emitReuse z x c updtHeader ys = do Lean.IR.EmitC.emit "if (lean_is_scalar(" Lean.IR.EmitC.emit x Lean.IR.EmitC.emitLn ")) {" Lean.IR.EmitC.emit " " Lean.IR.EmitC.emitLhs z Lean.IR.EmitC.emitAllocCtor c Lean.IR.EmitC.emitLn "} else {" Lean.IR.EmitC.emit " " Lean.IR.EmitC.emitLhs z Lean.IR.EmitC.emit x Lean.IR.EmitC.emitLn ";" let _do_jp : Unit → Lean.IR.EmitC.M Unit := fun y => do Lean.IR.EmitC.emitLn "}" Lean.IR.EmitC.emitCtorSetArgs z ys if updtHeader = true then do Lean.IR.EmitC.emit " lean_ctor_set_tag(" Lean.IR.EmitC.emit z Lean.IR.EmitC.emit ", " Lean.IR.EmitC.emit c.cidx let y ← Lean.IR.EmitC.emitLn ");" _do_jp y else do let y ← pure PUnit.unit _do_jp y
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 ");"
Equations
- Lean.IR.EmitC.emitUProj z i x = do Lean.IR.EmitC.emitLhs z Lean.IR.EmitC.emit "lean_ctor_get_usize(" Lean.IR.EmitC.emit x Lean.IR.EmitC.emit ", " Lean.IR.EmitC.emit i Lean.IR.EmitC.emitLn ");"
def
Lean.IR.EmitC.emitSProj
(z : Lean.IR.VarId)
(t : Lean.IR.IRType)
(n : Nat)
(offset : Nat)
(x : Lean.IR.VarId)
:
Equations
- Lean.IR.EmitC.emitSProj z t n offset x = do Lean.IR.EmitC.emitLhs z let _do_jp : Unit → Lean.IR.EmitC.M Unit := fun y => do Lean.IR.EmitC.emit "(" Lean.IR.EmitC.emit x Lean.IR.EmitC.emit ", " Lean.IR.EmitC.emitOffset n offset Lean.IR.EmitC.emitLn ");" match t with | Lean.IR.IRType.float => do let y ← Lean.IR.EmitC.emit "lean_ctor_get_float" _do_jp y | Lean.IR.IRType.uint8 => do let y ← Lean.IR.EmitC.emit "lean_ctor_get_uint8" _do_jp y | Lean.IR.IRType.uint16 => do let y ← Lean.IR.EmitC.emit "lean_ctor_get_uint16" _do_jp y | Lean.IR.IRType.uint32 => do let y ← Lean.IR.EmitC.emit "lean_ctor_get_uint32" _do_jp y | Lean.IR.IRType.uint64 => do let y ← Lean.IR.EmitC.emit "lean_ctor_get_uint64" _do_jp y | x => do let y ← throw "invalid instruction" _do_jp y
Equations
def
Lean.IR.EmitC.emitSimpleExternalCall
(f : String)
(ps : Array Lean.IR.Param)
(ys : Array Lean.IR.Arg)
:
Equations
- Lean.IR.EmitC.emitSimpleExternalCall f ps ys = do Lean.IR.EmitC.emit f Lean.IR.EmitC.emit "(" discard (Nat.foldM (fun i first => if Lean.IR.IRType.isIrrelevant (Array.getOp ps i).ty = true then pure first else let _do_jp := fun y => do Lean.IR.EmitC.emitArg (Array.getOp ys i) pure false; if first = true then do let y ← pure PUnit.unit _do_jp y else do let y ← Lean.IR.EmitC.emit ", " _do_jp y) true (Array.size ys)) Lean.IR.EmitC.emitLn ");" pure ()
def
Lean.IR.EmitC.emitExternCall
(f : Lean.IR.FunId)
(ps : Array Lean.IR.Param)
(extData : Lean.ExternAttrData)
(ys : Array Lean.IR.Arg)
:
Equations
- Lean.IR.EmitC.emitExternCall f ps extData ys = match Lean.getExternEntryFor extData `c with | some (Lean.ExternEntry.standard x extFn) => Lean.IR.EmitC.emitSimpleExternalCall extFn ps ys | some (Lean.ExternEntry.inline x pat) => do Lean.IR.EmitC.emit (Lean.expandExternPattern pat (Lean.IR.EmitC.toStringArgs ys)) Lean.IR.EmitC.emitLn ";" | some (Lean.ExternEntry.foreign x extFn) => Lean.IR.EmitC.emitSimpleExternalCall extFn ps ys | x => throw (toString "failed to emit extern application '" ++ toString f ++ toString "'")
Equations
- Lean.IR.EmitC.emitFullApp z f ys = do Lean.IR.EmitC.emitLhs z let decl ← Lean.IR.EmitC.getDecl f match decl with | Lean.IR.Decl.extern x ps x_1 extData => Lean.IR.EmitC.emitExternCall f ps extData ys | x => do Lean.IR.EmitC.emitCName f let _do_jp : Unit → Lean.IR.EmitC.M Unit := fun y => Lean.IR.EmitC.emitLn ";" if Array.size ys > 0 then do Lean.IR.EmitC.emit "(" Lean.IR.EmitC.emitArgs ys let y ← Lean.IR.EmitC.emit ")" _do_jp y else do let y ← pure PUnit.unit _do_jp y
Equations
- Lean.IR.EmitC.emitPartialApp z f ys = do let decl ← Lean.IR.EmitC.getDecl f let arity : Nat := Array.size (Lean.IR.Decl.params decl) Lean.IR.EmitC.emitLhs z Lean.IR.EmitC.emit "lean_alloc_closure((void*)(" Lean.IR.EmitC.emitCName f Lean.IR.EmitC.emit "), " Lean.IR.EmitC.emit arity Lean.IR.EmitC.emit ", " Lean.IR.EmitC.emit (Array.size ys) Lean.IR.EmitC.emitLn ");" Nat.forM (Array.size ys) fun i => let y := Array.getOp ys i; do Lean.IR.EmitC.emit "lean_closure_set(" Lean.IR.EmitC.emit z Lean.IR.EmitC.emit ", " Lean.IR.EmitC.emit i Lean.IR.EmitC.emit ", " Lean.IR.EmitC.emitArg y Lean.IR.EmitC.emitLn ");"
Equations
- Lean.IR.EmitC.emitApp z f ys = if Array.size ys > Lean.closureMaxArgs then do Lean.IR.EmitC.emit "{ lean_object* _aargs[] = {" Lean.IR.EmitC.emitArgs ys Lean.IR.EmitC.emitLn "};" Lean.IR.EmitC.emitLhs z Lean.IR.EmitC.emit "lean_apply_m(" Lean.IR.EmitC.emit f Lean.IR.EmitC.emit ", " Lean.IR.EmitC.emit (Array.size ys) Lean.IR.EmitC.emitLn ", _aargs); }" else do Lean.IR.EmitC.emitLhs z Lean.IR.EmitC.emit "lean_apply_" Lean.IR.EmitC.emit (Array.size ys) Lean.IR.EmitC.emit "(" Lean.IR.EmitC.emit f Lean.IR.EmitC.emit ", " Lean.IR.EmitC.emitArgs ys Lean.IR.EmitC.emitLn ");"
Equations
- Lean.IR.EmitC.emitBoxFn xType = match xType with | Lean.IR.IRType.usize => Lean.IR.EmitC.emit "lean_box_usize" | Lean.IR.IRType.uint32 => Lean.IR.EmitC.emit "lean_box_uint32" | Lean.IR.IRType.uint64 => Lean.IR.EmitC.emit "lean_box_uint64" | Lean.IR.IRType.float => Lean.IR.EmitC.emit "lean_box_float" | other => Lean.IR.EmitC.emit "lean_box"
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 ");"
Equations
- Lean.IR.EmitC.emitUnbox z t x = do Lean.IR.EmitC.emitLhs z let _do_jp : Unit → Lean.IR.EmitC.M Unit := fun y => do Lean.IR.EmitC.emit "(" Lean.IR.EmitC.emit x Lean.IR.EmitC.emitLn ");" match t with | Lean.IR.IRType.usize => do let y ← Lean.IR.EmitC.emit "lean_unbox_usize" _do_jp y | Lean.IR.IRType.uint32 => do let y ← Lean.IR.EmitC.emit "lean_unbox_uint32" _do_jp y | Lean.IR.IRType.uint64 => do let y ← Lean.IR.EmitC.emit "lean_unbox_uint64" _do_jp y | Lean.IR.IRType.float => do let y ← Lean.IR.EmitC.emit "lean_unbox_float" _do_jp y | other => do let y ← Lean.IR.EmitC.emit "lean_unbox" _do_jp y
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 ");"
Equations
Equations
- Lean.IR.EmitC.quoteString s = let q := "\""; let q := String.foldl (fun q c => q ++ if (c == Char.ofNat 10) = true then "\\n" else if (c == Char.ofNat 13) = true then "\\r" else if (c == Char.ofNat 9) = true then "\\t" else if (c == Char.ofNat 92) = true then "\\\\" else if (c == Char.ofNat 34) = true then "\\\"" else if Char.toNat c ≤ 31 then "\\x" ++ Lean.IR.EmitC.toHexDigit (Char.toNat c / 16) ++ Lean.IR.EmitC.toHexDigit (Char.toNat c % 16) else String.singleton c) q s; q ++ "\""
Equations
- Lean.IR.EmitC.emitNumLit t v = if Lean.IR.IRType.isObj t = true then if v < UInt32.size then do Lean.IR.EmitC.emit "lean_unsigned_to_nat(" Lean.IR.EmitC.emit v Lean.IR.EmitC.emit "u)" else do Lean.IR.EmitC.emit "lean_cstr_to_nat(\"" Lean.IR.EmitC.emit v Lean.IR.EmitC.emit "\")" else Lean.IR.EmitC.emit v
Equations
- Lean.IR.EmitC.emitLit z t v = do Lean.IR.EmitC.emitLhs z match v with | Lean.IR.LitVal.num v => do Lean.IR.EmitC.emitNumLit t v Lean.IR.EmitC.emitLn ";" | Lean.IR.LitVal.str v => do Lean.IR.EmitC.emit "lean_mk_string(" Lean.IR.EmitC.emit (Lean.IR.EmitC.quoteString v) Lean.IR.EmitC.emitLn ");"
Equations
- Lean.IR.EmitC.emitVDecl z t v = match v with | Lean.IR.Expr.ctor c ys => Lean.IR.EmitC.emitCtor z c ys | Lean.IR.Expr.reset n x => Lean.IR.EmitC.emitReset z n x | Lean.IR.Expr.reuse x c u ys => Lean.IR.EmitC.emitReuse z x c u ys | Lean.IR.Expr.proj i x => Lean.IR.EmitC.emitProj z i x | Lean.IR.Expr.uproj i x => Lean.IR.EmitC.emitUProj z i x | Lean.IR.Expr.sproj n o x => Lean.IR.EmitC.emitSProj z t n o x | Lean.IR.Expr.fap c ys => Lean.IR.EmitC.emitFullApp z c ys | Lean.IR.Expr.pap c ys => Lean.IR.EmitC.emitPartialApp z c ys | Lean.IR.Expr.ap x ys => Lean.IR.EmitC.emitApp z x ys | Lean.IR.Expr.box t x => Lean.IR.EmitC.emitBox z x t | Lean.IR.Expr.unbox x => Lean.IR.EmitC.emitUnbox z t x | Lean.IR.Expr.isShared x => Lean.IR.EmitC.emitIsShared z x | Lean.IR.Expr.isTaggedPtr x => Lean.IR.EmitC.emitIsTaggedPtr z x | Lean.IR.Expr.lit v => Lean.IR.EmitC.emitLit z t v
Equations
- Lean.IR.EmitC.isTailCall x v b = do let ctx ← read match v, b with | Lean.IR.Expr.fap f x, Lean.IR.FnBody.ret (Lean.IR.Arg.var y) => pure (f == ctx.mainFn && x == y) | x, x_1 => pure false
Equations
- Lean.IR.EmitC.paramEqArg p x = match x with | Lean.IR.Arg.var x => p.x == x | x => false
Equations
- Lean.IR.EmitC.overwriteParam ps ys = let n := Array.size ps; Nat.any (fun i => let p := Array.getOp ps i; Prod.anyI (fun j => Lean.IR.EmitC.paramEqArg p (Array.getOp ys j)) (i + 1, n)) n
Equations
- Lean.IR.EmitC.emitTailCall v = match v with | Lean.IR.Expr.fap x ys => do let ctx ← read let ps : Array Lean.IR.Param := ctx.mainParams let _do_jp : PUnit → Lean.IR.EmitC.M Unit := fun y => let _do_jp := fun y => Lean.IR.EmitC.emitLn "goto _start;"; if Lean.IR.EmitC.overwriteParam ps ys = true then do Lean.IR.EmitC.emitLn "{" Nat.forM (Array.size ps) fun i => let p := Array.getOp ps i; let y := Array.getOp ys i; if Lean.IR.EmitC.paramEqArg p y = true then pure PUnit.unit else do Lean.IR.EmitC.emit (Lean.IR.EmitC.toCType p.ty) Lean.IR.EmitC.emit " _tmp_" Lean.IR.EmitC.emit i Lean.IR.EmitC.emit " = " Lean.IR.EmitC.emitArg y Lean.IR.EmitC.emitLn ";" Nat.forM (Array.size ps) fun i => let p := Array.getOp ps i; let y := Array.getOp ys i; if Lean.IR.EmitC.paramEqArg p y = true then pure PUnit.unit else do Lean.IR.EmitC.emit p.x Lean.IR.EmitC.emit " = _tmp_" Lean.IR.EmitC.emit i Lean.IR.EmitC.emitLn ";" let y ← Lean.IR.EmitC.emitLn "}" _do_jp y else do let y ← Nat.forM (Array.size ys) fun i => let p := Array.getOp ps i; let y := Array.getOp ys i; if Lean.IR.EmitC.paramEqArg p y = true then pure PUnit.unit else do Lean.IR.EmitC.emit p.x Lean.IR.EmitC.emit " = " Lean.IR.EmitC.emitArg y Lean.IR.EmitC.emitLn ";" _do_jp y if (Array.size ps == Array.size ys) = true then do let y ← pure PUnit.unit _do_jp y else do let y ← throw "invalid tail call" _do_jp y | x => throw "bug at emitTailCall"
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
- Lean.IR.EmitC.emitDeclAux d = do let env ← Lean.IR.EmitC.getEnv let x : Lean.IR.VarTypeMap × Lean.IR.JPParamsMap := Lean.IR.mkVarJPMaps d match x with | (vMap, jpMap) => withReader (fun ctx => { env := ctx.env, modName := ctx.modName, jpMap := jpMap, mainFn := ctx.mainFn, mainParams := ctx.mainParams }) (if Lean.hasInitAttr env (Lean.IR.Decl.name d) = true then pure PUnit.unit else match d with | Lean.IR.Decl.fdecl f xs t b x => do let baseName ← Lean.IR.EmitC.toCName f let _do_jp : Unit → Lean.IR.EmitC.M Unit := fun y => do Lean.IR.EmitC.emit (Lean.IR.EmitC.toCType t) Lean.IR.EmitC.emit " " let _do_jp : Unit → Lean.IR.EmitC.M Unit := fun y => do Lean.IR.EmitC.emitLn " {" let _do_jp : Unit → Lean.IR.EmitC.M Unit := fun y => do Lean.IR.EmitC.emitLn "_start:" withReader (fun ctx => { env := ctx.env, modName := ctx.modName, jpMap := ctx.jpMap, mainFn := f, mainParams := xs }) (Lean.IR.EmitC.emitFnBody b) Lean.IR.EmitC.emitLn "}" if (decide (Array.size xs > Lean.closureMaxArgs) && Lean.IR.ExplicitBoxing.isBoxedName (Lean.IR.Decl.name d)) = true then do let y ← Nat.forM (Array.size xs) fun i => let x := Array.getOp xs i; do Lean.IR.EmitC.emit "lean_object* " Lean.IR.EmitC.emit x.x Lean.IR.EmitC.emit " = _args[" Lean.IR.EmitC.emit i Lean.IR.EmitC.emitLn "];" _do_jp y else do let y ← pure PUnit.unit _do_jp y if Array.size xs > 0 then do Lean.IR.EmitC.emit baseName Lean.IR.EmitC.emit "(" let _do_jp : Unit → Lean.IR.EmitC.M Unit := fun y => do let y ← Lean.IR.EmitC.emit ")" _do_jp y if (decide (Array.size xs > Lean.closureMaxArgs) && Lean.IR.ExplicitBoxing.isBoxedName (Lean.IR.Decl.name d)) = true then do let y ← Lean.IR.EmitC.emit "lean_object** _args" _do_jp y else do let y ← Nat.forM (Array.size xs) fun i => let _do_jp := fun y => let x := Array.getOp xs i; do Lean.IR.EmitC.emit (Lean.IR.EmitC.toCType x.ty) Lean.IR.EmitC.emit " " Lean.IR.EmitC.emit x.x; if i > 0 then do let y ← Lean.IR.EmitC.emit ", " _do_jp y else do let y ← pure PUnit.unit _do_jp y _do_jp y else do let y ← Lean.IR.EmitC.emit ("_init_" ++ baseName ++ "()") _do_jp y if (Array.size xs == 0) = true then do let y ← Lean.IR.EmitC.emit "static " _do_jp y else do let y ← Lean.IR.EmitC.emit "LEAN_EXPORT " _do_jp y | x => pure ())
Equations
- Lean.IR.EmitC.emitDecl d = let d := Lean.IR.Decl.normalizeIds d; tryCatch (Lean.IR.EmitC.emitDeclAux d) fun err => throw (toString "" ++ toString err ++ toString "\ncompiling:\n" ++ toString d ++ toString "")
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
Equations
- Lean.IR.EmitC.emitMarkPersistent d n = if Lean.IR.IRType.isObj (Lean.IR.Decl.resultType d) = true then do Lean.IR.EmitC.emit "lean_mark_persistent(" Lean.IR.EmitC.emitCName n Lean.IR.EmitC.emitLn ");" else pure PUnit.unit
Equations
- Lean.IR.EmitC.emitDeclInit d = do let env ← Lean.IR.EmitC.getEnv let n : Lean.IR.FunId := Lean.IR.Decl.name d if Lean.isIOUnitInitFn env n = true then do Lean.IR.EmitC.emit "res = " Lean.IR.EmitC.emitCName n Lean.IR.EmitC.emitLn "(lean_io_mk_world());" Lean.IR.EmitC.emitLn "if (lean_io_result_is_error(res)) return res;" Lean.IR.EmitC.emitLn "lean_dec_ref(res);" else if (Array.size (Lean.IR.Decl.params d) == 0) = true then match Lean.getInitFnNameFor? env (Lean.IR.Decl.name d) with | some initFn => let _do_jp := fun y => do Lean.IR.EmitC.emit "res = " Lean.IR.EmitC.emitCName initFn Lean.IR.EmitC.emitLn "(lean_io_mk_world());" Lean.IR.EmitC.emitLn "if (lean_io_result_is_error(res)) return res;" Lean.IR.EmitC.emitCName n Lean.IR.EmitC.emitLn " = lean_io_result_get_value(res);" Lean.IR.EmitC.emitMarkPersistent d n Lean.IR.EmitC.emitLn "lean_dec_ref(res);" if Option.isSome (Lean.getBuiltinInitFnNameFor? env (Lean.IR.Decl.name d)) = true then Lean.IR.EmitC.emit "}" else pure PUnit.unit; if Option.isSome (Lean.getBuiltinInitFnNameFor? env (Lean.IR.Decl.name d)) = true then do let y ← Lean.IR.EmitC.emit "if (builtin) {" _do_jp y else do let y ← pure PUnit.unit _do_jp y | x => do Lean.IR.EmitC.emitCName n Lean.IR.EmitC.emit " = " Lean.IR.EmitC.emitCInitName n Lean.IR.EmitC.emitLn "();" Lean.IR.EmitC.emitMarkPersistent d n else pure PUnit.unit
Equations
- Lean.IR.EmitC.emitInitFn = do let env ← Lean.IR.EmitC.getEnv let modName ← Lean.IR.EmitC.getModName Array.forM (fun imp => Lean.IR.EmitC.emitLn ("lean_object* " ++ Lean.mkModuleInitializationFunctionName imp.module ++ "(uint8_t builtin, lean_object*);")) (Lean.Environment.imports env) 0 (Array.size (Lean.Environment.imports env)) Lean.IR.EmitC.emitLns ["static bool _G_initialized = false;", "LEAN_EXPORT lean_object* " ++ Lean.mkModuleInitializationFunctionName modName ++ "(uint8_t builtin, lean_object* w) {", "lean_object * res;", "if (_G_initialized) return lean_io_result_mk_ok(lean_box(0));", "_G_initialized = true;"] Array.forM (fun imp => Lean.IR.EmitC.emitLns ["res = " ++ Lean.mkModuleInitializationFunctionName imp.module ++ "(builtin, lean_io_mk_world());", "if (lean_io_result_is_error(res)) return res;", "lean_dec_ref(res);"]) (Lean.Environment.imports env) 0 (Array.size (Lean.Environment.imports env)) let decls : List Lean.IR.Decl := Lean.IR.getDecls env List.forM (List.reverse decls) Lean.IR.EmitC.emitDeclInit Lean.IR.EmitC.emitLns ["return lean_io_result_mk_ok(lean_box(0));", "}"]
Equations
- Lean.IR.emitC env modName = match EStateM.run (Lean.IR.EmitC.main { env := env, modName := modName, jpMap := ∅, mainFn := default, mainParams := #[] }) "" with | EStateM.Result.ok x s => Except.ok s | EStateM.Result.error err x => Except.error err