A lightweight ORM

deriving Entity and deriving Relation map a Lean structure to a TypeDB entity or relation type (TypeDB.ORM.Deriving). The mapping is Lean-first: the structure is the source of truth, Schema.define generates the TypeQL define for it, and verifySchema checks a live database against it.

Fields map by their type:

• τ with a TypeDB value type: an owned attribute, required (@card(1..1));
• Option τ: an optional attribute; Array τ: a multi-valued attribute (@card(0..));
• Key τ: the type's key (@key);
• Role "r" (Ref β) or Role "r" (Array (Ref β)): in a relation, the instances playing role r;
• Attr "l" τ: overrides the attribute label, which is otherwise the field name in kebab-case.

A structure that extends a mapped structure maps to a subtype (sub) and inherits its attributes, roles and key. @[typedb "label"] on the structure sets the type label.

Instances are referenced by Ref α: by key value (Ref.key) or by IID (Ref.iid). insert returns an IID reference.

@[reducible, inline]

abbrev TypeDB.Key (α : Type) : Type

Marks the field holding the type's key attribute. Transparent: a Key String is a String.

Equations

• TypeDB.Key α = α

@[reducible, inline]

abbrev TypeDB.Role (_name : String) (α : Type) : Type

Marks a relation field holding the player(s) of role name.

Equations

• TypeDB.Role _name α = α

@[reducible, inline]

abbrev TypeDB.Attr (_label : String) (α : Type) : Type

Sets the TypeDB attribute label of a field.

Equations

• TypeDB.Attr _label α = α

inductive TypeDB.ORM.Target : Type

How a reference finds its instance.

• key (typeLabel keyAttr literal : String) : Target

  $x isa typeLabel, has keyAttr literal

• iid (iid : IID) : Target

def TypeDB.ORM.instDecidableEqTarget.decEq (x✝ x✝¹ : Target) : Decidable (x✝ = x✝¹)

Equations

• One or more equations did not get rendered due to their size.
• TypeDB.ORM.instDecidableEqTarget.decEq (TypeDB.ORM.Target.key typeLabel keyAttr literal) (TypeDB.ORM.Target.iid iid) = isFalse ⋯
• TypeDB.ORM.instDecidableEqTarget.decEq (TypeDB.ORM.Target.iid iid) (TypeDB.ORM.Target.key typeLabel keyAttr literal) = isFalse ⋯
• TypeDB.ORM.instDecidableEqTarget.decEq (TypeDB.ORM.Target.iid a) (TypeDB.ORM.Target.iid b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance TypeDB.ORM.instDecidableEqTarget : DecidableEq Target

Equations

• TypeDB.ORM.instDecidableEqTarget = TypeDB.ORM.instDecidableEqTarget.decEq

def TypeDB.ORM.instReprTarget.repr : Target → Nat → Std.Format

Equations

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

@[instance_reducible]

instance TypeDB.ORM.instReprTarget : Repr Target

Equations

• TypeDB.ORM.instReprTarget = { reprPrec := TypeDB.ORM.instReprTarget.repr }

@[instance_reducible]

instance TypeDB.ORM.instInhabitedTarget : Inhabited Target

Equations

• TypeDB.ORM.instInhabitedTarget = { default := TypeDB.ORM.instInhabitedTarget.default }

@[instance_reducible]

instance TypeDB.ORM.instHashableTarget : Hashable Target

Equations

• TypeDB.ORM.instHashableTarget = { hash := TypeDB.ORM.instHashableTarget.hash }

def TypeDB.ORM.instHashableTarget.hash : Target → UInt64

Equations

• TypeDB.ORM.instHashableTarget.hash (TypeDB.ORM.Target.key a a_1 a_2) = mixHash (mixHash (mixHash 0 (hash a)) (hash a_1)) (hash a_2)
• TypeDB.ORM.instHashableTarget.hash (TypeDB.ORM.Target.iid a) = mixHash 1 (hash a)

structure TypeDB.Ref (α : Type) : Type

A reference to an instance of the mapped type α.

• target : ORM.Target

def TypeDB.instDecidableEqRef.decEq {α✝ : Type} [DecidableEq α✝] (x✝ x✝¹ : Ref α✝) : Decidable (x✝ = x✝¹)

Equations

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

@[instance_reducible]

instance TypeDB.instDecidableEqRef {α✝ : Type} [DecidableEq α✝] : DecidableEq (Ref α✝)

Equations

• TypeDB.instDecidableEqRef = TypeDB.instDecidableEqRef.decEq

def TypeDB.instReprRef.repr {α✝ : Type} [Repr α✝] : Ref α✝ → Nat → Std.Format

Equations

• TypeDB.instReprRef.repr x✝ prec✝ = Std.Format.bracket "{ " (Std.Format.nil ++ Std.Format.text "target" ++ Std.Format.text " := " ++ (Std.Format.nest 10 (repr x✝.target)).group) " }"

@[instance_reducible]

instance TypeDB.instReprRef {α✝ : Type} [Repr α✝] : Repr (Ref α✝)

Equations

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

@[instance_reducible]

instance TypeDB.instInhabitedRef {a✝ : Type} : Inhabited (Ref a✝)

Equations

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

def TypeDB.instHashableRef.hash {α✝ : Type} [Hashable α✝] : Ref α✝ → UInt64

Equations

• TypeDB.instHashableRef.hash { target := a } = mixHash 0 (hash a)

@[instance_reducible]

instance TypeDB.instHashableRef {α✝ : Type} [Hashable α✝] : Hashable (Ref α✝)

Equations

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

@[instance_reducible]

instance TypeDB.instBEqRef {α : Type} : BEq (Ref α)

Equations

• TypeDB.instBEqRef = { beq := fun (a b : TypeDB.Ref α) => a.target == b.target }

inductive TypeDB.ORM.Kind : Type

• entity : Kind
• relation : Kind

@[instance_reducible]

instance TypeDB.ORM.instDecidableEqKind : DecidableEq Kind

Equations

• TypeDB.ORM.instDecidableEqKind x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance TypeDB.ORM.instReprKind : Repr Kind

Equations

• TypeDB.ORM.instReprKind = { reprPrec := TypeDB.ORM.instReprKind.repr }

def TypeDB.ORM.instReprKind.repr : Kind → Nat → Std.Format

Equations

• TypeDB.ORM.instReprKind.repr TypeDB.ORM.Kind.entity prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "TypeDB.ORM.Kind.entity")).group prec✝
• TypeDB.ORM.instReprKind.repr TypeDB.ORM.Kind.relation prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "TypeDB.ORM.Kind.relation")).group prec✝

