TypeQL text

typeql!"…" builds a Query from TypeQL text. Each {e} is rendered by ToTypeQL, which turns a Lean value into a TypeQL value literal: strings are quoted and escaped, so user data can never change a query's structure. Raw is the only way to splice text verbatim.

The query's transaction mode is inferred from the literal parts: define, undefine or redefine need a schema transaction, insert, delete, update or put a write transaction, anything else a read transaction. TypeQL braces must be escaped as \{ and \} because Lean uses {…} for interpolation.

inductive TypeDB.TxMode : Type

The kind of a transaction, ordered by what it may do: read ≤ write ≤ schema.

• read : TxMode
• write : TxMode
• schema : TxMode

@[instance_reducible]

instance TypeDB.instDecidableEqTxMode : DecidableEq TxMode

Equations

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

def TypeDB.instReprTxMode.repr : TxMode → Nat → Std.Format

Equations

• TypeDB.instReprTxMode.repr TypeDB.TxMode.read prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "TypeDB.TxMode.read")).group prec✝
• TypeDB.instReprTxMode.repr TypeDB.TxMode.write prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "TypeDB.TxMode.write")).group prec✝
• TypeDB.instReprTxMode.repr TypeDB.TxMode.schema prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "TypeDB.TxMode.schema")).group prec✝

@[instance_reducible]

instance TypeDB.instReprTxMode : Repr TxMode

Equations

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

@[instance_reducible]

instance TypeDB.instInhabitedTxMode : Inhabited TxMode

Equations

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

def TypeDB.instOrdTxMode.ord : TxMode → TxMode → Ordering

Equations

• TypeDB.instOrdTxMode.ord x✝ y✝ = compare x✝.ctorIdx y✝.ctorIdx

@[instance_reducible]

instance TypeDB.instOrdTxMode : Ord TxMode

Equations

• TypeDB.instOrdTxMode = { compare := TypeDB.instOrdTxMode.ord }

def TypeDB.TxMode.rank : TxMode → Nat

Equations

• TypeDB.TxMode.read.rank = 0
• TypeDB.TxMode.write.rank = 1
• TypeDB.TxMode.schema.rank = 2

@[instance_reducible]

instance TypeDB.TxMode.instLE : LE TxMode

Equations

• TypeDB.TxMode.instLE = { le := fun (a b : TypeDB.TxMode) => a.rank ≤ b.rank }

@[instance_reducible]

instance TypeDB.TxMode.instDecidableLe (a b : TxMode) : Decidable (a ≤ b)

Equations

• a.instDecidableLe b = { decide := a.rank.ble b.rank, reflects_decide := ⋯ }

@[instance_reducible]

instance TypeDB.TxMode.instMax : Max TxMode

Equations

• TypeDB.TxMode.instMax = { max := fun (a b : TypeDB.TxMode) => if a.rank ≤ b.rank then b else a }

def TypeDB.TxMode.code : TxMode → UInt8

The driver's TransactionType.

Equations

• TypeDB.TxMode.read.code = 0
• TypeDB.TxMode.write.code = 1
• TypeDB.TxMode.schema.code = 2

class TypeDB.TxMode.Allows (cur need : TxMode) : Prop

Allows cur need: a transaction of mode cur may run an operation that needs need. Resolved at compile time; a missing instance means the operation needs a stronger transaction.

• le : need ≤ cur

instance TypeDB.TxMode.instAllowsRead {m : TxMode} : m.Allows read

instance TypeDB.TxMode.instAllowsWrite : write.Allows write

instance TypeDB.TxMode.instAllowsSchemaWrite : schema.Allows write

instance TypeDB.TxMode.instAllowsSchema : schema.Allows schema

structure TypeDB.Query (need : TxMode) : Type

TypeQL text and the weakest transaction mode that may run it.

• text : String

@[instance_reducible]

instance TypeDB.instInhabitedQuery {a✝ : TxMode} : Inhabited (Query a✝)

Equations

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

@[instance_reducible]

instance TypeDB.instToStringQuery {m : TxMode} : ToString (Query m)

Equations

• TypeDB.instToStringQuery = { toString := TypeDB.Query.text }

def TypeDB.Query.raw (need : TxMode) (text : String) : Query need

A query from text the caller vouches for, with an explicit mode.

Equations

• TypeDB.Query.raw need text = { text := text }

def TypeDB.Query.withMode {m : TxMode} (q : Query m) (need : TxMode) : Query need

Runs the query under a different mode requirement, e.g. to require a write transaction for a read query whose mode the literal could not reveal.

Equations

• q.withMode need = { text := q.text }

def TypeDB.Query.append {m n : TxMode} (q₁ : Query m) (q₂ : Query n) : Query (max m n)

Pipes two queries: q₁ ++ q₂ runs q₂'s stages after q₁'s, needing the stronger mode.

Equations

• q₁.append q₂ = { text := q₁.text ++ "\n" ++ q₂.text }

structure TypeDB.Raw : Type

Text spliced into a query verbatim, such as a type label or a query fragment.

• text : String

@[instance_reducible]

instance TypeDB.instInhabitedRaw : Inhabited Raw

Equations

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

@[instance_reducible]

instance TypeDB.instReprRaw : Repr Raw

Equations

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

def TypeDB.instReprRaw.repr : Raw → Nat → Std.Format

Equations

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

