Native bindings

Thin @[extern] declarations over ffi/typedb_lean.c. Every function returns the driver's error as a NativeError in the same call, because the driver keeps its last error in thread-local state. Handles are external objects: dropping the last reference releases them, and the explicit close functions release them early.

This module is internal; TypeDB.Driver, TypeDB.Tx and TypeDB.Query wrap it.

structure TypeDB.Native.NativeError : Type

An error reported by the driver: its code (CXN05, TQL03, …) and message. Codes starting with TDBLEAN come from the shim itself.

• code : String
• message : String

@[instance_reducible]

instance TypeDB.Native.instReprNativeError : Repr NativeError

Equations

• TypeDB.Native.instReprNativeError = { reprPrec := TypeDB.Native.instReprNativeError.repr }

def TypeDB.Native.instReprNativeError.repr : NativeError → Nat → Std.Format

Equations

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

@[instance_reducible]

instance TypeDB.Native.instInhabitedNativeError : Inhabited NativeError

Equations

• TypeDB.Native.instInhabitedNativeError = { default := TypeDB.Native.instInhabitedNativeError.default }

opaque TypeDB.Native.DriverPointed : NonemptyType

def TypeDB.Native.DriverHandle : Type u_1

An open driver connection.

Equations

• TypeDB.Native.DriverHandle = TypeDB.Native.DriverPointed.type

instance TypeDB.Native.instNonemptyDriverHandle : Nonempty DriverHandle

opaque TypeDB.Native.TxPointed : NonemptyType

def TypeDB.Native.TxHandle : Type u_1

An open transaction, with the query options it runs queries with.

Equations

• TypeDB.Native.TxHandle = TypeDB.Native.TxPointed.type

instance TypeDB.Native.instNonemptyTxHandle : Nonempty TxHandle

opaque TypeDB.Native.RowsPointed : NonemptyType

def TypeDB.Native.RowsHandle : Type u_1

A stream of concept rows; valid only while its transaction is open.

Equations

• TypeDB.Native.RowsHandle = TypeDB.Native.RowsPointed.type

instance TypeDB.Native.instNonemptyRowsHandle : Nonempty RowsHandle

opaque TypeDB.Native.RowPointed : NonemptyType

def TypeDB.Native.RowHandle : Type u_1

Equations

• TypeDB.Native.RowHandle = TypeDB.Native.RowPointed.type

instance TypeDB.Native.instNonemptyRowHandle : Nonempty RowHandle

opaque TypeDB.Native.DocsPointed : NonemptyType

def TypeDB.Native.DocsHandle : Type u_1

A stream of JSON documents from a fetch; valid only while its transaction is open.

Equations

• TypeDB.Native.DocsHandle = TypeDB.Native.DocsPointed.type

instance TypeDB.Native.instNonemptyDocsHandle : Nonempty DocsHandle

inductive TypeDB.Native.RawAnswer : Type

What a query answered. Constructor order is mirrored by the shim.

• ok : RawAnswer
• rows (it : RowsHandle) : RawAnswer
• docs (it : DocsHandle) : RawAnswer

instance TypeDB.Native.instNonemptyRawAnswer : Nonempty RawAnswer

@[reducible, inline]

abbrev TypeDB.Native.NIO (α : Type) : Type

Equations

• TypeDB.Native.NIO = EIO TypeDB.Native.NativeError

@[extern tdb_driver_open]

opaque TypeDB.Native.driverOpen (address user password : String) (tls : Bool) (rootCA : String) (timeoutMs : Int64) : NIO DriverHandle

Opens a connection. An empty rootCA with tls uses the system's root certificates. A timeoutMs of 0 keeps the driver's default request timeout.

@[extern tdb_driver_close]

opaque TypeDB.Native.driverClose (d : DriverHandle) : NIO Unit

@[extern tdb_driver_is_open]

opaque TypeDB.Native.driverIsOpen (d : DriverHandle) : NIO Bool

@[extern tdb_db_create]

opaque TypeDB.Native.dbCreate (d : DriverHandle) (name : String) : NIO Unit

@[extern tdb_db_contains]

opaque TypeDB.Native.dbContains (d : DriverHandle) (name : String) : NIO Bool

@[extern tdb_db_delete]

opaque TypeDB.Native.dbDelete (d : DriverHandle) (name : String) : NIO Unit

@[extern tdb_db_schema]

opaque TypeDB.Native.dbSchema (d : DriverHandle) (name : String) (kind : UInt8) : NIO String

kind 0 is the full schema, 1 the type schema only.

@[extern tdb_db_all]

opaque TypeDB.Native.dbAll (d : DriverHandle) : NIO (Array String)

@[extern tdb_tx_open]

opaque TypeDB.Native.txOpen (d : DriverHandle) (db : String) (type : UInt8) (timeoutMs prefetch : Int64) : NIO TxHandle

type is 0 read, 1 write, 2 schema; a timeoutMs or prefetch of 0 keeps the default.

@[extern tdb_tx_commit]

opaque TypeDB.Native.txCommit (t : TxHandle) : NIO Unit

Commits and releases the transaction, whatever the outcome.

@[extern tdb_tx_rollback]

opaque TypeDB.Native.txRollback (t : TxHandle) : NIO Unit

@[extern tdb_tx_close]

opaque TypeDB.Native.txClose (t : TxHandle) : NIO Unit

Closes the transaction without committing and releases it, without waiting for the driver to finish closing it (like the Rust driver's drop). Idempotent.

@[extern tdb_wait_closes]

opaque TypeDB.Native.waitCloses : NIO Unit

Waits until every transaction closed so far has finished closing.

@[extern tdb_tx_is_open]

opaque TypeDB.Native.txIsOpen (t : TxHandle) : NIO Bool

@[extern tdb_tx_query]

opaque TypeDB.Native.txQuery (t : TxHandle) (query : String) : NIO RawAnswer

@[extern tdb_rows_next]

opaque TypeDB.Native.rowsNext (it : RowsHandle) : NIO (Option RowHandle)

@[extern tdb_rows_close]

opaque TypeDB.Native.rowsClose (it : RowsHandle) : NIO Unit

@[extern tdb_row_columns]

opaque TypeDB.Native.rowColumns (r : RowHandle) : NIO (Array String)

@[extern tdb_row_get]

opaque TypeDB.Native.rowGet (r : RowHandle) (col : String) (flags : UInt8) : NIO (Option Concept)

The concept in column col, or none if the row leaves it empty.

@[extern tdb_rows_next_batch]

opaque TypeDB.Native.rowsNextBatch (it : RowsHandle) (cols : Array String) (flags : ByteArray) (k : USize) : NIO (Array (Array (Option Concept)))

Pulls up to k rows and returns the concepts of cols in each, in one native call. A result shorter than k means the stream is exhausted (and already released).

@[extern tdb_docs_next]

opaque TypeDB.Native.docsNext (it : DocsHandle) : NIO (Option String)

@[extern tdb_docs_close]

opaque TypeDB.Native.docsClose (it : DocsHandle) : NIO Unit

def TypeDB.Native.wantLabel : UInt8

Column flags: read the concept's type label.

Equations

• TypeDB.Native.wantLabel = 1

def TypeDB.Native.wantIID : UInt8

Column flags: read the instance's IID.

Equations

• TypeDB.Native.wantIID = 2