def PostgREST.Query.pgFmtIdent (s : String) : String

Quote a SQL identifier by wrapping in double-quotes and escaping internal double-quotes. $$\text{pgFmtIdent}(s) = \texttt{"}\ s[\texttt{"} \mapsto \texttt{""}]\ \texttt{"}$$ This prevents SQL injection in identifier contexts.

Equations

• PostgREST.Query.pgFmtIdent s = "\"" ++ s.replace "\"" "\"\"" ++ "\""

def PostgREST.Query.pgFmtQi (qi : SchemaCache.Identifiers.QualifiedIdentifier) : String

Format a schema-qualified identifier as "schema"."name". $$\text{pgFmtQi}(qi) = \text{pgFmtIdent}(qi.\text{schema}) \cdot \texttt{.} \cdot \text{pgFmtIdent}(qi.\text{name})$$

Equations

• PostgREST.Query.pgFmtQi qi = PostgREST.Query.pgFmtIdent qi.qiSchema ++ "." ++ PostgREST.Query.pgFmtIdent qi.qiName

def PostgREST.Query.pgFmtLit (s : String) : String

Quote a SQL literal by wrapping in single-quotes and escaping internal single-quotes. $$\text{pgFmtLit}(s) = \texttt{'}\ s[\texttt{'} \mapsto \texttt{''}]\ \texttt{'}$$ Use for known-safe values only, NOT arbitrary user input (use parameterized queries for user input).

Equations

• PostgREST.Query.pgFmtLit s = "'" ++ s.replace "'" "''" ++ "'"

def PostgREST.Query.pgFmtColumn (table : SchemaCache.Identifiers.QualifiedIdentifier) (col : SchemaCache.Identifiers.FieldName) : String

Format a column reference: "schema"."table"."column". $$\text{pgFmtColumn}(t, c) = \text{pgFmtQi}(t) \cdot \texttt{.} \cdot \text{pgFmtIdent}(c)$$

Equations

• PostgREST.Query.pgFmtColumn table col = PostgREST.Query.pgFmtQi table ++ "." ++ PostgREST.Query.pgFmtIdent col

def PostgREST.Query.pgFmtField (cf : Plan.CoercibleField) (table : Option SchemaCache.Identifiers.QualifiedIdentifier) : String

Format a coercible field reference with optional JSON path traversal and type cast. $$\text{pgFmtField}(cf, t?) = \text{base} \circ \text{jsonOps} \circ \text{cast}$$ where base is "table"."col" or just "col", jsonOps chains -> and ->> operators, and cast appends ::type.

Equations

• One or more equations did not get rendered due to their size.

def PostgREST.Query.simpleOpToSql : String → String

Map a PostgREST simple operator name to its SQL equivalent. $$\text{simpleOpToSql} : \text{String} \to \text{String}$$

Equations

• PostgREST.Query.simpleOpToSql "eq" = "="
• PostgREST.Query.simpleOpToSql "neq" = "<>"
• PostgREST.Query.simpleOpToSql "gt" = ">"
• PostgREST.Query.simpleOpToSql "gte" = ">="
• PostgREST.Query.simpleOpToSql "lt" = "<"
• PostgREST.Query.simpleOpToSql "lte" = "<="
• PostgREST.Query.simpleOpToSql "like" = "LIKE"
• PostgREST.Query.simpleOpToSql "ilike" = "ILIKE"
• PostgREST.Query.simpleOpToSql "in" = "IN"
• PostgREST.Query.simpleOpToSql "is" = "IS"
• PostgREST.Query.simpleOpToSql "isdistinct" = "IS DISTINCT FROM"
• PostgREST.Query.simpleOpToSql "cs" = "@>"
• PostgREST.Query.simpleOpToSql "cd" = "<@"
• PostgREST.Query.simpleOpToSql "ov" = "&&"
• PostgREST.Query.simpleOpToSql "sl" = "<<"
• PostgREST.Query.simpleOpToSql "sr" = ">>"
• PostgREST.Query.simpleOpToSql "nxl" = "&<"
• PostgREST.Query.simpleOpToSql "nxr" = "&>"
• PostgREST.Query.simpleOpToSql "adj" = "-|-"
• PostgREST.Query.simpleOpToSql "match" = "~"
• PostgREST.Query.simpleOpToSql "imatch" = "~*"
• PostgREST.Query.simpleOpToSql x✝ = x✝

def PostgREST.Query.ftsOpToSql : String → String

Map a PostgREST full-text search operator to its SQL equivalent. All FTS variants use the @@ operator; the difference is in how the query term is constructed.

Equations

• PostgREST.Query.ftsOpToSql "fts" = "@@"
• PostgREST.Query.ftsOpToSql "plfts" = "@@"
• PostgREST.Query.ftsOpToSql "phfts" = "@@"
• PostgREST.Query.ftsOpToSql "wfts" = "@@"
• PostgREST.Query.ftsOpToSql x✝ = x✝

def PostgREST.Query.pgFmtFilter (f : Plan.CoercibleFilter) (table : Option SchemaCache.Identifiers.QualifiedIdentifier) : String

Format a filter expression as a SQL WHERE clause fragment. Uses $? as placeholder for parameterized values. $$\text{pgFmtFilter}(f, t?) = \text{field}\ \text{op}\ \$?$$

Equations

• One or more equations did not get rendered due to their size.

partial def PostgREST.Query.pgFmtLogicTree (lt : Plan.CoercibleLogicTree) (table : Option SchemaCache.Identifiers.QualifiedIdentifier) : String

Format a logic tree as a SQL boolean expression. $$\text{pgFmtLogicTree}(t, \text{tbl}?) = \begin{cases} \text{pgFmtFilter}(f, \text{tbl}?) & \text{if } t = \text{stmnt}(f) \\ [\lnot]\ (\text{child}_1\ \text{op}\ \text{child}_2\ \ldots) & \text{if } t = \text{expr}(\neg?, \text{op}, \text{children}) \end{cases}$$

def PostgREST.Query.pgFmtOrderTerm (t : Plan.CoercibleOrderTerm) (table : Option SchemaCache.Identifiers.QualifiedIdentifier) : String

Format an ORDER BY term as a SQL fragment. $$\text{pgFmtOrderTerm}(t, \text{tbl}?) = \text{field}\ \text{dir}\ [\text{NULLS FIRST|LAST}]$$

Equations

• One or more equations did not get rendered due to their size.

def PostgREST.Query.asJsonF (sql : String) : String

Wrap a SQL expression in json_agg with a coalesce fallback to '[]'. $$\text{asJsonF}(sql) = \texttt{coalesce(json\_agg(}sql\texttt{), '[]'::json)}$$

Equations

• PostgREST.Query.asJsonF sql = toString "coalesce(json_agg(" ++ toString sql ++ toString "), '[]'::json)"

def PostgREST.Query.asJsonSingleF (sql : String) : String

Wrap a SQL expression in json_agg and extract the first element, with a coalesce fallback to 'null'. $$\text{asJsonSingleF}(sql) = \texttt{coalesce((json\_agg(}sql\texttt{))->0, 'null'::json)}$$

Equations

• PostgREST.Query.asJsonSingleF sql = toString "coalesce((json_agg(" ++ toString sql ++ toString "))->0, 'null'::json)"

def PostgREST.Query.setConfigLocal (key value : String) : String

Generate a SET LOCAL statement for a GUC variable. The key is quoted as an identifier and the value as a literal. $$\text{setConfigLocal}(k, v) = \texttt{SET LOCAL}\ \text{pgFmtIdent}(k)\ \texttt{=}\ \text{pgFmtLit}(v)$$

Equations

• PostgREST.Query.setConfigLocal key value = toString "SET LOCAL " ++ toString (PostgREST.Query.pgFmtIdent key) ++ toString " = " ++ toString (PostgREST.Query.pgFmtLit value)

def PostgREST.Query.setConfigWithConstantName (key value : String) : String

Generate a SET LOCAL statement with a constant (unescaped) key name. Used for PostgREST internal settings where the key is a known constant. $$\text{setConfigWithConstantName}(k, v) = \texttt{SET LOCAL "}k\texttt{" =}\ \text{pgFmtLit}(v)$$

Equations

• PostgREST.Query.setConfigWithConstantName key value = toString "SET LOCAL \"" ++ toString key ++ toString "\" = " ++ toString (PostgREST.Query.pgFmtLit value)

def PostgREST.Query.pgFmtOrderClause (terms : Array Plan.CoercibleOrderTerm) (table : Option SchemaCache.Identifiers.QualifiedIdentifier) : Option String

Format an array of ORDER BY terms as a comma-separated SQL fragment. Returns none if the array is empty.

Equations

• One or more equations did not get rendered due to their size.

def PostgREST.Query.pgFmtWhereClause (filters : Array Plan.CoercibleFilter) (table : Option SchemaCache.Identifiers.QualifiedIdentifier) : Option String

Format an array of filters as an AND-connected WHERE clause fragment. Returns none if the array is empty.

Equations

• One or more equations did not get rendered due to their size.

theorem PostgREST.Query.pgFmtIdent_startsWith_dquote (s : String) : (pgFmtIdent s).startsWith "\"" = true

pgFmtIdent always produces a string starting with ". $$\forall s,\; \text{pgFmtIdent}(s).\text{startsWith}(\texttt{"}) = \text{true}$$

theorem PostgREST.Query.pgFmtLit_startsWith_squote (s : String) : (pgFmtLit s).startsWith "'" = true

pgFmtLit always produces a string starting with '. $$\forall s,\; \text{pgFmtLit}(s).\text{startsWith}(\texttt{'}) = \text{true}$$

theorem PostgREST.Query.pgFmtIdent_empty : pgFmtIdent "" = "\"\""

Quoting and then identity-quoting an empty string: pgFmtIdent "" = "\"\"". $$\text{pgFmtIdent}(\varepsilon) = \texttt{""}$$

theorem PostgREST.Query.pgFmtLit_empty : pgFmtLit "" = "''"

Quoting an empty literal yields '' (two single-quote characters). $$\text{pgFmtLit}(\varepsilon) = \texttt{''}$$