@[instance_reducible]

instance TypeDB.ORM.instInhabitedKind : Inhabited Kind

Equations

• TypeDB.ORM.instInhabitedKind = { default := TypeDB.ORM.instInhabitedKind.default }

@[instance_reducible]

instance TypeDB.ORM.instToStringKind : ToString Kind

Equations

• TypeDB.ORM.instToStringKind = { toString := fun (x : TypeDB.ORM.Kind) => match x with | TypeDB.ORM.Kind.entity => "entity" | TypeDB.ORM.Kind.relation => "relation" }

inductive TypeDB.ORM.Card : Type

• one : Card
• opt : Card
• many : Card

@[instance_reducible]

instance TypeDB.ORM.instDecidableEqCard : DecidableEq Card

Equations

• TypeDB.ORM.instDecidableEqCard x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def TypeDB.ORM.instReprCard.repr : Card → Nat → Std.Format

Equations

• TypeDB.ORM.instReprCard.repr TypeDB.ORM.Card.one prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "TypeDB.ORM.Card.one")).group prec✝
• TypeDB.ORM.instReprCard.repr TypeDB.ORM.Card.opt prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "TypeDB.ORM.Card.opt")).group prec✝
• TypeDB.ORM.instReprCard.repr TypeDB.ORM.Card.many prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "TypeDB.ORM.Card.many")).group prec✝

@[instance_reducible]

instance TypeDB.ORM.instReprCard : Repr Card

Equations

• TypeDB.ORM.instReprCard = { reprPrec := TypeDB.ORM.instReprCard.repr }

@[instance_reducible]

instance TypeDB.ORM.instInhabitedCard : Inhabited Card

Equations

• TypeDB.ORM.instInhabitedCard = { default := TypeDB.ORM.instInhabitedCard.default }

inductive TypeDB.ORM.Shape : Type

What a field stores.

• attr (valueType : String) (card : Card) : Shape
• role (player : String) (many : Bool) : Shape

  Players of a role; player is the label of the referenced type.

@[instance_reducible]

instance TypeDB.ORM.instDecidableEqShape : DecidableEq Shape

Equations

• TypeDB.ORM.instDecidableEqShape = TypeDB.ORM.instDecidableEqShape.decEq

def TypeDB.ORM.instDecidableEqShape.decEq (x✝ x✝¹ : Shape) : Decidable (x✝ = x✝¹)

Equations

