Postgres.DB

Reexports

Definitions

withConn : HasIO io => String -> (Conn -> io b) -> (ConnectionStatus -> io b) -> io b

  Open a connection to a Postgres database,
  perform some actions with it, and then close
  the connection.
  
  If the database connection is established successfully,
  the `onOpen` function will be executed. If the
  connection cannot be established, `onError` will be
  executed.
  
  You do _not_ call `pgOpen` or `pgClose` directly
  when using this function.

Visibility: export

data DBState : Type

Totality: total
Visibility: public export
Constructors:

Open : DBState

Closed : DBState

Hints:

TransitionIndexedMonad DBState Database

TransitionIndexedPointed DBState Database

data OpenResult : Type

Totality: total
Visibility: public export
Constructors:

OK : OpenResult

Failed : String -> OpenResult

OpenResultState : OpenResult -> DBState

Visibility: public export

data Connection : Type

Totality: total
Visibility: export
Constructor: 

MkConnection : Conn -> TypeDictionary -> Connection

data Database : (ty : Type) -> DBState -> (ty -> DBState) -> Type

Totality: total
Visibility: export
Constructors:

DBOpen : String -> Database OpenResult Closed OpenResultState

DBClose : Database () Open (const Closed)

Exec : (Connection -> IO a) -> Database a Open (const Open)

DIO : IO a -> Database a s1 (const s1)

GetTypes : Database TypeDictionary Open (const Open)

Pure : (x : a) -> Database a (stateFn x) stateFn

Bind : Database a s1 s2Fn -> ((x : a) -> Database b (s2Fn x) s3Fn) -> Database b s1 s3Fn

Hints:

TransitionIndexedMonad DBState Database

TransitionIndexedPointed DBState Database

liftIO' : IO a -> Database a s1 (const s1)

Visibility: export

evalDatabase : HasIO io => Database a Closed (const Closed) -> io a

Visibility: export

initDatabase : Database () Closed (const Closed)

Visibility: export

openDatabase : String -> Database OpenResult Closed OpenResultState

Visibility: export

closeDatabase : Database () Open (const Closed)

Visibility: export

exec : (Connection -> IO a) -> Database a Open (const Open)

Visibility: export

unsafeExec : (Conn -> IO a) -> Database a Open (const Open)

  You can execute arbitrary things against the lower-level
  Conn, including closing the database connection prematurely.

Visibility: export

withDB : HasIO io => String -> Database a Open (const Open) -> io (Either String a)

  Perform some operation on an open database without closing it.
  A database connection will be created beforehand and then
  properly disposed of afterward.

Visibility: export

debugDumpTypes : Database () Open (const Open)

  Dump the Postgres type dictionary for debugging purposes.

Visibility: export

stringQuery : (header : Bool) -> String -> Connection -> IO (Either String (StringResultset header))

  Query the database interpreting all columns as strings.

Visibility: export

jsonQuery : String -> Connection -> IO (Maybe JSON)

  Query the database expecting a JSON result is returned.

Visibility: export

expectedQuery : (expected : Vect cols Type) -> String -> All Castable expected => Connection -> IO (Either String (rowCount : Nat ** Vect rowCount (HVect expected)))

  Query the database expecting the given array of types in each
  row of the result returned.

Visibility: export

tableQuery : {auto {conArg:2932} : PostgresTable t} -> (table : t) -> (cols : Vect n (ColumnIdentifier, Type)) -> HasMappings IdrCast table cols => Connection -> IO (Either String (rowCount : Nat ** Vect rowCount (HVect (snd <$> cols))))

  Query the given table in the database mapping each row to the given Idris type.
  @param table The table to query against.
  @param cols A Vect of tuples where the first element is a column name to select and
              the second element is an Idris type to cast the column value to.
  @param conn A database connection.

Visibility: export

tableQuery' : {auto {conArg:3018} : PostgresTable t} -> (table : t) -> (cols : Vect n (String, Type)) -> HasMappings IdrCast table (mapFst (MkColumnId (aliasOrName table)) <$> cols) => Connection -> IO (Either String (rowCount : Nat ** Vect rowCount (HVect (snd <$> (mapFst (MkColumnId (aliasOrName table)) <$> cols)))))

  Query the given table in the database mapping each row to the given Idris type.
  @param table The table to query against.
  @param cols A Vect of tuples where the first element is a column name to select and
              the second element is an Idris type to cast the column value to.
  @param conn A database connection.

Visibility: export

perform : String -> Connection -> IO ResultStatus

  Perform the given command and instead of parsing the response
  just report the result status. This is useful when you don't
  care if/what the response looks like, just whether the command
  worked

Visibility: export

tableInsert : (table : PersistedTable) -> (cols : Vect n ColumnIdentifier) -> HVect colTypes -> HasLooseMappings PGCast table (cols `zip` colTypes) => Connection -> IO ResultStatus

  Insert the given values into the given table.
  @param table The table to insert into.
  @param cols A Vect of column names to insert into (does
              not need to be every column in the table but
              there is not currently protection against omitting
              a column with no default value).
  @param values The values to insert.
  @param conn A database connection.

Visibility: export

listen : String -> Connection -> IO ResultStatus

  Start listening for notifications on the given channel.

Visibility: export

nextNotification : Connection -> IO (Maybe Notification)

  Gets the next notification _of those sitting around locally_.
  Returns `Nothing` if there are no notifications.
  
  See `libpq` documentation on `PQnotifies` for details on the
  distinction between retrieving notifications from the server and
  getting the next notification that has already been retrieved.
  
  NOTE: This function _does_ consume input to make sure no notification
   sent by the server but not processed by the client yet gets
   missed.

Visibility: export

notificationStream : Connection -> Stream (IO Notification)

  Produce a potentially infinite stream of notifications.
  Unlike `nextNotificaiton`, this will wait for the server
  to deliver a notification.
  
  This _is_ an infinite sequence with a blocking wait for the
  next notification so it is of somewhat limited utility
  compared to checking for new notifications at a natural point
  in your programs existing logic loop unless your entire loop
  is dictated by notification arrival anyway.

Visibility: export