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