Language samples

This file defines the rows of a paper's language sample, after the CLDF StructureDataset: the languages of the sample, and the codes a language takes for a parameter the paper records. The parameters, their codes and the rows of a sample are generated per paper.

Main definitions

• Data.Structures.Language: a row of the LanguageTable.
• Data.Structures.Coded: a value of the ValueTable, a code with the marks a source puts on it.

Implementation notes

• Per-paper data lives in Linglib/Data/Structures/{AuthorYear}.json, an object holding the CLDF tables ContributionTable, LanguageTable, ParameterTable, CodeTable and ValueTable under CLDF column names, and is compiled by scripts/gen_structures.py into {AuthorYear}.lean, declaring namespace {AuthorYear}.Structures.
• Each parameter becomes an inductive type with a constructor for each code. The values, long in the JSON as CLDF has them, are emitted as one row per language with a field for each parameter, so a theorem about the sample reads each language once.
• Each table of a paper is a contribution with its own list of rows. Languages, parameters and codes are shared, so a language two tables list is one Language with a row in each.
• A language may take several codes for a parameter, or none: a row's field is a list.
• A language without a Glottocode is one the source names without saying which Glottolog language it means; the JSON records why.
• Comments, footnotes and the lineage a source prints are its record: the generator validates them and does not emit them.

structure Data.Structures.Language : Type

A Language is a row of a CLDF LanguageTable, a language of the sample.

• id : String

  The ID column holds a stable identifier keyed to the paper.

• name : String

  The Name column holds the language's name as the source prints it; where its tables print several, the JSON records the others.

• glottocode : Option Glottocode

  The Glottocode column holds the Glottocode, when the source's name determines one.

@[instance_reducible]

instance Data.Structures.instDecidableEqLanguage : DecidableEq Language

Equations

• Data.Structures.instDecidableEqLanguage = Data.Structures.instDecidableEqLanguage.decEq

def Data.Structures.instDecidableEqLanguage.decEq (x✝ x✝¹ : Language) : Decidable (x✝ = x✝¹)

Equations

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

def Data.Structures.instReprLanguage.repr : Language → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance Data.Structures.instReprLanguage : Repr Language

Equations

• Data.Structures.instReprLanguage = { reprPrec := Data.Structures.instReprLanguage.repr }

structure Data.Structures.Coded (C : Type u_1) : Type u_1

A Coded C is a value of a CLDF ValueTable: a code of the parameter C, with the marks a source may put on it.

• code : C

  The code.

• questionable : Bool

  The source marks the code as questionable.

• optional : Bool

  The source marks the strategy the code names as optional.

@[instance_reducible]

instance Data.Structures.instDecidableEqCoded {C✝ : Type u_1} [DecidableEq C✝] : DecidableEq (Coded C✝)

Equations

• Data.Structures.instDecidableEqCoded = Data.Structures.instDecidableEqCoded.decEq

def Data.Structures.instDecidableEqCoded.decEq {C✝ : Type u_1} [DecidableEq C✝] (x✝ x✝¹ : Coded C✝) : Decidable (x✝ = x✝¹)

Equations

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

@[instance_reducible]

instance Data.Structures.instReprCoded {C✝ : Type u_1} [Repr C✝] : Repr (Coded C✝)

Equations

• Data.Structures.instReprCoded = { reprPrec := Data.Structures.instReprCoded.repr }

def Data.Structures.instReprCoded.repr {C✝ : Type u_1} [Repr C✝] : Coded C✝ → ℕ → Std.Format

Equations

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