feat add cursor explain interface

Author: brenno.rodrigues

Main.lean

@@ -5,6 +5,20 @@ open IO
 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 @@ def printUser (fuel : Nat) (cursor : Sqlite.FFI.Cursor) : IO Unit := do
       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 @@ def main : IO Unit := do
   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 @@ structure Cursor where
   columnsCount : IO UInt32
   columnText : UInt32 → IO String
   columnInt : UInt32 → IO Int
+  cursorExplain : UInt32 → IO Int
 
 structure Connection where
   path : String
@@ -112,7 +113,10 @@ private opaque cursorColumnsCount : @&RawCursor → IO UInt32
 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 @@ private def sqlitePrepareWrap (conn : RawConn) (query : String) : IO (Except Str
                           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 @@ lean_obj_res lean_sqlite_config(int32_t config) {
 
   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));
 }