
   0 | module Sqlite3.Marshall
   1 | 
   2 | import Data.Bits
   3 | import Data.Buffer.Indexed
   4 | import Data.ByteString
   5 | import Data.String
   6 | import Data.Vect
   7 | import Sqlite3.Types
   8 | import public Data.List.Quantifiers.Extra
   9 | 
  10 | %default total
  11 | 
  12 | public export
  13 | 0 LAll : (0 f : k -> Type) -> List k -> Type
  14 | LAll = Data.List.Quantifiers.All.All
  15 | 
  16 | --------------------------------------------------------------------------------
  17 | -- FromCell
  18 | --------------------------------------------------------------------------------
  19 | 
  20 | ||| Inteface for converting an Idris value to a single cell in a table row.
  21 | public export
  22 | interface FromCell a where
  23 |   constructor MkFromCell
  24 |   fromCellType : SqliteType
  25 |   fromCell : Maybe (IdrisType fromCellType) -> Either SqlError a
  26 | 
  27 | ||| Utility alias for `fromCellType` with an explicit erased type argument.
  28 | public export %inline
  29 | FromCellType : (0 a : Type) -> FromCell a => SqliteType
  30 | FromCellType a = fromCellType {a}
  31 | 
  32 | ||| Utility for implementing `fromCell` for non-nullable data types.
  33 | |||
  34 | ||| In case of a `Nothing` (corresponding to `NULL` in SQL land),
  35 | ||| this fails with a `NullPointer` error that wraps the type name
  36 | ||| to display, what kind of data we tried to convert.
  37 | export
  38 | decodeJust :
  39 |      (type : String)
  40 |   -> (t -> Either SqlError a)
  41 |   -> Maybe t
  42 |   -> Either SqlError a
  43 | decodeJust str f Nothing  = Left (NullPointer str)
  44 | decodeJust str f (Just v) = f v
  45 | 
  46 | public export %inline
  47 | FromCell a => FromCell (Maybe a) where
  48 |   fromCellType      = FromCellType a
  49 |   fromCell Nothing  = Right Nothing
  50 |   fromCell v        = Just <$> fromCell v
  51 | 
  52 | public export
  53 | FromCell Integer where
  54 |   fromCellType = INTEGER
  55 |   fromCell     = decodeJust "Integer" (Right . cast)
  56 | 
  57 | public export
  58 | FromCell Nat where
  59 |   fromCellType = INTEGER
  60 |   fromCell     = decodeJust "Nat" (Right . cast)
  61 | 
  62 | public export
  63 | FromCell Int64 where
  64 |   fromCellType = INTEGER
  65 |   fromCell     = decodeJust "Int64" Right
  66 | 
  67 | public export
  68 | FromCell Int32 where
  69 |   fromCellType = INTEGER
  70 |   fromCell     = decodeJust "Int32" (Right . cast)
  71 | 
  72 | public export
  73 | FromCell Int16 where
  74 |   fromCellType = INTEGER
  75 |   fromCell     = decodeJust "Int16" (Right . cast)
  76 | 
  77 | public export
  78 | FromCell Int8 where
  79 |   fromCellType = INTEGER
  80 |   fromCell     = decodeJust "Int8" (Right . cast)
  81 | 
  82 | public export
  83 | FromCell Bits64 where
  84 |   fromCellType = INTEGER
  85 |   fromCell     = decodeJust "Bits64" (Right . cast)
  86 | 
  87 | public export
  88 | FromCell Bits32 where
  89 |   fromCellType = INTEGER
  90 |   fromCell     = decodeJust "Bits32" (Right . cast)
  91 | 
  92 | public export
  93 | FromCell Bits16 where
  94 |   fromCellType = INTEGER
  95 |   fromCell     = decodeJust "Bits16" (Right . cast)
  96 | 
  97 | public export
  98 | FromCell Bits8 where
  99 |   fromCellType = INTEGER
 100 |   fromCell     = decodeJust "Bits8" (Right . cast)
 101 | 
 102 | public export
 103 | FromCell String where
 104 |   fromCellType = TEXT
 105 |   fromCell     = decodeJust "String" Right
 106 | 
 107 | public export
 108 | FromCell ByteString where
 109 |   fromCellType = BLOB
 110 |   fromCell     = decodeJust "ByteString" Right
 111 | 
 112 | public export
 113 | FromCell Double where
 114 |   fromCellType = REAL
 115 |   fromCell     = decodeJust "Double" Right
 116 | 
 117 | public export
 118 | FromCell Bool where
 119 |   fromCellType = INTEGER
 120 |   fromCell     = decodeJust "Bool" (\case 0 => Right False; _ => Right True)
 121 | 
 122 | --------------------------------------------------------------------------------
 123 | -- ToCell
 124 | --------------------------------------------------------------------------------
 125 | 
 126 | ||| Inteface for converting an Idris value to a single cell in a table row.
 127 | public export
 128 | interface ToCell a where
 129 |   constructor MkToCell
 130 |   toCellType : SqliteType
 131 |   toCell     : a -> Maybe (IdrisType toCellType)
 132 | 
 133 | ||| Utility alias for `toCellType` with an explicit erased type argument.
 134 | public export %inline
 135 | ToCellType : (0 a : Type) -> ToCell a => SqliteType
 136 | ToCellType a = toCellType {a}
 137 | 
 138 | public export %inline
 139 | ToCell a => ToCell (Maybe a) where
 140 |   toCellType = ToCellType a
 141 |   toCell m   = m >>= toCell
 142 | 
 143 | public export
 144 | ToCell Int64 where
 145 |   toCellType = INTEGER
 146 |   toCell     = Just
 147 | 
 148 | public export
 149 | ToCell Int32 where
 150 |   toCellType = INTEGER
 151 |   toCell     = Just . cast
 152 | 
 153 | public export
 154 | ToCell Int16 where
 155 |   toCellType = INTEGER
 156 |   toCell     = Just . cast
 157 | 
 158 | public export
 159 | ToCell Int8 where
 160 |   toCellType = INTEGER
 161 |   toCell     = Just . cast
 162 | 
 163 | public export
 164 | ToCell Bits64 where
 165 |   toCellType = INTEGER
 166 |   toCell     = Just . cast
 167 | 
 168 | public export
 169 | ToCell Bits32 where
 170 |   toCellType = INTEGER
 171 |   toCell     = Just . cast
 172 | 
 173 | public export
 174 | ToCell Bits16 where
 175 |   toCellType = INTEGER
 176 |   toCell     = Just . cast
 177 | 
 178 | public export
 179 | ToCell Bits8 where
 180 |   toCellType = INTEGER
 181 |   toCell     = Just . cast
 182 | 
 183 | public export
 184 | ToCell String where
 185 |   toCellType = TEXT
 186 |   toCell     = Just
 187 | 
 188 | public export
 189 | ToCell ByteString where
 190 |   toCellType = BLOB
 191 |   toCell     = Just
 192 | 
 193 | public export
 194 | ToCell Double where
 195 |   toCellType = REAL
 196 |   toCell     = Just
 197 | 
 198 | public export
 199 | ToCell Bool where
 200 |   toCellType   = INTEGER
 201 |   toCell True  = Just 1
 202 |   toCell False = Just 0
 203 | 
 204 | --------------------------------------------------------------------------------
 205 | -- FromRow
 206 | --------------------------------------------------------------------------------
 207 | 
 208 | ||| Inteface for converting an Idris value from a row in a table.
 209 | public export
 210 | interface FromRow a where
 211 |   constructor MkFromRow
 212 |   fromRowTypes : List SqliteType
 213 |   fromRow      : LAll (Maybe . IdrisType) fromRowTypes -> Either SqlError a
 214 | 
 215 | public export
 216 | FromCell a => FromRow a where
 217 |   fromRowTypes = [FromCellType a]
 218 |   fromRow [v]  = fromCell v
 219 | 
 220 | ||| Utility alias for `fromRowTypes` with an explicit erased type argument.
 221 | public export %inline
 222 | FromRowTypes : (0 a : Type) -> FromRow a => List SqliteType
 223 | FromRowTypes a = fromRowTypes {a}
 224 | 
 225 | ||| List of SQLite types we require to read a sequence of
 226 | ||| several values with a `FromRow` implementation.
 227 | public export
 228 | FromRowsTypes : LAll (FromRow . f) ts -> List SqliteType
 229 | FromRowsTypes []        = []
 230 | FromRowsTypes (x :: xs) = fromRowTypes @{x} ++ FromRowsTypes xs
 231 | 
 232 | fromRowImpl :
 233 |      (ps : LAll (FromRow . f) ts)
 234 |   -> LAll (Maybe . IdrisType) (FromRowsTypes ps)
 235 |   -> Either SqlError (LAll f ts)
 236 | fromRowImpl []        [] = Right []
 237 | fromRowImpl (p :: ps) xs =
 238 |   let (qs,rs)  := splitAt (fromRowTypes @{p}) xs
 239 |       Right v  := fromRow @{p} qs   | Left err => Left err
 240 |       Right vs := fromRowImpl ps rs | Left err => Left err
 241 |    in Right (v::vs)
 242 | 
 243 | public export
 244 | {0 f : k -> Type} -> (ps : LAll (FromRow . f) ts) => FromRow (LAll f ts) where
 245 |   fromRowTypes = FromRowsTypes ps
 246 |   fromRow      = fromRowImpl ps
 247 | 
 248 | ||| We can also convert a row of values to a vector of values.
 249 | |||
 250 | ||| This function computes the types we need.
 251 | public export
 252 | FromRowsTypesN : Nat -> FromRow a -> List SqliteType
 253 | FromRowsTypesN 0     p = []
 254 | FromRowsTypesN (S k) p = fromRowTypes @{p} ++ FromRowsTypesN k p
 255 | 
 256 | fromRowVectImpl :
 257 |      (n : Nat)
 258 |   -> (p : FromRow a)
 259 |   -> LAll (Maybe . IdrisType) (FromRowsTypesN n p)
 260 |   -> Either SqlError (Vect n a)
 261 | fromRowVectImpl 0     p [] = Right []
 262 | fromRowVectImpl (S k) p xs =
 263 |   let (qs,rs)  := splitAt (fromRowTypes @{p}) xs
 264 |       Right v  := fromRow @{p} qs        | Left err => Left err
 265 |       Right vs := fromRowVectImpl k p rs | Left err => Left err
 266 |    in Right (v::vs)
 267 | 
 268 | public export
 269 | {n : _} -> (p : FromRow a) => FromRow (Vect n a) where
 270 |   fromRowTypes = FromRowsTypesN n p
 271 |   fromRow      = fromRowVectImpl n p
 272 | 
 273 | --------------------------------------------------------------------------------
 274 | -- ToRow
 275 | --------------------------------------------------------------------------------
 276 | 
 277 | ||| Inteface for converting an Idris value from a row in a table.
 278 | public export
 279 | interface ToRow a where
 280 |   constructor MkToRow
 281 |   toRowTypes : List SqliteType
 282 |   toRow      : a -> LAll (Maybe . IdrisType) toRowTypes
 283 | 
 284 | public export
 285 | ToCell a => ToRow a where
 286 |   toRowTypes = [ToCellType a]
 287 |   toRow v    = [toCell v]
 288 | 
 289 | ||| Utility alias for `fromRowTypes` with an explicit erased type argument.
 290 | public export %inline
 291 | ToRowTypes : (0 a : Type) -> ToRow a => List SqliteType
 292 | ToRowTypes a = toRowTypes {a}
 293 | 
 294 | ||| List of SQLite types we require to read a sequence of
 295 | ||| several values with a `ToRow` implementation.
 296 | public export
 297 | ToRowsTypes : LAll (ToRow . f) ts -> List SqliteType
 298 | ToRowsTypes []        = []
 299 | ToRowsTypes (p :: ps) = toRowTypes @{p} ++ ToRowsTypes ps
 300 | 
 301 | toRowImpl :
 302 |      (ps : LAll (ToRow . f) ts)
 303 |   -> LAll f ts
 304 |   -> LAll (Maybe . IdrisType) (ToRowsTypes ps)
 305 | toRowImpl []      []      = []
 306 | toRowImpl (p::ps) (v::vs) = toRow v ++ toRowImpl ps vs
 307 | 
 308 | public export
 309 | {0 f : k -> Type} -> (ps : LAll (ToRow . f) ts) => ToRow (LAll f ts) where
 310 |   toRowTypes = ToRowsTypes ps
 311 |   toRow      = toRowImpl ps
 312 | 
 313 | ||| We can also convert a vector of values to a (flat) row of values.
 314 | |||
 315 | ||| This function computes the types we need.
 316 | public export
 317 | ToRowsTypesN : Nat -> ToRow a -> List SqliteType
 318 | ToRowsTypesN 0     p = []
 319 | ToRowsTypesN (S k) p = toRowTypes @{p} ++ ToRowsTypesN k p
 320 | 
 321 | toRowVectImpl :
 322 |      (n : Nat)
 323 |   -> (p : ToRow a)
 324 |   -> Vect n a
 325 |   -> LAll (Maybe . IdrisType) (ToRowsTypesN n p)
 326 | toRowVectImpl 0     p []      = []
 327 | toRowVectImpl (S k) p (v::vs) = toRow @{p} v ++ toRowVectImpl k p vs
 328 | 
 329 | public export
 330 | {n : _} -> (p : ToRow a) => ToRow (Vect n a) where
 331 |   toRowTypes = ToRowsTypesN n p
 332 |   toRow      = toRowVectImpl n p
 333 | 
 334 | ||| List concatenation specialized to behave nicely during unification.
 335 | public export
 336 | Concat : List (List a) -> List a
 337 | Concat []        = []
 338 | Concat (x :: xs) = x ++ Concat xs
 339 | 
 340 | ||| Generalization of `Data.List.Quantifiers.splitAt`, to split a
 341 | ||| heterogeneous list based on a list of lists of its indices.
 342 | public export
 343 | splitAll : (v : List (List a)) -> LAll f (Concat v) -> LAll (LAll f) v
 344 | splitAll []          [] = []
 345 | splitAll (xs :: xss) ys =
 346 |   let (zs,r) := splitAt xs ys
 347 |    in zs :: splitAll xss r
 348 |