From 4e52283728c71648dc805dd333ae3eec17eec18c Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Fri, 18 Aug 2023 10:42:02 +0200 Subject: [PATCH] fix: FFI signature mismatches --- src/Lean/Compiler/IR/EmitLLVM.lean | 2 +- src/Lean/Compiler/IR/LLVMBindings.lean | 2 +- src/Lean/LocalContext.lean | 5 +++-- src/library/compiler/llvm.cpp | 12 +++++------- src/runtime/io.cpp | 2 +- src/runtime/platform.cpp | 2 +- 6 files changed, 12 insertions(+), 13 deletions(-) diff --git a/src/Lean/Compiler/IR/EmitLLVM.lean b/src/Lean/Compiler/IR/EmitLLVM.lean index 0d4655fc46..350dd49257 100644 --- a/src/Lean/Compiler/IR/EmitLLVM.lean +++ b/src/Lean/Compiler/IR/EmitLLVM.lean @@ -1145,7 +1145,7 @@ def emitFnArgs (builder : LLVM.Builder llvmctx) LLVM.buildStore builder pv alloca addVartoState params[i]!.x alloca llvmty else - let n := LLVM.countParams llvmfn + let n ← LLVM.countParams llvmfn for i in (List.range n.toNat) do let llvmty ← toLLVMType params[i]!.ty let alloca ← LLVM.buildAlloca builder llvmty s!"arg_{i}" diff --git a/src/Lean/Compiler/IR/LLVMBindings.lean b/src/Lean/Compiler/IR/LLVMBindings.lean index 3fcc45c675..e60a49abca 100644 --- a/src/Lean/Compiler/IR/LLVMBindings.lean +++ b/src/Lean/Compiler/IR/LLVMBindings.lean @@ -273,7 +273,7 @@ opaque printModuletoString (mod : Module ctx) : BaseIO (String) opaque printModuletoFile (mod : Module ctx) (file : @&String) : BaseIO Unit @[extern "llvm_count_params"] -opaque countParams (fn : Value ctx) : UInt64 +opaque countParams (fn : Value ctx) : BaseIO UInt64 @[extern "llvm_get_param"] opaque getParam (fn : Value ctx) (ix : UInt64) : BaseIO (Value ctx) diff --git a/src/Lean/LocalContext.lean b/src/Lean/LocalContext.lean index 21352f5b79..c7d0caeb77 100644 --- a/src/Lean/LocalContext.lean +++ b/src/Lean/LocalContext.lean @@ -177,9 +177,10 @@ def mkLocalDecl (lctx : LocalContext) (fvarId : FVarId) (userName : Name) (type let decl := LocalDecl.cdecl idx fvarId userName type bi kind { fvarIdToDecl := map.insert fvarId decl, decls := decls.push decl } +-- `mkLocalDecl` without `kind` @[export lean_local_ctx_mk_local_decl] -private def mkLocalDeclExported (lctx : LocalContext) (fvarId : FVarId) (userName : Name) (type : Expr) (bi : BinderInfo) (kind : LocalDeclKind := .default) : LocalContext := - mkLocalDecl lctx fvarId userName type bi kind +private def mkLocalDeclExported (lctx : LocalContext) (fvarId : FVarId) (userName : Name) (type : Expr) (bi : BinderInfo) : LocalContext := + mkLocalDecl lctx fvarId userName type bi /-- Low level API for let declarations. Do not use directly.-/ def mkLetDecl (lctx : LocalContext) (fvarId : FVarId) (userName : Name) (type : Expr) (value : Expr) (nonDep := false) (kind : LocalDeclKind := default) : LocalContext := diff --git a/src/library/compiler/llvm.cpp b/src/library/compiler/llvm.cpp index 6972b76015..428f6634fc 100644 --- a/src/library/compiler/llvm.cpp +++ b/src/library/compiler/llvm.cpp @@ -36,7 +36,7 @@ Lean's IR. #pragma GCC diagnostic ignored "-Wunused-parameter" #endif -extern "C" LEAN_EXPORT lean_object* lean_llvm_initialize_target_info() { +extern "C" LEAN_EXPORT lean_object* lean_llvm_initialize_target_info(lean_object * /* w */) { #ifdef LEAN_LLVM LLVMInitializeAllTargetInfos(); @@ -1015,15 +1015,15 @@ extern "C" LEAN_EXPORT lean_object *llvm_get_param(size_t ctx, size_t f, uint64_ #endif // LEAN_LLVM } -extern "C" LEAN_EXPORT uint64_t llvm_count_params(size_t ctx, size_t f, - lean_object * /* w */) { +extern "C" LEAN_EXPORT lean_object * llvm_count_params(size_t ctx, size_t f, + lean_object * /* w */) { #ifndef LEAN_LLVM lean_always_assert( false && ("Please build a version of Lean4 with -DLLVM=ON to invoke " "the LLVM backend function.")); #else int n = LLVMCountParams(lean_to_Value(f)); - return n; + return lean_io_result_mk_ok(lean_box_uint64(n)); #endif // LEAN_LLVM } @@ -1147,9 +1147,7 @@ extern "C" LEAN_EXPORT lean_object *lean_llvm_get_target_from_triple(size_t ctx, #endif // LEAN_LLVM } -// opaque getDefaultTargetTriple: IO String -extern "C" LEAN_EXPORT lean_object *lean_llvm_get_default_target_triple(size_t ctx, - lean_object * /* w */) { +extern "C" LEAN_EXPORT lean_object *lean_llvm_get_default_target_triple(lean_object * /* w */) { #ifndef LEAN_LLVM lean_always_assert( false && ("Please build a version of Lean4 with -DLLVM=ON to invoke " diff --git a/src/runtime/io.cpp b/src/runtime/io.cpp index 11e0410be8..a1143f2a97 100644 --- a/src/runtime/io.cpp +++ b/src/runtime/io.cpp @@ -659,7 +659,7 @@ extern "C" LEAN_EXPORT obj_res lean_io_remove_dir(b_obj_arg p, obj_arg) { } } -extern "C" LEAN_EXPORT obj_res lean_io_rename(b_obj_arg from, b_obj_arg to) { +extern "C" LEAN_EXPORT obj_res lean_io_rename(b_obj_arg from, b_obj_arg to, lean_object * /* w */) { if (std::rename(string_cstr(from), string_cstr(to)) == 0) { return io_result_mk_ok(box(0)); } else { diff --git a/src/runtime/platform.cpp b/src/runtime/platform.cpp index 129dbc214a..64d029e8ba 100644 --- a/src/runtime/platform.cpp +++ b/src/runtime/platform.cpp @@ -40,5 +40,5 @@ extern "C" LEAN_EXPORT uint8 lean_system_platform_emscripten(obj_arg) { #endif } -extern "C" object * lean_get_githash() { return lean_mk_string(LEAN_GITHASH); } +extern "C" object * lean_get_githash(obj_arg) { return lean_mk_string(LEAN_GITHASH); } }