• TypeDB.ORM.instDecidableEqShape.decEq (TypeDB.ORM.Shape.attr a a_1) (TypeDB.ORM.Shape.attr b b_1) = if h : a = b then h ▸ if h : a_1 = b_1 then h ▸ isTrue ⋯ else isFalse ⋯ else isFalse ⋯
• TypeDB.ORM.instDecidableEqShape.decEq (TypeDB.ORM.Shape.attr valueType card) (TypeDB.ORM.Shape.role player many) = isFalse ⋯
• TypeDB.ORM.instDecidableEqShape.decEq (TypeDB.ORM.Shape.role player many) (TypeDB.ORM.Shape.attr valueType card) = isFalse ⋯
• TypeDB.ORM.instDecidableEqShape.decEq (TypeDB.ORM.Shape.role a a_1) (TypeDB.ORM.Shape.role b b_1) = if h : a = b then h ▸ if h : a_1 = b_1 then h ▸ isTrue ⋯ else isFalse ⋯ else isFalse ⋯

@[instance_reducible]

instance TypeDB.ORM.instReprShape : Repr Shape

Equations

• TypeDB.ORM.instReprShape = { reprPrec := TypeDB.ORM.instReprShape.repr }

def TypeDB.ORM.instReprShape.repr : Shape → Nat → Std.Format

Equations

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

@[instance_reducible]

instance TypeDB.ORM.instInhabitedShape : Inhabited Shape

Equations

• TypeDB.ORM.instInhabitedShape = { default := TypeDB.ORM.instInhabitedShape.default }

structure TypeDB.ORM.FieldSpec : Type

One mapped field. name is the attribute label or the role name.

• field : String
• name : String
• shape : Shape
• key : Bool
• own : Bool

  Declared in this type rather than inherited from its supertype.

@[instance_reducible]

instance TypeDB.ORM.instDecidableEqFieldSpec : DecidableEq FieldSpec

Equations

• TypeDB.ORM.instDecidableEqFieldSpec = TypeDB.ORM.instDecidableEqFieldSpec.decEq

def TypeDB.ORM.instDecidableEqFieldSpec.decEq (x✝ x✝¹ : FieldSpec) : Decidable (x✝ = x✝¹)

Equations

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

@[instance_reducible]

instance TypeDB.ORM.instReprFieldSpec : Repr FieldSpec

Equations

• TypeDB.ORM.instReprFieldSpec = { reprPrec := TypeDB.ORM.instReprFieldSpec.repr }

def TypeDB.ORM.instReprFieldSpec.repr : FieldSpec → Nat → Std.Format

Equations

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

@[instance_reducible]

instance TypeDB.ORM.instInhabitedFieldSpec : Inhabited FieldSpec

Equations

• TypeDB.ORM.instInhabitedFieldSpec = { default := TypeDB.ORM.instInhabitedFieldSpec.default }

inductive TypeDB.ORM.FieldEnc : Type

A field's contribution to an insert.

• attrs (literals : Array String) : FieldEnc
• players (targets : Array Target) : FieldEnc

inductive TypeDB.ORM.FieldData : Type

What a field decodes from: attribute values or role players' IIDs.

• attrs (values : Array Value) : FieldData
• players (iids : Array IID) : FieldData

class TypeDB.ORM.ValueType (α : Type) : Type

TypeDB value types of Lean types.

• name : String

@[instance_reducible]

instance TypeDB.ORM.instValueTypeString : ValueType String

Equations

• TypeDB.ORM.instValueTypeString = { name := "string" }

@[instance_reducible]

instance TypeDB.ORM.instValueTypeBool : ValueType Bool

Equations

• TypeDB.ORM.instValueTypeBool = { name := "boolean" }

@[instance_reducible]

instance TypeDB.ORM.instValueTypeInt64 : ValueType Int64

Equations

• TypeDB.ORM.instValueTypeInt64 = { name := "integer" }

@[instance_reducible]

instance TypeDB.ORM.instValueTypeInt : ValueType Int

Equations

• TypeDB.ORM.instValueTypeInt = { name := "integer" }

@[instance_reducible]

instance TypeDB.ORM.instValueTypeNat : ValueType Nat

Equations

• TypeDB.ORM.instValueTypeNat = { name := "integer" }

@[instance_reducible]

instance TypeDB.ORM.instValueTypeFloat : ValueType Float

Equations

• TypeDB.ORM.instValueTypeFloat = { name := "double" }

@[instance_reducible]

instance TypeDB.ORM.instValueTypeDecimal : ValueType Decimal

Equations

• TypeDB.ORM.instValueTypeDecimal = { name := "decimal" }

@[instance_reducible]

instance TypeDB.ORM.instValueTypeDuration : ValueType Duration

