sqlast

The dialect-neutral SQL AST in Lean 4 — ANSI shapes parameterised over a dialect extension. Base of the leangres dependency graph. Dep-free (Lean core only), published as compiled oleans.

bazel_dep(name = "sqlast", version = "0.1.0")

View source & releases on GitHub ↗

The dialect-neutral SQL AST, in Lean 4.

ANSI-shape expressions and statements, parameterised over a dialect extension so that a dialect can contribute its own constructors without either modifying this module or losing the type-level distinction between generic and dialect-specific shapes.

Part of leangres. This is the base of the dependency graph: the Postgres layer extends it, and everything above that depends on it transitively.

The extension seam

Expr takes a type parameter for the dialect’s own constructors:

inductive Expr (Ext : Type) where
  | var       : String → Expr Ext
  | eq        : Expr Ext → Expr Ext → Expr Ext
  | call      : String → List (Expr Ext) → Expr Ext
  …
  | ext       : Ext → Expr Ext          -- the dialect hatch

A dialect then defines its own extension inductive and binds it:

abbrev Expr := Polyglot.Sql.Ast.Expr ExprExt

Sub-expressions cycle back through Ext, so a dialect constructor can carry Expr Ext fields. Dialect-specific literals, operators and table references belong in the dialect’s Ext, not here.

⚠ Expr Ext is a nested inductive — it carries List (Expr Ext). That has a consequence for anyone writing an evaluator over it: structural recursion is rejected on the list arms, and well-founded recursion is accepted but does not reduce under rfl (nor does simp with equation lemmas). Fuel-index the evaluator and prove a fuel-monotonicity lemma before stating anything universally quantified.

Contents

Dialect-specific DDL structures deliberately live in the dialect modules, because production consumers reference dialect-typed fields.

Dependencies

Lean core only. Ast.lean imports nothing; Render.lean imports only it.

No mathlib, no batteries — and please keep it that way. A nominal require batteries elsewhere in this ecosystem cost roughly 15 minutes on every CI run that pulled the module in, and mathlib’s own post-update hook has repeatedly defeated attempts to tree-shake it.

Consuming it

Published as compiled oleans, not shared as source, so downstream modules fetch an artifact instead of recompiling the tower:

bazel_dep(name = "sqlast", version = "0.1.0")

lean_library(
    name = "my_dialect",
    srcs = ["MyDialect/Ast.lean"],
    deps = ["@sqlast//lean:sqlast"],
)

.olean is a compacted heap image — neither Lean-version- nor architecture-portable. Pin the same Lean toolchain (leanprover/lean4:v4.30.0-rc2) and select the artifact matching your platform. Lean rejects a mismatch loudly at use rather than misbehaving quietly.

For scale: the same sources produce 3,232,109 bytes of oleans on linux and 3,224,810 on darwin. That difference is why publishing is per-arch.

Versioning

Plain semver, unlike its sibling leangres modules, which version as <pg_major>.<pg_minor>.<patch> because they model a specific Postgres release. This module doesn’t model Postgres — tagging it 17.6.0 would imply a coupling that doesn’t exist, and would force consumers through a compatibility_level bump on every Postgres major for no content change.

Provenance

Carved from fastverk/polyglot with git filter-repo, history preserved. Commit hashes quoted in those messages may refer to commits that were filtered out — harmless, but they will not resolve here.

License

MIT.

Conformance#

Dependencies#

Depends on

Used by (1 in the registry)

Versions#

1 published version, newest first. Each resolves to an immutable, integrity-checked archive.

Changelog#

← All modules