feat(ffi): add sqlite open method interface

Changes

5 changed files (+117/-3)

• Main.lean
  • @@ -1,7 +1,10 @@
    import FFI + open IO + def double (f : Nat -> Nat) n := f (f n) def inc := fun n => n + 1 - def main : IO Unit := - IO.println s!"Hello, {double inc 100} {myAdd 1 1} {myAdd 1 1} {myAdd 1 1}" + def main : IO Unit := do + let conn ← Sqlite.connect "test.sqlite3" + println s!"Hello, {double inc 100} {myAdd 1 1} {myAdd 1 1} {myAdd 1 1} {wasd 2} {conn}"
• ffi/c/ffi.c
  • @@ -10,3 +10,85 @@
    lean_obj_res myLeanFun() { return lean_io_result_mk_ok(lean_box(0)); } + + lean_external_class* g_sqlite_object_external_class = NULL; + + void noop_foreach(void* mod, b_lean_obj_arg fn) {} + + lean_object* box_connection(sqlite3 *conn) { + return lean_alloc_external(g_sqlite_object_external_class, conn); + } + + sqlite3* unbox_connection(lean_object *o) { + return (sqlite3*)lean_get_external_data(o); + } + + void connection_finalize(void* conn) { + if (!conn) return; + + sqlite3_close(conn); + } + + lean_obj_res lean_sqlite_initialize() { + g_sqlite_object_external_class = lean_register_external_class(connection_finalize, noop_foreach); + + return lean_io_result_mk_ok(lean_box(0)); + } + + lean_obj_res lean_sqlite_open(b_lean_obj_arg path) { + const char* path_str = lean_string_cstr(path); + sqlite3* conn = malloc(sizeof(sqlite3*)); + + int c = sqlite3_open(path_str, &conn); + + if (c == SQLITE_OK) + return lean_io_result_mk_ok(box_connection(conn)); + + lean_object *err = lean_mk_string(sqlite3_errmsg(conn)); + + sqlite3_close(conn); + + return lean_io_result_mk_error(lean_mk_io_error_other_error(c, err)); + } + + /* lean_obj_res lean_sqlite3_prepare(b_lean_obj_arg db, b_lean_obj_arg statement) { + const char* stmt_str = lean_string_cstr(statement); + + + + return lean_io_result_mk_ok(box()); + } */ + + int callback(void *NotUsed, int argc, char **argv, char **azColName){ + int i; + for(i=0; i<argc; i++){ + printf("%s = %s\n", azColName[i], argv[i] ? argv[i] : "NULL"); + } + printf("\n"); + return 0; + } + + uint32_t wasd(uint32_t a) { + printf("hello world\n"); + + sqlite3 *db; + char *zErrMsg = 0; + int err; + + err = sqlite3_open("test.sqlite3", &db); + if (err != SQLITE_OK) { + fprintf(stderr, "Can't open database: %s\n", sqlite3_errmsg(db)); + sqlite3_close(db); + return(1); + } + + err = sqlite3_exec(db, "select 1 = 1;", callback, 0, &zErrMsg); + if (err != SQLITE_OK) { + fprintf(stderr, "SQL error: %s\n", zErrMsg); + sqlite3_free(zErrMsg); + } + + sqlite3_close(db); + + return a; + }
• ffi/lakefile.lean
  • @@ -13,7 +13,7 @@
    target ffi.o pkg : FilePath := do let oFile := pkg.buildDir / "c" / "ffi.o" let srcJob ← inputTextFile <| pkg.dir / "c" / "ffi.c" - let weakArgs := #["-I", (← getLeanIncludeDir).toString] + let weakArgs := #["-I", (← getLeanIncludeDir).toString, "-I/nix/store/8r55amvr43sm771rgm0sszd05rm8j1cr-sqlite-3.46.0-dev/include/"] buildO oFile srcJob weakArgs #["-fPIC"] "clang" getLeanTrace extern_lib libleanffi pkg := do
• ffi/lean/FFI.lean
  • @@ -1,3 +1,31 @@
    @[extern "myAdd"] opaque myAdd : UInt32 → UInt32 → UInt32 + @[extern "wasd"] + opaque wasd : UInt32 → UInt32 + + namespace Sqlite + + private opaque Nonempty : NonemptyType + + private def RawConn : Type := Sqlite.Nonempty.type + + structure Connection where + path : String + conn : RawConn + + instance : ToString Connection where + toString (conn : Connection) := s!"Connection({conn.path})" + + @[extern "lean_sqlite_initialize"] + private opaque initSqlite : IO Unit + builtin_initialize initSqlite + + @[extern "lean_sqlite_open"] + private opaque openSqlite : String → IO RawConn + + def connect (s : String) : IO Connection := do + let raw ← openSqlite s + pure { path := s, conn := raw } + + end Sqlite
• lakefile.lean
  • @@ -8,6 +8,7 @@
    @[default_target] lean_exe flean where root := `Main + moreLinkArgs := #["-lsqlite3"] require ffi from "ffi" require batteries from git "https://github.com/leanprover-community/batteries" @ "main"