Idris2Doc : Sqlite3.Cmd

Sqlite3.Cmd

(source)
Definitions
toExprs : LAll (Maybe . IdrisType) ts -> LAll (Expr s) ts
  We can always convert a list of marshallable Idris values to
  a list of SQL expressions.

  Totality: total
  Visibility: export
record Val : SQLTable -> Type
  A single name-value pair in an `UPDATE` statement.

  Totality: total
  Visibility: public export
  Constructor: 
V : (name : String) -> {auto 0 prf : IsJust (FindCol name (t .cols))} -> Expr [<t] (TableColType name t) -> Val t

  Projections:
  
.name : Val t -> String
  
0 .prf : ({rec:0} : Val t) -> IsJust (FindCol (name {rec:0}) (t .cols))
  
.val : ({rec:0} : Val t) -> Expr [<t] (TableColType (name {rec:0}) t)
.name : Val t -> String
  Totality: total
  Visibility: public export
name : Val t -> String
  Totality: total
  Visibility: public export
0 .prf : ({rec:0} : Val t) -> IsJust (FindCol (name {rec:0}) (t .cols))
  Totality: total
  Visibility: public export
0 prf : ({rec:0} : Val t) -> IsJust (FindCol (name {rec:0}) (t .cols))
  Totality: total
  Visibility: public export
.val : ({rec:0} : Val t) -> Expr [<t] (TableColType (name {rec:0}) t)
  Totality: total
  Visibility: public export
val : ({rec:0} : Val t) -> Expr [<t] (TableColType (name {rec:0}) t)
  Totality: total
  Visibility: public export
(.=) : {auto to : ToCell a} -> (name : String) -> {auto 0 prf : IsJust (FindCol name (t .cols))} -> {auto 0 _ : TableColType name t = ToCellType a} -> a -> Val t
  Operator alias for the data constructor of `Val`,
  specialized for usage with Idris types with a
  `ToCell` implementation.

  Totality: total
  Visibility: public export
  Fixity Declaration: infix operator, level 1
data Action : Type
  Foreign Key Actions

  Totality: total
  Visibility: public export
  Constructors:
  
SET_NULL : Action
  
SET_DEFAULT : Action
  
CASCADE : Action
  
RESTRICT : Action
  
NO_ACTION : Action
data Event : Type
  Totality: total
  Visibility: public export
  Constructors:
  
ON_UPDATE : Action -> Event
  
ON_DELETE : Action -> Event
data Constraint : SQLTable -> Type
  Column and table constraints to be used when creating a new table.

  Totality: total
  Visibility: public export
  Constructors:
  
NOT_NULL : TColumn t x -> Constraint t
  
AUTOINCREMENT : TColumn t x -> Constraint t
  
UNIQUE : LAll (TColumn t) xs -> Constraint t
  
PRIMARY_KEY : LAll (TColumn t) xs -> Constraint t
  
ForeignKey : (s : SQLTable) -> LAll (TColumn t) xs -> LAll (TColumn s) xs -> List Event -> Constraint t
  
CHECK : Expr [<t] BOOL -> Constraint t
  
DEFAULT : (s : String) -> {auto 0 prf : IsJust (FindCol s (t .cols))} -> Expr [<t] (TableColType s t) -> Constraint t
FOREIGN_KEY : (s : SQLTable) -> LAll (TColumn t) xs -> LAll (TColumn s) xs -> Constraint t
  Convenience API to construct a foreign key constraint.

  Totality: total
  Visibility: public export
FOREIGN_KEY' : (s : SQLTable) -> LAll (TColumn t) xs -> LAll (TColumn s) xs -> List Event -> Constraint t
  Constructs a foreign key constraint with actions

  Totality: total
  Visibility: public export
data CmdType : Type
  Index used to distinguish different types of commands.
  
  This should facilitate writing combinator such as
  `IF_NOT_EXISTS` to operate only on certain commands.

  Totality: total
  Visibility: public export
  Constructors:
  
