Postgres.Data.PostgresTable

Reexports

Definitions

data Ident : Type

  A Postgres identifier, generally speaking. Could be a table name
  or a column name or more broadly speaking any proper name that
  Postgres syntactically recognizes between double-quotes.

Totality: total
Visibility: public export
Constructor: 

Id : String -> Ident

Hint: 

Show Ident

data Alias : Type

  An Alias is a valid table identifier that may either
  be a string specified by the programmer or it may be
  auto-generated in the course of creating subqueries.

Totality: total
Visibility: public export
Constructors:

Named : String -> Alias

Generated : Nat -> Alias

Hints:

Eq Alias

Show Alias

aliasIdentifier : Alias -> Ident

  Aliases can always be turned into identifiers.

Totality: total
Visibility: public export

toAlias : Ident -> Alias

  Turning an identifier into an alias is not inteded to be the lossless
  reversal of `aliasIdentifier`. An identifier will always become a named
  alias even if it was at one point a generated alias before being turned into
  an identifier.

Totality: total
Visibility: public export

data TableStatement : Type

  A table name or subquery.

Totality: total
Visibility: public export
Constructors:

Identifier : String -> Maybe Alias -> TableStatement

  A table name.

Subquery : String -> Alias -> TableStatement

  A subquery.

Fragment : String -> TableStatement

  A fragment (can be selected against, but is not named or aliased)

Hint: 

Show TableStatement

tableAlias : TableStatement -> Maybe Alias

Totality: total
Visibility: public export

tableAliasOrName : TableStatement -> Maybe Ident

  The table alias or name.

Totality: total
Visibility: public export

named : String -> {default Nothing _ : Maybe Alias} -> TableStatement

  Construct a table statement for a table with the given name.

Totality: total
Visibility: public export

subquery : String -> Alias -> TableStatement

  Construct a table statement using a subquery.

Totality: total
Visibility: export

record ColumnIdentifier : Type

  A column is identified by its name and optionally the alias
  of a table the column comes from. In some situations the `sourceTable`
  for a column will be needed in order to unambiguously refer to one
  of a few columns in the same query with the same name.
  
  Generally it will be clunky to create ColumnIdentifiers using the type's
  consutrctor directly so most column identifiers will come from string values
  because ColumnIdentifier's `FromString` conformance allows Idris 2 to transform
  strings into ColumnIdentifiers. This allows for:
  - "table1.column1" = MkColumnId (Just $ Named "table1") "column1"
  - "column1" = MkColumnId Nothing "column1"
  
  Table aliases here do not necessarily need to refer to a table that has
  been given a Postgres alias (a la "(select ...) AS an_alias"). A normal table
  or view name is appropriate and can be turned into an alias for use in a column
  identifier with the `toAlias` function.

Totality: total
Visibility: public export
Constructor: 

MkColumnId : Maybe Alias -> String -> ColumnIdentifier

Projections:

.name : ColumnIdentifier -> String

.sourceTable : ColumnIdentifier -> Maybe Alias

Hints:

FromString ColumnIdentifier

Show ColumnIdentifier

.sourceTable : ColumnIdentifier -> Maybe Alias

Totality: total
Visibility: public export

sourceTable : ColumnIdentifier -> Maybe Alias

Totality: total
Visibility: public export

.name : ColumnIdentifier -> String

Totality: total
Visibility: public export

name : ColumnIdentifier -> String

Totality: total
Visibility: public export

replaceSource : Maybe Alias -> ColumnIdentifier -> ColumnIdentifier

Totality: total
Visibility: public export

forgetSource : ColumnIdentifier -> ColumnIdentifier

Totality: total
Visibility: public export

data AnonymousColumnIdentifier : ColumnIdentifier -> Type

Totality: total
Visibility: public export
Constructor: 

Anon : AnonymousColumnIdentifier (MkColumnId Nothing {_:9968})

interface PostgresTable : Type -> Type

  Some representation of a Postgres table.

Parameters: t
Methods:

tableStatement : t -> TableStatement

  A table name or subselect statement from which the following columns could be selected.

columns : t -> List (ColumnIdentifier, Exists PColType)

  The columns this table offers. Column names should not include double quotes, even where they
  are needed when written down in SQL statements.

