## sql.Dialect


SQL syntax and semantics of one engine.


Usage

``` python
sql.Dialect(
    name,
    guards=True,
    finite=True,
    decimals=False,
)
```


Every hook takes SQL text for its operands (each already self-contained, e.g. parenthesised) and returns SQL text. The defaults are ANSI SQL; subclasses override what their engine writes differently and raise [Unsupported](sql.Unsupported.md#sverify.sql.Unsupported) for what it cannot do.

Use one of the dialect objects: [sverify.engines.DUCKDB](engines.DUCKDB.md#sverify.engines.DUCKDB), [sverify.engines.SNOWFLAKE](engines.SNOWFLAKE.md#sverify.engines.SNOWFLAKE) and [sverify.engines.SPARK](engines.SPARK.md#sverify.engines.SPARK). This is [sverify.engines.Dialect](engines.Dialect.md#sverify.engines.Dialect). Its fields ([name](engines.Dialect.md#sverify.engines.Dialect.name), [guards](sql.Dialect.md#sverify.sql.Dialect.guards), [finite](sql.Dialect.md#sverify.sql.Dialect.finite), [decimals](sql.Dialect.md#sverify.sql.Dialect.decimals)) are public; its SQL-writing methods change whenever a function lands, so they and subclassing are outside the 1.x promise (`docs/stability.md`).


## Attributes


`name: str`  
The engine's name, used in [Unsupported](sql.Unsupported.md#sverify.sql.Unsupported) messages.


## Methods

| Name | Description |
|----|----|
| [add_months()](#add_months) | `Time.addMonths`: the same day `months` months later, clamped to |
| [as_time()](#as_time) | `UnFn.asTime`: the timestamp `us` microseconds after 1970-01-01. |
| [bit_agg()](#bit_agg) | `AggFn.bit` (`bit_and`, `bit_or`, `bit_xor`) of the BIGINT column |
| [black_box()](#black_box) | The scalar black box `row` of `args` (`sverify.black_box`). |
| [black_box_agg()](#black_box_agg) | The aggregate black box `row` of the column `v`, NULLs skipped, |
| [canon()](#canon) | `x` with `-0.0` made `0.0`, the model's one zero: IEEE's |
| [cardinality()](#cardinality) | `UnFn.cardinality`: the number of elements, NULL ones included. |
| [case_when()](#case_when) | `t` when `c` is TRUE, else `e` (also when `c` is NULL). |
| [collect()](#collect) | `AggFn.collect` (#94): the non-NULL values of the column `v` as a |
| [covar()](#covar) | `AggFn.cov`/`corr` of the pairs `v` ([pair](sql.Dialect.md#sverify.sql.Dialect.pair)'s lists), the engine's own |
| [date_add_days()](#date_add_days) | `BinFn.dateAdd`: `n` days after the DATE `d`. |
| [date_days()](#date_days) | A DATE as days since 1970-01-01 (a BIGINT). |
| [date_diff_days()](#date_diff_days) | `BinFn.dateDiff`: the days from `b` to `a`. |
| [date_part()](#date_part) | `Time.datePart` of a timestamp: the proleptic Gregorian calendar, |
| [date_to_time()](#date_to_time) | The midnight of a DATE, for one `chrono` represents. |
| [date_trunc()](#date_trunc) | `Time.trunc`: rounded down to the unit, weeks from Monday. |
| [day_interval()](#day_interval) | `days` days, as a RANGE offset over a DATE. |
| [decimal_arith()](#decimal_arith) | `a op b` of decimals or integers, exactly, as a `DECIMAL(p, s)`. A |
| [decimal_avg()](#decimal_avg) | `SUM(v) / COUNT(v)` at scale `a.s + 4` (`decimalAvgs`); NULL with |
| [decimal_cast()](#decimal_cast) | A decimal, integer or double as a `DECIMAL(p, s)`, rounding half away |
| [decimal_div()](#decimal_div) | `a / b`, a decimal of scale `sa` by an integer, at scale `k.s`, |
| [decimal_lit()](#decimal_lit) | The `DECIMAL(p, s)` of unscaled value `m`. |
| [decimal_to_float()](#decimal_to_float) | Correctly rounded: through the decimal's text. |
| [decimal_to_int()](#decimal_to_int) | Truncated toward zero; fails outside 64 bits. |
| [fit_int()](#fit_int) | `overflow` = [mode](sql.Dialect.md#sverify.sql.Dialect.mode) (`SILENT` or `SATURATE`) of `op` (`+`, `-`, `*`, or |
| [float_ceil()](#float_ceil) | Exact; NaN/±inf stay. |
| [float_eq()](#float_eq) | Equality of doubles: NaN = NaN (IEEE has NaN \<\> NaN). |
| [float_extreme()](#float_extreme) | `AggFn.min`/`max` ([fn](sql.Dialect.md#sverify.sql.Dialect.fn) is `MIN` or `MAX`) of the doubles of `v`, over |
| [float_floor()](#float_floor) | Exact; NaN/±inf stay (a zero result goes through [canon](sql.Dialect.md#sverify.sql.Dialect.canon)). |
| [float_lit()](#float_lit) | A double: NaN, ±inf, or a number (`-0.0` is `0.0`). |
| [float_logb()](#float_logb) | `ln x / ln b`, for positive `x` and `b`, `b` not 1. |
| [float_lt()](#float_lt) | `<` of doubles: NaN is above everything else. |
| [float_mod()](#float_mod) | `BinFn.fmod`, C's `fmod`: the sign of `a`; NaN for a NaN or an |
| [float_neg()](#float_neg) | IEEE negation; NaN stays NaN ([canon](sql.Dialect.md#sverify.sql.Dialect.canon) makes `-0.0` zero). |
| [float_pow()](#float_pow) | C's `pow`: IEEE results, no errors. |
| [float_rank()](#float_rank) | 1 for NaN, 0 for other doubles, NULL for NULL: NaN is above `inf`. |
| [float_round()](#float_round) | To an integer, halves away from zero; NaN/±inf stay. |
| [float_round_to()](#float_round_to) | `ROUND(x, d)` as `FloatCode.roundTo` (DuckDB 2.0's, \#335): with |
| [float_sum()](#float_sum) | `floatSum`: the doubles of `v` added one by one in the order of the |
| [float_to_int()](#float_to_int) | `CAST(x AS BIGINT)`: truncation toward zero; NaN, ±inf and values |
| [float_to_int_or_null()](#float_to_int_or_null) | `TRY_CAST(x AS BIGINT)` (`UnFn.ftoiOrNull`, \#58): truncation toward |
| [float_var()](#float_var) | `AggFn.var` of the doubles of `v` with the engine's own algorithm |
| [fn()](#fn) | The function [name](engines.Dialect.md#sverify.engines.Dialect.name) of `args` (SQL text), as the function table |
| [greatest()](#greatest) | `GREATEST(a, b)`, skipping NULLs. |
| [ilike()](#ilike) | `LIKE` ignoring case (ASCII text only), with [like](sql.Dialect.md#sverify.sql.Dialect.like)'s escapes. |
| [int_avg()](#int_avg) | `AggFn.iavg` of the BIGINT column `v` (over the window `over`, or |
| [int_div()](#int_div) | `BinFn.idiv`: truncating; division by zero raises (Lean: NULL), but |
| [int_lit()](#int_lit) | A BIGINT constant; `i` is in the 64-bit range. |
| [int_mod()](#int_mod) | `BinFn.imod`: the sign of `a`; by zero raises (Lean: NULL), by -1 is 0; |
| [int_pow()](#int_pow) | `BinFn.ipow` with a constant exponent: a negative exponent, or a |
| [int_pow_var()](#int_pow_var) | `BinFn.ipow` with an exponent column: as [int_pow](sql.Dialect.md#sverify.sql.Dialect.int_pow), row by row. |
| [int_product()](#int_product) | `a` multiplied `n` times (1 ≤ n ≤ 64), raising on 64-bit overflow. |
| [int_sum()](#int_sum) | `SUM` of the BIGINT column `v`, exactly; a sum outside 64 bits |
| [int_to_str()](#int_to_str) | Decimal digits with a leading `-` for negatives (Lean's `toString`). |
| [is_ascii()](#is_ascii) | Is every character of `s` ASCII? (Its UTF-8 bytes are its characters.) |
| [is_inf()](#is_inf) | TRUE for `±∞`, NULL for NULL. |
| [is_nan()](#is_nan) | TRUE for NaN, NULL for NULL. |
| [is_true()](#is_true) | TRUE when `a` is TRUE, FALSE when it is FALSE or NULL. |
| [least()](#least) | `LEAST(a, b)`, skipping NULLs. |
| [like()](#like) | `s LIKE pattern` with `\` as the escape character; the pattern has |
| [like_pattern()](#like_pattern) | [like_pattern](sql.Dialect.md#sverify.sql.Dialect.like_pattern) of a computed pattern: a backslash appended when `p` |
| [list_element()](#list_element) | `UnFn.listElement`: zero-based, from the end for a negative offset, |
| [list_lit()](#list_lit) | A list literal of the SQL items, of kind [kind](io.SourceBatch.md#sverify.io.SourceBatch.kind) (#94). |
| [list_lt()](#list_lt) | `Value.listLt3`: `a < b` of two lists, lexicographically; a proper |
| [lowered()](#lowered) | [fn](sql.Dialect.md#sverify.sql.Dialect.fn) of `args` as the engine's generated, proved lowering writes it |
| [mode()](#mode) | `AggFn.mode` (#53): the most frequent value of the column `v`, of the |
| [narrow_or_null()](#narrow_or_null) | `TRY_CAST(x AS INT)` to `bits` bits (`UnFn.narrowOrNull`, \#58): `x`, |
| [octet_length()](#octet_length) | The size of `s` in UTF-8 bytes. |
| [over_frame()](#over_frame) | `OVER (PARTITION BY … ORDER BY … frame)`. |
| [pair()](#pair) | `BinFn.pair`: the two doubles as a list, NULL if either is (#54). |
| [pick()](#pick) | `AggFn.pick` (#55): the first or last value of the column `v`, NULLs |
| [quantile()](#quantile) | `AggFn.quantile` (#53) of the column `v` for the decimal literal `q`: |
| [raise_()](#raise_) | An expression of type [kind](io.SourceBatch.md#sverify.io.SourceBatch.kind) that fails at run time with `message` |
| [refused()](#refused) | The refusal of a function this dialect does not run. [to_sql](sql.to_sql.md#sverify.sql.to_sql) |
| [regex_extract()](#regex_extract) | `UnFn.regexExtract` (#50): group [group](group.md#sverify.group) of the first match of the |
| [regex_replace()](#regex_replace) | `UnFn.regexReplace` (#50): the first match of the constant `pattern` |
| [regex_search()](#regex_search) | Does the regular expression (a constant) match somewhere in `s`? |
| [repeat()](#repeat) | `s` `n` times, '' for `n ≤ 0`. |
| [replace()](#replace) | Every non-overlapping `pattern` (not empty) from the left. |
| [result_kind()](#result_kind) | Raise [Unsupported](sql.Unsupported.md#sverify.sql.Unsupported) if a result column cannot have this kind. |
| [row_ordinal()](#row_ordinal) | An expression numbering a base table's rows in a fixed scan order, |
| [sort_key()](#sort_key) | One ORDER BY key; [kind](io.SourceBatch.md#sverify.io.SourceBatch.kind) is what `expr` is (a double's sort is |
| [string_agg()](#string_agg) | `AggFn.concat` (#55): the strings of the column `v`, NULLs skipped, |
| [substring()](#substring) | Characters from 1-based `start` ≥ 1 on (`length` of them). |
| [time_add()](#time_add) | A time of day plus `0 ≤ micros` \< a day, wrapping around midnight |
| [time_diff()](#time_diff) | `a - b` for timestamps, as an interval. |
| [time_micros()](#time_micros) | A timestamp as microseconds since 1970-01-01 (a BIGINT). |
| [time_of_day()](#time_of_day) | `Time.timeOfDay`: the TIME of a timestamp. |
| [time_part()](#time_part) | `Time.partOf` of a time of day, for its clock parts (`millisecond` |
| [time_trunc()](#time_trunc) | `Time.trunc` of a time of day, to a unit of an hour or less. |
| [to_date()](#to_date) | `UnFn.toDate`: the calendar day of a timestamp (rounding down). |
| [trim()](#trim) | Remove characters of the set `chars` from the start and/or end. |
| [trunc_div()](#trunc_div) | `a / b` rounded toward zero, for `b <> 0`; must raise on `MIN / -1`. |
| [trunc_mod()](#trunc_mod) | The remainder of [trunc_div](sql.Dialect.md#sverify.sql.Dialect.trunc_div), with the sign of `a`, for `b` not 0 or -1. |
| [unnest_from()](#unnest_from) | [source](io.Sink.md#sverify.io.Sink.source) joined with the elements of its list column `lst`, as |
| [values()](#values) | A FROM item with these rows (at least one) and column names. |
| [window_float_sum()](#window_float_sum) | `floatSum`: the frame's doubles added left to right, from 0.0. |
| [window_float_var()](#window_float_var) | `varOf` of the frame's doubles (at least one, two for a sample): |
| [window_int_sum()](#window_int_sum) | `SUM` of BIGINTs over a frame; must raise where it leaves 64 bits. |
| [zero_pad()](#zero_pad) | The integer `n ≥ 0` in decimal, padded with zeros to `width` digits |

------------------------------------------------------------------------


#### add_months()


`Time.addMonths`: the same day `months` months later, clamped to


Usage

``` python
add_months(x, months, kind)
```


the end of that month ([kind](io.SourceBatch.md#sverify.io.SourceBatch.kind) is `date` or `time`).


------------------------------------------------------------------------


#### as_time()


`UnFn.asTime`: the timestamp `us` microseconds after 1970-01-01.


Usage

``` python
as_time(us)
```


------------------------------------------------------------------------


#### bit_agg()


`AggFn.bit` (`bit_and`, `bit_or`, `bit_xor`) of the BIGINT column


Usage

``` python
bit_agg(fn, v, over)
```


`v` (over the window `over`, or grouped for `''`): NULLs skipped, NULL without values (#53).


------------------------------------------------------------------------


#### black_box()


The scalar black box `row` of `args` (`sverify.black_box`).


Usage

``` python
black_box(row, args)
```


------------------------------------------------------------------------


#### black_box_agg()


The aggregate black box `row` of the column `v`, NULLs skipped,


Usage

``` python
black_box_agg(row, v)
```


`row.empty` without values.


------------------------------------------------------------------------


#### canon()


`x` with `-0.0` made `0.0`, the model's one zero: IEEE's


Usage

``` python
canon(x)
```


`-0.0 + 0.0` is `0.0`, and other values stay (`x` appears once).


------------------------------------------------------------------------


#### cardinality()


`UnFn.cardinality`: the number of elements, NULL ones included.


Usage

``` python
cardinality(x)
```


------------------------------------------------------------------------


#### case_when()


`t` when `c` is TRUE, else `e` (also when `c` is NULL).


Usage

``` python
case_when(c, t, e)
```


------------------------------------------------------------------------


#### collect()


`AggFn.collect` (#94): the non-NULL values of the column `v` as a


Usage

``` python
collect(v, order)
```


list, in the order `order`; NULL without values.


------------------------------------------------------------------------


#### covar()


`AggFn.cov`/`corr` of the pairs `v` ([pair](sql.Dialect.md#sverify.sql.Dialect.pair)'s lists), the engine's own


Usage

``` python
covar(fn, v)
```


algorithm (#54); NULL cases are the caller's.


------------------------------------------------------------------------


#### date_add_days()


`BinFn.dateAdd`: `n` days after the DATE `d`.


Usage

``` python
date_add_days(d, n)
```


------------------------------------------------------------------------


#### date_days()


A DATE as days since 1970-01-01 (a BIGINT).


Usage

``` python
date_days(d)
```


------------------------------------------------------------------------


#### date_diff_days()


`BinFn.dateDiff`: the days from `b` to `a`.


Usage

``` python
date_diff_days(a, b)
```


------------------------------------------------------------------------


#### date_part()


`Time.datePart` of a timestamp: the proleptic Gregorian calendar,


Usage

``` python
date_part(part, ts)
```


`week` the ISO week, `dow` from Sunday = 0, `millisecond` and `microsecond` within the minute; NULL outside the dates chrono represents (the years -262143 to 262142).


------------------------------------------------------------------------


#### date_to_time()


The midnight of a DATE, for one `chrono` represents.


Usage

``` python
date_to_time(d)
```


------------------------------------------------------------------------


#### date_trunc()


`Time.trunc`: rounded down to the unit, weeks from Monday.


Usage

``` python
date_trunc(unit, ts)
```


------------------------------------------------------------------------


#### day_interval()


`days` days, as a RANGE offset over a DATE.


Usage

``` python
day_interval(days)
```


------------------------------------------------------------------------


#### decimal_arith()


`a op b` of decimals or integers, exactly, as a `DECIMAL(p, s)`. A


Usage

``` python
decimal_arith(op, a, b, sa, k)
```


product widens `a` (of scale `sa`) to 38 digits first, so that the engine's own result type cannot overflow before the reference's.


------------------------------------------------------------------------


#### decimal_avg()


`SUM(v) / COUNT(v)` at scale `a.s + 4` (`decimalAvgs`); NULL with


Usage

``` python
decimal_avg(v, a, k)
```


no values.


------------------------------------------------------------------------


#### decimal_cast()


A decimal, integer or double as a `DECIMAL(p, s)`, rounding half away


Usage

``` python
decimal_cast(a, k)
```


from zero to a smaller scale.


------------------------------------------------------------------------


#### decimal_div()


`a / b`, a decimal of scale `sa` by an integer, at scale `k.s`,


Usage

``` python
decimal_div(a, b, sa, k)
```


rounded half away from zero (`roundDivInt?`), in 128-bit integers; NULL for `b = 0` (`BinFn.ddiv`).


------------------------------------------------------------------------


#### decimal_lit()


The `DECIMAL(p, s)` of unscaled value `m`.


Usage

``` python
decimal_lit(m, k)
```


------------------------------------------------------------------------


#### decimal_to_float()


Correctly rounded: through the decimal's text.


Usage

``` python
decimal_to_float(a)
```


------------------------------------------------------------------------


#### decimal_to_int()


Truncated toward zero; fails outside 64 bits.


Usage

``` python
decimal_to_int(a)
```


------------------------------------------------------------------------


#### fit_int()


`overflow` = [mode](sql.Dialect.md#sverify.sql.Dialect.mode) (`SILENT` or `SATURATE`) of `op` (`+`, `-`, `*`, or


Usage

``` python
fit_int(mode, bits, op, args)
```


`-` negating one argument) at `bits` bits (`UnFn.fit`, \#241).


------------------------------------------------------------------------


#### float_ceil()


Exact; NaN/±inf stay.


Usage

``` python
float_ceil(x)
```


------------------------------------------------------------------------


#### float_eq()


Equality of doubles: NaN = NaN (IEEE has NaN \<\> NaN).


Usage

``` python
float_eq(a, b)
```


------------------------------------------------------------------------


#### float_extreme()


`AggFn.min`/`max` ([fn](sql.Dialect.md#sverify.sql.Dialect.fn) is `MIN` or `MAX`) of the doubles of `v`, over


Usage

``` python
float_extreme(fn, v, over)
```


the window `over` or the group: by their codes, NaN above `+∞` (#371).


------------------------------------------------------------------------


#### float_floor()


Exact; NaN/±inf stay (a zero result goes through [canon](sql.Dialect.md#sverify.sql.Dialect.canon)).


Usage

``` python
float_floor(x)
```


------------------------------------------------------------------------


#### float_lit()


A double: NaN, ±inf, or a number (`-0.0` is `0.0`).


Usage

``` python
float_lit(f)
```


------------------------------------------------------------------------


#### float_logb()


`ln x / ln b`, for positive `x` and `b`, `b` not 1.


Usage

``` python
float_logb(x, b)
```


------------------------------------------------------------------------


#### float_lt()


`<` of doubles: NaN is above everything else.


Usage

``` python
float_lt(a, b)
```


------------------------------------------------------------------------


#### float_mod()


`BinFn.fmod`, C's `fmod`: the sign of `a`; NaN for a NaN or an


Usage

``` python
float_mod(a, b)
```


infinite `a`, and `a` for an infinite `b`. By zero it raises, as [int_mod](sql.Dialect.md#sverify.sql.Dialect.int_mod), but `NULL % 0.0` is NULL. The edge cases are written out, so that engines agree on them (Spark's ANSI `%` raises on zero, DuckDB gives NaN); only finite operands reach the engine's `%`.


------------------------------------------------------------------------


#### float_neg()


IEEE negation; NaN stays NaN ([canon](sql.Dialect.md#sverify.sql.Dialect.canon) makes `-0.0` zero).


Usage

``` python
float_neg(a)
```


------------------------------------------------------------------------


#### float_pow()


C's `pow`: IEEE results, no errors.


Usage

``` python
float_pow(a, b)
```


------------------------------------------------------------------------


#### float_rank()


1 for NaN, 0 for other doubles, NULL for NULL: NaN is above `inf`.


Usage

``` python
float_rank(x)
```


------------------------------------------------------------------------


#### float_round()


To an integer, halves away from zero; NaN/±inf stay.


Usage

``` python
float_round(x)
```


------------------------------------------------------------------------


#### float_round_to()


`ROUND(x, d)` as `FloatCode.roundTo` (DuckDB 2.0's, \#335): with


Usage

``` python
float_round_to(x, digits)
```


`m = 10^|d|`, `round(x · m) / m` for `d ≥ 0` and `round(x / m) · m` for `d < 0`, `x` where that is not finite; 0 for `d < 0` when `m` is `±∞`. `±∞` and NaN stay.


------------------------------------------------------------------------


#### float_sum()


`floatSum`: the doubles of `v` added one by one in the order of the


Usage

``` python
float_sum(v, o)
```


ordinal `o`, from +0.0 (rounding depends on the order).


------------------------------------------------------------------------


#### float_to_int()


`CAST(x AS BIGINT)`: truncation toward zero; NaN, ±inf and values


Usage

``` python
float_to_int(x)
```


outside 64 bits must raise (Lean: NULL).


------------------------------------------------------------------------


#### float_to_int_or_null()


`TRY_CAST(x AS BIGINT)` (`UnFn.ftoiOrNull`, \#58): truncation toward


Usage

``` python
float_to_int_or_null(x)
```


zero, NULL for NaN, ±inf and values outside 64 bits.


------------------------------------------------------------------------


#### float_var()


`AggFn.var` of the doubles of `v` with the engine's own algorithm


Usage

``` python
float_var(fn, v)
```


(#54): `VAR_SAMP`, `VAR_POP`, `STDDEV_SAMP` or `STDDEV_POP`.


------------------------------------------------------------------------


#### fn()


The function [name](engines.Dialect.md#sverify.engines.Dialect.name) of `args` (SQL text), as the function table


Usage

``` python
fn(name, *args)
```


writes it for this dialect (`sverify._functions`).


------------------------------------------------------------------------


#### greatest()


`GREATEST(a, b)`, skipping NULLs.


Usage

``` python
greatest(a, b)
```


------------------------------------------------------------------------


#### ilike()


`LIKE` ignoring case (ASCII text only), with [like](sql.Dialect.md#sverify.sql.Dialect.like)'s escapes.


Usage

``` python
ilike(s, pattern)
```


------------------------------------------------------------------------


#### int_avg()


`AggFn.iavg` of the BIGINT column `v` (over the window `over`, or


Usage

``` python
int_avg(v, over)
```


grouped for `''`): the exact mean, truncated toward zero; NULL without values (#209).


------------------------------------------------------------------------


#### int_div()


`BinFn.idiv`: truncating; division by zero raises (Lean: NULL), but


Usage

``` python
int_div(a, b)
```


`NULL / 0` is NULL, as in `Safety.lean` (only integers divide).


------------------------------------------------------------------------


#### int_lit()


A BIGINT constant; `i` is in the 64-bit range.


Usage

``` python
int_lit(i)
```


------------------------------------------------------------------------


#### int_mod()


`BinFn.imod`: the sign of `a`; by zero raises (Lean: NULL), by -1 is 0;


Usage

``` python
int_mod(a, b)
```


`NULL % 0` is NULL.


------------------------------------------------------------------------


#### int_pow()


`BinFn.ipow` with a constant exponent: a negative exponent, or a


Usage

``` python
int_pow(a, b)
```


result outside 64 bits, raises (Lean: NULL); NULL stays NULL.


------------------------------------------------------------------------


#### int_pow_var()


`BinFn.ipow` with an exponent column: as [int_pow](sql.Dialect.md#sverify.sql.Dialect.int_pow), row by row.


Usage

``` python
int_pow_var(a, b)
```


------------------------------------------------------------------------


#### int_product()


`a` multiplied `n` times (1 ≤ n ≤ 64), raising on 64-bit overflow.


Usage

``` python
int_product(a, n)
```


------------------------------------------------------------------------


#### int_sum()


`SUM` of the BIGINT column `v`, exactly; a sum outside 64 bits


Usage

``` python
int_sum(v)
```


raises (DataFusion wraps around, Lean's sum is the true one).


------------------------------------------------------------------------


#### int_to_str()


Decimal digits with a leading `-` for negatives (Lean's `toString`).


Usage

``` python
int_to_str(a)
```


------------------------------------------------------------------------


#### is_ascii()


Is every character of `s` ASCII? (Its UTF-8 bytes are its characters.)


Usage

``` python
is_ascii(s)
```


------------------------------------------------------------------------


#### is_inf()


TRUE for `±∞`, NULL for NULL.


Usage

``` python
is_inf(x)
```


------------------------------------------------------------------------


#### is_nan()


TRUE for NaN, NULL for NULL.


Usage

``` python
is_nan(x)
```


------------------------------------------------------------------------


#### is_true()


TRUE when `a` is TRUE, FALSE when it is FALSE or NULL.


Usage

``` python
is_true(a)
```


------------------------------------------------------------------------


#### least()


`LEAST(a, b)`, skipping NULLs.


Usage

``` python
least(a, b)
```


------------------------------------------------------------------------


#### like()


`s LIKE pattern` with `\` as the escape character; the pattern has


Usage

``` python
like(s, pattern)
```


no trailing lone backslash ([like_pattern](sql.Dialect.md#sverify.sql.Dialect.like_pattern)).


------------------------------------------------------------------------


#### like_pattern()


[like_pattern](sql.Dialect.md#sverify.sql.Dialect.like_pattern) of a computed pattern: a backslash appended when `p`


Usage

``` python
like_pattern(p)
```


ends with an odd number of them.


------------------------------------------------------------------------


#### list_element()


`UnFn.listElement`: zero-based, from the end for a negative offset,


Usage

``` python
list_element(x, offset)
```


NULL out of range (#94).


------------------------------------------------------------------------


#### list_lit()


A list literal of the SQL items, of kind [kind](io.SourceBatch.md#sverify.io.SourceBatch.kind) (#94).


Usage

``` python
list_lit(items, kind)
```


------------------------------------------------------------------------


#### list_lt()


`Value.listLt3`: `a < b` of two lists, lexicographically; a proper


Usage

``` python
list_lt(a, b)
```


prefix is smaller, two NULL elements are equal, and a NULL element against a value makes the result NULL (#207).


------------------------------------------------------------------------


#### lowered()


[fn](sql.Dialect.md#sverify.sql.Dialect.fn) of `args` as the engine's generated, proved lowering writes it


Usage

``` python
lowered(fn, args, kind)
```


(`sverify.sql.lowering`, \#241), or None where there is none and the printer writes it by hand. [kind](io.SourceBatch.md#sverify.io.SourceBatch.kind) is the result's.


------------------------------------------------------------------------


#### mode()


`AggFn.mode` (#53): the most frequent value of the column `v`, of the


Usage

``` python
mode(v, order)
```


values that tie the first in the order `order`; NULL without values.


------------------------------------------------------------------------


#### narrow_or_null()


`TRY_CAST(x AS INT)` to `bits` bits (`UnFn.narrowOrNull`, \#58): `x`,


Usage

``` python
narrow_or_null(x, bits)
```


or NULL where it does not fit.


------------------------------------------------------------------------


#### octet_length()


The size of `s` in UTF-8 bytes.


Usage

``` python
octet_length(s)
```


------------------------------------------------------------------------


#### over_frame()


`OVER (PARTITION BY … ORDER BY … frame)`.


Usage

``` python
over_frame(partition, order, frame)
```


------------------------------------------------------------------------


#### pair()


`BinFn.pair`: the two doubles as a list, NULL if either is (#54).


Usage

``` python
pair(a, b)
```


------------------------------------------------------------------------


#### pick()


`AggFn.pick` (#55): the first or last value of the column `v`, NULLs


Usage

``` python
pick(fn, v, order)
```


skipped, in the order `order`; NULL without values.


------------------------------------------------------------------------


#### quantile()


`AggFn.quantile` (#53) of the column `v` for the decimal literal `q`:


Usage

``` python
quantile(cont, v, q)
```


the value at position `⌈n·q⌉` (`quantile_disc`), or the linear interpolation of the doubles at `⌊(n−1)·q⌋` and `⌈(n−1)·q⌉` (`quantile_cont`); NULLs skipped, NULL without values.


------------------------------------------------------------------------


#### raise\_()


An expression of type [kind](io.SourceBatch.md#sverify.io.SourceBatch.kind) that fails at run time with `message`


Usage

``` python
raise_(message, dep, kind)
```


when evaluated (and is NULL when `dep` is NULL). Only evaluated in a `CASE` branch that needs it.


------------------------------------------------------------------------


#### refused()


The refusal of a function this dialect does not run. [to_sql](sql.to_sql.md#sverify.sql.to_sql)


Usage

``` python
refused(fn)
```


raises it before writing anything (`sverify._support`); the hooks of those functions raise it too, for a dialect the table misses.


------------------------------------------------------------------------


#### regex_extract()


`UnFn.regexExtract` (#50): group [group](group.md#sverify.group) of the first match of the


Usage

``` python
regex_extract(s, pattern, group)
```


constant `pattern` in `s`, `''` where there is none.


------------------------------------------------------------------------


#### regex_replace()


`UnFn.regexReplace` (#50): the first match of the constant `pattern`


Usage

``` python
regex_replace(s, pattern, replacement, every)
```


in `s`, or every match, replaced (`\1` is a group).


------------------------------------------------------------------------


#### regex_search()


Does the regular expression (a constant) match somewhere in `s`?


Usage

``` python
regex_search(s, pattern)
```


Regular expressions are black boxes in Lean; each engine has its own dialect, which agrees with Rust's on simple patterns.


------------------------------------------------------------------------


#### repeat()


`s` `n` times, '' for `n ≤ 0`.


Usage

``` python
repeat(s, n)
```


------------------------------------------------------------------------


#### replace()


Every non-overlapping `pattern` (not empty) from the left.


Usage

``` python
replace(s, pattern, replacement)
```


------------------------------------------------------------------------


#### result_kind()


Raise [Unsupported](sql.Unsupported.md#sverify.sql.Unsupported) if a result column cannot have this kind.


Usage

``` python
result_kind(kind)
```


------------------------------------------------------------------------


#### row_ordinal()


An expression numbering a base table's rows in a fixed scan order,


Usage

``` python
row_ordinal()
```


used where Lean's list order matters (below FETCH and windows).


------------------------------------------------------------------------


#### sort_key()


One ORDER BY key; [kind](io.SourceBatch.md#sverify.io.SourceBatch.kind) is what `expr` is (a double's sort is


Usage

``` python
sort_key(expr, desc, nulls_first, kind=None)
```


already split into rank and value keys).


------------------------------------------------------------------------


#### string_agg()


`AggFn.concat` (#55): the strings of the column `v`, NULLs skipped,


Usage

``` python
string_agg(v, sep, order)
```


in the order `order`, joined by `sep`; NULL without values.


------------------------------------------------------------------------


#### substring()


Characters from 1-based `start` ≥ 1 on (`length` of them).


Usage

``` python
substring(s, start, length)
```


------------------------------------------------------------------------


#### time_add()


A time of day plus `0 ≤ micros` \< a day, wrapping around midnight


Usage

``` python
time_add(t, micros)
```


(`Time.timeOfDay` of the sum).


------------------------------------------------------------------------


#### time_diff()


`a - b` for timestamps, as an interval.


Usage

``` python
time_diff(a, b)
```


------------------------------------------------------------------------


#### time_micros()


A timestamp as microseconds since 1970-01-01 (a BIGINT).


Usage

``` python
time_micros(ts)
```


------------------------------------------------------------------------


#### time_of_day()


`Time.timeOfDay`: the TIME of a timestamp.


Usage

``` python
time_of_day(ts)
```


------------------------------------------------------------------------


#### time_part()


`Time.partOf` of a time of day, for its clock parts (`millisecond`


Usage

``` python
time_part(part, t)
```


and `microsecond` within the minute).


------------------------------------------------------------------------


#### time_trunc()


`Time.trunc` of a time of day, to a unit of an hour or less.


Usage

``` python
time_trunc(unit, t)
```


------------------------------------------------------------------------


#### to_date()


`UnFn.toDate`: the calendar day of a timestamp (rounding down).


Usage

``` python
to_date(ts)
```


------------------------------------------------------------------------


#### trim()


Remove characters of the set `chars` from the start and/or end.


Usage

``` python
trim(s, chars, left, right)
```


------------------------------------------------------------------------


#### trunc_div()


`a / b` rounded toward zero, for `b <> 0`; must raise on `MIN / -1`.


Usage

``` python
trunc_div(a, b)
```


------------------------------------------------------------------------


#### trunc_mod()


The remainder of [trunc_div](sql.Dialect.md#sverify.sql.Dialect.trunc_div), with the sign of `a`, for `b` not 0 or -1.


Usage

``` python
trunc_mod(a, b)
```


------------------------------------------------------------------------


#### unnest_from()


joined with the elements of its list column `lst`, as


Usage

``` python
unnest_from(source, lst, alias)
```


`alias(e, i)`: element and 1-based position, no row for a NULL or empty list (`Rel.unnest`, \#94).


------------------------------------------------------------------------


#### values()


A FROM item with these rows (at least one) and column names.


Usage

``` python
values(rows, columns)
```


------------------------------------------------------------------------


#### window_float_sum()


`floatSum`: the frame's doubles added left to right, from 0.0.


Usage

``` python
window_float_sum(v, over)
```


------------------------------------------------------------------------


#### window_float_var()


`varOf` of the frame's doubles (at least one, two for a sample):


Usage

``` python
window_float_var(sample, sqrt, v, over)
```


their mean as `floatSum` over the count, then the squared deviations added left to right from 0.0, over `n - 1` or `n`, at least 0, and its square root for `STDDEV`.


------------------------------------------------------------------------


#### window_int_sum()


`SUM` of BIGINTs over a frame; must raise where it leaves 64 bits.


Usage

``` python
window_int_sum(v, over)
```


------------------------------------------------------------------------


#### zero_pad()


The integer `n ≥ 0` in decimal, padded with zeros to `width` digits


Usage

``` python
zero_pad(n, width)
```


(`lpad` would cut a longer one).