0 | module Control.RIO.Sqlite3
  1 |
  2 | import public Control.RIO.App
  3 | import public Sqlite3
  4 | import public Data.List.Quantifiers
  5 |
  6 | %default total
  7 |
  8 | parameters {auto has : Has SqlError es}
  9 |
 10 |   ||| Open a connection to the given database and use it to
 11 |   ||| run the given effectful computation.
 12 |   |||
 13 |   ||| This comes with the guarantees that the connection is properly
 14 |   ||| closed at the end.
 15 |   export
 16 |   withDB : String -> (DB => App es a) -> App es a
 17 |   withDB s f = do
 18 |     db <- injectIO $ sqliteOpen s
 19 |     finally (liftIO $ sqliteClose' db) (f @{db})
 20 |
 21 |   ||| Prepare an SQL statement and use it to run the given effectful computation.
 22 |   |||
 23 |   ||| This comes with the guarantees that the statement is properly
 24 |   ||| finalized at the end.
 25 |   export
 26 |   withStmt : DB => String -> (Stmt => App es a) -> App es a
 27 |   withStmt str f = do
 28 |     stmt <- injectIO $ sqlitePrepare str
 29 |     finally (liftIO $ sqliteFinalize' stmt) (f @{stmt})
 30 |
 31 |   ||| Prepare an SQL statement and use it to run the given effectful computation.
 32 |   |||
 33 |   ||| This comes with the guarantees that the statement is properly
 34 |   ||| finalized at the end.
 35 |   |||
 36 |   ||| This works just like `withStmt` but it also bind the given arguments.
 37 |   export
 38 |   bindParams : DB => Stmt => List Parameter -> App es ()
 39 |   bindParams ps = injectIO (sqliteBind ps)
 40 |
 41 |   ||| Prepare an SQL statement and use it to run the given effectful computation.
 42 |   |||
 43 |   ||| This comes with the guarantees that the statement is properly
 44 |   ||| finalized at the end.
 45 |   |||
 46 |   ||| This works just like `withStmt` but it also bind the given arguments.
 47 |   export
 48 |   withBoundStmt : DB => ParamStmt -> (Stmt => App es a) -> App es a
 49 |   withBoundStmt st f =
 50 |     let (ps, str) := runState init st
 51 |      in withStmt str (bindParams ps.args >> f)
 52 |
 53 |   ||| Runs an SQL statement, returning the response from the database.
 54 |   export
 55 |   step : (s : Stmt) => App es SqlResult
 56 |   step @{s} = liftIO $ sqliteStep s
 57 |
 58 |   ||| Prepares, executes and finalizes the given SQL statement.
 59 |   |||
 60 |   ||| The statement may hold a list of parameters, which will be
 61 |   ||| bound prior to executing the statement.
 62 |   export
 63 |   commit : DB => ParamStmt -> App es ()
 64 |   commit st = withBoundStmt st (ignore step)
 65 |
 66 |   ||| Prepares and executes the given SQL query and extracts up to
 67 |   ||| `n` rows of results.
 68 |   export
 69 |   selectRows : DB => FromRow a => ParamStmt -> (n : Nat) -> App es (List a)
 70 |   selectRows st n = withBoundStmt st (injectIO $ loadRows n)
 71 |
 72 |   ||| Prepares and executes the given SQL query and extracts the
 73 |   ||| first result.
 74 |   export
 75 |   selectRow : DB => FromRow a => ParamStmt -> App es a
 76 |   selectRow st = do
 77 |     [v] <- selectRows st 1 | _ => throw NoMoreData
 78 |     pure v
 79 |
 80 |   ||| Prepares and executes the given SQL query and extracts the
 81 |   ||| first result (if any).
 82 |   export
 83 |   findRow : DB => FromRow a => ParamStmt -> App es (Maybe a)
 84 |   findRow st = do
 85 |     [v] <- selectRows st 1 | _ => pure Nothing
 86 |     pure $ Just v
 87 |
 88 | --------------------------------------------------------------------------------
 89 | -- Runnings Commands
 90 | --------------------------------------------------------------------------------
 91 |
 92 |   ||| Executes the given SQL command.
 93 |   export %inline
 94 |   cmd : DB => Cmd t -> App es ()
 95 |   cmd = commit . encodeCmd
 96 |
 97 |   rollback : DB => HSum es -> App es a
 98 |   rollback x = ignore (withStmt "ROLLBACK TRANSACTION" step) >> fail x
 99 |
100 |   ||| Runs several commands in a single transaction.
101 |   |||
102 |   ||| If any of the commands fails, the whole transaction is rolled back.
103 |   export %inline
104 |   cmds : DB => Cmds -> App es ()
105 |   cmds cs = do
106 |     ignore $ withStmt "BEGIN TRANSACTION" step
107 |     catch rollback (runCommands cs)
108 |     ignore $ withStmt "COMMIT TRANSACTION" step
109 |
110 |     where
111 |       runCommands : Cmds -> App es ()
112 |       runCommands []      = pure ()
113 |       runCommands (c::cs) = cmd c >> runCommands cs
114 |
115 |   ||| Runs the given query and accumulates at most `n` rows.
116 |   export %inline
117 |   query : DB => Query t -> (n : Nat) -> App es (List t)
118 |   query q = selectRows (encodeQuery q)
119 |
120 |   ||| Runs the given query and accumulates at most `n` rows.
121 |   |||
122 |   ||| The result is stored in a `Table` with a proper header of
123 |   ||| column names.
124 |   export
125 |   queryTable :
126 |        {auto db : DB}
127 |     -> {auto tr : ToRow t}
128 |     -> (q : Query t)
129 |     -> {auto 0 prf : ToRowTypes t === FromRowTypes t}
130 |     -> Nat
131 |     -> App es (Table t)
132 |   queryTable {prf} q n = do
133 |     rs <- query q n
134 |     pure (T (rewrite prf in hmap columnName q.columns) rs)
135 |