Verb class catalogues: schema

Typed schema for a book's catalogue of verb classes: for each class, the section number and title the book prints, its members, and its properties, each an alternation of the book's catalogue of alternations, named by its section number, or a further property, with the diacritic and scope the book gives it. Generated catalogues live in Data/VerbClasses/<Book>.lean, emitted from the canonical <Book>.json by scripts/gen_verb_classes.py.

This is data: it imports nothing from Linglib/ and states no theorems. The vocabulary is that of Levin's catalogue: an alternation is named by its section number in her Part One, and the further properties are those her class descriptions name. A catalogue with another vocabulary, such as VerbNet's thematic roles and frames, needs its own schema.

References

• [Lev93]

inductive Data.VerbClasses.Diacritic : Type

A property carries no diacritic, an asterisk for a property the class lacks, or a question mark for a marginal one.

• none : Diacritic
• star : Diacritic
• question : Diacritic

@[instance_reducible]

instance Data.VerbClasses.instDecidableEqDiacritic : DecidableEq Diacritic

Equations

• Data.VerbClasses.instDecidableEqDiacritic x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Data.VerbClasses.instReprDiacritic : Repr Diacritic

Equations

• Data.VerbClasses.instReprDiacritic = { reprPrec := Data.VerbClasses.instReprDiacritic.repr }

def Data.VerbClasses.instReprDiacritic.repr : Diacritic → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance Data.VerbClasses.instFintypeDiacritic : Fintype Diacritic

Equations

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

@[instance_reducible]

instance Data.VerbClasses.instInhabitedDiacritic : Inhabited Diacritic

Equations

• Data.VerbClasses.instInhabitedDiacritic = { default := Data.VerbClasses.instInhabitedDiacritic.default }

inductive Data.VerbClasses.Scope : Type

The share of a class's members that a property line speaks for, as the book qualifies it: all of them when it does not, or "most", "many", "some" or "a few" verbs.

• all : Scope
• most : Scope
• many : Scope
• some : Scope
• few : Scope

@[instance_reducible]

instance Data.VerbClasses.instDecidableEqScope : DecidableEq Scope

Equations

• Data.VerbClasses.instDecidableEqScope x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Data.VerbClasses.instReprScope : Repr Scope

Equations

• Data.VerbClasses.instReprScope = { reprPrec := Data.VerbClasses.instReprScope.repr }

def Data.VerbClasses.instReprScope.repr : Scope → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance Data.VerbClasses.instFintypeScope : Fintype Scope

Equations

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

@[instance_reducible]

instance Data.VerbClasses.instInhabitedScope : Inhabited Scope

Equations

• Data.VerbClasses.instInhabitedScope = { default := Data.VerbClasses.instInhabitedScope.default }

inductive Data.VerbClasses.NominalReading : Type

A derived nominal may have only its active or only its passive interpretation.

• active : NominalReading
• passive : NominalReading

@[instance_reducible]

instance Data.VerbClasses.instDecidableEqNominalReading : DecidableEq NominalReading

Equations

• Data.VerbClasses.instDecidableEqNominalReading x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Data.VerbClasses.instReprNominalReading.repr : NominalReading → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance Data.VerbClasses.instReprNominalReading : Repr NominalReading

Equations

• Data.VerbClasses.instReprNominalReading = { reprPrec := Data.VerbClasses.instReprNominalReading.repr }

@[instance_reducible]

instance Data.VerbClasses.instFintypeNominalReading : Fintype NominalReading

Equations

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

inductive Data.VerbClasses.GoalPhrase : Type

The goal of a verb of communication is expressed by an object or by a to phrase.

• object : GoalPhrase
• toPhrase : GoalPhrase

@[instance_reducible]

instance Data.VerbClasses.instDecidableEqGoalPhrase : DecidableEq GoalPhrase

Equations

• Data.VerbClasses.instDecidableEqGoalPhrase x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Data.VerbClasses.instReprGoalPhrase.repr : GoalPhrase → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance Data.VerbClasses.instReprGoalPhrase : Repr GoalPhrase

Equations

• Data.VerbClasses.instReprGoalPhrase = { reprPrec := Data.VerbClasses.instReprGoalPhrase.repr }

@[instance_reducible]

instance Data.VerbClasses.instFintypeGoalPhrase : Fintype GoalPhrase

Equations

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

inductive Data.VerbClasses.GoalRealization : Type

A sentential complement's goal is expressed as the book leaves it, not at all, by a required phrase, or by an optional one.

