inductive PostgREST.SchemaCache.Volatility : Type

PostgreSQL function volatility classification. Determines cacheability and side effects.

• immutable : Volatility
• stable : Volatility
• volatile : Volatility

@[implicit_reducible]

instance PostgREST.SchemaCache.instBEqVolatility : BEq Volatility

Equations

• PostgREST.SchemaCache.instBEqVolatility = { beq := PostgREST.SchemaCache.instBEqVolatility.beq }

def PostgREST.SchemaCache.instBEqVolatility.beq : Volatility → Volatility → Bool

Equations

• PostgREST.SchemaCache.instBEqVolatility.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

def PostgREST.SchemaCache.instReprVolatility.repr : Volatility → Nat → Std.Format

Equations

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

@[implicit_reducible]

instance PostgREST.SchemaCache.instReprVolatility : Repr Volatility

Equations

• PostgREST.SchemaCache.instReprVolatility = { reprPrec := PostgREST.SchemaCache.instReprVolatility.repr }

@[implicit_reducible]

instance PostgREST.SchemaCache.instToStringVolatility : ToString Volatility

Equations

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

inductive PostgREST.SchemaCache.IsolationLevel : Type

Transaction isolation level for a routine.

• readCommitted : IsolationLevel
• repeatableRead : IsolationLevel
• serializable : IsolationLevel

def PostgREST.SchemaCache.instBEqIsolationLevel.beq : IsolationLevel → IsolationLevel → Bool

Equations

• PostgREST.SchemaCache.instBEqIsolationLevel.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

@[implicit_reducible]

instance PostgREST.SchemaCache.instBEqIsolationLevel : BEq IsolationLevel

Equations

• PostgREST.SchemaCache.instBEqIsolationLevel = { beq := PostgREST.SchemaCache.instBEqIsolationLevel.beq }

@[implicit_reducible]

instance PostgREST.SchemaCache.instReprIsolationLevel : Repr IsolationLevel

Equations

• PostgREST.SchemaCache.instReprIsolationLevel = { reprPrec := PostgREST.SchemaCache.instReprIsolationLevel.repr }

def PostgREST.SchemaCache.instReprIsolationLevel.repr : IsolationLevel → Nat → Std.Format

Equations

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

@[implicit_reducible]

instance PostgREST.SchemaCache.instToStringIsolationLevel : ToString IsolationLevel

Equations

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

inductive PostgREST.SchemaCache.ParamMode : Type

Parameter mode for a routine parameter.

• in_ : ParamMode
• out : ParamMode
• inout : ParamMode
• variadic : ParamMode

@[implicit_reducible]

instance PostgREST.SchemaCache.instBEqParamMode : BEq ParamMode

Equations

• PostgREST.SchemaCache.instBEqParamMode = { beq := PostgREST.SchemaCache.instBEqParamMode.beq }

def PostgREST.SchemaCache.instBEqParamMode.beq : ParamMode → ParamMode → Bool

Equations

• PostgREST.SchemaCache.instBEqParamMode.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

def PostgREST.SchemaCache.instReprParamMode.repr : ParamMode → Nat → Std.Format

Equations

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

@[implicit_reducible]

instance PostgREST.SchemaCache.instReprParamMode : Repr ParamMode

Equations

• PostgREST.SchemaCache.instReprParamMode = { reprPrec := PostgREST.SchemaCache.instReprParamMode.repr }

structure PostgREST.SchemaCache.RoutineParam : Type

A single parameter of a PostgreSQL function.

• ppName : String

  Parameter name (empty for unnamed positional parameters).

• ppType : String

  PostgreSQL type name.

• ppRequired : Bool

  Whether this parameter is required (has no default).

• ppMode : ParamMode

  Parameter mode.

def PostgREST.SchemaCache.instBEqRoutineParam.beq : RoutineParam → RoutineParam → Bool

Equations

• One or more equations did not get rendered due to their size.
• PostgREST.SchemaCache.instBEqRoutineParam.beq x✝¹ x✝ = false

@[implicit_reducible]

instance PostgREST.SchemaCache.instBEqRoutineParam : BEq RoutineParam

Equations

• PostgREST.SchemaCache.instBEqRoutineParam = { beq := PostgREST.SchemaCache.instBEqRoutineParam.beq }

def PostgREST.SchemaCache.instReprRoutineParam.repr : RoutineParam → Nat → Std.Format

Equations

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

@[implicit_reducible]

instance PostgREST.SchemaCache.instReprRoutineParam : Repr RoutineParam

Equations

• PostgREST.SchemaCache.instReprRoutineParam = { reprPrec := PostgREST.SchemaCache.instReprRoutineParam.repr }

inductive PostgREST.SchemaCache.RoutineReturnType : Type

Return type of a PostgreSQL function.

