0 | module Interactive.SQL
  1 |
  2 | import Derive.Sqlite3
  3 | import Control.RIO.Sqlite3
  4 | import Control.RIO.App
  5 | import Control.RIO
  6 | import Data.Sigma
  7 |
  8 | import Data.Container
  9 | import Data.Container.Morphism
 10 | import Data.Container.Kleene
 11 | import Data.Container.Descriptions.Maybe
 12 | import Data.Maybe
 13 | import Data.Either
 14 | import Data.Sum
 15 |
 16 | import Data.String.Parser
 17 |
 18 | import JSON.Derive
 19 | import System.File
 20 |
 21 | %language ElabReflection
 22 | %default total
 23 |
 24 | %hide Data.List.Alternating.infixr.(<+)
 25 | %hide Data.List.Alternating.infixl.(<+)
 26 | %hide Data.String.Extra.infixr.(<+)
 27 | %hide Data.String.Extra.infixl.(+>)
 28 |
 29 | -- A todo app is a very simple example of a real-world application with
 30 | -- a tangible user experience and engineering challenges that are representative
 31 | -- of the ones encountered in shipping software.
 32 |
 33 | ----------------------------------------------------------------------------------
 34 | -- Datatypes                                                                    --
 35 | ----------------------------------------------------------------------------------
 36 | -- First we define the type for our to-do items.
 37 |
 38 | -- Todo items will be identified with an ID
 39 | public export
 40 | ID : Type
 41 | ID = Integer
 42 |
 43 | -- And a status to indicate if the item is marked as done.
 44 | data Status = Done | NotDone
 45 |
 46 | toBool : Status -> Bool
 47 | toBool Done = True
 48 | toBool NotDone = False
 49 |
 50 | fromBool : Bool -> Status
 51 | fromBool True = Done
 52 | fromBool False = NotDone
 53 |
 54 | FromCell Status where
 55 |   fromCellType = INTEGER
 56 |   fromCell = map fromBool . fromCell
 57 |
 58 | ToCell Status where
 59 |   toCellType = INTEGER
 60 |   toCell = toCell . toBool
 61 |
 62 | -- The to-do item in itself is a record of an id, a content string and
 63 | -- a status
 64 | record Todo where
 65 |   constructor MkTodo
 66 |   id : ID
 67 |   content : String
 68 |   status : Status
 69 |
 70 | FromRow Todo where
 71 |   fromRowTypes = [INTEGER, TEXT, INTEGER]
 72 |   fromRow [i, c, s] = do id <- fromCell i
 73 |                          cont <- fromCell c
 74 |                          stat <- fromCell s
 75 |                          pure (MkTodo id cont stat)
 76 | ToRow Todo where
 77 |   toRowTypes = [INTEGER, TEXT, INTEGER]
 78 |   toRow (MkTodo id cont stat) = [toCell (cast {to = Int32} id), toCell cont, toCell stat]
 79 |
 80 | -- The todo app will display a list of items and provide 4 key functions:
 81 | -- - create a new item
 82 | -- - delete an existing item
 83 | -- - mark an existing item as complete
 84 | -- - Return the list of all items
 85 | --
 86 | -- A command is data sent from the client for the server to answer.
 87 | data TodoCommand
 88 |   = Create String
 89 |   | Delete ID
 90 |   | MarkComplete ID
 91 |   | RetrieveAll
 92 |
 93 | %runElab derive "TodoCommand" [Show,Eq,ToJSON,FromJSON]
 94 |
 95 | -- CmdReturn is the type returned by each command
 96 | -- All commands return Unit since they only perform a side-effect, except
 97 | -- for Retrieve, it returns a list of todo items.
 98 | CmdReturn : TodoCommand -> Type
 99 | CmdReturn (Create str) = Unit