as : t -> String -> t

  Set the alias on a table.

Fixity Declaration: infix operator, level 0

Implementations:

PostgresTable RuntimeTable

PostgresTable PersistedTable

tableStatement : PostgresTable t => t -> TableStatement

  A table name or subselect statement from which the following columns could be selected.

Totality: total
Visibility: public export

columns : PostgresTable t => t -> List (ColumnIdentifier, Exists PColType)

  The columns this table offers. Column names should not include double quotes, even where they
  are needed when written down in SQL statements.

Totality: total
Visibility: public export

as : PostgresTable t => t -> String -> t

  Set the alias on a table.

Totality: total
Visibility: public export
Fixity Declaration: infix operator, level 0

alias : PostgresTable t => t -> Maybe Alias

Totality: total
Visibility: export

aliasOrName : PostgresTable t => t -> Maybe Alias

  Get the alias or name of a table; prefer the alias, as a renamed table
  _should_ be referred to by its alias, but use the table's original name
  if one is available and there is no alias set.

Totality: total
Visibility: public export

record RuntimeTable : Type

  A runtime representation of a table. These have string fields and table statements so as to not limit
  themselves to nominal postgres tables; you can also represent joins naturally where the table statement is
  a SELECT with a JOIN instead of just a table's name.

Totality: total
Visibility: public export
Constructor: 

RT : TableStatement -> List (ColumnIdentifier, Exists PColType) -> RuntimeTable

Projections:

.columns : RuntimeTable -> List (ColumnIdentifier, Exists PColType)

.tableStatement : RuntimeTable -> TableStatement

Hint: 

PostgresTable RuntimeTable

.tableStatement : RuntimeTable -> TableStatement

Totality: total
Visibility: public export

tableStatement : RuntimeTable -> TableStatement

Totality: total
Visibility: public export

.columns : RuntimeTable -> List (ColumnIdentifier, Exists PColType)

Totality: total
Visibility: public export

columns : RuntimeTable -> List (ColumnIdentifier, Exists PColType)

Totality: total
Visibility: public export

record PersistedTable : Type

  A persisted table is an actual named (or view) table in the database.

Totality: total
Visibility: public export
Constructor: 

PT : String -> {default Nothing _ : Maybe Alias} -> List (String, Exists PColType) -> PersistedTable

Projections:

.alias : PersistedTable -> Maybe Alias

.columns : PersistedTable -> List (String, Exists PColType)

.tableName : PersistedTable -> String

Hint: 

PostgresTable PersistedTable

.tableName : PersistedTable -> String

Totality: total
Visibility: public export

tableName : PersistedTable -> String

Totality: total
Visibility: public export

.alias : PersistedTable -> Maybe Alias

Totality: total
Visibility: public export

alias : PersistedTable -> Maybe Alias

Totality: total
Visibility: public export

.columns : PersistedTable -> List (String, Exists PColType)

Totality: total
Visibility: public export

columns : PersistedTable -> List (String, Exists PColType)

Totality: total
Visibility: public export

aliasOrName : PersistedTable -> Alias

Totality: total
Visibility: public export

col : Nullability -> PType -> Exists PColType

  Construct an existential column type from a Postgres type and its
  nullability.

Totality: total
Visibility: public export

pgTable : String -> List (String, (Nullability, PType)) -> PersistedTable

  Construct a persisted table representation (a table name and the names,
  types, and nullabilities of the columns of a table.)
  
  ```idris example
  myTable = table "table1" [ ("id"            , NonNullable, PInteger)
                           , ("name"          , NonNullable, PString)
                           , ("favorite_color", Nullable   , PString)
                           ]
  ```

Totality: total
Visibility: public export

data LooseColumnMapping : (0 _ : (PType -> Type -> Type)) -> List (ColumnIdentifier, Exists PColType) -> (ColumnIdentifier, Type) -> Type

  A mapping between a column name and Idris type to some element in a list of column identifiers
  and Postgres types. This mapping proves that the column identifiers exists and that the Postgres
  type for that column can be cast to the Idris type specified. This mapping allows for "loose"
  matches where the ColumnIdentifier being matched against does not specify a source table but the
  column name can be found in the list of columns given. Loose matching is only ok if the match would
  not succeed against multiple columns (Postgres will complain of ambiguity, for good reason). Use the
  ColumnMapping type to avoid loose matches.