TCreate : CmdType
  
TDelete : CmdType
  
TDrop : CmdType
  
TInsert : CmdType
  
TSelect : CmdType
  
TUpdate : CmdType
data Cmd : CmdType -> Type
  Data management commands for creating tables and
  inserting, updating, or deleting rows in a table.

  Totality: total
  Visibility: public export
  Constructors:
  
CreateTable : (t : SQLTable) -> List (Constraint t) -> Bool -> Cmd TCreate
  Information used to create a new table.
  
  It is recommended to use a combination of `CREATE_TABLE` and
  `IF_NOT_EXISTS` instead of using this constructor directly.
  
DropTable : SQLTable -> Bool -> Cmd TDrop
  
INSERT : (t : SQLTable) -> LAll (TColumn t) ts -> LAll (Expr [<t]) ts -> Cmd TInsert
  Information required to insert data into a table.
  
  This is well suited if you want to have full control over
  the expressions used to insert data. If, however, you want
  to insert an Idris value with a `ToRow` implementation,
  consider using function `insert` instead.
  
REPLACE : (t : SQLTable) -> LAll (TColumn t) ts -> LAll (Expr [<t]) ts -> Cmd TInsert
  Information required to insert or replace data in a a table.
  
  This is like insert, but will replace values to fullfil `UNIQUE`
  constraints in the table. As such, it is useful for updating
  data that might not yet be present in a table.
  
  This is well suited if you want to have full control over
  the expressions used to replace data. If, however, you want
  to insert an Idris value with a `ToRow` implementation,
  consider using function `replace` instead.
  
UPDATE : (t : SQLTable) -> List (Val t) -> Expr [<t] BOOL -> Cmd TUpdate
  Information required to update values in table.
  
DELETE : (t : SQLTable) -> Expr [<t] BOOL -> Cmd TDelete
  Information required to delete values from a table.
insert : {auto as : ToRow v} -> (t : SQLTable) -> LAll (TColumn t) (ToRowTypes v) -> v -> Cmd TInsert
  Utility version of `INSERT` for those cases when you want to
  insert an Idris value with a `ToRow` implementation.

  Totality: total
  Visibility: export
replace : {auto as : ToRow v} -> (t : SQLTable) -> LAll (TColumn t) (ToRowTypes v) -> v -> Cmd TInsert
  Utility version of `REPLACE` for those cases when you want to
  replace an Idris value with a `ToRow` implementation.

  Totality: total
  Visibility: export
data Cmds : Type
  A list of different types of commands, with the
  command types being hidden.

  Totality: total
  Visibility: public export
  Constructors:
  
Nil : Cmds
  
(::) : Cmd t -> Cmds -> Cmds

  Hints:
  
Monoid Cmds
  
Semigroup Cmds
(++) : Cmds -> Cmds -> Cmds
  Totality: total
  Visibility: export
  Fixity Declaration: infixr operator, level 7
fromList : List (Cmd t) -> Cmds
  Totality: total
  Visibility: export
IF_NOT_EXISTS : Cmd TCreate -> Cmd TCreate
  Create a table only if it does not yet exist.

  Totality: total
  Visibility: public export
IF_EXISTS : Cmd TDrop -> Cmd TDrop
  Drop a table only if it exists.

  Totality: total
  Visibility: public export
CREATE_TABLE : (t : SQLTable) -> List (Constraint t) -> Cmd TCreate
  Convenience constructor for the `CreateTable` command

  Totality: total
  Visibility: public export
DROP_TABLE : SQLTable -> Cmd TDrop
  Convenience constructor for the `DropTable` command

  Totality: total
  Visibility: public export
0 JoinPred : Schema -> SQLTable -> Type
  Totality: total
  Visibility: public export
data Join : Schema -> SQLTable -> Type
  Totality: total
  Visibility: public export
  Constructors:
  
JOIN : (t : SQLTable) -> JoinPred (s :< t0) t -> Join (s :< t0) t
  
