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
103. 103
104. 104
105. 105
106. 106
107. 107
108. 108
109. 109
110. 110
111. 111
112. 112
113. 113
114. 114
115. 115
116. 116
117. 117
118. 118
119. 119
120. 120
121. 121
122. 122
123. 123
124. 124
125. 125
126. 126
127. 127
128. 128
129. 129
130. 130
131. 131
132. 132
133. 133
134. 134
135. 135
136. 136
137. 137
138. 138
139. 139
140. 140
141. 141
142. 142
143. 143
144. 144
145. 145
146. 146
147. 147
148. 148
149. 149
150. 150
151. 151
152. 152
153. 153
154. 154
155. 155
156. 156
157. 157
158. 158
159. 159
160. 160

namespace SQLite.FFI
namespace Constants

def SQLITE_CONFIG_SINGLETHREAD        : UInt32 := 1
def SQLITE_CONFIG_MULTITHREAD         : UInt32 := 2
def SQLITE_CONFIG_SERIALIZED          : UInt32 := 3
def SQLITE_CONFIG_MALLOC              : UInt32 := 4
def SQLITE_CONFIG_GETMALLOC           : UInt32 := 5
def SQLITE_CONFIG_SCRATCH             : UInt32 := 6
def SQLITE_CONFIG_PAGECACHE           : UInt32 := 7
def SQLITE_CONFIG_HEAP                : UInt32 := 8
def SQLITE_CONFIG_MEMSTATUS           : UInt32 := 9
def SQLITE_CONFIG_MUTEX               : UInt32 := 10
def SQLITE_CONFIG_GETMUTEX            : UInt32 := 11
-- /* previously SQLITE_CONFIG_CHUNKALLOC    12 which is now unused. */
def SQLITE_CONFIG_LOOKASIDE           : UInt32 := 13
def SQLITE_CONFIG_PCACHE              : UInt32 := 14
def SQLITE_CONFIG_GETPCACHE           : UInt32 := 15
def SQLITE_CONFIG_LOG                 : UInt32 := 16
def SQLITE_CONFIG_URI                 : UInt32 := 17
def SQLITE_CONFIG_PCACHE2             : UInt32 := 18
def SQLITE_CONFIG_GETPCACHE2          : UInt32 := 19
def SQLITE_CONFIG_COVERING_INDEX_SCAN : UInt32 := 20
def SQLITE_CONFIG_SQLLOG              : UInt32 := 21
def SQLITE_CONFIG_MMAP_SIZE           : UInt32 := 22
def SQLITE_CONFIG_WIN32_HEAPSIZE      : UInt32 := 23
def SQLITE_CONFIG_PCACHE_HDRSZ        : UInt32 := 24
def SQLITE_CONFIG_PMASZ               : UInt32 := 25
def SQLITE_CONFIG_STMTJRNL_SPILL      : UInt32 := 26
def SQLITE_CONFIG_SMALL_MALLOC        : UInt32 := 27
def SQLITE_CONFIG_SORTERREF_SIZE      : UInt32 := 28
def SQLITE_CONFIG_MEMDB_MAXSIZE       : UInt32 := 29
def SQLITE_CONFIG_ROWID_IN_VIEW       : UInt32 := 30

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 → Int32 → IO Unit
  reset : IO Unit
  columnsCount : IO UInt32
  columnText : UInt32 → IO String
  columnInt : UInt32 → IO Int32
  cursorExplain : 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 → Int32 → IO Unit

@[extern "lean_sqlite_cursor_bind_int64"]
private opaque cursorBindInt64 : @&RawCursor → UInt32 → Int64 → IO Unit

@[extern "lean_sqlite_cursor_bind_double"]
private opaque cursorBindDouble : @&RawCursor → UInt32 → Float → IO Unit

-- TODO: Support binding ByteArrays

@[extern "lean_sqlite_cursor_bind_parameter_name"]
private opaque cursorBindParameterName : @&RawCursor → Int32 → String → 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 Int32

@[extern "lean_sqlite_cursor_column_int64"]
private opaque cursorColumnInt64 : @&RawCursor → UInt32 → IO Int64

@[extern "lean_sqlite_cursor_column_double"]
private opaque cursorColumnDouble : @&RawCursor → UInt32 → IO Float

@[extern "lean_sqlite_cursor_explain"]
private opaque cursorExplain : @&RawCursor → UInt32 → IO Int

@[extern "lean_sqlite_threadsafe"]
opaque sqliteThreadsafe : IO Int

@[extern "lean_sqlite_config"]
opaque sqliteConfig : UInt32 → IO Unit

private def sqlitePrepareWrap (conn : RawConn) (query : String) : IO (Except String Cursor) := do
  return 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,
                          cursorExplain := cursorExplain c, }
  | Except.error e => Except.error e

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

end SQLite.FFI