inductive TypeDB.SchemaIssue : Type

One difference between a Lean mapping and the live schema, found by verifySchema.

• missingType (label : String) : SchemaIssue
• wrongKind (label expected actual : String) : SchemaIssue
• wrongSupertype (label expected : String) (actual : Option String) : SchemaIssue
• missingOwns (owner attr : String) : SchemaIssue
• wrongValueType (attr expected actual : String) : SchemaIssue
• missingRelates (relation role : String) : SchemaIssue
• missingPlays (player role : String) : SchemaIssue

@[instance_reducible]

instance TypeDB.instReprSchemaIssue : Repr SchemaIssue

Equations

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

def TypeDB.instReprSchemaIssue.repr : SchemaIssue → Nat → Std.Format

Equations

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

@[instance_reducible]

instance TypeDB.instBEqSchemaIssue : BEq SchemaIssue

Equations

• TypeDB.instBEqSchemaIssue = { beq := TypeDB.instBEqSchemaIssue.beq }

def TypeDB.instBEqSchemaIssue.beq : SchemaIssue → SchemaIssue → Bool

Equations

• TypeDB.instBEqSchemaIssue.beq (TypeDB.SchemaIssue.missingType a) (TypeDB.SchemaIssue.missingType b) = (a == b)
• TypeDB.instBEqSchemaIssue.beq (TypeDB.SchemaIssue.wrongKind a a_1 a_2) (TypeDB.SchemaIssue.wrongKind b b_1 b_2) = (a == b && (a_1 == b_1 && a_2 == b_2))
• TypeDB.instBEqSchemaIssue.beq (TypeDB.SchemaIssue.wrongSupertype a a_1 a_2) (TypeDB.SchemaIssue.wrongSupertype b b_1 b_2) = (a == b && (a_1 == b_1 && a_2 == b_2))
• TypeDB.instBEqSchemaIssue.beq (TypeDB.SchemaIssue.missingOwns a a_1) (TypeDB.SchemaIssue.missingOwns b b_1) = (a == b && a_1 == b_1)
• TypeDB.instBEqSchemaIssue.beq (TypeDB.SchemaIssue.wrongValueType a a_1 a_2) (TypeDB.SchemaIssue.wrongValueType b b_1 b_2) = (a == b && (a_1 == b_1 && a_2 == b_2))
• TypeDB.instBEqSchemaIssue.beq (TypeDB.SchemaIssue.missingRelates a a_1) (TypeDB.SchemaIssue.missingRelates b b_1) = (a == b && a_1 == b_1)
• TypeDB.instBEqSchemaIssue.beq (TypeDB.SchemaIssue.missingPlays a a_1) (TypeDB.SchemaIssue.missingPlays b b_1) = (a == b && a_1 == b_1)
• TypeDB.instBEqSchemaIssue.beq x✝¹ x✝ = false

@[instance_reducible]

instance TypeDB.instInhabitedSchemaIssue : Inhabited SchemaIssue

Equations

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

@[instance_reducible]

instance TypeDB.instToStringSchemaIssue : ToString SchemaIssue

Equations

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

inductive TypeDB.TypeDBError : Type

Everything that can go wrong talking to TypeDB.

• connection (code message : String) : TypeDBError

  The server could not be reached, or refused the connection or credentials.

• server (code message : String) : TypeDBError

  The server rejected a request; code is TypeDB's error code, e.g. TQL03.

• conflict (message : String) : TypeDBError

  A commit lost against a concurrent transaction; retrying may succeed.

• decode (column expected got : String) : TypeDBError

  A column or document did not have the shape the decoder expects.

• schemaMismatch (issues : List SchemaIssue) : TypeDBError

  The live schema differs from the Lean mappings.

• migration (version : Nat) (message : String) : TypeDBError

  A migration could not run; version names the step.

• io (message : String) : TypeDBError

  An IO error raised inside a transaction body.

• internal (message : String) : TypeDBError

  A misuse of the library or a driver failure with no TypeDB code.

def TypeDB.instReprTypeDBError.repr : TypeDBError → Nat → Std.Format

Equations

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

@[instance_reducible]

instance TypeDB.instReprTypeDBError : Repr TypeDBError

Equations

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

@[instance_reducible]

instance TypeDB.instInhabitedTypeDBError : Inhabited TypeDBError

Equations

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

def TypeDB.TypeDBError.isConflict : TypeDBError → Bool

Equations

• (TypeDB.TypeDBError.conflict message).isConflict = true
• x✝.isConflict = false

def TypeDB.TypeDBError.ofNative (e : Native.NativeError) : TypeDBError

Classifies a driver error. Commit conflicts are storage errors STC2 ("isolation conflict"), which the server may wrap in another error, so the whole message is searched.

Equations

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

def TypeDB.TypeDBError.toString : TypeDBError → String

Equations

• (TypeDB.TypeDBError.connection a a_1).toString = toString "connection error [" ++ toString a ++ toString "]: " ++ toString a_1
• (TypeDB.TypeDBError.server a a_1).toString = toString "server error [" ++ toString a ++ toString "]: " ++ toString a_1
• (TypeDB.TypeDBError.conflict a).toString = toString "commit conflict: " ++ toString a
• (TypeDB.TypeDBError.decode a a_1 a_2).toString = toString "cannot decode column '" ++ toString a ++ toString "': expected " ++ toString a_1 ++ toString ", got " ++ toString a_2
• (TypeDB.TypeDBError.schemaMismatch a).toString = "schema mismatch:\n" ++ "\n".intercalate (List.map (fun (x : TypeDB.SchemaIssue) => toString " - " ++ toString x) a)
• (TypeDB.TypeDBError.migration a a_1).toString = toString "migration " ++ toString a ++ toString ": " ++ toString a_1
• (TypeDB.TypeDBError.io a).toString = toString "IO error: " ++ toString a
• (TypeDB.TypeDBError.internal a).toString = toString "internal error: " ++ toString a

@[instance_reducible]

instance TypeDB.TypeDBError.instToString : ToString TypeDBError

Equations

• TypeDB.TypeDBError.instToString = { toString := TypeDB.TypeDBError.toString }

@[inline]

def TypeDB.mapError {ε ε' α : Type} (f : ε → ε') (x : EIO ε α) : EIO ε' α

Maps the error of an EIO action.

Equations

• TypeDB.mapError f x = do let __do_lift ← liftM x.toBaseIO match __do_lift with | Except.ok a => pure a | Except.error e => throw (f e)

@[instance_reducible]

instance TypeDB.instMonadLiftIOEIOTypeDBError : MonadLift IO (EIO TypeDBError)

IO actions run inside TypeDB code report their errors as TypeDBError.io.

Equations

• TypeDB.instMonadLiftIOEIOTypeDBError = { monadLift := fun {α : Type} (x : IO α) => IO.toEIO (fun (e : IO.Error) => TypeDB.TypeDBError.io (toString e)) x }

@[inline]

def TypeDB.native {α : Type} (x : Native.NIO α) : EIO TypeDBError α

Runs a native call, classifying its error.

Equations

• TypeDB.native x = TypeDB.mapError TypeDB.TypeDBError.ofNative x