structure PostgREST.Plan.NonnegRange : Type

A non-negative pagination range. $$\text{NonnegRange} = \{ \text{offset} : \mathbb{N},\; \text{limit} : \mathbb{N}? \}$$ Both offset and limit are guaranteed non-negative by using Nat.

• rangeOffset : Nat
• rangeLimit : Option Nat

@[implicit_reducible]

instance PostgREST.Plan.instBEqNonnegRange : BEq NonnegRange

Equations

• PostgREST.Plan.instBEqNonnegRange = { beq := PostgREST.Plan.instBEqNonnegRange.beq }

def PostgREST.Plan.instBEqNonnegRange.beq : NonnegRange → NonnegRange → Bool

Equations

• PostgREST.Plan.instBEqNonnegRange.beq { rangeOffset := a, rangeLimit := a_1 } { rangeOffset := b, rangeLimit := b_1 } = (a == b && a_1 == b_1)
• PostgREST.Plan.instBEqNonnegRange.beq x✝¹ x✝ = false

def PostgREST.Plan.instReprNonnegRange.repr : NonnegRange → Nat → Std.Format

Equations

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

@[implicit_reducible]

instance PostgREST.Plan.instReprNonnegRange : Repr NonnegRange

Equations

• PostgREST.Plan.instReprNonnegRange = { reprPrec := PostgREST.Plan.instReprNonnegRange.repr }

@[implicit_reducible]

instance PostgREST.Plan.instInhabitedNonnegRange : Inhabited NonnegRange

Equations

• PostgREST.Plan.instInhabitedNonnegRange = { default := PostgREST.Plan.instInhabitedNonnegRange.default }

def PostgREST.Plan.instInhabitedNonnegRange.default : NonnegRange

Equations

• PostgREST.Plan.instInhabitedNonnegRange.default = { rangeOffset := default, rangeLimit := default }

def PostgREST.Plan.NonnegRange.maxRows (r : NonnegRange) : Option Nat

The total number of rows this range can produce (if limit is known).

Equations

• r.maxRows = r.rangeLimit

def PostgREST.Plan.NonnegRange.isUnbounded (r : NonnegRange) : Bool

Whether this range is unbounded (no limit).

Equations

• r.isUnbounded = r.rangeLimit.isNone

def PostgREST.Plan.NonnegRange.allRows : NonnegRange

The default range: offset 0, no limit.

Equations

• PostgREST.Plan.NonnegRange.allRows = { }

structure PostgREST.Plan.ReadPlan : Type

A read plan represents a SELECT query with possible embedded sub-queries. $$\text{ReadPlan} = \{ \text{select} : [\text{SelectField}],\; \text{from} : \text{QI},\; \text{where} : [\text{Filter}],\; \text{order} : [\text{OrderTerm}],\; \text{range} : \text{NonnegRange},\; \text{embeds} : [(\text{Rel}, \text{ReadPlan})],\; \text{isInner} : \text{Bool} \}$$

• rpSelect: columns and expressions to select
• rpFrom: the source table or view
• rpWhere: filter conditions
• rpOrder: ordering specification
• rpRange: pagination (offset/limit)
• rpRelationships: embedded reads via lateral joins
• rpIsInner: whether the embed uses INNER (true) or LEFT (false) join
• rpAlias: optional alias for this read in the query

• rpSelect : Array CoercibleSelectField
• rpFrom : SchemaCache.Identifiers.QualifiedIdentifier
• rpWhere : Array CoercibleFilter
• rpOrder : Array CoercibleOrderTerm
• rpRange : NonnegRange
• rpRelationships : Array (SchemaCache.Relationship × ReadPlan)
• rpIsInner : Bool
• rpAlias : Option String

@[implicit_reducible]

instance PostgREST.Plan.instReprReadPlan : Repr ReadPlan

Equations

• PostgREST.Plan.instReprReadPlan = { reprPrec := PostgREST.Plan.instReprReadPlan.repr }

partial def PostgREST.Plan.instReprReadPlan.repr : ReadPlan → Nat → Std.Format

def PostgREST.Plan.ReadPlan.hasEmbeds (rp : ReadPlan) : Bool

Whether this read plan has any embedded sub-queries.

Equations

• rp.hasEmbeds = !rp.rpRelationships.isEmpty

def PostgREST.Plan.ReadPlan.embedCount (rp : ReadPlan) : Nat

The number of embedded sub-queries.

Equations

• rp.embedCount = rp.rpRelationships.size

def PostgREST.Plan.ReadPlan.hasFilters (rp : ReadPlan) : Bool

Whether this read plan applies any filters.

Equations

• rp.hasFilters = !rp.rpWhere.isEmpty

def PostgREST.Plan.ReadPlan.hasOrdering (rp : ReadPlan) : Bool

Whether this read plan specifies an ordering.

Equations

• rp.hasOrdering = !rp.rpOrder.isEmpty