0 | module FS.Sqlite3
  1 |
  2 | import public Sqlite3
  3 | import public FS
  4 |
  5 | %default total
  6 |
  7 | export
  8 | Resource (Async e) Stmt where
  9 |   cleanup = liftIO . sqliteFinalize'
 10 |
 11 | export
 12 | Resource (Async e) DB where
 13 |   cleanup = liftIO . sqliteClose'
 14 |
 15 | toRes : Chunk a -> UnfoldRes () () (List a)
 16 | toRes (More xs) = More xs ()
 17 | toRes (Done xs) = Last () xs
 18 |
 19 | parameters {auto has : Has SqlError es}
 20 |
 21 |   export %inline
 22 |   openSqlite : String -> Async e es DB
 23 |   openSqlite = injectIO . sqliteOpen
 24 |
 25 |   export %inline
 26 |   openStmt : DB => String -> Async e es Stmt
 27 |   openStmt = injectIO . sqlitePrepare
 28 |
 29 |   ||| Open a connection to the given database and use it to
 30 |   ||| run the given effectful computation.
 31 |   |||
 32 |   ||| This comes with the guarantees that the connection is properly
 33 |   ||| closed at the end.
 34 |   export
 35 |   withDB : String -> (DB => Async e es a) -> Async e es a
 36 |   withDB s f = use1 (openSqlite s) $ \_ => f
 37 |
 38 |   ||| Prepare an SQL statement and use it to run the given effectful computation.
 39 |   |||
 40 |   ||| This comes with the guarantees that the statement is properly
 41 |   ||| finalized at the end.
 42 |   export
 43 |   withStmt : DB => String -> (Stmt => Async e es a) -> Async e es a
 44 |   withStmt s f = use1 (openStmt s) $ \_ => f
 45 |
 46 |   ||| Prepare an SQL statement and use it to run the given effectful computation.
 47 |   |||
 48 |   ||| This comes with the guarantees that the statement is properly
 49 |   ||| finalized at the end.
 50 |   export
 51 |   bindParams : DB => Stmt => List Parameter -> Async e es ()
 52 |   bindParams = injectIO . sqliteBind
 53 |
 54 |   export
 55 |   openBoundStmt : DB => ParamStmt -> Async e es Stmt
 56 |   openBoundStmt st = Prelude.do
 57 |     let (ps, str) := runState init st
 58 |     st <- openStmt str
 59 |     bindParams ps.args
 60 |     pure st
 61 |
 62 |   ||| Prepare an SQL statement and use it to run the given effectful computation.
 63 |   |||
 64 |   ||| This comes with the guarantees that the statement is properly
 65 |   ||| finalized at the end.
 66 |   |||
 67 |   ||| This works just like `withStmt` but it also bind the given arguments.
 68 |   export
 69 |   withBoundStmt : DB => ParamStmt -> (Stmt => Async e es a) -> Async e es a
 70 |   withBoundStmt st f = use1 (openBoundStmt st) $ \_ => f
 71 |
 72 |   ||| Runs an SQL statement, returning the response from the database.
 73 |   export
 74 |   step : (s : Stmt) => Async e es SqlResult
 75 |   step @{s} = liftIO $ sqliteStep s
 76 |
 77 |   ||| Prepares, executes and finalizes the given SQL statement.
 78 |   |||
 79 |   ||| The statement may hold a list of parameters, which will be
 80 |   ||| bound prior to executing the statement.
 81 |   export
 82 |   commit : DB => ParamStmt -> Async e es ()
 83 |   commit st = withBoundStmt st (ignore step)
 84 |
 85 |   ||| Prepares and executes the given SQL query and extracts up to
 86 |   ||| `n` rows of results.
 87 |   export
 88 |   selectRows : DB => FromRow a => ParamStmt -> (n : Nat) -> Async e es (List a)
 89 |   selectRows st n = withBoundStmt st (injectIO $ loadRows n)
 90 |
 91 |   ||| Prepares and executes the given SQL query and extracts the
 92 |   ||| first result.
 93 |   export
 94 |   selectRow : DB => FromRow a => ParamStmt -> Async e es a
 95 |   selectRow st = do
 96 |     [v] <- selectRows st 1 | _ => throw NoMoreData
 97 |     pure v
 98 |
 99 |   ||| Prepares and executes the given SQL query and extracts the
100 |   ||| first result (if any).
101 |   export
102 |   findRow : DB => FromRow a => ParamStmt -> Async e es (Maybe a)
103 |   findRow st = do
104 |     [v] <- selectRows st 1 | _ => pure Nothing
105 |     pure $ Just v
106 |
107 |   export
108 |   rows :
109 |        {auto cs : ChunkSize}
110 |     -> {auto db : DB}
111 |     -> {auto fr : FromRow a}
112 |     -> ParamStmt
113 |     -> AsyncStream e es (List a)
114 |   rows {cs = CS sz} st =
115 |     resource (openBoundStmt st) $ \_ =>
116 |       unfoldEval () $ \_ => toRes <$> injectIO (loadChunk {a} sz)
117 |
118 | --------------------------------------------------------------------------------
119 | -- Runnings Commands
120 | --------------------------------------------------------------------------------
121 |
122 |   ||| Executes the given SQL command.
123 |   export %inline
124 |   cmd : DB => Cmd t -> Async e es ()
125 |   cmd = commit . encodeCmd
126 |
127 |   rollback : DB => HSum es -> Async e es a
128 |   rollback x = ignore (withStmt "ROLLBACK TRANSACTION" step) >> fail x
129 |
130 |   ||| Runs several commands in a single transaction.
131 |   |||
132 |   ||| If any of the commands fails, the whole transaction is rolled back.
133 |   export %inline
134 |   cmds : DB => Cmds -> Async e es ()
135 |   cmds cs =
136 |     uncancelable $ \poll => Prelude.do
137 |       ignore $ withStmt "BEGIN TRANSACTION" step
138 |       handleErrors rollback (runCommands cs)
139 |       ignore $ withStmt "COMMIT TRANSACTION" step
140 |
141 |     where
142 |       runCommands : Cmds -> Async e es ()
143 |       runCommands []      = pure ()
144 |       runCommands (c::cs) = cmd c >> runCommands cs
145 |
146 |   ||| Runs the given query and accumulates at most `n` rows.
147 |   export %inline
148 |   query : DB => Query t -> (n : Nat) -> Async e es (List t)
149 |   query q = selectRows (encodeQuery q)
150 |
151 |   ||| Runs the given query and returns the first result (if any).
152 |   export %inline
153 |   query1 : DB => Query t -> Async e es (Maybe t)
154 |   query1 q = map (\case h::_ => Just h; [] => Nothing) $ query q 1
155 |
156 |   ||| Streams the rows resulting from running the given query.
157 |   export %inline
158 |   queryRows : (cs : ChunkSize) => DB => Query t -> AsyncStream e es (List t)
159 |   queryRows q = rows (encodeQuery q)
160 |
161 |   ||| Runs the given query and accumulates at most `n` rows.
162 |   |||
163 |   ||| The result is stored in a `Table` with a proper header of
164 |   ||| column names.
165 |   export
166 |   queryTable :
167 |        {auto db : DB}
168 |     -> {auto tr : ToRow t}
169 |     -> (q : Query t)
170 |     -> {auto 0 prf : ToRowTypes t === FromRowTypes t}
171 |     -> Nat
172 |     -> Async e es (Table t)
173 |   queryTable {prf} q n = do
174 |     rs <- query q n
175 |     pure (T (rewrite prf in hmap columnName q.columns) rs)
176 |