OUTER_JOIN : (t : SQLTable) -> JoinPred (s :< t0) t -> Join (s :< t0) t
  
CROSS_JOIN : (t : SQLTable) -> Join (s :< t0) t
  
FROM : (t : SQLTable) -> Join [<] t
USING : (JoinPred s t -> Join s t) -> List (JColumn s t) -> Join s t
  Totality: total
  Visibility: public export
ON : (JoinPred s t -> Join s t) -> Expr (s :< t) BOOL -> Join s t
  Totality: total
  Visibility: public export
data From : Schema -> Type
  The `FROM` part in a select statement.

  Totality: total
  Visibility: public export
  Constructors:
  
Lin : From [<]
  
(:<) : From s -> Join s t -> From (s :< t)
data AscDesc : Type
  Tag indicating, whether results should be sorted in ascending
  or descending order.

  Totality: total
  Visibility: public export
  Constructors:
  
NoAsc : AscDesc
  
Asc : AscDesc
  
Desc : AscDesc
data Collation : SqliteType -> Type
  Different collations used during ordering.
  
  Currently, only `NO CASE` is supported.

  Totality: total
  Visibility: public export
  Constructors:
  
None : Collation t
  
NOCASE : Collation TEXT
record OrderingTerm : Schema -> Type
  Totality: total
  Visibility: public export
  Constructor: 
O : Expr s tpe -> Collation tpe -> AscDesc -> OrderingTerm s

  Projections:
  
.asc : OrderingTerm s -> AscDesc
  
.coll : ({rec:0} : OrderingTerm s) -> Collation (tpe {rec:0})
  
.expr : ({rec:0} : OrderingTerm s) -> Expr s (tpe {rec:0})
  
0 .tpe : OrderingTerm s -> SqliteType
0 .tpe : OrderingTerm s -> SqliteType
  Totality: total
  Visibility: public export
0 tpe : OrderingTerm s -> SqliteType
  Totality: total
  Visibility: public export
.expr : ({rec:0} : OrderingTerm s) -> Expr s (tpe {rec:0})
  Totality: total
  Visibility: public export
expr : ({rec:0} : OrderingTerm s) -> Expr s (tpe {rec:0})
  Totality: total
  Visibility: public export
.coll : ({rec:0} : OrderingTerm s) -> Collation (tpe {rec:0})
  Totality: total
  Visibility: public export
coll : ({rec:0} : OrderingTerm s) -> Collation (tpe {rec:0})
  Totality: total
  Visibility: public export
.asc : OrderingTerm s -> AscDesc
  Totality: total
  Visibility: public export
asc : OrderingTerm s -> AscDesc
  Totality: total
  Visibility: public export
ASC : Expr s t -> OrderingTerm s
  Totality: total
  Visibility: public export
DESC : Expr s t -> OrderingTerm s
  Totality: total
  Visibility: public export
COLLATE : (o : OrderingTerm s) -> Collation (o .tpe) -> OrderingTerm s
  Totality: total
  Visibility: public export
record GroupingTerm : Schema -> Type
  Totality: total
  Visibility: public export
  Constructor: 
G : Expr s tpe -> Collation tpe -> GroupingTerm s

  Projections:
  
.coll : ({rec:0} : GroupingTerm s) -> Collation (tpe {rec:0})
  
.expr : ({rec:0} : GroupingTerm s) -> Expr s (tpe {rec:0})
  
0 .tpe : GroupingTerm s -> SqliteType
0 .tpe : GroupingTerm s -> SqliteType
  Totality: total
  Visibility: public export
0 tpe : GroupingTerm s -> SqliteType
  Totality: total
  Visibility: public export
.expr : ({rec:0} : GroupingTerm s) -> Expr s (tpe {rec:0})
  Totality: total
  Visibility: public export
expr : ({rec:0} : GroupingTerm s) -> Expr s (tpe {rec:0})
  Totality: total
  Visibility: public export
