feat(ffi): add cursor reset method interface

Changes

2 changed files (+19/-1)

• ffi/c/ffi.c
  • @@ -129,6 +129,18 @@ 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)); } + lean_obj_res lean_sqlite_reset_cursor(b_lean_obj_arg cursor_box) { + cursor_t* cursor = unbox_cursor(cursor_box); + + int c = sqlite3_reset(cursor->stmt); + + if (c == SQLITE_OK) + return lean_io_result_mk_ok(lean_box(0)); + + 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)); + } + int callback(void *NotUsed, int argc, char **argv, char **azColName){ int i; for(i=0; i<argc; i++){
• ffi/lean/FFI.lean
  • @@ -34,7 +34,10 @@ @[extern "lean_sqlite_exec"]
    private opaque execSqlite : @&RawConn → String → IO Result @[extern "lean_sqlite_step"] - private opaque stepSqlite : Cursor → IO (Option (Array String)) + private opaque stepSqlite : @&Cursor → IO (Option (Array String)) + + @[extern "lean_sqlite_reset_cursor"] + private opaque resetCursorSqlite : @&Cursor → IO Unit def connect (s : String) : IO Connection := do let rawconn ← openSqlite s
  • @@ -45,5 +48,8 @@ execSqlite c.conn query
    def step (c : Cursor) : IO (Option (Array String)) := stepSqlite c + + def reset (c : Cursor) : IO Unit := + resetCursorSqlite c end Sqlite