Connecting and managing databases

Driver.connect opens one connection, which every transaction shares. The driver multiplexes concurrent transactions over it, so there is no pool.

inductive TypeDB.Tls : Type

TLS settings for a connection.

• disabled : Tls
• system : Tls

  TLS with the operating system's root certificates.

• rootCA (path : System.FilePath) : Tls

  TLS with a custom root CA certificate (PEM file).

@[instance_reducible]

instance TypeDB.instReprTls : Repr Tls

Equations

• TypeDB.instReprTls = { reprPrec := TypeDB.instReprTls.repr }

def TypeDB.instReprTls.repr : Tls → Nat → Std.Format

Equations

• One or more equations did not get rendered due to their size.
• TypeDB.instReprTls.repr TypeDB.Tls.disabled prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "TypeDB.Tls.disabled")).group prec✝
• TypeDB.instReprTls.repr TypeDB.Tls.system prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "TypeDB.Tls.system")).group prec✝

@[instance_reducible]

instance TypeDB.instInhabitedTls : Inhabited Tls

Equations

• TypeDB.instInhabitedTls = { default := TypeDB.instInhabitedTls.default }

structure TypeDB.Config : Type

How to reach and authenticate with a server.

• address : String
• username : String
• password : String
• tls : Tls
• requestTimeoutMs : Nat

  Request timeout in milliseconds; 0 keeps the driver's default.

@[instance_reducible]

instance TypeDB.instReprConfig : Repr Config

Equations

• TypeDB.instReprConfig = { reprPrec := TypeDB.instReprConfig.repr }

def TypeDB.instReprConfig.repr : Config → Nat → Std.Format

Equations

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

@[instance_reducible]

instance TypeDB.instInhabitedConfig : Inhabited Config

Equations

• TypeDB.instInhabitedConfig = { default := TypeDB.instInhabitedConfig.default }

structure TypeDB.TxOptions : Type

Options applied to every transaction a run opens.

• timeoutMs : Nat

  Transaction timeout in milliseconds; 0 keeps the server's default.

• prefetch : Nat

  How many answers the server sends ahead of the client's reads; 0 keeps the server's default, which is small enough to make large scans wait on the network.

• batchSize : Nat

  How many rows one native call decodes.

@[instance_reducible]

instance TypeDB.instReprTxOptions : Repr TxOptions

Equations

• TypeDB.instReprTxOptions = { reprPrec := TypeDB.instReprTxOptions.repr }

def TypeDB.instReprTxOptions.repr : TxOptions → Nat → Std.Format

Equations

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

@[instance_reducible]

instance TypeDB.instInhabitedTxOptions : Inhabited TxOptions

Equations

• TypeDB.instInhabitedTxOptions = { default := TypeDB.instInhabitedTxOptions.default }

structure TypeDB.Driver : Type

An open connection to a TypeDB server. Safe to share between threads.

• handle : Native.DriverHandle
• config : Config

def TypeDB.Driver.connect (config : Config := { }) : EIO TypeDBError Driver

Connects to a server. Fails with TypeDBError.connection if the server is unreachable or refuses the credentials.

Equations

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

def TypeDB.Driver.close (d : Driver) : EIO TypeDBError Unit

Closes the connection. Later calls on this driver fail.

Equations

• d.close = TypeDB.native (TypeDB.Native.driverClose d.handle)

def TypeDB.Driver.isOpen (d : Driver) : EIO TypeDBError Bool

Equations

• d.isOpen = TypeDB.native (TypeDB.Native.driverIsOpen d.handle)

def TypeDB.Driver.withDriver {α : Type} (config : Config) (f : Driver → EIO TypeDBError α) : EIO TypeDBError α

Connects, runs f, and closes the connection whatever f does.

Equations

• TypeDB.Driver.withDriver config f = do let d ← TypeDB.Driver.connect config tryFinally (f d) (discard (liftM d.close.toBaseIO))

Databases

def TypeDB.Driver.createDatabase (d : Driver) (name : String) : EIO TypeDBError Unit

Creates a database; fails if one with that name exists.

Equations

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

def TypeDB.Driver.databaseExists (d : Driver) (name : String) : EIO TypeDBError Bool

Equations

• d.databaseExists name = TypeDB.native (TypeDB.Native.dbContains d.handle name)

def TypeDB.Driver.deleteDatabase (d : Driver) (name : String) : EIO TypeDBError Unit

Equations

• d.deleteDatabase name = TypeDB.native (TypeDB.Native.dbDelete d.handle name)

def TypeDB.Driver.databases (d : Driver) : EIO TypeDBError (Array String)

Equations

• d.databases = TypeDB.native (TypeDB.Native.dbAll d.handle)

def TypeDB.Driver.schema (d : Driver) (name : String) : EIO TypeDBError String

The database's schema and functions as TypeQL define text.

Equations

• d.schema name = TypeDB.native (TypeDB.Native.dbSchema d.handle name 0)

def TypeDB.Driver.typeSchema (d : Driver) (name : String) : EIO TypeDBError String

The database's types only, without functions.

Equations

• d.typeSchema name = TypeDB.native (TypeDB.Native.dbSchema d.handle name 1)

def TypeDB.Driver.ensureDatabase (d : Driver) (name : String) : EIO TypeDBError Unit

Creates the database unless it exists.

Equations

• d.ensureDatabase name = do let __do_lift ← d.databaseExists name if __do_lift = true then pure () else d.createDatabase name