fix: prepare cursor without executing and represent result as Except

Changes

3 changed files (+29/-32)

• Main.lean
  • @@ -12,14 +12,18 @@ else
    match ← cursor.step with | false => pure () | true => do - println s!"id : {← cursor.columnInt 0}" - println s!"name: {← cursor.columnText 1}" + println s!"id: {← cursor.columnInt 0} | name: {← cursor.columnText 1}" 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 + | Except.error e => println s!"error {e}" + | Except.ok c => + printUser 10 c + println "----------------------------------------------------------------" match ← conn.exec "select count(1) from users;" with - | Sqlite.FFI.Result.rows c => + | Except.ok c => println s!"{c.columnsCount}" match ← c.step with | false => println "error"
  • @@ -27,9 +31,8 @@ | true => println "step"
    let count ← c.columnInt 0 println s!"count: {count}" match ← conn.exec "select * from users;" with - | Sqlite.FFI.Result.error e => println e - | Sqlite.FFI.Result.ok => println "ok" - | Sqlite.FFI.Result.rows c => + | Except.error e => println e + | Except.ok c => printUser count.toNat c - | _ => println "error" + | Except.error e => println s!"error: {e}" println s!"Hello, {conn}"
• Sqlite/FFI.lean
  • @@ -13,15 +13,10 @@ columnsCount : UInt32
    columnText : UInt32 → IO String columnInt : UInt32 → IO Int - inductive Result (t : Type) where - | ok : Result t - | rows (c : t) : Result t - | error (e : String) : Result t - structure Connection where path : String conn : RawConn - exec : String → IO (Result Cursor) + exec : String → IO (Except String Cursor) instance : ToString Connection where toString (conn : Connection) := s!"Connection('{conn.path}')"
  • @@ -33,8 +28,8 @@
    @[extern "lean_sqlite_open"] private opaque sqliteOpen : String → IO RawConn - @[extern "lean_sqlite_exec"] - private opaque sqliteExec : @&RawConn → String → IO (Result RawCursor) + @[extern "lean_sqlite_prepare"] + private opaque sqlitePrepare : @&RawConn → String → IO (Except String RawCursor) @[extern "lean_sqlite_cursor_step"] private opaque cursorStep : @&RawCursor → IO Bool
  • @@ -51,21 +46,20 @@
    @[extern "lean_sqlite_cursor_column_int"] private opaque cursorColumnInt : @&RawCursor → UInt32 → IO Int - def sqliteExecWrap (conn : RawConn) (query : String) : IO (Result Cursor) := do - pure $ match ← sqliteExec conn query with - | Result.rows c => Result.rows { cursor := c, - step := cursorStep c, - reset := cursorReset c, - columnsCount := cursorColumnsCount c, - columnText := cursorColumnText c, - columnInt := cursorColumnInt c } - | Result.ok => Result.ok - | Result.error e => Result.error e + 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, + reset := cursorReset c, + columnsCount := cursorColumnsCount c, + columnText := cursorColumnText c, + columnInt := cursorColumnInt c } + | Except.error e => Except.error e def connect (s : String) : IO Connection := do let rawconn ← sqliteOpen s pure { path := s, conn := rawconn, - exec := (sqliteExecWrap rawconn ·) } + exec := (sqlitePrepareWrap rawconn ·) } end Sqlite.FFI
• native/ffi.c
  • @@ -66,7 +66,7 @@
    return lean_io_result_mk_error(lean_mk_io_error_other_error(c, err)); } - lean_obj_res lean_sqlite_exec(b_lean_obj_arg conn_box, b_lean_obj_arg query_str) { + lean_obj_res lean_sqlite_prepare(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);
  • @@ -77,15 +77,15 @@
    if (c != 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(c, err)); + + lean_object* res = lean_alloc_ctor(0, 1, 0); + lean_ctor_set(res, 0, err); + return lean_io_result_mk_ok(res); } cursor->cols = (uint32_t) sqlite3_column_count(cursor->stmt); - if (cursor->cols == 0) - return lean_io_result_mk_ok(lean_box(0)); - - lean_object *res = lean_alloc_ctor(1, 1, 0); + lean_object* res = lean_alloc_ctor(1, 1, 0); lean_ctor_set(res, 0, box_cursor(cursor)); return lean_io_result_mk_ok(res); }