Totality: total
Visibility: public export
Constructors:

HereNul : (ident : ColumnIdentifier) -> (ty : Type) -> castTy pt ty => LooseColumnMapping castTy ((ident, Evidence pt (MkColType Nullable pt)) :: xs) (ident, Maybe ty)

HereNulLoose : (columnName : String) -> (ty : Type) -> castTy pt ty => LooseColumnMapping castTy ((MkColumnId {_:10677} columnName, Evidence pt (MkColType Nullable pt)) :: xs) (MkColumnId Nothing columnName, Maybe ty)

Here : (ident : ColumnIdentifier) -> (ty : Type) -> castTy pt ty => LooseColumnMapping castTy ((ident, Evidence pt (MkColType NonNullable pt)) :: xs) (ident, ty)

HereLoose : (columnName : String) -> (ty : Type) -> castTy pt ty => LooseColumnMapping castTy ((MkColumnId {_:10764} columnName, Evidence pt (MkColType NonNullable pt)) :: xs) (MkColumnId Nothing columnName, ty)

There : LooseColumnMapping castTy xs (ident, ty) -> LooseColumnMapping castTy (x :: xs) (ident, ty)

HasLooseMappings : (0 _ : (PType -> Type -> Type)) -> PostgresTable t => t -> Vect n (ColumnIdentifier, Type) -> Type

Totality: total
Visibility: public export

data ColumnMapping : (0 _ : (PType -> Type -> Type)) -> List (ColumnIdentifier, Exists PColType) -> (ColumnIdentifier, Type) -> Type

  A mapping between a column name and Idris type to some element in a list of column identifiers
  and Postgres types. This mapping proves that the column identifiers exists and that the Postgres
  type for that column can be cast to the Idris type specified.

Totality: total
Visibility: public export
Constructors:

HereNul : (ident : ColumnIdentifier) -> (ty : Type) -> castTy pt ty => ColumnMapping castTy ((ident, Evidence pt (MkColType Nullable pt)) :: xs) (ident, Maybe ty)

Here : (ident : ColumnIdentifier) -> (ty : Type) -> castTy pt ty => ColumnMapping castTy ((ident, Evidence pt (MkColType NonNullable pt)) :: xs) (ident, ty)

There : ColumnMapping castTy xs (ident, ty) -> ColumnMapping castTy (x :: xs) (ident, ty)

HasMappings : (0 _ : (PType -> Type -> Type)) -> PostgresTable t => t -> Vect n (ColumnIdentifier, Type) -> Type

Totality: total
Visibility: public export

select : {auto {conArg:11210} : PostgresTable t} -> (table : t) -> (cols : Vect n (ColumnIdentifier, Type)) -> {auto 0 _ : HasMappings IdrCast table cols} -> String

  Create a select statement based on the columns you would like to grab from the
  given table.

Totality: total
Visibility: public export

insert : (table : PersistedTable) -> (cols : Vect n ColumnIdentifier) -> HVect colTypes -> HasLooseMappings PGCast table (cols `zip` colTypes) => String

  Insert the given values into the given columns of a new row in the given table.

Totality: total
Visibility: public export

data Join : t1 -> t2 -> Type

Totality: total
Visibility: public export
Constructor: 

On : {auto {conArg:11507} : PostgresTable t} -> {auto {conArg:11510} : PostgresTable u} -> (c1 : ColumnIdentifier) -> (c2 : ColumnIdentifier) -> {auto 0 _ : Elem c1 (fst <$> columns t1)} -> {auto 0 _ : Elem c2 (fst <$> columns t2)} -> Join t1 t2

HasOnMapping : ColumnIdentifier -> PostgresTable t => t -> Type

Totality: total
Visibility: public export

elemForOnMapping : {auto {conArg:11617} : PostgresTable t} -> (table : t) -> (c : ColumnIdentifier) -> HasOnMapping c table -> (c' : ColumnIdentifier ** Elem c' (fst <$> columns table))

