Idris2Doc : Sqlite3.Expr

Sqlite3.Expr

(source)
Definitions
data Numeric : SqliteType -> Type
  Totality: total
  Visibility: public export
  Constructors:
  
N_INTEGER : Numeric INTEGER
  
N_REAL : Numeric REAL
data Expr : Schema -> SqliteType -> Type
  A syntax tree type representing well-typed SQLite expressions.

  Totality: total
  Visibility: public export
  Constructors:
  
Lit : (t : SqliteType) -> IdrisType t -> Expr s t
  A literal value in an SQL expression
  
NULL : Expr s t
  The `NULL` literal
  
TRUE : Expr s BOOL
  Alias for the literal `1`, which corresponds to `True` in
  boolean expressions
  
FALSE : Expr s BOOL
  Alias for the literal `0`, which corresponds to `False` in
  boolean expressions
  
Raw : String -> Expr s t
  A raw expressions string that will be used as given.
  
Col : (col : String) -> {auto 0 p : IsJust (FindSchemaCol col s)} -> Expr s (SchemaColType col s)
  A column in a list of tables. Typically, it is convenient to
  use string literals directly for this (see `Expr.fromString`).
  
(>) : Expr s t -> Expr s t -> Expr s BOOL
  Greater-than operator.
  
  Note, that this is subject to SQL's three-valued logic in the
  presence of `NULL`.
  
(<) : Expr s t -> Expr s t -> Expr s BOOL
  Less-than operator.
  
  Note, that this is subject to SQL's three-valued logic in the
  presence of `NULL`.
  
(>=) : Expr s t -> Expr s t -> Expr s BOOL
  Greater-than or equals operator.
  
  Note, that this is subject to SQL's three-valued logic in the
  presence of `NULL`.
  
(<=) : Expr s t -> Expr s t -> Expr s BOOL
  Less-than or equals operator.
  
  Note, that this is subject to SQL's three-valued logic in the
  presence of `NULL`.
  
(==) : Expr s t -> Expr s t -> Expr s BOOL
  Equality operator.
  
  Note, that this is subject to SQL's three-valued logic in the
  presence of `NULL`.
  
(/=) : Expr s t -> Expr s t -> Expr s BOOL
  Inequality operator.
  
  We use the same operator as in the `Eq` interface here, but this
  corresponds to SQL's `<>` (or `!=`) operator.
  
  Note, that this is subject to SQL's three-valued logic in the
  presence of `NULL`.
  
IS : Expr s t -> Expr s t -> Expr s BOOL
  Equality test.
  
  Unlike `(==)`, this will always result in `TRUE` or `FALSE`
  even in the presence of `NULL`.
  
IS_NOT : Expr s t -> Expr s t -> Expr s BOOL
  Inequality test.
  
  Unlike `(==)`, this will always result in `TRUE` or `FALSE`
  even in the presence of `NULL`.
  
(&&) : Expr s BOOL -> Expr s BOOL -> Expr s BOOL
  Logical `AND`.
  
  Note, that this is subject to SQL's three-valued logic in the
  presence of `NULL`.
  
(||) : Expr s BOOL -> Expr s BOOL -> Expr s BOOL
  Logical `OR`.
  
  Note, that this is subject to SQL's three-valued logic in the
  presence of `NULL`.
  
NOT : Expr s BOOL -> Expr s BOOL
  Logical negation.
  
  Note, that this is subject to SQL's three-valued logic in the
  presence of `NULL`.
  
(.&.) : Expr s INTEGER -> Expr s INTEGER -> Expr s INTEGER
  Bit-wise `AND`.
  
  This corresponds to SQLite's `&` operator.
  
(.|.) : Expr s INTEGER -> Expr s INTEGER -> Expr s INTEGER
  Bit-wise `OR`.
  
  This corresponds to SQLite's `|` operator.
  
ShiftL : Expr s INTEGER -> Expr s INTEGER -> Expr s INTEGER
  Bit-wise left shift.
  
  This corresponds to SQLite's `<<` operator.
  
ShiftR : Expr s INTEGER -> Expr s INTEGER -> Expr s INTEGER
  Bit-wise right shift.
  
  This corresponds to SQLite's `>>` operator.
  
Add : {auto 0 _ : Numeric t} -> Expr s t -> Expr s t -> Expr s t
  Numeric addition.
  
  Since `Expr s t` implements `Num` for numeric types `t`, you can
  typically use the addition operator `(+)` instead of this constructor.
  
Mult : {auto 0 _ : Numeric t} -> Expr s t -> Expr s t -> Expr s t
  Numeric multiplication.
  
  Since `Expr s t` implements `Num` for numeric types `t`, you can
  typically use the multiplication operator `(*)` instead of this
  constructor.
  