100 | CmdReturn (Delete i) = Unit
101 | CmdReturn (MarkComplete i) = Unit
102 | CmdReturn RetrieveAll = Table Todo
103 |
104 | ----------------------------------------------------------------------------------
105 | -- SQL                                                                          --
106 | ----------------------------------------------------------------------------------
107 |
108 | -- A valid query is one with a type that has the appropriate instances
109 | -- for row conversions
110 | record ValidQuery where
111 |   constructor MkValidQuery
112 |   0 ty : Type
113 |   tr : ToRow ty
114 |   qy : Query ty
115 |   {auto 0 chk : ToRowTypes ty = FromRowTypes ty}
116 |
117 | -- We can run any valid query and obtain the list of rows for that query
118 | runValid : Has SqlError e => DB => (x : ValidQuery) -> App e (Table (x .ty))
119 | runValid (MkValidQuery ty tr qy ) = queryTable qy 1000
120 |
121 | -- The schema of our database. We onlye have
122 | -- a single table with all the todo items.
123 | Todos : SQLTable
124 | Todos =
125 |   table "todos"
126 |     [ C "todo_id" INTEGER
127 |     , C "content" TEXT
128 |     , C "status"  BOOL
129 |     ]
130 |
131 | -- We hard-code a SQL command to create our table. This is going to
132 | -- be called when we setup the table
133 | createTodos : Cmd TCreate
134 | createTodos =
135 |   IF_NOT_EXISTS $ CREATE_TABLE Todos
136 |     [ PRIMARY_KEY   ["todo_id"]
137 |     , AUTOINCREMENT  "todo_id"
138 |     , NOT_NULL       "content"
139 |     , NOT_NULL       "status"
140 |     ]
141 |
142 | -- SQL command to add an item to the todo table
143 | addTodoItem : String -> Cmd TInsert
144 | addTodoItem str = INSERT Todos ["content", "status"] (val str :: 0 :: [])
145 |
146 | -- SQL command to delete an item from the todo table
147 | deleteItem : Bits32 -> Cmd TDelete
148 | deleteItem i = DELETE Todos ("todo_id" == val i)
149 |
150 | -- SQL command to mark an item done
151 | itemMarkDone : Bits32 -> Cmd TUpdate
152 | itemMarkDone i = UPDATE Todos ["status" .= True] ("todo_id" == val i)
153 |
154 | -- SQL query to obtain all the todo items
155 | getAllItems : Query Todo
156 | getAllItems = SELECT ["todo_id", "content", "status"] [< FROM Todos]
157 |
158 | ----------------------------------------------------------------------------------
159 | -- Containers                                                                   --
160 | ----------------------------------------------------------------------------------
161 |
162 | -- The errors that our program will deal with
163 | 0 Errs : List Type
164 | Errs = [SqlError]
165 |
166 | -- The monad in which we run our program as an endofunctor in Cont
167 | 0 FM : Container -> Container
168 | FM x = F (App Errs) x
169 |
170 | -- The CLI is represented as a container that expects strings as input
171 | -- and returns strings as output.
172 | CLI : Container
173 | CLI = String :- String
174 |
175 | -- AppOp is the abstract API of our app, we take in commands, and returns
176 | -- either unit, or tables from queries. Will run in FM.
177 | AppOp : Container
178 | AppOp = (!>) TodoCommand CmdReturn
179 |
180 | -- Interface for database commands. Commands only perform side-effects so the
181 | -- results are always Unit
182 | DBCmd : Container
183 | DBCmd = Σ CmdType Cmd :- ()
184 |
185 | -- Interface of a database queries. Queries always return tables of a matching type
186 | 0 DBQry : Container
187 | DBQry = (x : ValidQuery) !> Table x.ty
188 |
189 | ----------------------------------------------------------------------------------
190 | -- Containers Morphisms                                                         --
191 | ----------------------------------------------------------------------------------
192 |
193 | ---------------------------------
194 | -- Running database operations --
195 | ---------------------------------
196 |
197 | -- Running a command as a costate
198 | CmdCostate : DB => Costate (FM DBCmd)
199 | CmdCostate = costate (\x => cmd {t = x.π1} x.π2)
200 |
201 | -- Running a query as a costate
202 | DBQueryCostate : DB => Costate (FM DBQry)
203 | DBQueryCostate = costate runValid
204 |
205 | -- Running either a command or a query on a database as a costate
206 | DBCostate : DB => Costate (FM (DBCmd + DBQry))
207 | DBCostate = distrib_plus {f = App Errs, a = DBCmd, b = DBQry}
208 |          |> CmdCostate + DBQueryCostate |> dia
209 |
210 | ---------------------------------------
211 | -- Interacting with the command line --
212 | ---------------------------------------
213 |
214 | -- We need a parser to parse command line arguments and translate them into
215 | -- internal Todo commands.
216 | cmdParser : Parser TodoCommand
217 | cmdParser = assert_total $
218 |             string "create" *> spaces *> char '"' *> Create <$> takeWhile (/= '"')
219 |         <|> string "done" *> spaces *> MarkComplete <$> cast <$> natural
220 |         <|> string "delete" *> spaces *> Delete <$> cast <$> natural
221 |         <|> string "print" *> pure RetrieveAll
222 |
223 | parseInput' : String -> Maybe TodoCommand
224 | parseInput' str = eitherToMaybe $ map fst $ parse cmdParser str
225 |
226 | -- Convert a string-based api into the AppOp interface
227 | -- MaybeA is the error monad where all errors need to be handled
228 | cliParser : CLI =%> MaybeA AppOp
229 | cliParser = MkMorphism parseInput' printOutput
230 |   where
231 |     printResult : (v : TodoCommand ** CmdReturn v) -> String
232 |     printResult (RetrieveAll ** b)  = prettyTable b
233 |     printResult (MarkComplete id ** y) = "done"
234 |     printResult (Create content ** y) = "done"
235 |     printResult (Delete id ** y)  = "deleted \{show id}"
236 |
237 |     printOutput : (x : String) -> (Sometimes CmdReturn (parseInput' x)) -> String
238 |     printOutput x y with (parseInput' x)
239 |       printOutput x Nah | Nothing = "could not parse '\{x}'"
240 |       printOutput x (Aye y) | (Just z) = printResult (z ** y)
241 |
242 | -- The parser lifted into effectful bidirectional programs
243 | -- Note that the parser itself does not concern itself with effects but
244 | -- we can lift it to make to compatible with effectful programs.
245 | parser : FM CLI =%> FM (MaybeA AppOp)
246 | parser = f_functor cliParser
247 |
248 | ---------------------------------------
249 | -- Converting to database operations --
250 | ---------------------------------------
251 |
252 | -- Converting from internal app commands to database commands
253 | -- Again, notice that this is a pure interface, but the monad on containers
254 | -- will make this compatible with the rest of the infrastructure.
255 | OpToDB : AppOp =%> DBCmd + DBQry
256 | OpToDB = MkMorphism convertCommand convertBack
257 |   where
258 |     convertCommand : TodoCommand -> Σ CmdType Cmd + ValidQuery
259 |     convertCommand (Create str) = <+ (_ ## addTodoItem str)
260 |     convertCommand (Delete i) = <+ (_ ## deleteItem (cast i))
261 |     convertCommand (MarkComplete i) = <+ (_ ## itemMarkDone (cast i))
262 |     convertCommand RetrieveAll = +> MkValidQuery _ %search getAllItems
263 |
264 |     convertBack : (x : TodoCommand) -> (DBCmd + DBQry).pos (convertCommand x) ->
265 |                   CmdReturn x
266 |     convertBack (Create str) y = ()
267 |     convertBack (Delete i) y = ()
268 |     convertBack (MarkComplete i) y = ()
269 |     convertBack RetrieveAll y = y
270 |
271 | -- Commands translated to database operations lifted into the correct monads
272 | -- We lift our translatin to database operation through both FM and MaybeA
273 | commands : DB => FM (MaybeA AppOp) =%> MaybeA (FM (DBCmd + DBQry))
274 | commands = distribMaybeAF {a = AppOp} |> map_MaybeA (f_functor OpToDB)
275 |
276 | -- The application itself as a Costate of FM CLI
277 | -- - First run the parser
278 | -- - Then convert commands into database operations
279 | -- - Then run the database
280 | appCont : DB => Costate (FM CLI)
281 | appCont = parser |> commands  |> map_MaybeA DBCostate |> maybeAUnit
282 |
283 | ----------------------------------------------------------------------------------
284 | -- Running the app as a REPL                                                    --
285 | ----------------------------------------------------------------------------------
286 |
287 | partial
288 | repl : HasIO io => (String -> io String) -> io ()
289 | repl f = do
290 |   line <- getLine
291 |   output <- f line
292 |   putStrLn output
293 |   repl f
294 |
295 | -- Running the repl with our String -> String function extracted from the
296 | -- costate `Costate (FM CLI)`
297 | partial
298 | app : DB => App Errs Unit
299 | app = repl (extract appCont)
300 |
301 | -- Running the database commands to setup an initial state
302 | partial
303 | runDB : App Errs Unit
304 | runDB = withDB ":memory:" $
305 |         cmd createTodos *> app
306 |
307 | -- Running the main app using RIO
308 | partial
309 | main : IO ()
310 | main = runApp [ printLn ] runDB
311 |
312 |