Schema generation and verification

Schema.defineText turns the mapped types into one TypeQL define: attribute types with their value types, entity and relation types with sub, owns (with @key and @card) and relates, and the plays of every role player. Schema.verify checks a live database against the same mappings and lists every difference.

structure TypeDB.TypeSpec : Type

What the schema needs to know about one mapped type.

• label : String
• kind : ORM.Kind
• parent : Option String
• fields : Array ORM.FieldSpec

@[instance_reducible]

instance TypeDB.instReprTypeSpec : Repr TypeSpec

Equations

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

def TypeDB.instReprTypeSpec.repr : TypeSpec → Nat → Std.Format

Equations

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

@[instance_reducible]

instance TypeDB.instInhabitedTypeSpec : Inhabited TypeSpec

Equations

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

def TypeDB.TypeSpec.of (α : Type) [ORM.Mapped α] : TypeSpec

The schema description of a mapped type: TypeSpec.of Person.

Equations

• TypeDB.TypeSpec.of α = { label := TypeDB.ORM.Mapped.label α, kind := TypeDB.ORM.Mapped.kind α, parent := TypeDB.ORM.Mapped.parent α, fields := TypeDB.ORM.Mapped.fields α }

def TypeDB.Schema.defineText (specs : List TypeSpec) : Except String String

The TypeQL define for the mapped types, or an error if two types give the same attribute different value types.

Equations

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

def TypeDB.Schema.define (specs : List TypeSpec) : Except String (Query TxMode.schema)

The define query for the mapped types.

Equations

• TypeDB.Schema.define specs = (fun (x : String) => { text := x }) <$> TypeDB.Schema.defineText specs

def TypeDB.Schema.defineTx {m : TxMode} [m.Allows TxMode.schema] (specs : List TypeSpec) : Tx m Unit

Defines the mapped types in the current schema transaction. Unchanged types are left as they are, so running it again is harmless.

Equations

• TypeDB.Schema.defineTx specs = match TypeDB.Schema.define specs with | Except.ok q => TypeDB.exec q | Except.error e => TypeDB.Tx.fail (TypeDB.TypeDBError.internal e)

def TypeDB.Schema.load {m : TxMode} [m.Allows TxMode.schema] (path : System.FilePath) : Tx m Unit

Runs the TypeQL in a file, e.g. a define schema.

Equations

• TypeDB.Schema.load path = do let __do_lift ← liftM (IO.FS.readFile path) TypeDB.exec (TypeDB.Query.raw TypeDB.TxMode.schema __do_lift)

def TypeDB.Schema.verify {m : TxMode} [m.Allows TxMode.read] (specs : List TypeSpec) : Tx m (List SchemaIssue)

Every difference between the mapped types and the database's schema.

Equations

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

def TypeDB.Schema.verify! {m : TxMode} [m.Allows TxMode.read] (specs : List TypeSpec) : Tx m Unit

Fails with TypeDBError.schemaMismatch unless the database matches the mapped types.

Equations

• TypeDB.Schema.verify! specs = do let issues ← TypeDB.Schema.verify specs if issues.isEmpty = true then pure () else TypeDB.Tx.fail (TypeDB.TypeDBError.schemaMismatch issues)