
   0 | module Sqlite3.Table
   1 | 
   2 | import public Data.List1
   3 | import public Data.Maybe
   4 | import public Data.SnocList
   5 | import public Data.String
   6 | import Data.Bits
   7 | import Data.Buffer.Indexed
   8 | import Data.ByteString
   9 | import Sqlite3.Marshall
  10 | import Sqlite3.Types
  11 | 
  12 | %default total
  13 | 
  14 | --------------------------------------------------------------------------------
  15 | -- SQL Columns and Tables
  16 | --------------------------------------------------------------------------------
  17 | 
  18 | ||| A column in an SQLite table: A name paired with the type of
  19 | ||| values stored in the column.
  20 | |||
  21 | ||| Note: With this definition, we do not include any constraints with
  22 | |||       our columns. These should be passed on separately when
  23 | |||       using the `CREATE_TABLE` command.
  24 | public export
  25 | record Column where
  26 |   constructor C
  27 |   name  : String
  28 |   type  : SqliteType
  29 | 
  30 | ||| An SQLite table: A name paired with a list of columns.
  31 | public export
  32 | record SQLTable where
  33 |   constructor ST
  34 |   ||| The table's name
  35 |   name : String
  36 | 
  37 |   ||| Field `as` is used to rename tables within a `SELECT` statement.
  38 |   ||| This is, for instance, needed when `JOIN`ing a table with itself.
  39 |   as   : String
  40 | 
  41 |   ||| The list of table columns
  42 |   cols : List Column
  43 | 
  44 | ||| Utility constructor for tables that sets fields `name` and `as`
  45 | ||| both the value of the string argument.
  46 | public export %inline
  47 | table : String -> List Column -> SQLTable
  48 | table n = ST n n
  49 | 
  50 | ||| Utility to change the name of a table in a `SELECT` statement.
  51 | |||
  52 | ||| The name was chosen to resemble SQL syntax, and it is recommended
  53 | ||| to use this in infix notation:
  54 | |||
  55 | ||| ```idris
  56 | ||| students `AS` "st"
  57 | ||| ```
  58 | public export %inline
  59 | AS : SQLTable -> String -> SQLTable
  60 | AS (ST n _ cs) as = ST n as cs
  61 | 
  62 | ||| Computes the types of columns stored in a table.
  63 | public export %inline
  64 | ColTypes : SQLTable -> List SqliteType
  65 | ColTypes = map type . cols
  66 | 
  67 | ||| Tries to look up a column type by name
  68 | ||| in a list of columns.
  69 | |||
  70 | ||| We use this often in proofs, therefore this comes with
  71 | ||| an upper-case name.
  72 | public export
  73 | FindCol : String -> List Column -> Maybe SqliteType
  74 | FindCol s []        = Nothing
  75 | FindCol s (x :: xs) = if x.name == s then Just x.type else FindCol s xs
  76 | 
  77 | ||| Column type of a column (given by name) in a list of
  78 | ||| columns.
  79 | |||
  80 | ||| This requires a proof that the column actually is in the
  81 | ||| table.
  82 | public export %inline
  83 | ListColType :
  84 |      (s        : String)
  85 |   -> (cs       : List Column)
  86 |   -> {auto 0 p : IsJust (FindCol s cs)}
  87 |   -> SqliteType
  88 | ListColType s cs = fromJust (FindCol s cs)
  89 | 
  90 | ||| Column type of a column (given by name) in a table.
  91 | |||
  92 | ||| This requires a proof that the column actually is in the
  93 | ||| table.
  94 | public export %inline
  95 | TableColType :
  96 |      (s        : String)
  97 |   -> (t        : SQLTable)
  98 |   -> {auto 0 p : IsJust (FindCol s t.cols)}
  99 |   -> SqliteType
 100 | TableColType s t = fromJust (FindCol s t.cols)
 101 | 
 102 | --------------------------------------------------------------------------------
 103 | -- Typed SQL Columns
 104 | --------------------------------------------------------------------------------
 105 | 
 106 | ||| A column in the given table: This is just a column name
 107 | ||| paired with a proof that the column exists in table `t`
 108 | ||| and has type `tpe`.
 109 | public export
 110 | data TColumn : (t : SQLTable) -> (tpe : SqliteType) -> Type where
 111 |   TC :
 112 |        {0 t        : SQLTable}
 113 |     -> (name       : String)
 114 |     -> {auto 0 prf : IsJust (FindCol name t.cols)}
 115 |     -> TColumn t (TableColType name t)
 116 | 
 117 | ||| Extracts the name of a `TColumn`.
 118 | public export %inline
 119 | (.name) : TColumn t x -> String
 120 | (.name) (TC n) = n
 121 | 
 122 | namespace TColumn
 123 |   public export %inline
 124 |   fromString :
 125 |        {0 t      : SQLTable}
 126 |     -> (name     : String)
 127 |     -> {auto 0 p : IsJust (FindCol name t.cols)}
 128 |     -> TColumn t (TableColType name t)
 129 |   fromString = TC
 130 | 
 131 | --------------------------------------------------------------------------------
 132 | -- Schemata
 133 | --------------------------------------------------------------------------------
 134 | 
 135 | ||| A database schema is a (snoc-)list of tables.
 136 | |||
 137 | ||| The reason for preferring `SnocList` over `List` is that we
 138 | ||| typically build up a schema via joins in a query, and it is
 139 | ||| more natural to append table from left to right in a complex
 140 | ||| join statement than the other way round.
 141 | public export
 142 | 0 Schema : Type
 143 | Schema = SnocList SQLTable
 144 | 
 145 | ||| Looks up a table and column name in a schema.
 146 | |||
 147 | ||| This is called from `FindSchemaCol` after verifying that the
 148 | ||| column identifier has been fully qualified by prefixing it with
 149 | ||| a table name.
 150 | |||
 151 | ||| The table name is checked against the `as` field of the tables.
 152 | ||| This allows us to rename tables as part of a `SELECT` statement,
 153 | ||| which is especially important when joining a table with itself.
 154 | public export
 155 | FindSchemaCol2 : (table, column : String) -> Schema -> Maybe SqliteType
 156 | FindSchemaCol2 t c [<]       = Nothing
 157 | FindSchemaCol2 t c (sx :< x) =
 158 |   if x.as == t then FindCol c x.cols else FindSchemaCol2 t c sx
 159 | 
 160 | ||| Looks up an unqualified column name in a schema.
 161 | |||
 162 | ||| In order for this to succeed, the schema must either consist of
 163 | ||| only a single table, or the last table in the schema must be unnamed.
 164 | |||
 165 | ||| The latter case (the last table being unnamed) occurs, when we
 166 | ||| give column names to arbitrary SQL expressions in a `SELECT`
 167 | ||| statement. Since these expressions are evaluated after the
 168 | ||| rest of the schema is known (the rest of the schema comes from
 169 | ||| the `FROM` part of a `SELECT` statement), it is natural to just
 170 | ||| append an unnamed table with custom column names at the end of
 171 | ||| the schema.
 172 | public export
 173 | FindSchemaCol1 : String -> Schema -> Maybe SqliteType
 174 | FindSchemaCol1 n [< t]             = FindCol n t.cols
 175 | FindSchemaCol1 n (_:< ST "" "" cs) = FindCol n cs
 176 | FindSchemaCol1 n _                 = Nothing
 177 | 
 178 | ||| Looks up a - possibly qualified - column name in a schema.
 179 | |||
 180 | ||| This invokes `FindSchemaCol1` or `FindSchemaCol2` depending on
 181 | ||| whether the column name is fully qualified or not. A qualified
 182 | ||| column name is prefixed with the corresponding table's name
 183 | ||| followed by a dot: `"employees.name"`.
 184 | public export
 185 | FindSchemaCol : String -> Schema -> Maybe SqliteType
 186 | FindSchemaCol str s =
 187 |   case split ('.' ==) str of
 188 |     n:::[]  => FindSchemaCol1 n s
 189 |     t:::[n] => FindSchemaCol2 t n s
 190 |     _       => Nothing
 191 | 
 192 | ||| Computes the SQLite column type associated with column `column`
 193 | ||| in table `table` in the given list of tables.
 194 | public export
 195 | SchemaColType :
 196 |      (name : String)
 197 |   -> (s             : Schema)
 198 |   -> {auto 0 prf    : IsJust (FindSchemaCol name s)}
 199 |   -> SqliteType
 200 | SchemaColType n s = fromJust (FindSchemaCol n s)
 201 | 
 202 | ||| Proof that a column with the given name exists in
 203 | ||| the given list of tables.
 204 | public export
 205 | SchemaHasCol : Schema -> String -> Bool
 206 | SchemaHasCol [<]       s = False
 207 | SchemaHasCol (sx :< x) s = any ((s==) . name) x.cols || SchemaHasCol sx s
 208 | 
 209 | --------------------------------------------------------------------------------
 210 | -- Shared Columns
 211 | --------------------------------------------------------------------------------
 212 | 
 213 | ||| A column used in a `JOIN ... USING` statement: The column name must
 214 | ||| appear in both schemata.
 215 | public export
 216 | record JColumn (s : Schema) (t : SQLTable) where
 217 |   constructor JC
 218 |   name       : String
 219 |   {auto 0 p1 : SchemaHasCol s name === True}
 220 |   {auto 0 p2 : IsJust (FindCol name t.cols)}
 221 | 
 222 | namespace JColumn
 223 |   public export %inline
 224 |   fromString :
 225 |        {0 s       : Schema}
 226 |     -> {0 t       : SQLTable}
 227 |     -> (name      : String)
 228 |     -> {auto 0 p1 : SchemaHasCol s name === True}
 229 |     -> {auto 0 p2 : IsJust (FindCol name t.cols)}
 230 |     -> JColumn s t
 231 |   fromString = JC
 232 | 
 233 | --------------------------------------------------------------------------------
 234 | -- Idris Tables
 235 | --------------------------------------------------------------------------------
 236 | 
 237 | ||| A table of values together with a fitting header
 238 | public export
 239 | record Table a where
 240 |   constructor T
 241 |   {auto torow : ToRow a}
 242 |   header : LAll (const String) (ToRowTypes a)
 243 |   rows   : List a
 244 | 
 245 | hexChar : Bits8 -> Char
 246 | hexChar 0 = '0'
 247 | hexChar 1 = '1'
 248 | hexChar 2 = '2'
 249 | hexChar 3 = '3'
 250 | hexChar 4 = '4'
 251 | hexChar 5 = '5'
 252 | hexChar 6 = '6'
 253 | hexChar 7 = '7'
 254 | hexChar 8 = '8'
 255 | hexChar 9 = '9'
 256 | hexChar 10 = 'a'
 257 | hexChar 11 = 'b'
 258 | hexChar 12 = 'c'
 259 | hexChar 13 = 'd'
 260 | hexChar 14 = 'e'
 261 | hexChar _  = 'f'
 262 | 
 263 | export %inline
 264 | quote : Char
 265 | quote = '\''
 266 | 
 267 | ||| Encodes a `ByteString` as an SQL literal.
 268 | |||
 269 | ||| Every byte is encodec with two hexadecimal digits, and the
 270 | ||| whole string is wrapped in single quotes prefixed with an "X".
 271 | |||
 272 | ||| For instance, `encodeBytes (fromList [0xa1, 0x77])` yields the
 273 | ||| string "X'a177'".
 274 | export
 275 | encodeBytes : ByteString -> String
 276 | encodeBytes = pack . (\x => 'X'::quote::x) . foldr acc [quote]
 277 |   where
 278 |     %inline acc : Bits8 -> List Char -> List Char
 279 |     acc b cs = hexChar (b `shiftR` 4) :: hexChar (b .&. 0xf) :: cs
 280 | 
 281 | encode : (t : SqliteType) -> Maybe (IdrisType t) -> String
 282 | encode _ Nothing  = "NULL"
 283 | encode BLOB    (Just v) = encodeBytes v
 284 | encode TEXT    (Just v) = v
 285 | encode INTEGER (Just v) = show v
 286 | encode REAL    (Just v) = show v
 287 | 
 288 | pad : SqliteType -> Nat -> String -> String
 289 | pad BLOB    k = padRight k ' '
 290 | pad TEXT    k = padRight k ' '
 291 | pad INTEGER k = padLeft k ' '
 292 | pad REAL    k = padLeft k ' '
 293 | 
 294 | center : Nat -> String -> String
 295 | center k s =
 296 |   let ki := cast {to = Integer} (k `minus` length s)
 297 |       pl := ki `div` 2
 298 |       pr := ki - pl
 299 |    in replicate (cast pl) ' ' ++ s ++ replicate (cast pr) ' '
 300 | 
 301 | maxLength : Nat -> String -> Nat
 302 | maxLength n = max n . length
 303 | 
 304 | barSep : LAll (const String) ts -> String
 305 | barSep = fastConcat . intersperse " | " . forget
 306 | 
 307 | bar : LAll (const Nat) ts -> String
 308 | bar = fastConcat . intersperse "---" . map (`replicate` '-') . forget
 309 | 
 310 | export
 311 | prettyRows :
 312 |      {ts : _}
 313 |   -> (header : LAll (const String) ts)
 314 |   -> (rows   : List (LAll (Maybe . IdrisType) ts))
 315 |   -> String
 316 | prettyRows h rs =
 317 |   let cells   := map (hmapW encode) rs
 318 |       lengths := foldl (hzipWith maxLength) (hconst 0) (h :: cells)
 319 |       rows    := map (barSep . hzipWithW pad lengths) cells
 320 |       header  := barSep $ hzipWith center lengths h
 321 |    in fastUnlines (header :: bar lengths :: rows)
 322 | 
 323 | export
 324 | prettyTable : Table a -> String
 325 | prettyTable (T h rs) = prettyRows h (map toRow rs)
 326 | 
 327 | export %inline
 328 | printTable : HasIO io => Table a -> io ()
 329 | printTable = putStrLn . prettyTable
 330 |