feat: added parameters binding to prepared query cursor

Changes

3 changed files (+51/-11)

• Main.lean
  • @@ -17,12 +17,14 @@ printUser (fuel - 1) cursor
    def main : IO Unit := do let conn ← Sqlite.FFI.connect "test.sqlite3" - match ← conn.exec "insert into users values (7, 'tanner');" with + match ← conn.prepare "insert into users values (?, ?);" with | Except.error e => println s!"error {e}" | Except.ok c => + c.bindInt 1 154 + c.bindText 2 "giga chad" printUser 10 c println "----------------------------------------------------------------" - match ← conn.exec "select count(1) from users;" with + match ← conn.prepare "select count(1) from users;" with | Except.ok c => println s!"{c.columnsCount}" match ← c.step with
  • @@ -30,7 +32,7 @@ | false => println "error"
    | true => println "step" let count ← c.columnInt 0 println s!"count: {count}" - match ← conn.exec "select * from users;" with + match ← conn.prepare "select * from users;" with | Except.error e => println e | Except.ok c => printUser count.toNat c
• Sqlite/FFI.lean
  • @@ -8,6 +8,8 @@
    structure Cursor where cursor : RawCursor step : IO Bool + bindText : UInt32 → String → IO Unit + bindInt : UInt32 → Int → IO Unit reset : IO Unit columnsCount : UInt32 columnText : UInt32 → IO String
  • @@ -16,7 +18,7 @@
    structure Connection where path : String conn : RawConn - exec : String → IO (Except String Cursor) + prepare : String → IO (Except String Cursor) instance : ToString Connection where toString (conn : Connection) := s!"Connection('{conn.path}')"
  • @@ -31,6 +33,12 @@
    @[extern "lean_sqlite_prepare"] private opaque sqlitePrepare : @&RawConn → String → IO (Except String RawCursor) + @[extern "lean_sqlite_cursor_bind_text"] + private opaque cursorBindText : @&RawCursor → UInt32 → String → IO Unit + + @[extern "lean_sqlite_cursor_bind_int"] + private opaque cursorBindInt : @&RawCursor → UInt32 → Int → IO Unit + @[extern "lean_sqlite_cursor_step"] private opaque cursorStep : @&RawCursor → IO Bool
  • @@ -50,6 +58,8 @@ private def sqlitePrepareWrap (conn : RawConn) (query : String) : IO (Except String Cursor) := do
    pure $ match ← sqlitePrepare conn query with | Except.ok c => pure { cursor := c, step := cursorStep c, + bindText := cursorBindText c, + bindInt := cursorBindInt c, reset := cursorReset c, columnsCount := cursorColumnsCount c, columnText := cursorColumnText c,
  • @@ -60,6 +70,6 @@ def connect (s : String) : IO Connection := do
    let rawconn ← sqliteOpen s pure { path := s, conn := rawconn, - exec := (sqlitePrepareWrap rawconn ·) } + prepare := (sqlitePrepareWrap rawconn ·) } end Sqlite.FFI
• native/ffi.c
  • @@ -4,7 +4,7 @@ #include <stdio.h>
    typedef struct { sqlite3_stmt* stmt; - int cols; + uint32_t cols; } cursor_t; lean_external_class* g_sqlite_object_external_class = NULL;
  • @@ -54,12 +54,12 @@ 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_v2(path_str, &conn, SQLITE_OPEN_READWRITE | SQLITE_OPEN_CREATE, NULL); + int32_t c = sqlite3_open_v2(path_str, &conn, SQLITE_OPEN_READWRITE | SQLITE_OPEN_CREATE, NULL); if (c == SQLITE_OK) return lean_io_result_mk_ok(box_connection(conn)); - lean_object *err = lean_mk_string(sqlite3_errmsg(conn)); + lean_object* err = lean_mk_string(sqlite3_errmsg(conn)); sqlite3_close(conn);
  • @@ -72,7 +72,7 @@ const char* query = lean_string_cstr(query_str);
    cursor_t* cursor = malloc(sizeof(cursor_t*)); - int c = sqlite3_prepare_v2(conn, query, -1, &cursor->stmt, NULL); + int32_t c = sqlite3_prepare_v2(conn, query, -1, &cursor->stmt, NULL); if (c != SQLITE_OK) { lean_object* err = lean_mk_string(sqlite3_errmsg(conn));
  • @@ -90,6 +90,34 @@ lean_ctor_set(res, 0, box_cursor(cursor));
    return lean_io_result_mk_ok(res); } + lean_obj_res lean_sqlite_cursor_bind_text(b_lean_obj_arg cursor_box, uint32_t col, b_lean_obj_arg value) { + cursor_t* cursor = unbox_cursor(cursor_box); + const char* value_str = lean_string_cstr(value); + + const int32_t c = sqlite3_bind_text(cursor->stmt, col, value_str, -1, NULL); + + if (c != SQLITE_OK) { + lean_object* err = lean_mk_string(sqlite3_errmsg(sqlite3_db_handle(cursor->stmt))); + return lean_io_result_mk_error(lean_mk_io_error_other_error(c, err)); + } + + return lean_io_result_mk_ok(lean_box(0)); + } + + lean_obj_res lean_sqlite_cursor_bind_int(b_lean_obj_arg cursor_box, uint32_t col, b_lean_obj_arg value_box) { + cursor_t* cursor = unbox_cursor(cursor_box); + int32_t value = (int32_t) lean_unbox(value_box); + + const int32_t c = sqlite3_bind_int(cursor->stmt, col, value); + + if (c != SQLITE_OK) { + lean_object* err = lean_mk_string(sqlite3_errmsg(sqlite3_db_handle(cursor->stmt))); + return lean_io_result_mk_error(lean_mk_io_error_other_error(c, err)); + } + + return lean_io_result_mk_ok(lean_box(0)); + } + lean_obj_res lean_sqlite_cursor_column_text(b_lean_obj_arg cursor_box, uint32_t col) { cursor_t* cursor = unbox_cursor(cursor_box);
  • @@ -111,7 +139,7 @@
    lean_obj_res lean_sqlite_cursor_step(b_lean_obj_arg cursor_box) { cursor_t* cursor = unbox_cursor(cursor_box); - int c = sqlite3_step(cursor->stmt); + int32_t c = sqlite3_step(cursor->stmt); if (c == SQLITE_ROW) { return lean_io_result_mk_ok(lean_box(1));
  • @@ -128,7 +156,7 @@
    lean_obj_res lean_sqlite_cursor_reset(b_lean_obj_arg cursor_box) { cursor_t* cursor = unbox_cursor(cursor_box); - int c = sqlite3_reset(cursor->stmt); + int32_t c = sqlite3_reset(cursor->stmt); if (c == SQLITE_OK) return lean_io_result_mk_ok(lean_box(0));