
   0 | module Sqlite3.Cmd
   1 | 
   2 | import Data.List.Quantifiers
   3 | import Sqlite3.Expr
   4 | import Sqlite3.Marshall
   5 | import Sqlite3.Table
   6 | import Sqlite3.Types
   7 | 
   8 | %default total
   9 | 
  10 | export infix 1 .=
  11 | 
  12 | ||| We can always convert a list of marshallable Idris values to
  13 | ||| a list of SQL expressions.
  14 | export
  15 | toExprs : {ts : _} -> LAll (Maybe . IdrisType) ts -> LAll (Expr s) ts
  16 | toExprs {ts = []}    []      = []
  17 | toExprs {ts = t::ts} (v::vs) = maybe NULL (Lit t) v :: toExprs vs
  18 | 
  19 | ||| A single name-value pair in an `UPDATE` statement.
  20 | public export
  21 | record Val (t : SQLTable) where
  22 |   constructor V
  23 |   name        : String
  24 |   {auto 0 prf : IsJust (FindCol name t.cols)}
  25 |   val         : Expr [<t] (TableColType name t)
  26 | 
  27 | ||| Operator alias for the data constructor of `Val`,
  28 | ||| specialized for usage with Idris types with a
  29 | ||| `ToCell` implementation.
  30 | public export %inline
  31 | (.=) :
  32 |      {0 t        : SQLTable}
  33 |   -> {auto to    : ToCell a}
  34 |   -> (name       : String)
  35 |   -> {auto 0 prf : IsJust (FindCol name t.cols)}
  36 |   -> {auto 0 eq  : TableColType name t === ToCellType a}
  37 |   -> (val        : a)
  38 |   -> Val t
  39 | (.=) name v = V name (rewrite eq in val v)
  40 | 
  41 | 
  42 | ||| Foreign Key Actions
  43 | public export
  44 | data Action
  45 |   = SET_NULL
  46 |   | SET_DEFAULT
  47 |   | CASCADE
  48 |   | RESTRICT
  49 |   | NO_ACTION
  50 | 
  51 | public export
  52 | data Event
  53 |   = ON_UPDATE Action
  54 |   | ON_DELETE Action
  55 | 
  56 | ||| Column and table constraints to be used when creating a new table.
  57 | public export
  58 | data Constraint : SQLTable -> Type where
  59 |   NOT_NULL      : {0 x : _} -> TColumn t x -> Constraint t
  60 |   AUTOINCREMENT : {0 x : _} -> TColumn t x -> Constraint t
  61 |   UNIQUE        : {0 xs : _} -> LAll (TColumn t) xs -> Constraint t
  62 |   PRIMARY_KEY   : {0 xs : _} -> LAll (TColumn t) xs -> Constraint t
  63 |   ForeignKey    :
  64 |        {0 xs : _}
  65 |     -> {0 t : SQLTable}
  66 |     -> (s   : SQLTable)
  67 |     -> LAll (TColumn t) xs
  68 |     -> LAll (TColumn s) xs
  69 |     -> List Event
  70 |     -> Constraint t
  71 |   CHECK         : Expr [<t] BOOL -> Constraint t
  72 |   DEFAULT       :
  73 |        {0 t        : SQLTable}
  74 |     -> (s          : String)
  75 |     -> {auto 0 prf : IsJust (FindCol s t.cols)}
  76 |     -> (expr       : Expr [<t] (TableColType s t))
  77 |     -> Constraint t
  78 | 
  79 | ||| Convenience API to construct a foreign key constraint.
  80 | public export
  81 | FOREIGN_KEY :
  82 |      {0 xs : _}
  83 |   -> {0 t : SQLTable}
  84 |   -> (s   : SQLTable)
  85 |   -> LAll (TColumn t) xs
  86 |   -> LAll (TColumn s) xs
  87 |   -> Constraint t
  88 | FOREIGN_KEY s a b = ForeignKey s a b []
  89 | 
  90 | ||| Constructs a foreign key constraint with actions
  91 | public export
  92 | FOREIGN_KEY' :
  93 |      {0 xs : _}
  94 |   -> {0 t : SQLTable}
  95 |   -> (s   : SQLTable)
  96 |   -> LAll (TColumn t) xs
  97 |   -> LAll (TColumn s) xs
  98 |   -> List Event
  99 |   -> Constraint t
 100 | FOREIGN_KEY' = ForeignKey
 101 | 
 102 | ||| Index used to distinguish different types of commands.
 103 | |||
 104 | ||| This should facilitate writing combinator such as
 105 | ||| `IF_NOT_EXISTS` to operate only on certain commands.
 106 | public export
 107 | data CmdType : Type where
 108 |   TCreate : CmdType
 109 |   TDelete : CmdType
 110 |   TDrop   : CmdType
 111 |   TInsert : CmdType
 112 |   TSelect : CmdType
 113 |   TUpdate : CmdType
 114 | 
 115 | ||| Data management commands for creating tables and
 116 | ||| inserting, updating, or deleting rows in a table.
 117 | public export
 118 | data Cmd : CmdType -> Type where
 119 |   ||| Information used to create a new table.
 120 |   |||
 121 |   ||| It is recommended to use a combination of `CREATE_TABLE` and
 122 |   ||| `IF_NOT_EXISTS` instead of using this constructor directly.
 123 |   CreateTable :
 124 |        (t           : SQLTable)
 125 |     -> (attrs       : List (Constraint t))
 126 |     -> (ifNotExists : Bool)
 127 |     -> Cmd TCreate
 128 | 
 129 |   DropTable : (t : SQLTable) -> (ifExists : Bool) -> Cmd TDrop
 130 | 
 131 |   ||| Information required to insert data into a table.
 132 |   |||
 133 |   ||| This is well suited if you want to have full control over
 134 |   ||| the expressions used to insert data. If, however, you want
 135 |   ||| to insert an Idris value with a `ToRow` implementation,
 136 |   ||| consider using function `insert` instead.
 137 |   INSERT :
 138 |        {0 ts : List SqliteType}
 139 |     -> (t    : SQLTable)
 140 |     -> (cols : LAll (TColumn t) ts)
 141 |     -> (vals : LAll (Expr [<t]) ts)
 142 |     -> Cmd TInsert
 143 | 
 144 |   ||| Information required to insert or replace data in a a table.
 145 |   |||
 146 |   ||| This is like insert, but will replace values to fullfil `UNIQUE`
 147 |   ||| constraints in the table. As such, it is useful for updating
 148 |   ||| data that might not yet be present in a table.
 149 |   |||
 150 |   ||| This is well suited if you want to have full control over
 151 |   ||| the expressions used to replace data. If, however, you want
 152 |   ||| to insert an Idris value with a `ToRow` implementation,
 153 |   ||| consider using function `replace` instead.
 154 |   REPLACE :
 155 |        {0 ts : List SqliteType}
 156 |     -> (t : SQLTable)
 157 |     -> (cols : LAll (TColumn t) ts)
 158 |     -> (vals : LAll (Expr [<t]) ts)
 159 |     -> Cmd TInsert
 160 | 
 161 |   ||| Information required to update values in table.
 162 |   UPDATE :
 163 |        (t      : SQLTable)
 164 |     -> (set    : List (Val t))
 165 |     -> (where_ : Expr [<t] BOOL)
 166 |     -> Cmd TUpdate
 167 | 
 168 |   ||| Information required to delete values from a table.
 169 |   DELETE :
 170 |        (t      : SQLTable)
 171 |     -> (where_ : Expr [<t] BOOL)
 172 |     -> Cmd TDelete
 173 | 
 174 | ||| Utility version of `INSERT` for those cases when you want to
 175 | ||| insert an Idris value with a `ToRow` implementation.
 176 | export
 177 | insert :
 178 |     {auto as : ToRow v}
 179 |   ->(t       : SQLTable)
 180 |   -> LAll (TColumn t) (ToRowTypes v)
 181 |   -> (value : v)
 182 |   -> Cmd TInsert
 183 | insert t cs value = INSERT t cs (toExprs $ toRow value)
 184 | 
 185 | ||| Utility version of `REPLACE` for those cases when you want to
 186 | ||| replace an Idris value with a `ToRow` implementation.
 187 | export
 188 | replace :
 189 |     {auto as : ToRow v}
 190 |   ->(t       : SQLTable)
 191 |   -> LAll (TColumn t) (ToRowTypes v)
 192 |   -> (value : v)
 193 |   -> Cmd TInsert
 194 | replace t cs value = REPLACE t cs (toExprs $ toRow value)
 195 | 
 196 | namespace Cmds
 197 |   ||| A list of different types of commands, with the
 198 |   ||| command types being hidden.
 199 |   public export
 200 |   data Cmds : Type where
 201 |     Nil  : Cmds
 202 |     (::) : {0 t : _} -> Cmd t -> Cmds -> Cmds
 203 | 
 204 |   export
 205 |   (++) : Cmds -> Cmds -> Cmds
 206 |   []     ++ cs = cs
 207 |   (h::t) ++ cs = h :: (t ++ cs)
 208 | 
 209 |   export %inline
 210 |   Semigroup Cmds where (<+>) = (++)
 211 | 
 212 |   export %inline
 213 |   Monoid Cmds where neutral = []
 214 | 
 215 |   export
 216 |   fromList : List (Cmd t) -> Cmds
 217 |   fromList []      = []
 218 |   fromList (c::cs) = c :: fromList cs
 219 | 
 220 | ||| Create a table only if it does not yet exist.
 221 | public export
 222 | IF_NOT_EXISTS : Cmd TCreate -> Cmd TCreate
 223 | IF_NOT_EXISTS (CreateTable t attrs _) = CreateTable t attrs True
 224 | 
 225 | ||| Drop a table only if it exists.
 226 | public export
 227 | IF_EXISTS : Cmd TDrop -> Cmd TDrop
 228 | IF_EXISTS (DropTable t _) = DropTable t True
 229 | 
 230 | ||| Convenience constructor for the `CreateTable` command
 231 | public export %inline
 232 | CREATE_TABLE : (t : SQLTable) -> List (Constraint t) -> Cmd TCreate
 233 | CREATE_TABLE t as = CreateTable t as False
 234 | 
 235 | ||| Convenience constructor for the `DropTable` command
 236 | public export %inline
 237 | DROP_TABLE : (t : SQLTable) -> Cmd TDrop
 238 | DROP_TABLE t = DropTable t False
 239 | 
 240 | public export
 241 | 0 JoinPred : Schema -> SQLTable -> Type
 242 | JoinPred s t = Either (List $ JColumn  s t) (Expr (s:<t) BOOL)
 243 | 
 244 | public export
 245 | data Join : (s : Schema) -> (t : SQLTable) -> Type where
 246 |   JOIN :
 247 |        {0 t0 : SQLTable}
 248 |     -> {0 s  : Schema}
 249 |     -> (t : SQLTable)
 250 |     -> JoinPred (s:<t0) t
 251 |     -> Join (s:<t0) t
 252 | 
 253 |   OUTER_JOIN :
 254 |        {0 t0 : SQLTable}
 255 |     -> {0 s  : Schema}
 256 |     -> (t : SQLTable)
 257 |     -> JoinPred (s:<t0) t
 258 |     -> Join (s:<t0) t
 259 | 
 260 |   CROSS_JOIN : {0 t0 : _} -> {0 s : _} -> (t : SQLTable) -> Join (s:<t0) t
 261 | 
 262 |   FROM : (t : SQLTable) -> Join [<] t
 263 | 
 264 | public export %inline
 265 | USING : (JoinPred s t -> Join s t) -> List (JColumn s t) -> Join s t
 266 | USING f = f . Left
 267 | 
 268 | public export %inline
 269 | ON : (JoinPred s t -> Join s t) -> Expr (s:<t) BOOL -> Join s t
 270 | ON f = f . Right
 271 | 
 272 | ||| The `FROM` part in a select statement.
 273 | public export
 274 | data From : (s : Schema) -> Type where
 275 |   Lin  : From [<]
 276 |   (:<) : From s -> Join s t -> From (s :< t)
 277 | 
 278 | ||| Tag indicating, whether results should be sorted in ascending
 279 | ||| or descending order.
 280 | public export
 281 | data AscDesc = NoAsc | Asc | Desc
 282 | 
 283 | ||| Different collations used during ordering.
 284 | |||
 285 | ||| Currently, only `NO CASE` is supported.
 286 | public export
 287 | data Collation : (t : SqliteType) -> Type where
 288 |   None   : Collation t
 289 |   NOCASE : Collation TEXT
 290 | 
 291 | public export
 292 | record OrderingTerm (s : Schema) where
 293 |   constructor O
 294 |   {0 tpe : SqliteType}
 295 |   expr : Expr s tpe
 296 |   coll : Collation tpe
 297 |   asc  : AscDesc
 298 | 
 299 | public export %inline
 300 | ASC : Expr s t -> OrderingTerm s
 301 | ASC x = O x None Asc
 302 | 
 303 | public export %inline
 304 | DESC : Expr s t -> OrderingTerm s
 305 | DESC x = O x None Desc
 306 | 
 307 | public export %inline
 308 | COLLATE : (o : OrderingTerm s) -> Collation o.tpe -> OrderingTerm s
 309 | COLLATE o c = {coll := c} o
 310 | 
 311 | public export
 312 | record GroupingTerm (s : Schema) where
 313 |   constructor G
 314 |   {0 tpe : SqliteType}
 315 |   expr : Expr s tpe
 316 |   coll : Collation tpe
 317 | 
 318 | namespace GroupingTerm
 319 |   public export %inline
 320 |   fromString :
 321 |        {s        : Schema}
 322 |     -> (col      : String)
 323 |     -> {auto 0 p : IsJust (FindSchemaCol col s)}
 324 |     -> GroupingTerm s
 325 |   fromString col = G (fromString col) None
 326 | 
 327 | public export %inline
 328 | ord : GroupingTerm s -> OrderingTerm s
 329 | ord (G x c) = O x c NoAsc
 330 | 
 331 | public export
 332 | record NamedExpr (s : Schema) (t : SqliteType) where
 333 |   constructor AS
 334 |   expr : Expr s t
 335 |   name : String
 336 | 
 337 | namespace NameExpr
 338 |   public export %inline
 339 |   fromString :
 340 |        {s        : Schema}
 341 |     -> (col      : String)
 342 |     -> {auto 0 p : IsJust (FindSchemaCol col s)}
 343 |     -> NamedExpr s (SchemaColType col s)
 344 |   fromString col = Col col `AS` ""
 345 | 
 346 | ||| Extracts the column name we use to reference a named
 347 | ||| expression.
 348 | |||
 349 | ||| If a custom name has been set, this will be returned. Otherwise,
 350 | ||| if the expression references a table column, that columns (possibly
 351 | ||| qualified) name will be returned.
 352 | export
 353 | columnName : NamedExpr s t -> String
 354 | columnName (AS (Col col) "") = col
 355 | columnName (AS _         n)  = n
 356 | 
 357 | ||| Computes a list of named and typed columns from a list of
 358 | ||| name expressions.
 359 | |||
 360 | ||| Expressions with an empty string as their name are not included in
 361 | ||| the result.
 362 | public export
 363 | ExprColumns : {ts : _} -> LAll (NamedExpr s) ts -> List Column
 364 | ExprColumns             []              = []
 365 | ExprColumns             (AS _ "" :: xs) = ExprColumns xs
 366 | ExprColumns {ts = t::_} (AS _ n  :: xs) = C n t :: ExprColumns xs
 367 | 
 368 | ||| Appends an unnamed table with the list of columns coming from
 369 | ||| the given list of named expressions to a schema.
 370 | |||
 371 | ||| Expressions with an empty string as their name are not included in
 372 | ||| the result.
 373 | |||
 374 | ||| This is used to compute the full `Schema` to be used in
 375 | ||| those fields of `Query` that are used for filtering, grouping, and
 376 | ||| sorting.
 377 | public export
 378 | ExprSchema : {s : _} -> {ts : _} -> LAll (NamedExpr s) ts -> Schema
 379 | ExprSchema xs =
 380 |   case ExprColumns xs of
 381 |     [] => s
 382 |     cs => s :< ST "" "" cs
 383 | 
 384 | ||| Different types of `SELECT` commands.
 385 | public export
 386 | record Query (t : Type) where
 387 |   [noHints]
 388 |   constructor Q
 389 |   {auto fromRow : FromRow t}
 390 |   distinct      : Bool
 391 |   schema        : Schema
 392 |   from          : From schema
 393 |   columns       : LAll (NamedExpr schema) (FromRowTypes t)
 394 |   where_        : Expr (ExprSchema columns) BOOL
 395 |   having        : Expr (ExprSchema columns) BOOL
 396 |   group_by      : List (GroupingTerm (ExprSchema columns))
 397 |   order_by      : List (OrderingTerm (ExprSchema columns))
 398 |   limit         : Maybe Nat
 399 |   offset        : Nat
 400 | 
 401 | public export %inline %hint
 402 | queryAsRow : (q : Query t) => FromRow t
 403 | queryAsRow = q.fromRow
 404 | 
 405 | public export
 406 | 0 LQuery : List Type -> Type
 407 | LQuery = Query . HList
 408 | 
 409 | export infixl 7 `GROUP_BY`,`ORDER_BY`,`WHERE`, `LIMIT`, `OFFSET`, `HAVING`
 410 | 
 411 | public export %inline
 412 | SELECT :
 413 |      {s : _}
 414 |   -> {auto fromRow : FromRow t}
 415 |   -> LAll (NamedExpr s) (FromRowTypes t)
 416 |   -> From s
 417 |   -> Query t
 418 | SELECT xs from = Q False s from xs TRUE TRUE [] [] Nothing 0
 419 | 
 420 | public export %inline
 421 | SELECT_DISTINCT :
 422 |      {s : _}
 423 |   -> {auto fromRow : FromRow t}
 424 |   -> LAll (NamedExpr s) (FromRowTypes t)
 425 |   -> From s
 426 |   -> Query t
 427 | SELECT_DISTINCT xs from = Q True s from xs TRUE TRUE [] [] Nothing 0
 428 | 
 429 | public export %inline
 430 | GROUP_BY : (q : Query t) -> List (GroupingTerm $ ExprSchema q.columns) -> Query t
 431 | GROUP_BY q gs = {group_by := gs} q
 432 | 
 433 | public export %inline
 434 | WHERE : (q : Query t) -> Expr (ExprSchema q.columns) BOOL -> Query t
 435 | WHERE q p = {where_ := p} q
 436 | 
 437 | public export %inline
 438 | HAVING : (q : Query t) -> Expr (ExprSchema q.columns) BOOL -> Query t
 439 | HAVING q p = {having := p} q
 440 | 
 441 | public export %inline
 442 | ORDER_BY : (q : Query t) -> List (OrderingTerm (ExprSchema q.columns)) -> Query t
 443 | ORDER_BY q os = {order_by := os} q
 444 | 
 445 | public export %inline
 446 | LIMIT : (q : Query t) -> Nat -> Query t
 447 | LIMIT q n = {limit := Just n} q
 448 | 
 449 | public export %inline
 450 | OFFSET : (q : Query t) -> Nat -> Query t
 451 | OFFSET q n = {offset := n} q
 452 |