
   0 | module Sqlite3.Expr
   1 | 
   2 | import Data.Bits
   3 | import Data.Buffer.Indexed
   4 | import Data.ByteString
   5 | import Data.String
   6 | 
   7 | import Sqlite3.Marshall
   8 | import Sqlite3.Table
   9 | import Sqlite3.Types
  10 | 
  11 | %default total
  12 | 
  13 | public export
  14 | data Numeric : SqliteType -> Type where
  15 |   N_INTEGER : Numeric INTEGER
  16 |   N_REAL    : Numeric REAL
  17 | 
  18 | ||| A syntax tree type representing well-typed SQLite expressions.
  19 | public export
  20 | data Expr : Schema -> SqliteType -> Type where
  21 |   ||| A literal value in an SQL expression
  22 |   Lit    : (t : SqliteType) -> (v : IdrisType t) -> Expr s t
  23 | 
  24 |   ||| The `NULL` literal
  25 |   NULL   : Expr s t
  26 | 
  27 |   ||| Alias for the literal `1`, which corresponds to `True` in
  28 |   ||| boolean expressions
  29 |   TRUE   : Expr s BOOL
  30 | 
  31 |   ||| Alias for the literal `0`, which corresponds to `False` in
  32 |   ||| boolean expressions
  33 |   FALSE  : Expr s BOOL
  34 | 
  35 |   ||| A raw expressions string that will be used as given.
  36 |   Raw    : String -> Expr s t
  37 | 
  38 |   ||| A column in a list of tables. Typically, it is convenient to
  39 |   ||| use string literals directly for this (see `Expr.fromString`).
  40 |   Col    :
  41 |        {0 s      : Schema}
  42 |     -> (col      : String)
  43 |     -> {auto 0 p : IsJust (FindSchemaCol col s)}
  44 |     -> Expr s (SchemaColType col s)
  45 | 
  46 |   ||| Greater-than operator.
  47 |   |||
  48 |   ||| Note, that this is subject to SQL's three-valued logic in the
  49 |   ||| presence of `NULL`.
  50 |   (>)    : Expr s t -> Expr s t -> Expr s BOOL
  51 | 
  52 |   ||| Less-than operator.
  53 |   |||
  54 |   ||| Note, that this is subject to SQL's three-valued logic in the
  55 |   ||| presence of `NULL`.
  56 |   (<)    : Expr s t -> Expr s t -> Expr s BOOL
  57 | 
  58 |   ||| Greater-than or equals operator.
  59 |   |||
  60 |   ||| Note, that this is subject to SQL's three-valued logic in the
  61 |   ||| presence of `NULL`.
  62 |   (>=)   : Expr s t -> Expr s t -> Expr s BOOL
  63 | 
  64 |   ||| Less-than or equals operator.
  65 |   |||
  66 |   ||| Note, that this is subject to SQL's three-valued logic in the
  67 |   ||| presence of `NULL`.
  68 |   (<=)   : Expr s t -> Expr s t -> Expr s BOOL
  69 | 
  70 |   ||| Equality operator.
  71 |   |||
  72 |   ||| Note, that this is subject to SQL's three-valued logic in the
  73 |   ||| presence of `NULL`.
  74 |   (==)   : Expr s t -> Expr s t -> Expr s BOOL
  75 | 
  76 |   ||| Inequality operator.
  77 |   |||
  78 |   ||| We use the same operator as in the `Eq` interface here, but this
  79 |   ||| corresponds to SQL's `<>` (or `!=`) operator.
  80 |   |||
  81 |   ||| Note, that this is subject to SQL's three-valued logic in the
  82 |   ||| presence of `NULL`.
  83 |   (/=)   : Expr s t -> Expr s t -> Expr s BOOL
  84 | 
  85 |   ||| Equality test.
  86 |   |||
  87 |   ||| Unlike `(==)`, this will always result in `TRUE` or `FALSE`
  88 |   ||| even in the presence of `NULL`.
  89 |   IS     : Expr s t -> Expr s t -> Expr s BOOL
  90 | 
  91 |   ||| Inequality test.
  92 |   |||
  93 |   ||| Unlike `(==)`, this will always result in `TRUE` or `FALSE`
  94 |   ||| even in the presence of `NULL`.
  95 |   IS_NOT : Expr s t -> Expr s t -> Expr s BOOL
  96 | 
  97 |   ||| Logical `AND`.
  98 |   |||
  99 |   ||| Note, that this is subject to SQL's three-valued logic in the
 100 |   ||| presence of `NULL`.
 101 |   (&&)   : Expr s BOOL -> Expr s BOOL -> Expr s BOOL
 102 | 
 103 |   ||| Logical `OR`.
 104 |   |||
 105 |   ||| Note, that this is subject to SQL's three-valued logic in the
 106 |   ||| presence of `NULL`.
 107 |   (||)   : Expr s BOOL -> Expr s BOOL -> Expr s BOOL
 108 | 
 109 |   ||| Logical negation.
 110 |   |||
 111 |   ||| Note, that this is subject to SQL's three-valued logic in the
 112 |   ||| presence of `NULL`.
 113 |   NOT    : Expr s BOOL -> Expr s BOOL
 114 | 
 115 |   ||| Bit-wise `AND`.
 116 |   |||
 117 |   ||| This corresponds to SQLite's `&` operator.
 118 |   (.&.)  : Expr s INTEGER -> Expr s INTEGER -> Expr s INTEGER
 119 | 
 120 |   ||| Bit-wise `OR`.
 121 |   |||
 122 |   ||| This corresponds to SQLite's `|` operator.
 123 |   (.|.)  : Expr s INTEGER -> Expr s INTEGER -> Expr s INTEGER
 124 | 
 125 |   ||| Bit-wise left shift.
 126 |   |||
 127 |   ||| This corresponds to SQLite's `<<` operator.
 128 |   ShiftL : Expr s INTEGER -> Expr s INTEGER -> Expr s INTEGER
 129 | 
 130 |   ||| Bit-wise right shift.
 131 |   |||
 132 |   ||| This corresponds to SQLite's `>>` operator.
 133 |   ShiftR : Expr s INTEGER -> Expr s INTEGER -> Expr s INTEGER
 134 | 
 135 | 
 136 |   ||| Numeric addition.
 137 |   |||
 138 |   ||| Since `Expr s t` implements `Num` for numeric types `t`, you can
 139 |   ||| typically use the addition operator `(+)` instead of this constructor.
 140 |   Add   : (0 prf : Numeric t) => Expr s t -> Expr s t -> Expr s t
 141 | 
 142 |   ||| Numeric multiplication.
 143 |   |||
 144 |   ||| Since `Expr s t` implements `Num` for numeric types `t`, you can
 145 |   ||| typically use the multiplication operator `(*)` instead of this
 146 |   ||| constructor.
 147 |   Mult  : (0 prf : Numeric t) => Expr s t -> Expr s t -> Expr s t
 148 | 
 149 |   ||| Numeric subtraction.
 150 |   |||
 151 |   ||| Since `Expr s t` implements `Neg` for numeric types `t`, you can
 152 |   ||| typically use the subtraction operator `(-)` instead of this
 153 |   ||| constructor.
 154 |   Sub   : (0 prf : Numeric t) => Expr s t -> Expr s t -> Expr s t
 155 | 
 156 |   ||| Computes the absolute of an expressions.
 157 |   |||
 158 |   ||| This corresponds to the `abs()` function.
 159 |   Abs   : (0 prf : Numeric t) => Expr s t -> Expr s t
 160 | 
 161 |   ||| Numeric negation.
 162 |   Neg   : (0 prf : Numeric t) => Expr s t -> Expr s t
 163 | 
 164 |   ||| Numeric division.
 165 |   |||
 166 |   ||| Since `Expr s t` implements `Integral` for numeric types `INTEGER`,
 167 |   ||| you can typically use `div` for integer division. Likewise, you can
 168 |   ||| use `(/)` for floating point division.
 169 |   Div   : (0 prf : Numeric t) => Expr s t -> Expr s t -> Expr s t
 170 | 
 171 |   ||| Computes the modulus of two integers.
 172 |   |||
 173 |   ||| This corresponds to the `%` operator in SQL.
 174 |   Mod   : Expr s INTEGER -> Expr s INTEGER -> Expr s INTEGER
 175 | 
 176 |   ||| String concatenation.
 177 |   |||
 178 |   ||| This corresponds to the `||` operator in SQL.
 179 |   (++)   : Expr s TEXT -> Expr s TEXT -> Expr s TEXT
 180 | 
 181 |   ||| The current time as a string.
 182 |   CURRENT_TIME      : Expr s TEXT
 183 | 
 184 |   ||| The current date as a string.
 185 |   CURRENT_DATE      : Expr s TEXT
 186 | 
 187 |   ||| The current date and time as a string.
 188 |   CURRENT_TIMESTAMP : Expr s TEXT
 189 | 
 190 |   ||| Matches the given text expression against the given
 191 |   ||| text pattern.
 192 |   LIKE              : Expr s TEXT -> (pattern : Expr s TEXT) -> Expr s BOOL
 193 | 
 194 |   ||| Matches the given text expression against the given
 195 |   ||| GLOB pattern.
 196 |   GLOB              : Expr s TEXT -> (pattern : Expr s TEXT) -> Expr s BOOL
 197 | 
 198 |   ||| True, if the given value appears in the given list of values.
 199 |   IN                : Expr s t -> List (Expr s t) -> Expr s BOOL
 200 | 
 201 |   ||| Returns the first non-NULL value in the given list of expressions.
 202 |   COALESCE          : List (Expr s t) -> Expr s t
 203 | 
 204 |   ||| Counts the number of aggregated values.
 205 |   |||
 206 |   ||| This is typically used with a `GROUP BY` statement.
 207 |   COUNT             : Expr s t -> Expr s INTEGER
 208 | 
 209 |   ||| Returns the average of accumulated values.
 210 |   |||
 211 |   ||| This is typically used with a `GROUP BY` statement.
 212 |   AVG               : (0 prf : Numeric t) => Expr s t -> Expr s REAL
 213 | 
 214 |   ||| Returns the sum of accumulated values.
 215 |   |||
 216 |   ||| This is typically used with a `GROUP BY` statement.
 217 |   SUM               : (0 prf : Numeric t) => Expr s t -> Expr s t
 218 | 
 219 |   ||| Returns the minimum of accumulated values.
 220 |   |||
 221 |   ||| This is typically used with a `GROUP BY` statement.
 222 |   MIN               : Expr s t -> Expr s t
 223 | 
 224 |   ||| Returns the maximum of accumulated values.
 225 |   |||
 226 |   ||| This is typically used with a `GROUP BY` statement.
 227 |   MAX               : Expr s t -> Expr s t
 228 | 
 229 |   ||| Concatenates aggregated text values using the given separator.
 230 |   |||
 231 |   ||| This is typically used with a `GROUP BY` statement.
 232 |   GROUP_CONCAT      : Expr s TEXT -> (sep : String) -> Expr s TEXT
 233 | 
 234 | export %inline
 235 | Num (Expr s INTEGER) where
 236 |   fromInteger = Lit INTEGER . fromInteger
 237 |   (+) = Add
 238 |   (*) = Mult
 239 | 
 240 | export %inline
 241 | Neg (Expr s INTEGER) where
 242 |   negate = Neg
 243 |   (-)    = Sub
 244 | 
 245 | export %inline
 246 | Integral (Expr s INTEGER) where
 247 |   div = Div
 248 |   mod = Mod
 249 | 
 250 | export %inline
 251 | Num (Expr s REAL) where
 252 |   fromInteger = Lit REAL . fromInteger
 253 |   (+) = Add
 254 |   (*) = Mult
 255 | 
 256 | export %inline
 257 | Neg (Expr s REAL) where
 258 |   negate = Neg
 259 |   (-)    = Sub
 260 | 
 261 | export %inline
 262 | Fractional (Expr s REAL) where
 263 |   (/) = Div
 264 | 
 265 | export %inline
 266 | FromDouble (Expr s REAL) where
 267 |   fromDouble = Lit REAL
 268 | 
 269 | export %inline
 270 | fromString :
 271 |      {s        : Schema}
 272 |   -> (col      : String)
 273 |   -> {auto 0 p : IsJust (FindSchemaCol col s)}
 274 |   -> Expr s (SchemaColType col s)
 275 | fromString = Col
 276 | 
 277 | ||| Convert a value of a marshallable type to a literal expression.
 278 | export
 279 | val : ToCell a => a -> Expr s (ToCellType a)
 280 | val x =
 281 |   case toCell x of
 282 |     Nothing => NULL
 283 |     Just v  => Lit _ v
 284 | 
 285 | export %inline
 286 | text : String -> Expr s TEXT
 287 | text = val
 288 | 
 289 | export %inline
 290 | int : Int64 -> Expr s INTEGER
 291 | int = val
 292 | 
 293 | export %inline
 294 | blob : ByteString -> Expr s BLOB
 295 | blob = val
 296 | 
 297 | export %inline
 298 | real : Double -> Expr s REAL
 299 | real = val
 300 | 
 301 | --------------------------------------------------------------------------------
 302 | -- Encode
 303 | --------------------------------------------------------------------------------
 304 | 
 305 | ||| Converts a list of values to strings and concatenates them using
 306 | ||| a comma as the separator.
 307 | export
 308 | commaSep : (a -> String) -> List a -> String
 309 | commaSep f = concat . intersperse ", " . map f
 310 | 
 311 | ||| Encodes a `String` as an SQL literal.
 312 | |||
 313 | ||| The whole string is wrapped in single quotes. Single quotes withing
 314 | ||| the string are escaped by doubling them.
 315 | export
 316 | encodeText : String -> String
 317 | encodeText = go [<quote] . unpack
 318 |   where
 319 |     go : SnocList Char -> List Char -> String
 320 |     go sc []           = pack $ sc <>> [quote]
 321 |     go sc ('\'' :: xs) = go (sc :< quote :< quote) xs
 322 |     go sc (x    :: xs) = go (sc :< x) xs
 323 | 
 324 | ||| Encodes an SQL literal as a string.
 325 | export
 326 | encodeLit : (t : SqliteType) -> IdrisType t -> String
 327 | encodeLit BLOB x    = encodeBytes x
 328 | encodeLit TEXT x    = encodeText x
 329 | encodeLit INTEGER x = show x
 330 | encodeLit REAL x    = show x
 331 | 
 332 | encOp : String -> Expr s t -> Expr s t -> String
 333 | 
 334 | encPrefix : String -> Expr s t -> String
 335 | 
 336 | encExprs : SnocList String -> List (Expr s t) -> String
 337 | 
 338 | encFun1 : String -> Expr s t -> String
 339 | 
 340 | encFun : String -> List (Expr s t) -> String
 341 | 
 342 | ||| Encodes an expression as a string.
 343 | |||
 344 | ||| Literals will be correctly escaped and converted.
 345 | |||
 346 | ||| Note: See module `Sqlite3.Parameter` for encoding of expressions
 347 | |||       with SQL parameters that will be bound separately when
 348 | |||       binding the statement.
 349 | export
 350 | encodeExpr : Expr s t -> String
 351 | encodeExpr (Lit t v)    = encodeLit t v
 352 | encodeExpr (Add x y)    = encOp "+" x y
 353 | encodeExpr (Mult x y)   = encOp "*" x y
 354 | encodeExpr (Sub x y)    = encOp "-" x y
 355 | encodeExpr (Div x y)    = encOp "/" x y
 356 | encodeExpr (Mod x y)    = encOp "%" x y
 357 | encodeExpr (Abs y)      = encFun1 "abs" y
 358 | encodeExpr (x < y)      = encOp "<" x y
 359 | encodeExpr (x > y)      = encOp ">" x y
 360 | encodeExpr (x <= y)     = encOp "<=" x y
 361 | encodeExpr (x >= y)     = encOp ">=" x y
 362 | encodeExpr (x == y)     = encOp "==" x y
 363 | encodeExpr (IS x y)     = encOp "IS" x y
 364 | encodeExpr (IS_NOT x y) = encOp "IS NOT" x y
 365 | encodeExpr (x /= y)     = encOp "!=" x y
 366 | encodeExpr (x && y)     = encOp "AND" x y
 367 | encodeExpr (x || y)     = encOp "OR" x y
 368 | encodeExpr (x ++ y)     = encOp "||" x y
 369 | encodeExpr (x .&. y)    = encOp "&" x y
 370 | encodeExpr (x .|. y)    = encOp "|" x y
 371 | encodeExpr (ShiftR x y) = encOp ">>" x y
 372 | encodeExpr (ShiftL x y) = encOp "<<" x y
 373 | encodeExpr (NOT x)      = encPrefix "NOT" x
 374 | encodeExpr (Neg x)      = encPrefix "-" x
 375 | encodeExpr (Raw s)      = s
 376 | encodeExpr (Col c)      = c
 377 | encodeExpr NULL         = "NULL"
 378 | encodeExpr TRUE         = "1"
 379 | encodeExpr FALSE        = "0"
 380 | encodeExpr CURRENT_TIME      = "CURRENT_TIME"
 381 | encodeExpr CURRENT_DATE      = "CURRENT_DATE"
 382 | encodeExpr CURRENT_TIMESTAMP = "CURRENT_TIMESTAMP"
 383 | encodeExpr (LIKE x y)        = encOp "LIKE" x y
 384 | encodeExpr (GLOB x y)        = encOp "GLOB" x y
 385 | encodeExpr (IN x xs)         = "\{encodeExpr x} IN (\{encExprs [<] xs})"
 386 | encodeExpr (COALESCE xs)     = encFun "coalesce" xs
 387 | encodeExpr (COUNT x)         = encFun1 "count" x
 388 | encodeExpr (AVG x)           = encFun1 "avg" x
 389 | encodeExpr (SUM x)           = encFun1 "sum" x
 390 | encodeExpr (MIN x)           = encFun1 "min" x
 391 | encodeExpr (MAX x)           = encFun1 "max" x
 392 | encodeExpr (GROUP_CONCAT x s) = "group_concat(\{encodeExpr x}, \{s})"
 393 | 
 394 | encOp s x y =
 395 |   let sx := encodeExpr x
 396 |       sy := encodeExpr y
 397 |    in "(\{sx} \{s} \{sy})"
 398 | 
 399 | encPrefix s x = "\{s}(\{encodeExpr x})"
 400 | 
 401 | encExprs sc []      = commaSep id (sc <>> [])
 402 | encExprs sc (x::xs) = encExprs (sc :< encodeExpr x) xs
 403 | 
 404 | encFun f xs      = "\{f}(\{encExprs [<] xs})"
 405 | 
 406 | encFun1 f x      = "\{f}(\{encodeExpr x})"
 407 |