Decoding answers

A RowDecoder α reads named columns of a concept row and builds an α. Decoders compose as an applicative, and every decoder knows up front which columns it reads and which parts of each concept it needs (its plan). The query layer hands the plan to the native batch call, which returns exactly those concepts for many rows at once.

FromConcept says how one column becomes a Lean value. deriving FromRow (see TypeDB.Deriving.FromRow) maps each structure field to the query variable of the same name.

def TypeDB.wantZone : UInt8

Column flag, Lean side only: resolve the UTC offset of IANA-zoned datetimes.

Equations

• TypeDB.wantZone = 4

class TypeDB.FromConcept (α : Type) : Type

How one column of a row becomes a Lean value.

• expected : String

  The expected shape, for decode errors ("string", "entity", …).

• flags : UInt8

  Which parts of the concept the native layer must read (see Native.wantLabel).

• decode : Concept → Except String α

  The value, or a description of what the concept is instead.

@[instance_reducible]

def TypeDB.FromConcept.ofValue {α : Type} (expected : String) (f : Value → Option α) (flags : UInt8 := 0) : FromConcept α

Decodes the value of an attribute or value concept with f.

Equations

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

@[instance_reducible]

instance TypeDB.instFromConceptString : FromConcept String

Equations

• TypeDB.instFromConceptString = TypeDB.FromConcept.ofValue "string" fun (x : TypeDB.Value) => match x with | TypeDB.Value.string s => some s | x => none

@[instance_reducible]

instance TypeDB.instFromConceptBool : FromConcept Bool

Equations

• TypeDB.instFromConceptBool = TypeDB.FromConcept.ofValue "boolean" fun (x : TypeDB.Value) => match x with | TypeDB.Value.bool b => some b | x => none

@[instance_reducible]

instance TypeDB.instFromConceptInt64 : FromConcept Int64

Equations

• TypeDB.instFromConceptInt64 = TypeDB.FromConcept.ofValue "integer" fun (x : TypeDB.Value) => match x with | TypeDB.Value.integer i => some i | x => none

@[instance_reducible]

instance TypeDB.instFromConceptInt : FromConcept Int

Equations

• TypeDB.instFromConceptInt = TypeDB.FromConcept.ofValue "integer" fun (x : TypeDB.Value) => match x with | TypeDB.Value.integer i => some i.toInt | x => none

@[instance_reducible]

instance TypeDB.instFromConceptNat : FromConcept Nat

Rejects negative integers.

Equations

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

@[instance_reducible]

instance TypeDB.instFromConceptFloat : FromConcept Float

Equations

• TypeDB.instFromConceptFloat = TypeDB.FromConcept.ofValue "double" fun (x : TypeDB.Value) => match x with | TypeDB.Value.double d => some d | x => none

@[instance_reducible]

instance TypeDB.instFromConceptDecimal : FromConcept Decimal

Equations

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

@[instance_reducible]

instance TypeDB.instFromConceptDuration : FromConcept Duration

Equations

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

@[instance_reducible]

instance TypeDB.instFromConceptPlainDate : FromConcept Std.Time.PlainDate

Equations

• TypeDB.instFromConceptPlainDate = TypeDB.FromConcept.ofValue "date" fun (x : TypeDB.Value) => match x with | TypeDB.Value.date s => some (TypeDB.Time.plainDateOfSeconds s) | x => none

@[instance_reducible]

instance TypeDB.instFromConceptPlainDateTime : FromConcept Std.Time.PlainDateTime

Equations

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

@[instance_reducible]

instance TypeDB.instFromConceptDatetimeTZ : FromConcept DatetimeTZ

Equations

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

@[instance_reducible]

instance TypeDB.instFromConceptDateTime : FromConcept Std.Time.DateTime

A Std.Time.DateTime at the value's offset; see DatetimeTZ.toDateTime.

Equations

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

@[instance_reducible]

instance TypeDB.instFromConceptValue : FromConcept Value

Equations

• TypeDB.instFromConceptValue = { expected := "value", decode := fun (c : TypeDB.Concept) => match c.value? with | some v => Except.ok v | none => Except.error c.describe }

@[instance_reducible]

instance TypeDB.instFromConceptIID : FromConcept IID

Equations

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

@[instance_reducible]

instance TypeDB.instFromConceptConcept : FromConcept Concept

The whole concept, with its label and IID.

Equations

• TypeDB.instFromConceptConcept = { expected := "concept", flags := TypeDB.Native.wantLabel ||| TypeDB.Native.wantIID, decode := Except.ok }

structure TypeDB.Label : Type

The type label of a concept: an instance's type, or a type itself.

• name : String

def TypeDB.instDecidableEqLabel.decEq (x✝ x✝¹ : Label) : Decidable (x✝ = x✝¹)

Equations

• TypeDB.instDecidableEqLabel.decEq { name := a } { name := b } = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance TypeDB.instDecidableEqLabel : DecidableEq Label

