0 | module Oracle.Internal.Either
 1 |
 2 | ||| Monadic composition for Oracle operations that return `Either` values inside `IO`.
 3 | |||
 4 | ||| If the first action succeeds, its result is passed to the supplied continuation.
 5 | |||
 6 | ||| If the first action fails with `Left`, the error is propagated immediately and the continuation is not executed.
 7 | |||
 8 | ||| This function is useful for sequencing database operations while automatically propagating `OracleError` values without deeply nested pattern matching.
 9 | |||
10 | ||| Example:
11 | |||
12 | ||| ```idris
13 | ||| query conn sql params =
14 | |||   withStatement conn sql $ \stmt =>
15 | |||     bind stmt params `andThen` \_ =>
16 | |||     execute stmt     `andThen` \_ =>
17 | |||     fetchRaw stmt
18 | ||| ```
19 | |||
20 | ||| This behaves similarly to `(>>=)` for `Either e`, but operates on values of type `IO (Either e a)`.
21 | |||
22 | export
23 | andThen : IO (Either e a) -> (a -> IO (Either e b)) -> IO (Either e b)
24 | andThen action f = do
25 |   result <- action
26 |   case result of
27 |     Left err    =>
28 |       pure (Left err)
29 |     Right value =>
30 |       f value
31 |
32 | export infixl 1 >>==
33 | ||| Infix version of `andThen`.
34 | |||
35 | ||| Allows sequencing Oracle operations using monadic-style syntax.
36 | |||
37 | ||| Example:
38 | |||
39 | ||| ```idris
40 | ||| bind stmt params >>== \_ =>
41 | ||| execute stmt     >>== \_ =>
42 | ||| fetchRaw stmt
43 | ||| ```
44 | |||
45 | ||| Equivalent to:
46 | |||
47 | ||| ```idris
48 | ||| andThen (bind stmt params) (\_ =>
49 | |||   andThen (execute stmt) (\_ =>
50 | |||     fetchRaw stmt))
51 | ||| ```
52 | |||
53 | export
54 | (>>==) : IO (Either e a) -> (a -> IO (Either e b)) -> IO (Either e b)
55 | (>>==) = andThen
56 |