class TypeDB.ToTypeQL (α : Type) : Type

Renders a Lean value as a TypeQL value literal.

• render : α → String

def TypeDB.TypeQL.quote (s : String) : String

Quotes and escapes a string as a TypeQL string literal.

Equations

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

def TypeDB.TypeQL.civilOfDays (z : Int) : Int × Nat × Nat

Civil date (year, month, day) of a day count since 1970-01-01 (Hinnant's algorithm).

Equations

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

def TypeDB.TypeQL.dateText (days : Int) : String

Equations

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

def TypeDB.TypeQL.datetimeText (seconds : Int) (nanos : Nat) : String

YYYY-MM-DDTHH:MM:SS[.fffffffff] for UTC seconds and nanoseconds since the epoch.

Equations

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

def TypeDB.TypeQL.offsetText (offset : Int) : String

±HH:MM for an offset in seconds.

Equations

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

def TypeDB.TypeQL.exactDouble (f : Float) : Option String

The exact decimal expansion of a finite double, or none for NaN and infinities. Every double is m · 2^e, whose decimal expansion is finite, so the literal parses back to exactly the same double.

Equations

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

@[instance_reducible]

instance TypeDB.instToTypeQLString : ToTypeQL String

Equations

• TypeDB.instToTypeQLString = { render := TypeDB.TypeQL.quote }

@[instance_reducible]

instance TypeDB.instToTypeQLRaw : ToTypeQL Raw

Equations

• TypeDB.instToTypeQLRaw = { render := TypeDB.Raw.text }

@[instance_reducible]

instance TypeDB.instToTypeQLBool : ToTypeQL Bool

Equations

• TypeDB.instToTypeQLBool = { render := fun (b : Bool) => if b = true then "true" else "false" }

@[instance_reducible]

instance TypeDB.instToTypeQLInt : ToTypeQL Int

Equations

• TypeDB.instToTypeQLInt = { render := toString }

@[instance_reducible]

instance TypeDB.instToTypeQLNat : ToTypeQL Nat

Equations

• TypeDB.instToTypeQLNat = { render := toString }

@[instance_reducible]

instance TypeDB.instToTypeQLInt64 : ToTypeQL Int64

Equations

• TypeDB.instToTypeQLInt64 = { render := fun (i : Int64) => toString i.toInt }

@[instance_reducible]

instance TypeDB.instToTypeQLInt32 : ToTypeQL Int32

Equations

• TypeDB.instToTypeQLInt32 = { render := fun (i : Int32) => toString i.toInt }

@[instance_reducible]

instance TypeDB.instToTypeQLUInt64 : ToTypeQL UInt64

Equations

• TypeDB.instToTypeQLUInt64 = { render := fun (i : UInt64) => toString i.toNat }

@[instance_reducible]

instance TypeDB.instToTypeQLUInt32 : ToTypeQL UInt32

Equations

• TypeDB.instToTypeQLUInt32 = { render := fun (i : UInt32) => toString i.toNat }

@[instance_reducible]

instance TypeDB.instToTypeQLFloat : ToTypeQL Float

Doubles render exactly. NaN and infinities have no TypeQL literal and render as NaN or inf, which the server rejects.

Equations

• TypeDB.instToTypeQLFloat = { render := fun (f : Float) => (TypeDB.TypeQL.exactDouble f).getD (if f.isNaN = true then "NaN" else "inf") }

@[instance_reducible]

instance TypeDB.instToTypeQLDecimal : ToTypeQL Decimal

Equations

• TypeDB.instToTypeQLDecimal = { render := fun (d : TypeDB.Decimal) => d.toString ++ "dec" }

@[instance_reducible]

instance TypeDB.instToTypeQLDuration : ToTypeQL Duration

Equations

• TypeDB.instToTypeQLDuration = { render := TypeDB.Duration.toISO }

@[instance_reducible]

instance TypeDB.instToTypeQLIID : ToTypeQL IID

Equations

• TypeDB.instToTypeQLIID = { render := TypeDB.IID.hex }

@[instance_reducible]

instance TypeDB.instToTypeQLPlainDate : ToTypeQL Std.Time.PlainDate

Equations

• TypeDB.instToTypeQLPlainDate = { render := fun (d : Std.Time.PlainDate) => TypeDB.TypeQL.dateText d.toEpochDay.val }

@[instance_reducible]

instance TypeDB.instToTypeQLPlainDateTime : ToTypeQL Std.Time.PlainDateTime

Equations

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

@[instance_reducible]

instance TypeDB.instToTypeQLDatetimeTZ : ToTypeQL DatetimeTZ

Equations

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

@[instance_reducible]

instance TypeDB.instToTypeQLDateTime : ToTypeQL Std.Time.DateTime

Equations

• TypeDB.instToTypeQLDateTime = { render := fun (dt : Std.Time.DateTime) => TypeDB.render (TypeDB.DatetimeTZ.ofDateTime dt) }

def TypeDB.TypeQL.inferMode (text : String) : TxMode

The weakest mode that can run TypeQL text, from its keywords outside string literals.

Equations

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

def TypeDB.TypeQL.modeSyntax : TxMode → Lean.MacroM Lean.Term

Equations

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

def TypeDB.termTypeql!_ : Lean.ParserDescr

TypeQL text with {e} holes rendered by ToTypeQL. Its transaction mode is inferred from the literal text; see the module docs.

Equations

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