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