Equations

• TypeDB.ORM.instValueTypeDuration = { name := "duration" }

@[instance_reducible]

instance TypeDB.ORM.instValueTypePlainDate : ValueType Std.Time.PlainDate

Equations

• TypeDB.ORM.instValueTypePlainDate = { name := "date" }

@[instance_reducible]

instance TypeDB.ORM.instValueTypePlainDateTime : ValueType Std.Time.PlainDateTime

Equations

• TypeDB.ORM.instValueTypePlainDateTime = { name := "datetime" }

@[instance_reducible]

instance TypeDB.ORM.instValueTypeDatetimeTZ : ValueType DatetimeTZ

Equations

• TypeDB.ORM.instValueTypeDatetimeTZ = { name := "datetime-tz" }

@[instance_reducible]

instance TypeDB.ORM.instValueTypeDateTime : ValueType Std.Time.DateTime

Equations

• TypeDB.ORM.instValueTypeDateTime = { name := "datetime-tz" }

class TypeDB.ORM.FieldCodec (β : Type) : Type

How a field type is stored and read back.

• shape : Shape
• encode : β → FieldEnc
• decode : FieldData → Except String β

@[instance_reducible, instance 100]

instance TypeDB.ORM.instFieldCodecOfValueTypeOfToTypeQLOfFromConcept {γ : Type} [ValueType γ] [ToTypeQL γ] [FromConcept γ] : FieldCodec γ

Equations

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

@[instance_reducible]

instance TypeDB.ORM.instFieldCodecOptionOfValueTypeOfToTypeQLOfFromConcept {γ : Type} [ValueType γ] [ToTypeQL γ] [FromConcept γ] : FieldCodec (Option γ)

Equations

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

@[instance_reducible]

instance TypeDB.ORM.instFieldCodecArrayOfValueTypeOfToTypeQLOfFromConcept {γ : Type} [ValueType γ] [ToTypeQL γ] [FromConcept γ] : FieldCodec (Array γ)

Equations

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

class TypeDB.ORM.Mapped (α : Type) : Type

A Lean type mapped to a TypeDB entity or relation type. Derive it with deriving Entity or deriving Relation. fields, encode and decode cover every field, inherited ones included, in the same order.

• label : String
• kind : Kind
• parent : Option String
• fields : Array FieldSpec
• encode : α → Array FieldEnc
• decode : Array FieldData → Except String α

class TypeDB.ORM.Keyed (α : Type) (K : outParam Type) : Type

Mapped types with a key attribute of type K.

• keyAttr : String

@[instance_reducible]

instance TypeDB.ORM.instFieldCodecRefOfMapped {γ : Type} [Mapped γ] : FieldCodec (Ref γ)

Equations

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

@[instance_reducible]

instance TypeDB.ORM.instFieldCodecArrayRefOfMapped {γ : Type} [Mapped γ] : FieldCodec (Array (Ref γ))

Equations

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

structure TypeDB.ORM.Field (α β : Type) : Type

A typed handle on one attribute field of α, generated as α.field.<name>.

• attr : String
• card : Card

def TypeDB.Ref.iid {α : Type} (i : IID) : Ref α

Equations

• TypeDB.Ref.iid i = { target := TypeDB.ORM.Target.iid i }

def TypeDB.Ref.key {α K : Type} [ORM.Mapped α] [ORM.Keyed α K] [ToTypeQL K] (k : K) : Ref α

A reference by key value. Only types with a key attribute have one.

Equations

• TypeDB.Ref.key k = { target := TypeDB.ORM.Target.key (TypeDB.ORM.Mapped.label α) (TypeDB.ORM.Keyed.keyAttr α) (TypeDB.render k) }

def TypeDB.Ref.iid? {α : Type} (r : Ref α) : Option IID

Equations

• r.iid? = match r.target with | TypeDB.ORM.Target.iid i => some i | TypeDB.ORM.Target.key typeLabel keyAttr literal => none

def TypeDB.Ref.up {α β : Type} (r : Ref α) : Ref β

The same instance seen as a supertype.

Equations

• r.up = { target := r.target }

def TypeDB.ORM.Target.pattern (var label : String) : Target → String

A TypeQL pattern binding var to the referenced instance of type label.

Equations

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

def TypeDB.ORM.insertText {α : Type} [Mapped α] (x : α) : String

The insert query for a value, with match clauses for its role players.

Equations

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

def TypeDB.ORM.assemble (fields : Array FieldSpec) (attrs : Array Concept) (players : Array (String × IID)) : Array FieldData