.coll : ({rec:0} : GroupingTerm s) -> Collation (tpe {rec:0})
  Totality: total
  Visibility: public export
coll : ({rec:0} : GroupingTerm s) -> Collation (tpe {rec:0})
  Totality: total
  Visibility: public export
fromString : (col : String) -> {auto 0 _ : IsJust (FindSchemaCol col s)} -> GroupingTerm s
  Totality: total
  Visibility: public export
ord : GroupingTerm s -> OrderingTerm s
  Totality: total
  Visibility: public export
record NamedExpr : Schema -> SqliteType -> Type
  Totality: total
  Visibility: public export
  Constructor: 
AS : Expr s t -> String -> NamedExpr s t

  Projections:
  
.expr : NamedExpr s t -> Expr s t
  
.name : NamedExpr s t -> String
.expr : NamedExpr s t -> Expr s t
  Totality: total
  Visibility: public export
expr : NamedExpr s t -> Expr s t
  Totality: total
  Visibility: public export
.name : NamedExpr s t -> String
  Totality: total
  Visibility: public export
name : NamedExpr s t -> String
  Totality: total
  Visibility: public export
fromString : (col : String) -> {auto 0 p : IsJust (FindSchemaCol col s)} -> NamedExpr s (SchemaColType col s)
  Totality: total
  Visibility: public export
columnName : NamedExpr s t -> String
  Extracts the column name we use to reference a named
  expression.
  
  If a custom name has been set, this will be returned. Otherwise,
  if the expression references a table column, that columns (possibly
  qualified) name will be returned.

  Totality: total
  Visibility: export
ExprColumns : LAll (NamedExpr s) ts -> List Column
  Computes a list of named and typed columns from a list of
  name expressions.
  
  Expressions with an empty string as their name are not included in
  the result.

  Totality: total
  Visibility: public export
ExprSchema : LAll (NamedExpr s) ts -> Schema
  Appends an unnamed table with the list of columns coming from
  the given list of named expressions to a schema.
  
  Expressions with an empty string as their name are not included in
  the result.
  
  This is used to compute the full `Schema` to be used in
  those fields of `Query` that are used for filtering, grouping, and
  sorting.

  Totality: total
  Visibility: public export
record Query : Type -> Type
  Different types of `SELECT` commands.

  Totality: total
  Visibility: public export
  Constructor: 
Q : {auto fromRow : FromRow t} -> Bool -> (schema : Schema) -> From schema -> (columns : LAll (NamedExpr schema) (FromRowTypes t)) -> Expr (ExprSchema columns) BOOL -> Expr (ExprSchema columns) BOOL -> List (GroupingTerm (ExprSchema columns)) -> List (OrderingTerm (ExprSchema columns)) -> Maybe Nat -> Nat -> Query t

  Projections:
  
.columns : ({rec:0} : Query t) -> LAll (NamedExpr (schema {rec:0})) (FromRowTypes t)
  
.distinct : Query t -> Bool
  
.from : ({rec:0} : Query t) -> From (schema {rec:0})
  
.fromRow : Query t -> FromRow t
  
.group_by : ({rec:0} : Query t) -> List (GroupingTerm (ExprSchema (columns {rec:0})))
  
.having : ({rec:0} : Query t) -> Expr (ExprSchema (columns {rec:0})) BOOL
  
.limit : Query t -> Maybe Nat
  
.offset : Query t -> Nat
  
.order_by : ({rec:0} : Query t) -> List (OrderingTerm (ExprSchema (columns {rec:0})))
  
.schema : Query t -> Schema
  
.where_ : ({rec:0} : Query t) -> Expr (ExprSchema (columns {rec:0})) BOOL

  Hint: 
Query t => FromRow t
.fromRow : Query t -> FromRow t
  Totality: total
  Visibility: public export
fromRow : Query t -> FromRow t
  Totality: total
  Visibility: public export
