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

namespace Sqlite.FFI
namespace Constants

def SQLITE_OPEN_READONLY      : UInt32 := 1
def SQLITE_OPEN_READWRITE     : UInt32 := 2
def SQLITE_OPEN_CREATE        : UInt32 := 4
def SQLITE_OPEN_DELETEONCLOSE : UInt32 := 8
def SQLITE_OPEN_EXCLUSIVE     : UInt32 := 16
def SQLITE_OPEN_AUTOPROXY     : UInt32 := 32
def SQLITE_OPEN_URI           : UInt32 := 64
def SQLITE_OPEN_MEMORY        : UInt32 := 128
def SQLITE_OPEN_MAIN_DB       : UInt32 := 256
def SQLITE_OPEN_TEMP_DB       : UInt32 := 512
def SQLITE_OPEN_TRANSIENT_DB  : UInt32 := 1024
def SQLITE_OPEN_MAIN_JOURNAL  : UInt32 := 2048
def SQLITE_OPEN_TEMP_JOURNAL  : UInt32 := 4096
def SQLITE_OPEN_SUBJOURNAL    : UInt32 := 8192
def SQLITE_OPEN_SUPER_JOURNAL : UInt32 := 16384
def SQLITE_OPEN_NOMUTEX       : UInt32 := 32768
def SQLITE_OPEN_FULLMUTEX     : UInt32 := 65536
def SQLITE_OPEN_SHAREDCACHE   : UInt32 := 131072
def SQLITE_OPEN_PRIVATECACHE  : UInt32 := 262144
def SQLITE_OPEN_WAL           : UInt32 := 524288
def SQLITE_OPEN_NOFOLLOW      : UInt32 := 16777216
def SQLITE_OPEN_EXRESCODE     : UInt32 := 33554432

end Constants

private opaque Nonempty : NonemptyType

def RawConn : Type := Nonempty.type
def RawCursor : Type := Nonempty.type

structure Cursor where
  cursor : RawCursor
  step : IO Bool
  bindText : UInt32 → String → IO Unit
  bindInt : UInt32 → Int → IO Unit
  reset : IO Unit
  columnsCount : IO UInt32
  columnText : UInt32 → IO String
  columnInt : UInt32 → IO Int

structure Connection where
  path : String
  conn : RawConn
  prepare : String → IO (Except String Cursor)

instance : ToString Connection where
  toString (conn : Connection) := s!"Connection('{conn.path}')"

@[extern "lean_sqlite_initialize"]
private opaque sqliteInit : IO Unit
builtin_initialize sqliteInit

@[extern "lean_sqlite_open"]
private opaque sqliteOpen : String → UInt32 → IO RawConn

@[extern "lean_sqlite_prepare"]
private opaque sqlitePrepare : @&RawConn → String → IO (Except String RawCursor)

@[extern "lean_sqlite_cursor_bind_text"]
private opaque cursorBindText : @&RawCursor → UInt32 → String → IO Unit

@[extern "lean_sqlite_cursor_bind_int"]
private opaque cursorBindInt : @&RawCursor → UInt32 → Int → IO Unit

@[extern "lean_sqlite_cursor_step"]
private opaque cursorStep : @&RawCursor → IO Bool

@[extern "lean_sqlite_cursor_reset"]
private opaque cursorReset : @&RawCursor → IO Unit

@[extern "lean_sqlite_cursor_columns_count"]
private opaque cursorColumnsCount : @&RawCursor → IO UInt32

@[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 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,
                          bindText := cursorBindText c,
                          bindInt := cursorBindInt c,
                          reset := cursorReset c,
                          columnsCount := cursorColumnsCount c,
                          columnText := cursorColumnText c,
                          columnInt := cursorColumnInt c }
  | Except.error e => Except.error e

def connect (s : String) (flags : UInt32) : IO Connection := do
  let rawconn ← sqliteOpen s flags
  pure { path := s,
         conn := rawconn,
         prepare := (sqlitePrepareWrap rawconn ·) }

end Sqlite.FFI