Running queries

All functions run inside a transaction body and need [Allows m need]: the transaction's mode m must be at least the query's need.

• exec runs a query for its effect.
• query decodes every row into an Array; query1? and queryOne take the first row.
• queryFold, queryFoldM and for x in stream q do … decode rows one batch at a time, in memory that does not grow with the answer. Result streams never leave the transaction: they are released when the loop ends, breaks or throws.
• fetch decodes the JSON documents of a fetch query with Lean.FromJson.

opaque TypeDB.zoneRules : IO.Ref (Std.HashMap String Std.Time.TimeZone.ZoneRules)

UTC offsets of IANA zones need the zone's rules; they are loaded once per zone.

def TypeDB.Tx.answer {m need : TxMode} [m.Allows need] (q : Query need) : Tx m Native.RawAnswer

The raw answer of a query. Prefer the decoding functions.

Equations

• TypeDB.Tx.answer q = do let __do_lift ← TypeDB.Tx.ctx TypeDB.Tx.native (TypeDB.Native.txQuery __do_lift.handle q.text)

def TypeDB.Tx.foldRowsM {m need : TxMode} {α β : Type} [m.Allows need] (d : RowDecoder α) (q : Query need) (init : β) (f : β → α → Tx m (ForInStep β)) : Tx m β

Folds f over the decoded rows, one native batch at a time. f returns none to stop.

Equations

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

def TypeDB.Tx.exec {m need : TxMode} [m.Allows need] (q : Query need) : Tx m Unit

Runs a query for its effect, draining any rows it answers.

Equations

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

def TypeDB.Tx.queryWith {m need : TxMode} {α : Type} [m.Allows need] (d : RowDecoder α) (q : Query need) : Tx m (Array α)

Every row, decoded with d, in answer order.

Equations

• TypeDB.queryWith d q = TypeDB.Tx.foldRowsM d q #[] fun (acc : Array α) (a : α) => pure (ForInStep.yield (acc.push a))

def TypeDB.Tx.query {m need : TxMode} {α : Type} [m.Allows need] [FromRow α] (q : Query need) : Tx m (Array α)

Every row, decoded with FromRow α, in answer order.

Equations

• TypeDB.query q = TypeDB.queryWith TypeDB.FromRow.decoder q

def TypeDB.Tx.query1? {m need : TxMode} {α : Type} [m.Allows need] [FromRow α] (q : Query need) : Tx m (Option α)

The first row, if any.

Equations

• TypeDB.query1? q = TypeDB.Tx.foldRowsM TypeDB.FromRow.decoder q none fun (x : Option α) (a : α) => pure (ForInStep.done (some a))

def TypeDB.Tx.queryOne {m need : TxMode} {α : Type} [m.Allows need] [FromRow α] (q : Query need) : Tx m α

The first row; fails if the answer is empty.

Equations

• TypeDB.queryOne q = do let __do_lift ← TypeDB.query1? q match __do_lift with | some a => pure a | none => TypeDB.Tx.fail (TypeDB.TypeDBError.decode "" "at least one row" "no rows")

def TypeDB.Tx.queryFold {m need : TxMode} {α β : Type} [m.Allows need] [FromRow α] (q : Query need) (init : β) (f : β → α → β) : Tx m β

Folds over the rows in constant memory.

Equations

• TypeDB.queryFold q init f = TypeDB.Tx.foldRowsM TypeDB.FromRow.decoder q init fun (b : β) (a : α) => pure (ForInStep.yield (f b a))

def TypeDB.Tx.queryFoldM {m need : TxMode} {α β : Type} [m.Allows need] [FromRow α] (q : Query need) (init : β) (f : β → α → Tx m β) : Tx m β

Equations

• TypeDB.queryFoldM q init f = TypeDB.Tx.foldRowsM TypeDB.FromRow.decoder q init fun (b : β) (a : α) => do let __do_lift ← f b a pure (ForInStep.yield __do_lift)

def TypeDB.Tx.queryPerValue {m need : TxMode} {α : Type} [m.Allows need] (d : RowDecoder α) (q : Query need) : Tx m (Array α)

Rows decoded one native call per value (the unbatched path), for comparison with query.

Equations

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

def TypeDB.Tx.fetchJson {m need : TxMode} [m.Allows need] (q : Query need) : Tx m (Array Lean.Json)

The JSON documents of a fetch query.

Equations

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

def TypeDB.Tx.fetch {m need : TxMode} {α : Type} [m.Allows need] [Lean.FromJson α] (q : Query need) : Tx m (Array α)

The documents of a fetch query, decoded with FromJson.

Equations

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

structure TypeDB.Tx.RowStream (need : TxMode) (α : Type) : Type

A query whose rows are decoded lazily by a for loop inside the transaction.

• query : Query need
• decoder : RowDecoder α

def TypeDB.Tx.stream {need : TxMode} {α : Type} [FromRow α] (q : Query need) : RowStream need α

Equations

• TypeDB.stream q = { query := q, decoder := TypeDB.FromRow.decoder }

def TypeDB.Tx.streamWith {need : TxMode} {α : Type} (d : RowDecoder α) (q : Query need) : RowStream need α

Equations

• TypeDB.streamWith d q = { query := q, decoder := d }

@[instance_reducible]

instance TypeDB.Tx.instForInRowStreamOfAllows {m need : TxMode} {α : Type} [m.Allows need] : ForIn (Tx m) (RowStream need α) α

Equations

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