1. 1
2. 2
3. 3
4. 4
5. 5
6. 6
7. 7
8. 8
9. 9
10. 10
11. 11
12. 12
13. 13
14. 14
15. 15
16. 16
17. 17
18. 18
19. 19
20. 20
21. 21
22. 22
23. 23
24. 24
25. 25
26. 26
27. 27
28. 28
29. 29
30. 30
31. 31
32. 32
33. 33
34. 34
35. 35
36. 36
37. 37
38. 38
39. 39
40. 40
41. 41
42. 42
43. 43
44. 44
45. 45
46. 46
47. 47
48. 48
49. 49
50. 50
51. 51
52. 52
53. 53
54. 54
55. 55
56. 56
57. 57
58. 58
59. 59
60. 60
61. 61
62. 62
63. 63

import Sqlite

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 ()
  else
    match ← cursor.step with
    | false => pure ()
    | true => do
      println s!"id: {← cursor.columnInt 0} | name: {← cursor.columnText 1}"
      printUser (fuel - 1) cursor

def main : IO Unit := do
  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 =>
    c.bindInt 1 154
    c.bindText 2 "giga chad"
    printUser 10 c
  println "----------------------------------------------------------------"
  match ← conn.prepare "select count(1) from users;" with
  | Except.ok c =>
    println s!"{← c.columnsCount}"
    match ← c.step with
    | false => println "error"
    | true => println "step"
    let count ← c.columnInt 0
    println s!"count: {count}"
    match ← conn.prepare "select * from users;" with
     | Except.error e => println e
     | Except.ok c =>
       printUser count.toNat c
  | Except.error e => println s!"error: {e}"
  println s!"Hello, {conn}"