feat(ffi): add sqlite prepare interface

Changes

3 changed files (+64/-10)

• Main.lean
  • @@ -7,4 +7,8 @@ def inc := fun n => n + 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}" + let a := + match ← Sqlite.exec conn "select 1 + 1;" with + | Sqlite.Result.error e => e + | _ => "ok" + println s!"Hello, {conn} {a}"
• ffi/c/ffi.c
  • @@ -11,7 +11,13 @@ lean_obj_res myLeanFun() {
    return lean_io_result_mk_ok(lean_box(0)); } + typedef struct { + sqlite3_stmt* stmt; + int cols; + } cursor_t; + lean_external_class* g_sqlite_object_external_class = NULL; + lean_external_class* g_sqlite_cursor_external_class = NULL; void noop_foreach(void* mod, b_lean_obj_arg fn) {}
  • @@ -19,8 +25,16 @@ 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); + sqlite3* unbox_connection(lean_object* o) { + return (sqlite3*) lean_get_external_data(o); + } + + lean_object* box_cursor(cursor_t* cursor) { + return lean_alloc_external(g_sqlite_cursor_external_class, cursor); + } + + cursor_t* unbox_cursor(lean_object* o) { + return (cursor_t*) lean_get_external_data(o); } void connection_finalize(void* conn) {
  • @@ -29,9 +43,19 @@
    sqlite3_close(conn); } + void cursor_finalize(void* cursor_ptr) { + cursor_t* cursor = (cursor_t*) cursor_ptr; + + if (!cursor->stmt) return; + sqlite3_finalize(cursor->stmt); + + if (!cursor) return; + free(cursor); + } + lean_obj_res lean_sqlite_initialize() { g_sqlite_object_external_class = lean_register_external_class(connection_finalize, noop_foreach); - + g_sqlite_cursor_external_class = lean_register_external_class(cursor_finalize, noop_foreach); return lean_io_result_mk_ok(lean_box(0)); }
  • @@ -51,13 +75,27 @@
    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); + lean_obj_res lean_sqlite_exec(b_lean_obj_arg conn_box, b_lean_obj_arg query_str) { + sqlite3* conn = unbox_connection(conn_box); + const char* query = lean_string_cstr(query_str); + cursor_t* cursor = malloc(sizeof(cursor_t*)); + int rc = sqlite3_prepare_v2(conn, query, -1, &cursor->stmt, NULL); - return lean_io_result_mk_ok(box()); - } */ + if (rc != SQLITE_OK) { + lean_object *err = lean_mk_string(sqlite3_errmsg(conn)); + free(cursor); + return lean_io_result_mk_error(lean_mk_io_error_other_error(rc, err)); + } + + cursor->cols = sqlite3_column_count(cursor->stmt); + + if (cursor->cols == 0) + return lean_io_result_mk_ok(lean_box(0)); + + return lean_io_result_mk_ok(box_cursor(cursor)); + } int callback(void *NotUsed, int argc, char **argv, char **azColName){ int i;
• ffi/lean/FFI.lean
  • @@ -9,6 +9,7 @@
    private opaque Nonempty : NonemptyType private def RawConn : Type := Sqlite.Nonempty.type + private def Cursor : Type := Sqlite.Nonempty.type structure Connection where path : String
  • @@ -17,6 +18,11 @@
    instance : ToString Connection where toString (conn : Connection) := s!"Connection({conn.path})" + inductive Result where + | ok : Result + | rows : Cursor → Result + | error : String → Result + @[extern "lean_sqlite_initialize"] private opaque initSqlite : IO Unit builtin_initialize initSqlite
  • @@ -24,8 +30,14 @@
    @[extern "lean_sqlite_open"] private opaque openSqlite : String → IO RawConn + @[extern "lean_sqlite_exec"] + opaque execSqlite : @&RawConn → String → IO Result + def connect (s : String) : IO Connection := do - let raw ← openSqlite s - pure { path := s, conn := raw } + let rawconn ← openSqlite s + pure { path := s, conn := rawconn } + + def exec (c : Connection) (query : String) : IO Result := + execSqlite c.conn query end Sqlite