0 | module Sqlite3.Types
  1 |
  2 | import Data.ByteString
  3 | import Derive.Prelude
  4 |
  5 | %default total
  6 | %language ElabReflection
  7 |
  8 | --------------------------------------------------------------------------------
  9 | --          Status Info
 10 | --------------------------------------------------------------------------------
 11 |
 12 | ||| Possible result codes when interacting with the SQLite C interface.
 13 | |||
 14 | ||| These result codes are described in greater detail in the
 15 | ||| [SQLite C interface documentation](https://www.sqlite.org/rescode.html).
 16 | public export
 17 | data SqlResult : Type where
 18 |   SQLITE_OK         : SqlResult -- Successful result
 19 |   SQLITE_ERROR      : SqlResult -- Generic error
 20 |   SQLITE_INTERNAL   : SqlResult -- Internal logic error in SQLite
 21 |   SQLITE_PERM       : SqlResult -- Access permission denied
 22 |   SQLITE_ABORT      : SqlResult -- Callback routine requested an abort
 23 |   SQLITE_BUSY       : SqlResult -- The database file is locked
 24 |   SQLITE_LOCKED     : SqlResult -- A table in the database is locked
 25 |   SQLITE_NOMEM      : SqlResult -- A malloc() failed
 26 |   SQLITE_READONLY   : SqlResult -- Attempt to write a readonly database
 27 |   SQLITE_INTERRUPT  : SqlResult -- Operation terminated by sqlite3_interrupt()
 28 |   SQLITE_IOERR      : SqlResult -- Some kind of disk I/O error occurred
 29 |   SQLITE_CORRUPT    : SqlResult -- The database disk image is malformed
 30 |   SQLITE_NOTFOUND   : SqlResult -- Unknown opcode in sqlite3_file_control()
 31 |   SQLITE_FULL       : SqlResult -- Insertion failed because database is full
 32 |   SQLITE_CANTOPEN   : SqlResult -- Unable to open the database file
 33 |   SQLITE_PROTOCOL   : SqlResult -- Database lock protocol error
 34 |   SQLITE_EMPTY      : SqlResult -- Internal use only
 35 |   SQLITE_SCHEMA     : SqlResult -- The database schema changed
 36 |   SQLITE_TOOBIG     : SqlResult -- String or BLOB exceeds size limit
 37 |   SQLITE_CONSTRAINT : SqlResult -- Abort due to constraint violation
 38 |   SQLITE_MISMATCH   : SqlResult -- Data type mismatch
 39 |   SQLITE_MISUSE     : SqlResult -- Library used incorrectly
 40 |   SQLITE_NOLFS      : SqlResult -- Uses OS features not supported on host
 41 |   SQLITE_AUTH       : SqlResult -- Authorization denied
 42 |   SQLITE_FORMAT     : SqlResult -- Not used
 43 |   SQLITE_RANGE      : SqlResult -- 2nd parameter to sqlite3_bind out of range
 44 |   SQLITE_NOTADB     : SqlResult -- File opened that is not a database file
 45 |   SQLITE_NOTICE     : SqlResult -- Notifications from sqlite3_log()
 46 |   SQLITE_WARNING    : SqlResult -- Warnings from sqlite3_log()
 47 |   SQLITE_ROW        : SqlResult -- sqlite3_step() has another row ready
 48 |   SQLITE_DONE       : SqlResult -- sqlite3_step() has finished executing
 49 |   Unknown           : SqlResult -- error code unknown
 50 |
 51 | %runElab derive "SqlResult" [Show,Eq,Ord]
 52 |
 53 | public export
 54 | fromInt : Int -> SqlResult
 55 | fromInt 0   = SQLITE_OK
 56 | fromInt 1   = SQLITE_ERROR
 57 | fromInt 2   = SQLITE_INTERNAL
 58 | fromInt 3   = SQLITE_PERM
 59 | fromInt 4   = SQLITE_ABORT
 60 | fromInt 5   = SQLITE_BUSY
 61 | fromInt 6   = SQLITE_LOCKED
 62 | fromInt 7   = SQLITE_NOMEM
 63 | fromInt 8   = SQLITE_READONLY
 64 | fromInt 9   = SQLITE_INTERRUPT
 65 | fromInt 10  = SQLITE_IOERR
 66 | fromInt 11  = SQLITE_CORRUPT
 67 | fromInt 12  = SQLITE_NOTFOUND
 68 | fromInt 13  = SQLITE_FULL
 69 | fromInt 14  = SQLITE_CANTOPEN
 70 | fromInt 15  = SQLITE_PROTOCOL
 71 | fromInt 16  = SQLITE_EMPTY
 72 | fromInt 17  = SQLITE_SCHEMA
 73 | fromInt 18  = SQLITE_TOOBIG
 74 | fromInt 19  = SQLITE_CONSTRAINT
 75 | fromInt 20  = SQLITE_MISMATCH
 76 | fromInt 21  = SQLITE_MISUSE
 77 | fromInt 22  = SQLITE_NOLFS
 78 | fromInt 23  = SQLITE_AUTH
 79 | fromInt 24  = SQLITE_FORMAT
 80 | fromInt 25  = SQLITE_RANGE
 81 | fromInt 26  = SQLITE_NOTADB
 82 | fromInt 27  = SQLITE_NOTICE
 83 | fromInt 28  = SQLITE_WARNING
 84 | fromInt 100 = SQLITE_ROW
 85 | fromInt 101 = SQLITE_DONE
 86 | fromInt _   = Unknown
 87 |
 88 | --------------------------------------------------------------------------------
 89 | --          Schema
 90 | --------------------------------------------------------------------------------
 91 |
 92 | ||| Enumeration listing the different types of data that can be stored in
 93 | ||| an SQLite table column.
 94 | |||
 95 | ||| Note: Strictly speaking, `BOOL` is not an officially supported SQL type
 96 | |||       but just an integer internally. However, being able to distinguish
 97 | |||       between `BOOL` and `INTEGER` allows us to get clearer types
 98 | |||       in the expressions we use in filters and checks.
 99 | public export
100 | data SqliteType : Type where
101 |   BLOB    : SqliteType
102 |   TEXT    : SqliteType
103 |   INTEGER : SqliteType
104 |   REAL    : SqliteType
105 |
106 | %runElab derive "SqliteType" [Show,Eq,Ord]
107 |
108 | ||| This is an alias for `INTEGER` that helps with making the intention
109 | ||| behind certain SQL expressions clearer.
110 | |||
111 | ||| SQLite does not have a native boolean type, so this is used
112 | ||| as a reminder than some expression are used in accordance with
113 | ||| boolean logic.
114 | public export %inline
115 | BOOL : SqliteType
116 | BOOL = INTEGER
117 |
118 | ||| Associates an `SqliteType` with the corresponding Idris type.
119 | public export
120 | 0 IdrisType : SqliteType -> Type
121 | IdrisType BLOB    = ByteString
122 | IdrisType TEXT    = String
123 | IdrisType INTEGER = Int64
124 | IdrisType REAL    = Double
125 |
126 | --------------------------------------------------------------------------------
127 | --          Error Type
128 | --------------------------------------------------------------------------------
129 |
130 | ||| Error type that can occur when interacting with the unsafe world of
131 | ||| SQLite.
132 | public export
133 | data SqlError : Type where
134 |   ResultError   : SqlResult -> (msg : String) -> SqlError
135 |   DecodingError : SqliteType -> String -> SqlError
136 |   TypeMismatch  : (expected, found : SqliteType) -> SqlError
137 |   NullPointer   : String -> SqlError
138 |   NoMoreData    : SqlError
139 |
140 | %runElab derive "SqlError" [Show,Eq]
141 |
142 | export
143 | Interpolation SqlError where
144 |   interpolate (ResultError x m)   = "SQL error \{show x}: \{m}"
145 |   interpolate (DecodingError x s) = "Error when decoding \{show x}: \{s}"
146 |   interpolate (TypeMismatch x f)  = "Type mismatch: Expected \{show x} but found \{show f}"
147 |   interpolate (NullPointer s)     = "Exception when decoding \{s}: Value is NULL"
148 |   interpolate NoMoreData          = "Exception when decoding row: No more data"
149 |