Sub : {auto 0 _ : Numeric t} -> Expr s t -> Expr s t -> Expr s t
  Numeric subtraction.
  
  Since `Expr s t` implements `Neg` for numeric types `t`, you can
  typically use the subtraction operator `(-)` instead of this
  constructor.
  
Abs : {auto 0 _ : Numeric t} -> Expr s t -> Expr s t
  Computes the absolute of an expressions.
  
  This corresponds to the `abs()` function.
  
Neg : {auto 0 _ : Numeric t} -> Expr s t -> Expr s t
  Numeric negation.
  
Div : {auto 0 _ : Numeric t} -> Expr s t -> Expr s t -> Expr s t
  Numeric division.
  
  Since `Expr s t` implements `Integral` for numeric types `INTEGER`,
  you can typically use `div` for integer division. Likewise, you can
  use `(/)` for floating point division.
  
Mod : Expr s INTEGER -> Expr s INTEGER -> Expr s INTEGER
  Computes the modulus of two integers.
  
  This corresponds to the `%` operator in SQL.
  
(++) : Expr s TEXT -> Expr s TEXT -> Expr s TEXT
  String concatenation.
  
  This corresponds to the `||` operator in SQL.
  
CURRENT_TIME : Expr s TEXT
  The current time as a string.
  
CURRENT_DATE : Expr s TEXT
  The current date as a string.
  
CURRENT_TIMESTAMP : Expr s TEXT
  The current date and time as a string.
  
LIKE : Expr s TEXT -> Expr s TEXT -> Expr s BOOL
  Matches the given text expression against the given
  text pattern.
  
GLOB : Expr s TEXT -> Expr s TEXT -> Expr s BOOL
  Matches the given text expression against the given
  GLOB pattern.
  
IN : Expr s t -> List (Expr s t) -> Expr s BOOL
  True, if the given value appears in the given list of values.
  
COALESCE : List (Expr s t) -> Expr s t
  Returns the first non-NULL value in the given list of expressions.
  
COUNT : Expr s t -> Expr s INTEGER
  Counts the number of aggregated values.
  
  This is typically used with a `GROUP BY` statement.
  
AVG : {auto 0 _ : Numeric t} -> Expr s t -> Expr s REAL
  Returns the average of accumulated values.
  
  This is typically used with a `GROUP BY` statement.
  
SUM : {auto 0 _ : Numeric t} -> Expr s t -> Expr s t
  Returns the sum of accumulated values.
  
  This is typically used with a `GROUP BY` statement.
  
MIN : Expr s t -> Expr s t
  Returns the minimum of accumulated values.
  
  This is typically used with a `GROUP BY` statement.
  
MAX : Expr s t -> Expr s t
  Returns the maximum of accumulated values.
  
  This is typically used with a `GROUP BY` statement.
  
GROUP_CONCAT : Expr s TEXT -> String -> Expr s TEXT
  Concatenates aggregated text values using the given separator.
  
  This is typically used with a `GROUP BY` statement.

  Hints:
  
Fractional (Expr s REAL)
  
FromDouble (Expr s REAL)
  
Integral (Expr s INTEGER)
  
Neg (Expr s INTEGER)
  
Neg (Expr s REAL)
  
Num (Expr s INTEGER)
  
Num (Expr s REAL)
fromString : (col : String) -> {auto 0 p : IsJust (FindSchemaCol col s)} -> Expr s (SchemaColType col s)
  Totality: total
  Visibility: export
val : {auto {conArg:13694} : ToCell a} -> a -> Expr s (ToCellType a)
  Convert a value of a marshallable type to a literal expression.

  Totality: total
  Visibility: export
text : String -> Expr s TEXT
  Totality: total
  Visibility: export
int : Int64 -> Expr s INTEGER
  Totality: total
  Visibility: export
blob : ByteString -> Expr s BLOB
  Totality: total
  Visibility: export
real : Double -> Expr s REAL
  Totality: total
  Visibility: export
commaSep : (a -> String) -> List a -> String
  Converts a list of values to strings and concatenates them using
  a comma as the separator.

  Totality: total
  Visibility: export
encodeText : String -> String
  Encodes a `String` as an SQL literal.
  
  The whole string is wrapped in single quotes. Single quotes withing
  the string are escaped by doubling them.

  Totality: total
  Visibility: export
encodeLit : (t : SqliteType) -> IdrisType t -> String
  Encodes an SQL literal as a string.

  Totality: total
  Visibility: export
encodeExpr : Expr s t -> String
  Encodes an expression as a string.
  
  Literals will be correctly escaped and converted.
  
  Note: See module `Sqlite3.Parameter` for encoding of expressions
        with SQL parameters that will be bound separately when
        binding the statement.

  Totality: total
  Visibility: export