record Column : Type A column in an SQLite table: A name paired with the type of
values stored in the column.
Note: With this definition, we do not include any constraints with
our columns. These should be passed on separately when
using the `CREATE_TABLE` command.
Totality: total
Visibility: public export
Constructor: C : String -> SqliteType -> Column
Projections:
.name : Column -> String.type : Column -> SqliteType
.name : Column -> String- Totality: total
Visibility: public export name : Column -> String- Totality: total
Visibility: public export .type : Column -> SqliteType- Totality: total
Visibility: public export type : Column -> SqliteType- Totality: total
Visibility: public export record SQLTable : Type An SQLite table: A name paired with a list of columns.
Totality: total
Visibility: public export
Constructor: ST : String -> String -> List Column -> SQLTable
Projections:
.as : SQLTable -> String Field `as` is used to rename tables within a `SELECT` statement.
This is, for instance, needed when `JOIN`ing a table with itself.
.cols : SQLTable -> List Column The list of table columns
.name : SQLTable -> String The table's name
.name : SQLTable -> String The table's name
Totality: total
Visibility: public exportname : SQLTable -> String The table's name
Totality: total
Visibility: public export.as : SQLTable -> String Field `as` is used to rename tables within a `SELECT` statement.
This is, for instance, needed when `JOIN`ing a table with itself.
Totality: total
Visibility: public exportas : SQLTable -> String Field `as` is used to rename tables within a `SELECT` statement.
This is, for instance, needed when `JOIN`ing a table with itself.
Totality: total
Visibility: public export.cols : SQLTable -> List Column The list of table columns
Totality: total
Visibility: public exportcols : SQLTable -> List Column The list of table columns
Totality: total
Visibility: public exporttable : String -> List Column -> SQLTable Utility constructor for tables that sets fields `name` and `as`
both the value of the string argument.
Totality: total
Visibility: public exportAS : SQLTable -> String -> SQLTable Utility to change the name of a table in a `SELECT` statement.
The name was chosen to resemble SQL syntax, and it is recommended
to use this in infix notation:
```idris
students `AS` "st"
```
Totality: total
Visibility: public exportColTypes : SQLTable -> List SqliteType Computes the types of columns stored in a table.
Totality: total
Visibility: public exportFindCol : String -> List Column -> Maybe SqliteType Tries to look up a column type by name
in a list of columns.
We use this often in proofs, therefore this comes with
an upper-case name.
Totality: total
Visibility: public exportListColType : (s : String) -> (cs : List Column) -> {auto 0 _ : IsJust (FindCol s cs)} -> SqliteType Column type of a column (given by name) in a list of
columns.
This requires a proof that the column actually is in the
table.
Totality: total
Visibility: public exportTableColType : (s : String) -> (t : SQLTable) -> {auto 0 _ : IsJust (FindCol s (t .cols))} -> SqliteType Column type of a column (given by name) in a table.
This requires a proof that the column actually is in the
table.
Totality: total
Visibility: public exportdata TColumn : SQLTable -> SqliteType -> Type A column in the given table: This is just a column name
paired with a proof that the column exists in table `t`
and has type `tpe`.
Totality: total
Visibility: public export
Constructor: TC : (name : String) -> {auto 0 prf : IsJust (FindCol name (t .cols))} -> TColumn t (TableColType name t)
.name : TColumn t x -> String Extracts the name of a `TColumn`.
Totality: total
Visibility: public exportfromString : (name : String) -> {auto 0 p : IsJust (FindCol name (t .cols))} -> TColumn t (TableColType name t)- Totality: total
Visibility: public export 0 Schema : Type A database schema is a (snoc-)list of tables.
The reason for preferring `SnocList` over `List` is that we
typically build up a schema via joins in a query, and it is
more natural to append table from left to right in a complex
join statement than the other way round.
Totality: total
Visibility: public exportFindSchemaCol2 : String -> String -> Schema -> Maybe SqliteType Looks up a table and column name in a schema.
This is called from `FindSchemaCol` after verifying that the
column identifier has been fully qualified by prefixing it with
a table name.
The table name is checked against the `as` field of the tables.
This allows us to rename tables as part of a `SELECT` statement,
which is especially important when joining a table with itself.
Totality: total
Visibility: public exportFindSchemaCol1 : String -> Schema -> Maybe SqliteType Looks up an unqualified column name in a schema.
In order for this to succeed, the schema must either consist of
only a single table, or the last table in the schema must be unnamed.
The latter case (the last table being unnamed) occurs, when we
give column names to arbitrary SQL expressions in a `SELECT`
statement. Since these expressions are evaluated after the
rest of the schema is known (the rest of the schema comes from
the `FROM` part of a `SELECT` statement), it is natural to just
append an unnamed table with custom column names at the end of
the schema.
Totality: total
Visibility: public exportFindSchemaCol : String -> Schema -> Maybe SqliteType Looks up a - possibly qualified - column name in a schema.
This invokes `FindSchemaCol1` or `FindSchemaCol2` depending on
whether the column name is fully qualified or not. A qualified
column name is prefixed with the corresponding table's name
followed by a dot: `"employees.name"`.
Totality: total
Visibility: public exportSchemaColType : (name : String) -> (s : Schema) -> {auto 0 _ : IsJust (FindSchemaCol name s)} -> SqliteType Computes the SQLite column type associated with column `column`
in table `table` in the given list of tables.
Totality: total
Visibility: public exportSchemaHasCol : Schema -> String -> Bool Proof that a column with the given name exists in
the given list of tables.
Totality: total
Visibility: public exportrecord JColumn : Schema -> SQLTable -> Type A column used in a `JOIN ... USING` statement: The column name must
appear in both schemata.
Totality: total
Visibility: public export
Constructor: JC : (name : String) -> {auto 0 _ : SchemaHasCol s name = True} -> {auto 0 _ : IsJust (FindCol name (t .cols))} -> JColumn s t
Projections:
.name : JColumn s t -> String0 .p1 : ({rec:0} : JColumn s t) -> SchemaHasCol s (name {rec:0}) = True0 .p2 : ({rec:0} : JColumn s t) -> IsJust (FindCol (name {rec:0}) (t .cols))
.name : JColumn s t -> String- Totality: total
Visibility: public export name : JColumn s t -> String- Totality: total
Visibility: public export 0 .p1 : ({rec:0} : JColumn s t) -> SchemaHasCol s (name {rec:0}) = True- Totality: total
Visibility: public export 0 p1 : ({rec:0} : JColumn s t) -> SchemaHasCol s (name {rec:0}) = True- Totality: total
Visibility: public export 0 .p2 : ({rec:0} : JColumn s t) -> IsJust (FindCol (name {rec:0}) (t .cols))- Totality: total
Visibility: public export 0 p2 : ({rec:0} : JColumn s t) -> IsJust (FindCol (name {rec:0}) (t .cols))- Totality: total
Visibility: public export fromString : (name : String) -> {auto 0 _ : SchemaHasCol s name = True} -> {auto 0 _ : IsJust (FindCol name (t .cols))} -> JColumn s t- Totality: total
Visibility: public export record Table : Type -> Type A table of values together with a fitting header
Totality: total
Visibility: public export
Constructor: T : {auto torow : ToRow a} -> LAll (const String) (ToRowTypes a) -> List a -> Table a
Projections:
.rows : Table a -> List a.torow : Table a -> ToRow a
.torow : Table a -> ToRow a- Totality: total
Visibility: public export torow : Table a -> ToRow a- Totality: total
Visibility: public export - Totality: total
Visibility: public export - Totality: total
Visibility: public export .rows : Table a -> List a- Totality: total
Visibility: public export rows : Table a -> List a- Totality: total
Visibility: public export quote : Char- Totality: total
Visibility: export encodeBytes : ByteString -> String Encodes a `ByteString` as an SQL literal.
Every byte is encodec with two hexadecimal digits, and the
whole string is wrapped in single quotes prefixed with an "X".
For instance, `encodeBytes (fromList [0xa1, 0x77])` yields the
string "X'a177'".
Totality: total
Visibility: exportprettyRows : LAll (const String) ts -> List (LAll (Maybe . IdrisType) ts) -> String- Totality: total
Visibility: export prettyTable : Table a -> String- Totality: total
Visibility: export printTable : HasIO io => Table a -> io ()- Totality: total
Visibility: export