0 | module Stellar.SQL
  1 |
  2 | import Derive.Sqlite3
  3 | import Control.RIO.Sqlite3
  4 | import Control.RIO.App
  5 | import Control.RIO
  6 |
  7 | import Stellar.API
  8 | import Stellar.API.Morphism
  9 | import Stellar.API.Kleene
 10 | import Stellar.API.Maybe
 11 |
 12 | import Data.Maybe
 13 | import Data.Either
 14 | import Data.Coproduct
 15 | import Data.Sigma
 16 |
 17 | import Data.String.Parser
 18 |
 19 | import JSON.Derive
 20 | import System.File
 21 |
 22 | %language ElabReflection
 23 | %default total
 24 |
 25 | %hide Data.List.Alternating.infixl.(+>)
 26 | %hide Data.List.Alternating.infixr.(<+)
 27 | %hide Data.String.Extra.infixr.(<+)
 28 | %hide Data.String.Extra.infixl.(+>)
 29 | %hide JSON.ToJSON.infixr.(.=)
 30 | %hide Prelude.Ops.infixl.(|>)
 31 |
 32 | ----------------------------------------------------------------------------------
 33 | -- SQL                                                                          --
 34 | ----------------------------------------------------------------------------------
 35 |
 36 | -- A valid query is one with a type that has the appropriate instances
 37 | -- for row conversions
 38 | public export
 39 | record ValidQuery where
 40 |   constructor MkValidQuery
 41 |   0 ty : Type
 42 |   tr : ToRow ty
 43 |   qy : Query ty
 44 |   {auto 0 chk : ToRowTypes ty = FromRowTypes ty}
 45 |
 46 | -- We can run any valid query and obtain the list of rows for that query
 47 | export
 48 | runValid : Has SqlError e => DB => (x : ValidQuery) -> App e (Table (x .ty))
 49 | runValid (MkValidQuery ty tr qy ) = queryTable qy 1000
 50 |
 51 |
 52 | ----------------------------------------------------------------------------------
 53 | -- APIs                                                                   --
 54 | ----------------------------------------------------------------------------------
 55 |
 56 | -- The errors that our program will deal with
 57 | public export
 58 | 0 Errs : List Type
 59 | Errs = [SqlError]
 60 |
 61 | -- The monad in which we run our program as an endofunctor in Cont
 62 | public export
 63 | 0 SQLM : API -> API
 64 | SQLM x = Lift (App Errs) x
 65 |
 66 | -- Interface for database commands. Commands only perform side-effects so the
 67 | -- results are always Unit
 68 | public export
 69 | DBCmd : API
 70 | DBCmd = Σ CmdType Cmd :- ()
 71 |
 72 | -- Interface of a database queries. Queries always return tables of a matching type
 73 | public export
 74 | 0 DBQry : API
 75 | DBQry = (x : ValidQuery) !> Table x.ty
 76 |
 77 | ---------------------------------
 78 | -- Running database operations --
 79 | ---------------------------------
 80 |
 81 | -- Running a command as a costate
 82 | export
 83 | CmdCostate : DB => Costate (SQLM DBCmd)
 84 | CmdCostate = costate (\x => cmd {t = x.π1} x.π2)
 85 |
 86 | -- Running a query as a costate
 87 | export
 88 | DBQueryCostate : DB => Costate (SQLM DBQry)
 89 | DBQueryCostate = costate runValid
 90 |
 91 | public export
 92 | 0 SQL : API
 93 | SQL = DBCmd + DBQry
 94 |
 95 | -- Running either a command or a query on a database as a costate
 96 | export
 97 | DBCostate : DB => Costate (SQLM SQL)
 98 | DBCostate = distrib_plus {f = App Errs, a = DBCmd, b = DBQry}
 99 |          |&> choice CmdCostate DBQueryCostate |&> dia
100 |
101 | export
102 | execSeqDB : DB => (x : (SQLM (SQL .star)).message) -> (SQLM (SQL .star)).response x
103 | execSeqDB Done = pure StarU
104 | execSeqDB (More (MkEx (<+ x) cont)) = cmd {t = x.π1} x.π2 >> map (StarM ()) (execSeqDB (cont ()))
105 | execSeqDB (More (MkEx (+> x) cont)) = runValid x >>= \tbl => map (StarM tbl) (execSeqDB (cont tbl))
106 |
107 | ||| Run any amount of DB queries wrapped in SQL errors
108 | export
109 | DBStarCostate : DB => Costate (SQLM (SQL .star))
110 | DBStarCostate = costate execSeqDB
111 |