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
64. 64
65. 65
66. 66
67. 67
68. 68
69. 69
70. 70
71. 71
72. 72
73. 73
74. 74
75. 75
76. 76
77. 77
78. 78
79. 79
80. 80
81. 81
82. 82
83. 83
84. 84
85. 85
86. 86
87. 87
88. 88
89. 89
90. 90
91. 91
92. 92
93. 93
94. 94
95. 95
96. 96
97. 97
98. 98
99. 99
100. 100
101. 101
102. 102

import Sqlite
import LSpec

open LSpec
open Sqlite.FFI
open Sqlite.FFI.Constants

instance (b : Bool) : Testable b :=
  if h : b = true then
    .isTrue h
  else
    .isFalse h s!"Expected true but got false"

structure TestContext where
  conn : Connection

def setup (s : String) : IO TestContext := do
  let flags := SQLITE_OPEN_READWRITE ||| SQLITE_OPEN_CREATE
  let conn ← connect s flags

  match ← conn.prepare "CREATE TABLE IF NOT EXISTS users (id INTEGER PRIMARY KEY, name TEXT NOT NULL);" with
  | Except.ok cursor => cursor.step
  | Except.error _ => pure false

  match ← conn.prepare "INSERT INTO users (id, name) VALUES (1, 'John Doe');" with
  | Except.ok cursor => cursor.step
  | Except.error _ => pure false

  pure ⟨conn⟩

def cleanup (ctx : TestContext) : IO Unit := do
  match ← ctx.conn.prepare "DROP TABLE IF EXISTS users;" with
  | Except.ok cursor => do
    let _ ← cursor.step
    pure ()
  | Except.error _ => pure ()

def withTest (test : TestContext → IO Bool) : IO Bool := do
  let ctx ← setup "test.sqlite3"
  try
    let result ← test ctx
    cleanup ctx
    pure result
  catch e =>
    IO.println s!"Error: {e}"
    cleanup ctx
    pure false

def testInsertData (ctx : TestContext) : IO Bool := do
  match ← ctx.conn.prepare "INSERT INTO users (id, name) VALUES (?, ?);" with
  | Except.ok cursor =>
    cursor.bindInt 1 2
    cursor.bindText 2 "Jane Doe"
    let _ ← cursor.step
    pure true
  | Except.error _ => pure false

def testSelectData (ctx : TestContext) : IO Bool := do
  match ← ctx.conn.prepare "SELECT * FROM users WHERE id = 1;" with
  | Except.ok cursor =>
    let hasRow ← cursor.step
    if hasRow then
      let id ← cursor.columnInt 0
      let name ← cursor.columnText 1
      pure (id = 1 && name == "John Doe")
    else
      pure false
  | Except.error _ => pure false

def testParameterBinding (ctx : TestContext) : IO Bool := do
  match ← ctx.conn.prepare "SELECT * FROM users WHERE id = ? AND name = ?;" with
  | Except.ok cursor =>
    cursor.bindInt 1 1
    cursor.bindText 2 "John Doe"
    pure true
  | Except.error _ => pure false

def testColumnCount (ctx : TestContext) : IO Bool := do
  match ← ctx.conn.prepare "SELECT * FROM users;" with
  | Except.ok cursor =>
    let count ← cursor.columnsCount
    pure (count = 2)
  | Except.error _ => pure false

def testInvalidSyntax (ctx : TestContext) : IO Bool := do
  match ← ctx.conn.prepare "INVALID SQL QUERY;" with
  | Except.error _ => pure true
  | Except.ok _ => pure false

def testNonExistentTable (ctx : TestContext) : IO Bool := do
  match ← ctx.conn.prepare "SELECT * FROM non_existent_table;" with
  | Except.error _ => pure true
  | Except.ok _ => pure false

def main := do
  lspecIO $
    test "can insert data" (← withTest testInsertData) $
    test "can select data" (← withTest testSelectData) $
    test "can bind parameters" (← withTest testParameterBinding) $
    test "can get column count" (← withTest testColumnCount) $
    test "handles invalid SQL syntax" (← withTest testInvalidSyntax) $
    test "handles non-existent table" (← withTest testNonExistentTable)