.distinct : Query t -> Bool
  Totality: total
  Visibility: public export
distinct : Query t -> Bool
  Totality: total
  Visibility: public export
.schema : Query t -> Schema
  Totality: total
  Visibility: public export
schema : Query t -> Schema
  Totality: total
  Visibility: public export
.from : ({rec:0} : Query t) -> From (schema {rec:0})
  Totality: total
  Visibility: public export
from : ({rec:0} : Query t) -> From (schema {rec:0})
  Totality: total
  Visibility: public export
.columns : ({rec:0} : Query t) -> LAll (NamedExpr (schema {rec:0})) (FromRowTypes t)
  Totality: total
  Visibility: public export
columns : ({rec:0} : Query t) -> LAll (NamedExpr (schema {rec:0})) (FromRowTypes t)
  Totality: total
  Visibility: public export
.where_ : ({rec:0} : Query t) -> Expr (ExprSchema (columns {rec:0})) BOOL
  Totality: total
  Visibility: public export
where_ : ({rec:0} : Query t) -> Expr (ExprSchema (columns {rec:0})) BOOL
  Totality: total
  Visibility: public export
.having : ({rec:0} : Query t) -> Expr (ExprSchema (columns {rec:0})) BOOL
  Totality: total
  Visibility: public export
having : ({rec:0} : Query t) -> Expr (ExprSchema (columns {rec:0})) BOOL
  Totality: total
  Visibility: public export
.group_by : ({rec:0} : Query t) -> List (GroupingTerm (ExprSchema (columns {rec:0})))
  Totality: total
  Visibility: public export
group_by : ({rec:0} : Query t) -> List (GroupingTerm (ExprSchema (columns {rec:0})))
  Totality: total
  Visibility: public export
.order_by : ({rec:0} : Query t) -> List (OrderingTerm (ExprSchema (columns {rec:0})))
  Totality: total
  Visibility: public export
order_by : ({rec:0} : Query t) -> List (OrderingTerm (ExprSchema (columns {rec:0})))
  Totality: total
  Visibility: public export
.limit : Query t -> Maybe Nat
  Totality: total
  Visibility: public export
limit : Query t -> Maybe Nat
  Totality: total
  Visibility: public export
.offset : Query t -> Nat
  Totality: total
  Visibility: public export
offset : Query t -> Nat
  Totality: total
  Visibility: public export
queryAsRow : Query t => FromRow t
  Totality: total
  Visibility: public export
0 LQuery : List Type -> Type
  Totality: total
  Visibility: public export
SELECT : {auto fromRow : FromRow t} -> LAll (NamedExpr s) (FromRowTypes t) -> From s -> Query t
  Totality: total
  Visibility: public export
SELECT_DISTINCT : {auto fromRow : FromRow t} -> LAll (NamedExpr s) (FromRowTypes t) -> From s -> Query t
  Totality: total
  Visibility: public export
GROUP_BY : (q : Query t) -> List (GroupingTerm (ExprSchema (q .columns))) -> Query t
  Totality: total
  Visibility: public export
  Fixity Declaration: infixl operator, level 7
WHERE : (q : Query t) -> Expr (ExprSchema (q .columns)) BOOL -> Query t
  Totality: total
  Visibility: public export
  Fixity Declaration: infixl operator, level 7
HAVING : (q : Query t) -> Expr (ExprSchema (q .columns)) BOOL -> Query t
  Totality: total
  Visibility: public export
  Fixity Declaration: infixl operator, level 7
ORDER_BY : (q : Query t) -> List (OrderingTerm (ExprSchema (q .columns))) -> Query t
  Totality: total
  Visibility: public export
  Fixity Declaration: infixl operator, level 7
LIMIT : Query t -> Nat -> Query t
  Totality: total
  Visibility: public export
  Fixity Declaration: infixl operator, level 7
OFFSET : Query t -> Nat -> Query t
  Totality: total
  Visibility: public export
  Fixity Declaration: infixl operator, level 7