
   0 | ||| This was taken mostly verbatim from MarcelineVQ's unfinished idris-sqlite3
   1 | ||| project: [https://github.com/MarcelineVQ/idris-sqlite3]
   2 | module Sqlite3.Prim
   3 | 
   4 | import Data.Buffer
   5 | import Data.ByteString
   6 | import Data.List.Quantifiers
   7 | 
   8 | import Sqlite3.Expr
   9 | import Sqlite3.Marshall
  10 | import Sqlite3.Parameter
  11 | import Sqlite3.Types
  12 | 
  13 | %default total
  14 | 
  15 | export
  16 | idris_sqlite : String -> String
  17 | idris_sqlite fn = "C:" ++ fn ++ ",libsqlite3-idris"
  18 | 
  19 | --------------------------------------------------------------------------------
  20 | --          Pointers
  21 | --------------------------------------------------------------------------------
  22 | 
  23 | ||| Database pointer tag.
  24 | export
  25 | data DBPtr : Type where
  26 | 
  27 | ||| Pointer to an sqlite3 database.
  28 | public export
  29 | record DB where
  30 |   [noHints]
  31 |   constructor D
  32 |   db : Ptr DBPtr
  33 | 
  34 | ||| SQL statement pointer tag.
  35 | export
  36 | data StmtPtr : Type where
  37 | 
  38 | ||| Pointer to an SQL statement
  39 | public export
  40 | record Stmt where
  41 |   [noHints]
  42 |   constructor S
  43 |   stmt : Ptr StmtPtr
  44 | 
  45 | --------------------------------------------------------------------------------
  46 | --          FFI
  47 | --------------------------------------------------------------------------------
  48 | 
  49 | %foreign (idris_sqlite "newptr")
  50 | prim__newptr : PrimIO AnyPtr
  51 | 
  52 | %foreign (idris_sqlite "ptr_free")
  53 | prim__ptr_free : AnyPtr -> PrimIO ()
  54 | 
  55 | %foreign (idris_sqlite "null")
  56 | prim__null : AnyPtr
  57 | 
  58 | %foreign (idris_sqlite "deref")
  59 | prim__deref : Ptr AnyPtr -> PrimIO AnyPtr
  60 | 
  61 | %foreign (idris_sqlite "mkString")
  62 | prim__mkString : String -> PrimIO (Ptr String)
  63 | 
  64 | %foreign (idris_sqlite "getString")
  65 | prim__getString : Ptr String -> PrimIO String
  66 | 
  67 | %foreign (idris_sqlite "copy_buffer")
  68 | prim__copy_buffer : Bits32 -> Buffer -> AnyPtr -> PrimIO ()
  69 | 
  70 | %foreign (idris_sqlite "sqlver")
  71 | prim__sqlite_ver : PrimIO ()
  72 | 
  73 | %foreign (idris_sqlite "sqlite3_free")
  74 | prim__sqlite3_free : AnyPtr -> PrimIO AnyPtr
  75 | 
  76 | %foreign (idris_sqlite "sqlite3_malloc")
  77 | prim__sqlite3_malloc : Int -> PrimIO AnyPtr
  78 | 
  79 | %foreign (idris_sqlite "sqlite3_open")
  80 | prim__sqlite_open : String -> Ptr (Ptr DBPtr) -> PrimIO Int
  81 | 
  82 | -- open takes an sqlite3**
  83 | %foreign (idris_sqlite "sqlite3_open_v2")
  84 | prim__sqlite_open_v2 : String -> Ptr (Ptr DBPtr) -> Int -> String -> PrimIO Int
  85 | 
  86 | %foreign (idris_sqlite "sqlite3_close")
  87 | prim__sqlite_close : Ptr DBPtr -> PrimIO Int
  88 | 
  89 | %foreign (idris_sqlite "sqlite3_prepare_v2")
  90 | prim__sqlite_prepare : Ptr DBPtr -> String -> Int -> Ptr (Ptr StmtPtr) -> Ptr (Ptr String) -> PrimIO Int
  91 | 
  92 | %foreign (idris_sqlite "sqlite3_step")
  93 | prim__sqlite_step : Ptr StmtPtr -> PrimIO Int
  94 | 
  95 | %foreign (idris_sqlite "sqlite3_exec")
  96 | prim__sqlite_exec : Ptr DBPtr -> String -> AnyPtr -> AnyPtr -> Ptr String -> PrimIO Int
  97 | 
  98 | %foreign (idris_sqlite "sqlite3_finalize")
  99 | prim__sqlite3_finalize : Ptr StmtPtr -> PrimIO Int
 100 | 
 101 | %foreign (idris_sqlite "sqlite3_extended_errcode")
 102 | prim__sqlite3_extended_errcode : Ptr DBPtr -> PrimIO Int
 103 | 
 104 | %foreign (idris_sqlite "sqlite3_errmsg")
 105 | prim__sqlite3_errmsg : Ptr DBPtr -> PrimIO String
 106 | 
 107 | %foreign (idris_sqlite "sqlite3_errstr")
 108 | prim__sqlite3_errstr : Int -> PrimIO String
 109 | 
 110 | %foreign (idris_sqlite "sqlite3_column_text")
 111 | prim__sqlite3_column_text : Ptr StmtPtr -> (iCol : Bits32) -> PrimIO (Ptr String)
 112 | 
 113 | %foreign (idris_sqlite "sqlite3_column_blob")
 114 | prim__sqlite3_column_blob : Ptr StmtPtr -> (iCol : Bits32) -> PrimIO AnyPtr
 115 | 
 116 | %foreign (idris_sqlite "sqlite3_column_double")
 117 | prim__sqlite3_column_double : Ptr StmtPtr -> (iCol : Bits32) -> PrimIO Double
 118 | 
 119 | %foreign (idris_sqlite "sqlite3_column_type")
 120 | prim__sqlite3_column_type : Ptr StmtPtr -> (iCol : Bits32) -> PrimIO Bits8
 121 | 
 122 | %foreign (idris_sqlite "sqlite3_column_int")
 123 | prim__sqlite3_column_int32 : Ptr StmtPtr -> (iCol : Bits32) -> PrimIO Int32
 124 | 
 125 | %foreign (idris_sqlite "sqlite3_column_int64")
 126 | prim__sqlite3_column_int64 : Ptr StmtPtr -> (iCol : Bits32) -> PrimIO Int64
 127 | 
 128 | %foreign (idris_sqlite "sqlite3_column_bytes")
 129 | prim__sqlite3_column_bytes : Ptr StmtPtr -> (iCol : Bits32) -> PrimIO Bits32
 130 | 
 131 | %foreign (idris_sqlite "sqlite3_column_count")
 132 | prim__sqlite3_column_count : Ptr StmtPtr -> PrimIO Bits32
 133 | 
 134 | %foreign (idris_sqlite "bind_text")
 135 | prim__sqlite3_bind_text : Ptr StmtPtr -> (ix : Bits32) -> String -> PrimIO Int
 136 | 
 137 | %foreign (idris_sqlite "bind_buffer")
 138 | prim__sqlite3_bind_blob : Ptr StmtPtr -> (ix : Bits32) -> Buffer ->  (size : Bits32) -> PrimIO Int
 139 | 
 140 | %foreign (idris_sqlite "sqlite3_bind_double")
 141 | prim__sqlite3_bind_double : Ptr StmtPtr -> (ix : Bits32) -> Double -> PrimIO Int
 142 | 
 143 | %foreign (idris_sqlite "sqlite3_bind_int")
 144 | prim__sqlite3_bind_int32 : Ptr StmtPtr -> (ix : Bits32) -> Int32 -> PrimIO Int
 145 | 
 146 | %foreign (idris_sqlite "sqlite3_bind_int64")
 147 | prim__sqlite3_bind_int64 : Ptr StmtPtr -> (ix : Bits32) -> Int64 -> PrimIO Int
 148 | 
 149 | %foreign (idris_sqlite "sqlite3_bind_parameter_index")
 150 | prim__sqlite3_bind_parameter_index : Ptr StmtPtr -> String -> PrimIO Bits32
 151 | 
 152 | %foreign (idris_sqlite "sqlite3_bind_null")
 153 | prim__sqlite3_bind_null : Ptr StmtPtr -> (ix : Bits32) -> PrimIO Int
 154 | 
 155 | %foreign (idris_sqlite "sqlite3_last_insert_rowid")
 156 | prim__sqlite3_last_insert_rowid : Ptr DBPtr -> PrimIO Int64
 157 | 
 158 | --------------------------------------------------------------------------------
 159 | --          Pointers
 160 | --------------------------------------------------------------------------------
 161 | 
 162 | ||| Free the given pointer.
 163 | export %inline
 164 | ptrFree : Ptr t -> IO ()
 165 | ptrFree ptr = primIO $ prim__ptr_free $ prim__forgetPtr ptr
 166 | 
 167 | ||| Allocate a new pointer.
 168 | export %inline
 169 | newAnyPtr : IO AnyPtr
 170 | newAnyPtr = primIO prim__newptr
 171 | 
 172 | ||| Allocate a new tagged pointer.
 173 | export %inline
 174 | newPtr : IO (Ptr t)
 175 | newPtr = prim__castPtr <$> newAnyPtr
 176 | 
 177 | ||| Dereference the given pointer.
 178 | export %inline
 179 | dereference : Ptr (Ptr t) -> IO (Ptr t)
 180 | dereference ptr =
 181 |   prim__castPtr <$> (primIO $ prim__deref (believe_me ptr))
 182 | 
 183 | export %inline
 184 | strToPtr : String -> IO (Ptr String)
 185 | strToPtr = primIO . prim__mkString
 186 | 
 187 | ||| The `null` pointer
 188 | export %inline
 189 | nullPtr : Ptr t
 190 | nullPtr = prim__castPtr $ prim__null
 191 | 
 192 | ||| Act with a pointer and free it afterwards
 193 | export
 194 | withPtr : Ptr a -> (Ptr a -> IO b) -> IO b
 195 | withPtr ptr act = act ptr <* ptrFree ptr
 196 | 
 197 | ||| Allocate a pointer, act upon it, and free it afterwards
 198 | export
 199 | withPtrAlloc : (Ptr a -> IO b) -> IO b
 200 | withPtrAlloc act = newPtr >>= (`withPtr` act)
 201 | 
 202 | ||| Convert an FFI string to an Idris string.
 203 | export %inline
 204 | ptrToStr : Ptr String -> IO String
 205 | ptrToStr = primIO . prim__getString
 206 | 
 207 | --------------------------------------------------------------------------------
 208 | --          Status and Errors
 209 | --------------------------------------------------------------------------------
 210 | 
 211 | ||| Get the current error message.
 212 | export %inline
 213 | sqlite3ErrMsg : (d : DB) => IO String
 214 | sqlite3ErrMsg = primIO $ prim__sqlite3_errmsg d.db
 215 | 
 216 | export %inline
 217 | sqlFailRes : DB => SqlResult -> IO (Either SqlError a)
 218 | sqlFailRes r = do
 219 |   msg <- sqlite3ErrMsg
 220 |   pure (Left $ ResultError r msg)
 221 | 
 222 | export %inline
 223 | sqlFail : DB => Int -> IO (Either SqlError a)
 224 | sqlFail = sqlFailRes . fromInt
 225 | 
 226 | --------------------------------------------------------------------------------
 227 | --          Accessing Columns
 228 | --------------------------------------------------------------------------------
 229 | 
 230 | ||| Returns the generated row ID of the last successfull INSERT statement.
 231 | export %inline
 232 | sqlite3LastInsertRowID : DB => IO Int64
 233 | sqlite3LastInsertRowID @{D p} = primIO $ prim__sqlite3_last_insert_rowid p
 234 | 
 235 | ||| Get the current column count for the given statement.
 236 | export %inline
 237 | sqlite3ColumnCount : (s : Stmt) => IO Bits32
 238 | sqlite3ColumnCount = primIO $ prim__sqlite3_column_count s.stmt
 239 | 
 240 | ||| Try to read the text stored in the current column.
 241 | |||
 242 | ||| Note: This assumes that callers have already verified that the
 243 | |||       stored value is not a null pointer, for instance, by first
 244 | |||       invoking prim__sqlite3_column_type
 245 | export %inline
 246 | sqlite3ColumnText : (s : Stmt) => (iCol : Bits32) -> IO String
 247 | sqlite3ColumnText iCol = do
 248 |   ptr <- primIO $ prim__sqlite3_column_text s.stmt iCol
 249 |   ptrToStr ptr
 250 | 
 251 | ||| Try to read the bytestring stored in the current column.
 252 | |||
 253 | ||| Note: This assumes that callers have already verified that the
 254 | |||       stored value is not a null pointer, for instance, by first
 255 | |||       invoking prim__sqlite3_column_type
 256 | export
 257 | sqlite3ColumnBlob : (s : Stmt) => (iCol : Bits32) -> IO ByteString
 258 | sqlite3ColumnBlob iCol = do
 259 |   ptr <- primIO $ prim__sqlite3_column_blob s.stmt iCol
 260 |   n        <- primIO $ prim__sqlite3_column_bytes s.stmt iCol
 261 |   Just buf <- newBuffer (cast n) | Nothing => pure empty
 262 |   primIO $ prim__copy_buffer n buf ptr
 263 |   pure $ unsafeByteString (cast n) buf
 264 | 
 265 | ||| Read the floating point number stored in the current column.
 266 | export %inline
 267 | sqlite3ColumnDouble : (s : Stmt) => (iCol : Bits32) -> IO Double
 268 | sqlite3ColumnDouble = primIO . prim__sqlite3_column_double s.stmt
 269 | 
 270 | ||| Read the 32bit integer stored in the current column.
 271 | export %inline
 272 | sqlite3ColumnInt32 : (s : Stmt) => (iCol : Bits32) -> IO Int32
 273 | sqlite3ColumnInt32 = primIO . prim__sqlite3_column_int32 s.stmt
 274 | 
 275 | ||| Read the 64bit integer stored in the current column.
 276 | export %inline
 277 | sqlite3ColumnInt64 : (s : Stmt) => (iCol : Bits32) -> IO Int64
 278 | sqlite3ColumnInt64 = primIO . prim__sqlite3_column_int64 s.stmt
 279 | 
 280 | --------------------------------------------------------------------------------
 281 | --          Working with Connections
 282 | --------------------------------------------------------------------------------
 283 | 
 284 | ||| Tries to open a connection to the given database.
 285 | |||
 286 | ||| `path` is typically a relative or absolute path on the file system
 287 | ||| pointing to the database we want to work on. If `path` equals `":memory:"`,
 288 | ||| a temporary in-memory database will be created until the connection is
 289 | ||| closed. If `path` is the empty string, a temporary on-disk database will be
 290 | ||| created, which will be deleted once the connection is closed.
 291 | export
 292 | sqliteOpen : (path : String) -> IO (Either SqlError DB)
 293 | sqliteOpen fn = withPtrAlloc $ \db_ptr => do
 294 |     0 <- primIO (prim__sqlite_open fn db_ptr)
 295 |       | r => pure (Left $ ResultError (fromInt r) "unable to open connect to \{fn}")
 296 |     Right . D <$> dereference db_ptr
 297 | 
 298 | ||| Closes the given database connection returning an `SqlResult` describing
 299 | ||| if all went well.
 300 | export %inline
 301 | sqliteClose : DB -> IO SqlResult
 302 | sqliteClose d = fromInt <$> primIO (prim__sqlite_close d.db)
 303 | 
 304 | ||| Convenience alias for `ingore . sqliteClose`.
 305 | export %inline
 306 | sqliteClose' : DB -> IO ()
 307 | sqliteClose' = ignore . sqliteClose
 308 | 
 309 | --------------------------------------------------------------------------------
 310 | --          Working with Statements
 311 | --------------------------------------------------------------------------------
 312 | 
 313 | ||| Deletes a prepared SQL statement.
 314 | |||
 315 | ||| This can be called on a statement at any time, even if there is still
 316 | ||| more data available or the statement has not been evaluated at all.
 317 | export %inline
 318 | sqliteFinalize : Stmt -> IO SqlResult
 319 | sqliteFinalize s = fromInt <$> primIO (prim__sqlite3_finalize s.stmt)
 320 | 
 321 | ||| Convenience alias for `ignore . sqliteFinalize`.
 322 | export %inline
 323 | sqliteFinalize' : Stmt -> IO ()
 324 | sqliteFinalize' = ignore . sqliteFinalize
 325 | 
 326 | ||| Prepares an SQL statement for execution with the given database connection.
 327 | export
 328 | sqlitePrepare : (d : DB) => String -> IO (Either SqlError Stmt)
 329 | sqlitePrepare s = withPtrAlloc $ \stmt_ptr => do
 330 |     0 <- primIO (prim__sqlite_prepare d.db s (-1) stmt_ptr nullPtr)
 331 |       | r => sqlFail r
 332 |     Right . S <$> dereference stmt_ptr
 333 | 
 334 | bindParam : DB => Stmt -> Parameter -> IO Int
 335 | bindParam s (P n t v) = do
 336 |   ix <- fromPrim $ prim__sqlite3_bind_parameter_index s.stmt n
 337 |   case t of
 338 |     INTEGER => fromPrim $ prim__sqlite3_bind_int64 s.stmt ix v
 339 |     REAL    => fromPrim $ prim__sqlite3_bind_double s.stmt ix v
 340 |     TEXT    => fromPrim $ prim__sqlite3_bind_text s.stmt ix v
 341 |     BLOB    => do
 342 |       buf <- toBuffer v
 343 |       fromPrim $ prim__sqlite3_bind_blob s.stmt ix buf (cast v.size)
 344 | 
 345 | bindParams : DB => Stmt -> List Parameter -> IO Int
 346 | bindParams stmt []        = pure 0
 347 | bindParams stmt (x :: xs) = do
 348 |   0 <- bindParam stmt x | x => pure x
 349 |   bindParams stmt xs
 350 | 
 351 | ||| Binds the given parameters to an SQLite statement.
 352 | export
 353 | sqliteBind : (d : DB) => (s : Stmt) => List Parameter -> IO (Either SqlError ())
 354 | sqliteBind xs = do
 355 |   0 <- bindParams s xs | r => sqlFail r
 356 |   pure (Right ())
 357 | 
 358 | ||| Evaluates the given prepared SQL statement.
 359 | |||
 360 | ||| Some of the possible results
 361 | |||  * `SQLITE_DONE`   : Execution has finished and there is no more data
 362 | |||  * `SQLITE_ROW`    : Another row of output is available
 363 | |||  * `SQLITE_MISUSE` : Invalid use of statement (perhaps it was already finalized?)
 364 | |||  * `SQLITE_BUSY`   : If the statement is a commit you can retry it
 365 | |||
 366 | ||| More details about the possible results can be found at the
 367 | ||| [documentation of the SQLite C interface](https://www.sqlite.org/c3ref/step.html).
 368 | export %inline
 369 | sqliteStep : Stmt -> IO SqlResult
 370 | sqliteStep s = fromInt <$> primIO (prim__sqlite_step s.stmt)
 371 | 
 372 | --------------------------------------------------------------------------------
 373 | --          Loading Rows
 374 | --------------------------------------------------------------------------------
 375 | 
 376 | tryLoad :
 377 |      {auto s : Stmt}
 378 |   -> Bits8
 379 |   -> (t : SqliteType)
 380 |   -> Bits32
 381 |   -> IO (Either SqlError $ Maybe (IdrisType t))
 382 | tryLoad 1 INTEGER ix = Right . Just <$> sqlite3ColumnInt64 ix
 383 | tryLoad 2 REAL    ix = Right . Just <$> sqlite3ColumnDouble ix
 384 | tryLoad 3 TEXT    ix = Right . Just <$> sqlite3ColumnText ix
 385 | tryLoad 4 BLOB    ix = Right . Just <$> sqlite3ColumnBlob ix
 386 | tryLoad 5 _       ix = pure (Right Nothing)
 387 | tryLoad 1 t       ix = pure $ Left (TypeMismatch t INTEGER)
 388 | tryLoad 2 t       ix = pure $ Left (TypeMismatch t REAL)
 389 | tryLoad 3 t       ix = pure $ Left (TypeMismatch t TEXT)
 390 | tryLoad _ t       ix = pure $ Left (TypeMismatch t BLOB)
 391 | 
 392 | loadCell :
 393 |      {t : _}
 394 |   -> {auto s : Stmt}
 395 |   -> Bits32
 396 |   -> IO (Either SqlError $ Maybe (IdrisType t))
 397 | loadCell ix = do
 398 |   tpe     <- fromPrim $ prim__sqlite3_column_type s.stmt ix
 399 |   tryLoad tpe t ix
 400 | 
 401 | ||| Tries to read a single row of data from an SQL statement.
 402 | |||
 403 | ||| Only invoke this utility after `sqliteStep` returned with result
 404 | ||| `SQLITE_ROW`.
 405 | export
 406 | loadRow :
 407 |      {ts     : List SqliteType}
 408 |   -> {auto s : Stmt}
 409 |   -> IO (Either SqlError $ All (Maybe . IdrisType) ts)
 410 | loadRow = do
 411 |   ncols <- sqlite3ColumnCount
 412 |   go (cast ncols) 0 ts
 413 | 
 414 |   where
 415 |     go :
 416 |          Nat
 417 |       -> Bits32
 418 |       -> (ss : List SqliteType)
 419 |       -> IO (Either SqlError $ All (Maybe . IdrisType) ss)
 420 |     go _     _   []      = pure (Right [])
 421 |     go 0     _   (t::ss) = pure (Left NoMoreData)
 422 |     go (S k) col (t::ss) = do
 423 |       Right c  <- loadCell col     | Left err => pure (Left err)
 424 |       Right cs <- go k (col +1) ss | Left err => pure (Left err)
 425 |       pure (Right $ c :: cs)
 426 | 
 427 | ||| Tries to extract up to `max` lines of data from a prepared SQL statement.
 428 | export
 429 | loadRows :
 430 |      {auto db : DB}
 431 |   -> {auto s  : Stmt}
 432 |   -> {auto ps : FromRow a}
 433 |   -> (max     : Nat)
 434 |   -> IO (Either SqlError $ List a)
 435 | loadRows = go [<]
 436 |   where
 437 |     go : SnocList a -> Nat -> IO (Either SqlError $ List a)
 438 |     go sr 0     = pure (Right $ sr <>> [])
 439 |     go sr (S k) = do
 440 |       SQLITE_ROW <- sqliteStep s
 441 |         | SQLITE_DONE => pure (Right $ sr <>> [])
 442 |         | res         => sqlFailRes res
 443 |       Right r  <- loadRow | Left err => pure (Left err)
 444 |       case fromRow {a} r of
 445 |         Right v  => go (sr :< v) k
 446 |         Left err => pure (Left err)
 447 |