• single (typeName : String) : RoutineReturnType

  Returns a single value of the given type.

• setof (typeName : String) : RoutineReturnType

  Returns a set of rows (SETOF).

• void : RoutineReturnType

  Returns void (procedure or RETURNS VOID).

@[implicit_reducible]

instance PostgREST.SchemaCache.instBEqRoutineReturnType : BEq RoutineReturnType

Equations

• PostgREST.SchemaCache.instBEqRoutineReturnType = { beq := PostgREST.SchemaCache.instBEqRoutineReturnType.beq }

def PostgREST.SchemaCache.instBEqRoutineReturnType.beq : RoutineReturnType → RoutineReturnType → Bool

Equations

• PostgREST.SchemaCache.instBEqRoutineReturnType.beq (PostgREST.SchemaCache.RoutineReturnType.single a) (PostgREST.SchemaCache.RoutineReturnType.single b) = (a == b)
• PostgREST.SchemaCache.instBEqRoutineReturnType.beq (PostgREST.SchemaCache.RoutineReturnType.setof a) (PostgREST.SchemaCache.RoutineReturnType.setof b) = (a == b)
• PostgREST.SchemaCache.instBEqRoutineReturnType.beq PostgREST.SchemaCache.RoutineReturnType.void PostgREST.SchemaCache.RoutineReturnType.void = true
• PostgREST.SchemaCache.instBEqRoutineReturnType.beq x✝¹ x✝ = false

def PostgREST.SchemaCache.instReprRoutineReturnType.repr : RoutineReturnType → Nat → Std.Format

Equations

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

@[implicit_reducible]

instance PostgREST.SchemaCache.instReprRoutineReturnType : Repr RoutineReturnType

Equations

• PostgREST.SchemaCache.instReprRoutineReturnType = { reprPrec := PostgREST.SchemaCache.instReprRoutineReturnType.repr }

def PostgREST.SchemaCache.RoutineReturnType.isSetof : RoutineReturnType → Bool

Does this return type produce multiple rows?

Equations

• (PostgREST.SchemaCache.RoutineReturnType.setof typeName).isSetof = true
• x✝.isSetof = false

structure PostgREST.SchemaCache.Routine : Type

A PostgreSQL function or procedure. $$\text{Routine} = \{ \text{schema}, \text{name}, \text{params}, \text{returnType}, \text{volatility} \}$$

• funcSchema : Identifiers.Schema

  Function schema.

• funcName : Identifiers.FunctionName

  Function name.

• funcDescription : Option String

  Human-readable description.

• funcParams : Array RoutineParam

  Function parameters.

• funcReturnType : RoutineReturnType

  Return type.

• funcVolatility : Volatility

  Volatility classification.

• funcIsoLevel : Option IsolationLevel

  Transaction isolation level (if specified).

• funcReturnsComposite : Bool

  Whether the function returns a composite type (TABLE / record).

• funcReturnTypeOid : Option Nat

  The OID of the return type (for composite type column discovery).

@[implicit_reducible]

instance PostgREST.SchemaCache.instReprRoutine : Repr Routine

Equations

• PostgREST.SchemaCache.instReprRoutine = { reprPrec := PostgREST.SchemaCache.instReprRoutine.repr }

def PostgREST.SchemaCache.instReprRoutine.repr : Routine → Nat → Std.Format

Equations

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

def PostgREST.SchemaCache.Routine.toQi (r : Routine) : Identifiers.QualifiedIdentifier

Get the qualified identifier for a routine.

Equations

• r.toQi = { qiSchema := r.funcSchema, qiName := r.funcName }

def PostgREST.SchemaCache.Routine.requiredParams (r : Routine) : Array String

Get the required parameter names.

Equations

• r.requiredParams = Array.map (fun (x : PostgREST.SchemaCache.RoutineParam) => x.ppName) (Array.filter (fun (x : PostgREST.SchemaCache.RoutineParam) => x.ppRequired) r.funcParams)

def PostgREST.SchemaCache.Routine.isSafeForGet (r : Routine) : Bool

Whether this routine can be called with a GET request (only immutable/stable functions).

Equations

• r.isSafeForGet = (r.funcVolatility != PostgREST.SchemaCache.Volatility.volatile)

@[implicit_reducible]

instance PostgREST.SchemaCache.instToStringRoutine : ToString Routine

Equations

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

theorem PostgREST.SchemaCache.Routine.isSafeForGet_iff_not_volatile (r : Routine) : r.isSafeForGet = true ↔ r.funcVolatility ≠ Volatility.volatile

isSafeForGet is true if and only if the volatility is not .volatile. $$\text{isSafeForGet}(r) = \text{true} \iff r.\text{funcVolatility} \neq \text{volatile}$$ This witnesses that only immutable and stable functions are safe for GET.