• unspecified : GoalRealization
• absent : GoalRealization
• required (g : GoalPhrase) : GoalRealization
• optional (g : GoalPhrase) : GoalRealization

def Data.VerbClasses.instDecidableEqGoalRealization.decEq (x✝ x✝¹ : GoalRealization) : Decidable (x✝ = x✝¹)

Equations

• One or more equations did not get rendered due to their size.
• Data.VerbClasses.instDecidableEqGoalRealization.decEq Data.VerbClasses.GoalRealization.unspecified Data.VerbClasses.GoalRealization.unspecified = isTrue ⋯
• Data.VerbClasses.instDecidableEqGoalRealization.decEq Data.VerbClasses.GoalRealization.unspecified (Data.VerbClasses.GoalRealization.required g) = isFalse ⋯
• Data.VerbClasses.instDecidableEqGoalRealization.decEq Data.VerbClasses.GoalRealization.unspecified (Data.VerbClasses.GoalRealization.optional g) = isFalse ⋯
• Data.VerbClasses.instDecidableEqGoalRealization.decEq Data.VerbClasses.GoalRealization.absent Data.VerbClasses.GoalRealization.absent = isTrue ⋯
• Data.VerbClasses.instDecidableEqGoalRealization.decEq Data.VerbClasses.GoalRealization.absent (Data.VerbClasses.GoalRealization.required g) = isFalse ⋯
• Data.VerbClasses.instDecidableEqGoalRealization.decEq Data.VerbClasses.GoalRealization.absent (Data.VerbClasses.GoalRealization.optional g) = isFalse ⋯
• Data.VerbClasses.instDecidableEqGoalRealization.decEq (Data.VerbClasses.GoalRealization.required g) Data.VerbClasses.GoalRealization.unspecified = isFalse ⋯
• Data.VerbClasses.instDecidableEqGoalRealization.decEq (Data.VerbClasses.GoalRealization.required g) Data.VerbClasses.GoalRealization.absent = isFalse ⋯
• Data.VerbClasses.instDecidableEqGoalRealization.decEq (Data.VerbClasses.GoalRealization.required a) (Data.VerbClasses.GoalRealization.required b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯
• Data.VerbClasses.instDecidableEqGoalRealization.decEq (Data.VerbClasses.GoalRealization.required g) (Data.VerbClasses.GoalRealization.optional g_1) = isFalse ⋯
• Data.VerbClasses.instDecidableEqGoalRealization.decEq (Data.VerbClasses.GoalRealization.optional g) Data.VerbClasses.GoalRealization.unspecified = isFalse ⋯
• Data.VerbClasses.instDecidableEqGoalRealization.decEq (Data.VerbClasses.GoalRealization.optional g) Data.VerbClasses.GoalRealization.absent = isFalse ⋯
• Data.VerbClasses.instDecidableEqGoalRealization.decEq (Data.VerbClasses.GoalRealization.optional g) (Data.VerbClasses.GoalRealization.required g_1) = isFalse ⋯
• Data.VerbClasses.instDecidableEqGoalRealization.decEq (Data.VerbClasses.GoalRealization.optional a) (Data.VerbClasses.GoalRealization.optional b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Data.VerbClasses.instDecidableEqGoalRealization : DecidableEq GoalRealization

Equations

• Data.VerbClasses.instDecidableEqGoalRealization = Data.VerbClasses.instDecidableEqGoalRealization.decEq

def Data.VerbClasses.instReprGoalRealization.repr : GoalRealization → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance Data.VerbClasses.instReprGoalRealization : Repr GoalRealization

Equations

• Data.VerbClasses.instReprGoalRealization = { reprPrec := Data.VerbClasses.instReprGoalRealization.repr }

inductive Data.VerbClasses.PageProperty : Type

A property the book lists for a class that is not one of its alternations.

• zeroRelatedNominal : PageProperty
• erNominal : PageProperty
• ingNominal : PageProperty
• processNominal : PageProperty
• resultNominal : PageProperty
• derivedNominal (reading : NominalReading) : PageProperty
• ableAdjective : PageProperty
• zeroRelatedAdjective : PageProperty
• sententialComplement (goal : GoalRealization) : PageProperty
• extraposition : PageProperty
• directSpeech : PageProperty
• parentheticalUse : PageProperty
• infinitivalCopularClause : PageProperty
• measurePhrase : PageProperty
• pathPhrase : PageProperty
• depictivePhrase : PageProperty
• substanceObject : PageProperty
• bodyPartObject : PageProperty
• collectiveNPSubject : PageProperty
• impersonalPassive : PageProperty
• passivePrepositionChoice : PageProperty
• fromPhrase : PageProperty
• withAlternatesWithIn : PageProperty
• ofAlternatesWithOut : PageProperty
• unspecifiedObjectPlusLocativePP : PageProperty
• coreferentialInterpretationVaries : PageProperty

@[instance_reducible]

instance Data.VerbClasses.instDecidableEqPageProperty : DecidableEq PageProperty

Equations

• Data.VerbClasses.instDecidableEqPageProperty = Data.VerbClasses.instDecidableEqPageProperty.decEq

def Data.VerbClasses.instDecidableEqPageProperty.decEq (x✝ x✝¹ : PageProperty) : Decidable (x✝ = x✝¹)

Equations

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

@[instance_reducible]

instance Data.VerbClasses.instReprPageProperty : Repr PageProperty

Equations

• Data.VerbClasses.instReprPageProperty = { reprPrec := Data.VerbClasses.instReprPageProperty.repr }

def Data.VerbClasses.instReprPageProperty.repr : PageProperty → ℕ → Std.Format

Equations

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

inductive Data.VerbClasses.Heading : Type

A property line names an alternation by its section number in the book's catalogue of alternations, or a further property.

• alternation (number : List ℕ) : Heading
• property (p : PageProperty) : Heading

@[instance_reducible]

instance Data.VerbClasses.instDecidableEqHeading : DecidableEq Heading

Equations

• Data.VerbClasses.instDecidableEqHeading = Data.VerbClasses.instDecidableEqHeading.decEq

def Data.VerbClasses.instDecidableEqHeading.decEq (x✝ x✝¹ : Heading) : Decidable (x✝ = x✝¹)

Equations

• Data.VerbClasses.instDecidableEqHeading.decEq (Data.VerbClasses.Heading.alternation a) (Data.VerbClasses.Heading.alternation b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯
• Data.VerbClasses.instDecidableEqHeading.decEq (Data.VerbClasses.Heading.alternation number) (Data.VerbClasses.Heading.property p) = isFalse ⋯
• Data.VerbClasses.instDecidableEqHeading.decEq (Data.VerbClasses.Heading.property p) (Data.VerbClasses.Heading.alternation number) = isFalse ⋯
• Data.VerbClasses.instDecidableEqHeading.decEq (Data.VerbClasses.Heading.property a) (Data.VerbClasses.Heading.property b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯

def Data.VerbClasses.instReprHeading.repr : Heading → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance Data.VerbClasses.instReprHeading : Repr Heading

Equations

• Data.VerbClasses.instReprHeading = { reprPrec := Data.VerbClasses.instReprHeading.repr }

structure Data.VerbClasses.PropertyLine : Type

A line of a class's property table records what it names, its diacritic and scope, and any further qualifier the book prints with it, such as "based on with variant" or "except kill".

• heading : Heading
• diacritic : Diacritic
• scope : Scope
• qualifier : Option String

def Data.VerbClasses.instDecidableEqPropertyLine.decEq (x✝ x✝¹ : PropertyLine) : Decidable (x✝ = x✝¹)

Equations

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

@[instance_reducible]

instance Data.VerbClasses.instDecidableEqPropertyLine : DecidableEq PropertyLine

Equations

• Data.VerbClasses.instDecidableEqPropertyLine = Data.VerbClasses.instDecidableEqPropertyLine.decEq

@[instance_reducible]

instance Data.VerbClasses.instReprPropertyLine : Repr PropertyLine

Equations

• Data.VerbClasses.instReprPropertyLine = { reprPrec := Data.VerbClasses.instReprPropertyLine.repr }

def Data.VerbClasses.instReprPropertyLine.repr : PropertyLine → ℕ → Std.Format

Equations

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

structure Data.VerbClasses.VerbClass : Type

A verb class as the book describes it has the section number and title the book prints, the page on which the class begins, the members and those of them the book marks as doubtful, and the property table in the book's order.

• number : String
• title : String
• page : ℕ
• members : List String
• doubtful : List String
• properties : List PropertyLine

@[instance_reducible]

instance Data.VerbClasses.instReprVerbClass : Repr VerbClass

Equations

• Data.VerbClasses.instReprVerbClass = { reprPrec := Data.VerbClasses.instReprVerbClass.repr }

def Data.VerbClasses.instReprVerbClass.repr : VerbClass → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance Data.VerbClasses.instInhabitedVerbClass : Inhabited VerbClass

Equations

• Data.VerbClasses.instInhabitedVerbClass = { default := { number := "", title := "", page := 0, members := [], doubtful := [], properties := [] } }