feat add cursor explain interface

Changes

3 changed files (+39/-4)

• Main.lean
  • @@ -5,6 +5,20 @@
    def double (f : Nat -> Nat) n := f (f n) def inc := fun n => n + 1 + def cursorExplain (c : Sqlite.FFI.Connection) (emode : UInt32) : IO Unit := do + match ← c.prepare "select * from users limit 50;" with + | Except.error e => println s!"error {e}" + | Except.ok q => do + let _ ← q.cursorExplain emode + let c ← q.columnsCount + println s!"columnsCount: {c}" + for i in [0:100] do + match ← q.step with + | false => pure () + | true => do + println s!"{i} explain: {← q.columnInt 0} {← q.columnText 1}" + + def printUser (fuel : Nat) (cursor : Sqlite.FFI.Cursor) : IO Unit := do if fuel = 0 then pure ()
  • @@ -16,7 +30,16 @@ 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" + println $ ← Sqlite.FFI.sqliteThreadsafe + println Sqlite.FFI.Constants.SQLITE_CONFIG_SINGLETHREAD + println Sqlite.FFI.Constants.SQLITE_CONFIG_MULTITHREAD + println $ ← Sqlite.FFI.sqliteConfig Sqlite.FFI.Constants.SQLITE_CONFIG_MULTITHREAD + let flags := Sqlite.FFI.Constants.SQLITE_OPEN_READWRITE ||| Sqlite.FFI.Constants.SQLITE_OPEN_CREATE + let conn ← Sqlite.FFI.connect "test.sqlite3" flags + cursorExplain conn 1 + match ← conn.prepare "delete from users where id = 154;" with + | Except.ok c => c.step + | _ => pure false match ← conn.prepare "insert into users values (?, ?);" with | Except.error e => println s!"error {e}" | Except.ok c =>
  • @@ -26,7 +49,7 @@ printUser 10 c
    println "----------------------------------------------------------------" match ← conn.prepare "select count(1) from users;" with | Except.ok c => - println s!"{c.columnsCount}" + println s!"{← c.columnsCount}" match ← c.step with | false => println "error" | true => println "step"
• Sqlite/FFI.lean
  • @@ -71,6 +71,7 @@ reset : IO Unit
    columnsCount : IO UInt32 columnText : UInt32 → IO String columnInt : UInt32 → IO Int + cursorExplain : UInt32 → IO Int structure Connection where path : String
  • @@ -112,7 +113,10 @@ @[extern "lean_sqlite_cursor_column_text"]
    private opaque cursorColumnText : @&RawCursor → UInt32 → IO String @[extern "lean_sqlite_cursor_column_int"] - private opaque cursorColumnInt : @&RawCursor → UInt32 → IO Int + private opaque cursorColumnInt : @&RawCursor → UInt32 → IO Int32 + + @[extern "lean_sqlite_cursor_explain"] + private opaque cursorExplain : @&RawCursor → UInt32 → IO Int @[extern "lean_sqlite_threadsafe"] opaque sqliteThreadsafe : IO Int
  • @@ -129,7 +133,8 @@ bindInt := cursorBindInt c,
    reset := cursorReset c, columnsCount := cursorColumnsCount c, columnText := cursorColumnText c, - columnInt := cursorColumnInt c } + columnInt := cursorColumnInt c, + cursorExplain := cursorExplain c, } | Except.error e => Except.error e def connect (s : String) (flags : UInt32) : IO Connection := do
• native/ffi.c
  • @@ -194,4 +194,11 @@ }
    return lean_io_result_mk_ok(lean_box(0)); } + + lean_obj_res lean_sqlite_cursor_explain(b_lean_obj_arg cursor_box, int32_t emode) { + sqlite3_stmt* cursor = unbox_cursor(cursor_box); + + const int c = sqlite3_stmt_explain(cursor, emode); + + return lean_io_result_mk_ok(lean_box(c)); }