8.6

This shows how to make a todo list application using HTML forms, backed by a PostgreSQL database.

First, some imports. Note that the PostgreSQL client is coupled with the HTTP2 server (yes, they should be untangled).

module Demo.TodoList

import AIO.ASCII as ASCII
import AIO.Cont as Cont
import AIO.Http2WithPg as H2
import AIO.Responder
import AIO.PGTypes as PGTypes

import Data.String as S

Idris definitions must be in order, so we start out with functions with no dependencies.

This one takes an SQL row returned by PostgreSQL, and renders it as a HTML snippet. Each todo item can be marked undone if it is done, and vice versa.

Aside: HTML should ideally be handled in a separate library like e.g. Blaze for Haskell. But I don’t know of such a library for Idris, yet.

partial
renderRow : List DataRowElement -> String
renderRow
  [ MkDataRowElement elemId
  , MkDataRowElement descBytes
  , MkDataRowElement [doneByte]] =
  let
    escapeHtml =
      replaceStr "<" "<"
      . replaceStr "\"" """
      . replaceStr "&" "&"
    escapedDescription =
      escapeHtml $ ASCII.pack8 descBytes
    formHtml =
      if chr8 doneByte /= ’t’
        then """
                <form action=/mark_done method=get>
                <input type=hidden name=id value=
                "\{ escapeHtml $ ASCII.pack8  elemId }"
                ><input type=submit value=’mark done’></form>
             """
        else """
                <form action=/mark_undone method=get><input type=hidden name=id value=
                "\{ escapeHtml $ ASCII.pack8  elemId }"
                ><input type=submit value=’mark undone’></form>
             """
  in escapedDescription <+> " " <+> formHtml
renderRow _ = "unexpected row"

These prefixes are used for determining the action requested by the client. All actions are using the GET verb for HTTP, since I don’t know of a multi-part form decoder.

donePrefix : String
donePrefix = "/mark_done?id="
undonePrefix : String
undonePrefix = "/mark_undone?id="
newPrefix : String
newPrefix = "/new?descr="

Now we can start defining utility functions that work on InnerCont. InnerCont is a type synonym used for a HTTP route handler. It is a continuation that talks to both HTTP and PostgreSQL on separate channels.

The following function takes a prefix and a path. If the path has the given prefix, it calls the callback, which is the last argument. The callback is given whatever comes after the prefix, which, used with the prefixes above, will be the ID of the todo item, or the description of the new todo item to be added.

partial
onPrefix : String -> String -> (String -> InnerCont Unit) -> InnerCont Unit
onPrefix prefi path cb =
  when (prefi ‘S.isPrefixOf‘ path) $ do
    let intLen = cast $ Prelude.String.length prefi
        idx = S.strSubstr intLen (intLen + 1) path
    cb idx

We need another utility function to avoid invalid SQL queries where the ID can’t be cast to a numeric value. Because it only allows digits, it also removes any malicious quoting.

onlyDigitsOrZero : String -> String
onlyDigitsOrZero inp =
  case Prelude.List.filter (‘elem‘ [’0’..’9’]) $ unpack inp of
    [] => "0"
    nonEmpty => pack nonEmpty

Now for the first function that executes SQL.

If the boolean is set to true, it sets any matching todo item to done.
If the boolean is set to false, it sets any matching todo item to undone.

partial
isPrefix : String -> String -> Bool -> InnerCont Unit
isPrefix prefi path newState =
  onPrefix prefi path $ \idx => do
    let
      sql =
        """
          update todo set done=
          \{ the  String $ if  newState  then "true" else "false" }
          where id =
          ’\{ onlyDigitsOrZero  idx }’
        """
    [] <- Cont.yieldGet2 sql
    pure ()

Now we have all the utility functions needed to define the request handler.

partial
okReplyAndBody2 : Bits32 -> String -> InnerCont (List Frame)
okReplyAndBody2 streamIdent path = do
  isPrefix donePrefix path True
  isPrefix undonePrefix path False
  onPrefix newPrefix path $ \newDescr => do
    [] <- Cont.yieldGet2
      """
        insert into todo (descr, done) values
          ( ’\{ replaceStr "’" "”" newDescr }’
          , false
          )
      """
    pure ()

  rows <- Cont.yieldGet2 "select id, descr, done from todo order by id"
  let
    htmlBody : Payload
    htmlBody = MkPayload $ ASCII.unpack8 $
      """
        \{ S.joinBy "<br>" $ map  renderRow  rows }
        <form action=new method=get>
          <input placeholder=’todo item description...’ name=descr>
          <input type=submit>
        </form>
      """
    bodyResp : Bits32 -> List Frame
    bodyResp streamIdent =
      [MkFrame Data (MkFlags END_STREAM) streamIdent htmlBody]
  pure (headersResp streamIdent ++ bodyResp streamIdent)

We pass the request handler to the library, which will run a server that uses it. It also connects to PostgreSQL with a currently hardcoded configuration.

partial
responder: Responder
responder = MkResponder okReplyAndBody2

partial
main : IO Unit
main = H2.runHttp2WithPostgres responder