Totality: total
Visibility: public export

(==) : {auto {conArg:11687} : PostgresTable t} -> {auto {conArg:11690} : PostgresTable u} -> (c1 : ColumnIdentifier) -> (c2 : ColumnIdentifier) -> HasOnMapping c1 t1 => HasOnMapping c2 t2 => Join t1 t2

  In a join-statement, produce the clause that links the two tables together by
  a shared column. In pseudo-code: "table1 join table2 'on' col1 = col2".
  
  ```idris example
  innerJoin' table1 table2 ("col_from_table1" == "col_from_table2")
  ```

Totality: total
Visibility: public export
Fixity Declaration: infix operator, level 6

column1 : Join t u -> ColumnIdentifier

Totality: total
Visibility: public export

column2 : Join t u -> ColumnIdentifier

Totality: total
Visibility: public export

innerJoin' : PostgresTable t => (table1 : t) -> PostgresTable u => (table2 : u) -> Join table1 table2 -> RuntimeTable

  Construct a runtime table by inner-joining two other tables on a specified column.
  
  ```idris example
  innerJoin' table1 table2 ("col_from_table1" == "col_from_table2")
  ```

Totality: total
Visibility: public export

leftJoin' : PostgresTable t => (table1 : t) -> PostgresTable u => (table2 : u) -> Join table1 table2 -> RuntimeTable

  Construct a runtime table by left-joining two other tables on a specified column.
  
  ```idris example
  leftJoin' table1 table2 ("col_from_table1" == "col_from_table2")
  ```

Totality: total
Visibility: public export

rightJoin' : PostgresTable t => (table1 : t) -> PostgresTable u => (table2 : u) -> Join table1 table2 -> RuntimeTable

  Construct a runtime table by right-joining two other tables on a specified column.
  
  ```idris example
  rightJoin' table1 table2 ("col_from_table1" == "col_from_table2")
  ```

Totality: total
Visibility: public export

data JoinType : Type

Totality: total
Visibility: public export
Constructors:

Inner : JoinType

Left : JoinType

Right : JoinType

data TablePair : table1 -> table2 -> Type

Totality: total
Visibility: public export
Constructor: 

MkTP : JoinType -> PostgresTable t => PostgresTable u => (table1 : t) -> (table2 : u) -> TablePair table1 table2

innerJoin : PostgresTable t => PostgresTable u => (table1 : t) -> (table2 : u) -> TablePair table1 table2

  Inner-join two tables.
  This produces a pair of tables and a join strategy. You then need to use `onColumns` to take the table pair
  and add the columns that the join should occur over.

Totality: total
Visibility: public export
Fixity Declaration: infixl operator, level 10

leftJoin : PostgresTable t => PostgresTable u => (table1 : t) -> (table2 : u) -> TablePair table1 table2

  Left-join two tables.
  This produces a pair of tables and a join strategy. You then need to use `onColumns` to take the table pair
  and add the columns that the join should occur over.

Totality: total
Visibility: public export
Fixity Declaration: infixl operator, level 10

rightJoin : PostgresTable t => PostgresTable u => (table1 : t) -> (table2 : u) -> TablePair table1 table2

  Right-join two tables.
  This produces a pair of tables and a join strategy. You then need to use `onColumns` to take the table pair
  and add the columns that the join should occur over.

Totality: total
Visibility: public export
Fixity Declaration: infixl operator, level 10

onColumns : TablePair table1 table2 -> Join table1 table2 -> RuntimeTable

  Given that you've already paired two tables up (see `innerJoin`, `leftJoin`, `rightJoin`)
  you use `onColumns` to specify which columns from each table in the pair should be equal
  in the joined table. The end result is a new table.
  
  Psuedo-example:
    table1 `innerJoin` table2 `onColumns` ("table1.col1" == "table2.col2")

Totality: total
Visibility: public export
Fixity Declaration: infixl operator, level 10

allCastable : {auto {conArg:12589} : PostgresTable t} -> (table : t) -> HasMappings IdrCast table cols => All Castable (snd <$> cols)

Totality: total
Visibility: export