The field data of one instance from its attributes and role players. Fields that share a role take its players in order: a single field one player, an array field the rest.

Equations

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

def TypeDB.ORM.fetchRaw {m : TxMode} [m.Allows TxMode.read] (pattern : String) (isRelation : Bool) : Tx m (Array (IID × String × Array Concept × Array (String × IID)))

The attributes and role players of every instance matched by pattern (which binds $x): two queries, whatever the number of instances.

Equations

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

def TypeDB.ORM.fetchInstances {m : TxMode} [m.Allows TxMode.read] (pattern : String) (fields : Array FieldSpec) (isRelation : Bool) : Tx m (Array (IID × String × Array FieldData))

Decodes the instances matched by pattern with the given fields.

Equations

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

Helpers the deriving handlers call: each is typed by a field's projection, so generated code never spells out field types.

@[reducible, inline]

abbrev TypeDB.ORM.TypeOf {σ β : Type} : (σ → β) → Type

Equations

• TypeDB.ORM.TypeOf x✝ = β

def TypeDB.ORM.shapeOf {σ β : Type} [FieldCodec β] : (σ → β) → Shape

Equations

• TypeDB.ORM.shapeOf x✝ = TypeDB.ORM.FieldCodec.shape β

def TypeDB.ORM.cardOf {σ β : Type} [FieldCodec β] : (σ → β) → Card

Equations

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

def TypeDB.ORM.encodeField {β : Type} [FieldCodec β] (x : β) : FieldEnc

Equations

• TypeDB.ORM.encodeField x = TypeDB.ORM.FieldCodec.encode x

def TypeDB.ORM.decodeField {σ β : Type} [FieldCodec β] : (σ → β) → (name : String) → (d : Array FieldData) → (i : Nat) → Except String β

Equations

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

def TypeDB.ORM.columnOf {σ β : Type} [FromColumn β] : (σ → β) → (name : String) → RowDecoder β

Equations

• TypeDB.ORM.columnOf x✝ name = TypeDB.FromColumn.column name

class TypeDB.Entity (α : Type) : Prop

Marks a structure derived as a TypeDB entity type (deriving Entity).

• mapped : Nonempty (ORM.Mapped α)

class TypeDB.Relation (α : Type) : Prop

Marks a structure derived as a TypeDB relation type (deriving Relation).

• mapped : Nonempty (ORM.Mapped α)

Operations on mapped types

def TypeDB.Entity.insert {α : Type} {m : TxMode} [ORM.Mapped α] [m.Allows TxMode.write] (x : α) : Tx m (Ref α)

Inserts the value and returns an IID reference to it. Fails if a referenced role player does not exist, in which case nothing is inserted.

Equations

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

def TypeDB.Entity.get? {α : Type} {m : TxMode} [ORM.Mapped α] [m.Allows TxMode.read] (r : Ref α) : Tx m (Option α)

The instance a reference points to, or none.

Equations

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

def TypeDB.Entity.all {α : Type} {m : TxMode} [ORM.Mapped α] [m.Allows TxMode.read] : Tx m (Array (Ref α × α))

Every instance of the type (and its subtypes), with an IID reference to each.

Equations

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

def TypeDB.Entity.update {α β : Type} {m : TxMode} [ORM.Mapped α] [m.Allows TxMode.write] [ORM.FieldCodec β] (r : Ref α) (f : ORM.Field α β) (v : β) : Tx m Unit

Replaces the value(s) of one attribute.

Equations

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

def TypeDB.Entity.delete {α : Type} {m : TxMode} [ORM.Mapped α] [m.Allows TxMode.write] (r : Ref α) : Tx m Unit

Deletes the instance.

Equations

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

def TypeDB.Entity.count {α : Type} {m : TxMode} [ORM.Mapped α] [m.Allows TxMode.read] : Tx m Nat

How many instances of the type (and its subtypes) exist.

Equations

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

Polymorphic decoding

class TypeDB.Polymorphic (α : Type) : Type

A sum type whose constructors wrap mapped types, decoded by each instance's concrete type. Derive it with deriving Polymorphic; the first constructor's type is the root that is queried.

• root : String
• isRelation : Bool
• variants : Array (String × Array ORM.FieldSpec × (Array ORM.FieldData → Except String α))

  Fields and decoder for the constructor of concrete type label.

def TypeDB.Polymorphic.all {α : Type} {m : TxMode} [Polymorphic α] [m.Allows TxMode.read] : Tx m (Array (IID × α))

Every instance of the root type, each decoded into the constructor of its concrete type. Instances of an unmapped subtype decode as the closest constructor listed first.

Equations

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