Sqlite3.Prim

(source)

This was taken mostly verbatim from MarcelineVQ's unfinished idris-sqlite3
project: [https://github.com/MarcelineVQ/idris-sqlite3]

Definitions

idris_sqlite : String -> String

Totality: total
Visibility: export

data DBPtr : Type

  Database pointer tag.

Totality: total
Visibility: export

record DB : Type

  Pointer to an sqlite3 database.

Totality: total
Visibility: public export
Constructor:

D : Ptr DBPtr -> DB

Projection:

.db : DB -> Ptr DBPtr

.db : DB -> Ptr DBPtr

Totality: total
Visibility: public export

db : DB -> Ptr DBPtr

Totality: total
Visibility: public export

data StmtPtr : Type

  SQL statement pointer tag.

Totality: total
Visibility: export

record Stmt : Type

  Pointer to an SQL statement

Totality: total
Visibility: public export
Constructor:

S : Ptr StmtPtr -> Stmt

Projection:

.stmt : Stmt -> Ptr StmtPtr

.stmt : Stmt -> Ptr StmtPtr

Totality: total
Visibility: public export

stmt : Stmt -> Ptr StmtPtr

Totality: total
Visibility: public export

ptrFree : Ptr t -> IO ()

  Free the given pointer.

Totality: total
Visibility: export

newAnyPtr : IO AnyPtr

  Allocate a new pointer.

Totality: total
Visibility: export

newPtr : IO (Ptr t)

  Allocate a new tagged pointer.

Totality: total
Visibility: export

dereference : Ptr (Ptr t) -> IO (Ptr t)

  Dereference the given pointer.

Totality: total
Visibility: export

strToPtr : String -> IO (Ptr String)

Totality: total
Visibility: export

nullPtr : Ptr t

  The `null` pointer

Totality: total
Visibility: export

withPtr : Ptr a -> (Ptr a -> IO b) -> IO b

  Act with a pointer and free it afterwards

Totality: total
Visibility: export

withPtrAlloc : (Ptr a -> IO b) -> IO b

  Allocate a pointer, act upon it, and free it afterwards

Totality: total
Visibility: export

ptrToStr : Ptr String -> IO String

  Convert an FFI string to an Idris string.

Totality: total
Visibility: export

sqlite3ErrMsg : DB => IO String

  Get the current error message.

Totality: total
Visibility: export

sqlFailRes : DB => SqlResult -> IO (Either SqlError a)

Totality: total
Visibility: export

sqlFail : DB => Int -> IO (Either SqlError a)

Totality: total
Visibility: export

sqlite3LastInsertRowID : DB => IO Int64

  Returns the generated row ID of the last successfull INSERT statement.

Totality: total
Visibility: export

sqlite3ColumnCount : Stmt => IO Bits32

  Get the current column count for the given statement.

Totality: total
Visibility: export

sqlite3ColumnText : Stmt => Bits32 -> IO String

  Try to read the text stored in the current column.
  
  Note: This assumes that callers have already verified that the
        stored value is not a null pointer, for instance, by first
        invoking prim__sqlite3_column_type

Totality: total
Visibility: export

sqlite3ColumnBlob : Stmt => Bits32 -> IO ByteString

  Try to read the bytestring stored in the current column.
  
  Note: This assumes that callers have already verified that the
        stored value is not a null pointer, for instance, by first
        invoking prim__sqlite3_column_type

Totality: total
Visibility: export

sqlite3ColumnDouble : Stmt => Bits32 -> IO Double

  Read the floating point number stored in the current column.

Totality: total
Visibility: export

sqlite3ColumnInt32 : Stmt => Bits32 -> IO Int32

  Read the 32bit integer stored in the current column.

Totality: total
Visibility: export

sqlite3ColumnInt64 : Stmt => Bits32 -> IO Int64

  Read the 64bit integer stored in the current column.

Totality: total
Visibility: export

sqliteOpen : String -> IO (Either SqlError DB)

  Tries to open a connection to the given database.
  
  `path` is typically a relative or absolute path on the file system
  pointing to the database we want to work on. If `path` equals `":memory:"`,
  a temporary in-memory database will be created until the connection is
  closed. If `path` is the empty string, a temporary on-disk database will be
  created, which will be deleted once the connection is closed.

Totality: total
Visibility: export

sqliteClose : DB -> IO SqlResult

  Closes the given database connection returning an `SqlResult` describing
  if all went well.

Totality: total
Visibility: export

sqliteClose' : DB -> IO ()

  Convenience alias for `ingore . sqliteClose`.

Totality: total
Visibility: export

sqliteFinalize : Stmt -> IO SqlResult

  Deletes a prepared SQL statement.
  
  This can be called on a statement at any time, even if there is still
  more data available or the statement has not been evaluated at all.

Totality: total
Visibility: export

sqliteFinalize' : Stmt -> IO ()

  Convenience alias for `ignore . sqliteFinalize`.

Totality: total
Visibility: export

sqlitePrepare : DB => String -> IO (Either SqlError Stmt)

  Prepares an SQL statement for execution with the given database connection.

Totality: total
Visibility: export

sqliteBind : DB => Stmt => List Parameter -> IO (Either SqlError ())

  Binds the given parameters to an SQLite statement.

Totality: total
Visibility: export

sqliteStep : Stmt -> IO SqlResult

  Evaluates the given prepared SQL statement.
  
  Some of the possible results
   * `SQLITE_DONE`   : Execution has finished and there is no more data
   * `SQLITE_ROW`    : Another row of output is available
   * `SQLITE_MISUSE` : Invalid use of statement (perhaps it was already finalized?)
   * `SQLITE_BUSY`   : If the statement is a commit you can retry it
  
  More details about the possible results can be found at the
  [documentation of the SQLite C interface](https://www.sqlite.org/c3ref/step.html).

Totality: total
Visibility: export

loadRow : Stmt => IO (Either SqlError (All (Maybe . IdrisType) ts))

  Tries to read a single row of data from an SQL statement.
  
  Only invoke this utility after `sqliteStep` returned with result
  `SQLITE_ROW`.

Totality: total
Visibility: export

data Chunk : Type -> Type

Totality: total
Visibility: public export
Constructors:

More : List a -> Chunk a
Done : List a -> Chunk a

Hint:

Cast (Chunk a) (List a)

loadChunk : DB => Stmt => FromRow a => Nat -> IO (Either SqlError (Chunk a))

  Tries to extract up to `max` lines of data from a prepared SQL statement.
  
  In case of a success, the result distinguishes between the query being
  exhausted (the internal call of `sqliteStep` returned `SQLITE_DONE`) and
  potentially more data being available.

Totality: total
Visibility: export

loadRows : DB => Stmt => FromRow a => Nat -> IO (Either SqlError (List a))

  Tries to extract up to `max` lines of data from a prepared SQL statement.

Totality: total
Visibility: export