Equations

• TypeDB.instDecidableEqLabel = TypeDB.instDecidableEqLabel.decEq

def TypeDB.instReprLabel.repr : Label → Nat → Std.Format

Equations

• TypeDB.instReprLabel.repr x✝ prec✝ = Std.Format.bracket "{ " (Std.Format.nil ++ Std.Format.text "name" ++ Std.Format.text " := " ++ (Std.Format.nest 8 (repr x✝.name)).group) " }"

@[instance_reducible]

instance TypeDB.instReprLabel : Repr Label

Equations

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

@[instance_reducible]

instance TypeDB.instInhabitedLabel : Inhabited Label

Equations

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

def TypeDB.instHashableLabel.hash : Label → UInt64

Equations

• TypeDB.instHashableLabel.hash { name := a } = mixHash 0 (hash a)

@[instance_reducible]

instance TypeDB.instHashableLabel : Hashable Label

Equations

• TypeDB.instHashableLabel = { hash := TypeDB.instHashableLabel.hash }

@[instance_reducible]

instance TypeDB.instFromConceptLabel : FromConcept Label

Equations

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

structure TypeDB.RowDecoder (α : Type) : Type

Reads columns of a concept row. columns lists, in order, the variables it reads and the flags for each; run gets the concepts for those columns starting at offset.

• columns : Array (String × UInt8)
• run : Array (Option Concept) → (offset : Nat) → Except TypeDBError α

@[instance_reducible]

instance TypeDB.RowDecoder.instFunctor : Functor RowDecoder

Equations

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

@[instance_reducible]

instance TypeDB.RowDecoder.instApplicative : Applicative RowDecoder

Equations

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

def TypeDB.RowDecoder.guard {α : Type} (ok : α → Bool) (err : α → TypeDBError) (d : RowDecoder α) : RowDecoder α

Fails the decode of every row with err if ok is false.

Equations

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

def TypeDB.RowDecoder.plan {α : Type} (d : RowDecoder α) : Array String × ByteArray

Column names and per-column flags, as the native batch call takes them.

Equations

• d.plan = (Array.map (fun (x : String × UInt8) => x.fst) d.columns, { data := Array.map (fun (x : String × UInt8) => x.snd) d.columns })

def TypeDB.col {α : Type} (name : String) [i : FromConcept α] : RowDecoder α

The required column name.

Equations

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

def TypeDB.colOpt {α : Type} (name : String) [i : FromConcept α] : RowDecoder (Option α)

The optional column name: none when the row leaves it empty (e.g. from a try).

Equations

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

class TypeDB.FromColumn (α : Type) : Type

How a structure field reads its column; Option fields are optional.

• column : String → RowDecoder α

@[instance_reducible, instance 100]

instance TypeDB.instFromColumnOfFromConcept {α : Type} [FromConcept α] : FromColumn α

Equations

• TypeDB.instFromColumnOfFromConcept = { column := fun (n : String) => TypeDB.col n }

@[instance_reducible]

instance TypeDB.instFromColumnOptionOfFromConcept {α : Type} [FromConcept α] : FromColumn (Option α)

Equations

• TypeDB.instFromColumnOptionOfFromConcept = { column := fun (n : String) => TypeDB.colOpt n }

class TypeDB.FromRow (α : Type) : Type

Types decoded from a whole row. Derive it for structures with deriving FromRow.

• decoder : RowDecoder α

structure TypeDB.Col (name : String) (α : Type) : Type

A single named column.

• val : α

@[instance_reducible]

instance TypeDB.instReprCol {name✝ : String} {α✝ : Type} [Repr α✝] : Repr (Col name✝ α✝)

Equations

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

def TypeDB.instReprCol.repr {name✝ : String} {α✝ : Type} [Repr α✝] : Col name✝ α✝ → Nat → Std.Format

Equations

• TypeDB.instReprCol.repr x✝ prec✝ = Std.Format.bracket "{ " (Std.Format.nil ++ Std.Format.text "val" ++ Std.Format.text " := " ++ (Std.Format.nest 7 (repr x✝.val)).group) " }"

@[instance_reducible]

instance TypeDB.instInhabitedCol {a✝ : String} {a✝¹ : Type} [Inhabited a✝¹] : Inhabited (Col a✝ a✝¹)

Equations

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

@[instance_reducible]

instance TypeDB.instFromRowColOfFromConcept {name : String} {α : Type} [FromConcept α] : FromRow (Col name α)

Equations

• TypeDB.instFromRowColOfFromConcept = { decoder := (fun (x : α) => { val := x }) <$> TypeDB.col name }

@[instance_reducible]

instance TypeDB.instFromRowProd {α β : Type} [FromRow α] [FromRow β] : FromRow (α × β)

Equations

• TypeDB.instFromRowProd = { decoder := Prod.mk <$> TypeDB.FromRow.decoder <*> TypeDB.FromRow.decoder }