Skip to main content

sql.to_sql()

SQL for a Substrait JSON plan, with the semantics Rel.eval gives it.

Usage

Source

sql.to_sql(
    plan,
    dialect,
    *,
    deterministic=False,
    guards=True,
    unchecked=None,
    finite=True,
    tie_free=None
)

The result has the plan’s output names (RelRoot.names, else c0, …), and is ordered as Lean orders it when the plan has a FETCH or a window. Raises Unsupported for plans outside the Lean model. This is sverify.engines.to_sql.

deterministic=True promises that no two rows tie on any window’s PARTITION BY and ORDER BY columns (what a contract report’s deterministic says, and what Report.run(deterministic=True) requires). Then windows need no ordinal tiebreak, so engines without a stable scan order can run them; FETCH still needs one.

guards=False leaves out the run-time checks (Dialect.guards). Only pass it for a plan whose contract report is guard_free, and run the SQL on data that meets the contract’s preconditions.

unchecked leaves them out of some expressions only: pass a contract report’s unchecked for the same plan, and run the SQL on data that meets its preconditions (Rel.evalG_marks). The other expressions, and every aggregate, keep their checks.

Parameters

plan: dict | str

A Substrait JSON plan, as a string or parsed (json.loads), such as a node’s internal_plan or sverify.engines.written_plan’s output.

dialect: Dialect

The engine to write SQL for: sverify.engines.DUCKDB, sverify.engines.SNOWFLAKE or sverify.engines.SPARK.

deterministic: bool = False

Promise that windows have no ties on their PARTITION BY and ORDER BY columns (Report.deterministic). Default: False.

guards: bool = True

Write the run-time checks. Default: True.

unchecked: dict | None = None

The expressions to write without checks, as a contract report’s unchecked (sverify.Report.unchecked) for this plan. Default: None (all of them keep their checks).

finite: bool = True

Write the check that finite doubles do not overflow to ±∞ (Dialect.finite), the reference’s precondition (#575). Default: True; False for a plan verified with semantics="duckdb".

tie_free: bool | None = None
Deprecated alias of deterministic.

Returns

str

One SQL query in the dialect. It reads the plan’s tables by their

names, quoted.

Raises

Unsupported
The plan is outside the Lean model, its root names do not match its columns, the dialect cannot express it, or unchecked is for another plan.

Examples

The plan of a transform, as Snowflake SQL:

import json

import pyarrow as pa
import sverify as sv
from sverify.engines import SNOWFLAKE, to_sql
from sverify.io import StaticSource

orders = StaticSource(pa.table({"id": [1, 2], "amount": [30, 5]}), name="orders")


@sv.transform()
def big_orders(orders):
    return orders.filter(orders.amount > 10)


print(to_sql(big_orders(orders).internal_plan, SNOWFLAKE))
# SELECT s1."c0" AS "id", s1."c1" AS "amount" FROM (SELECT s2."c0" AS "c0", ...