The gloss line as structured data

A glossed token is already structured: the Leipzig Glossing Rules segment the surface word and its gloss at the same affix and clitic boundaries (Rule 2), separate by periods the several metalanguage elements that render one object-language element (Rule 4), and write grammatical category labels in capitals (Rule 3), so a row's gloss line determines a morph-by-morph token stream without any analysis beyond the source's own. This file reads that structure: a GlossedWord is a token's surface morphs beside their glosses, a gloss element is a category label or a lexical gloss by its capitalization, and Datum.glossedWords lists a row's well-aligned tokens. Readers built on it consult the row's form rather than a curated feature, the first step from annotated stimuli toward parsed ones.

Main definitions

• Gloss.toLower: Char.toLower extended over the Latin-1 Supplement and Latin Extended-A capitals, for sentence-initial tokens in European orthographies.
• Gloss.segments: the morphs of a token, split at the - and = boundaries.
• Gloss.elements, Gloss.IsLabel, Gloss.labels: the period-separated elements of a morph's gloss, an element being a category label when written without lower-case letters, and the labels of a gloss.
• GlossedWord, Datum.glossedWords: a token's aligned surface and gloss morphs, and a row's well-aligned tokens.
• GlossedWord.stem, GlossedWord.wordform, GlossedWord.labels, GlossedWord.lexicalGloss?, GlossedWord.lexicalMorph?: the first surface morph and the joined word, decapitalized, the word's category labels, and its first lexical gloss with the morph it glosses.

Implementation notes

• Everything is defined on List Char: the kernel reduces list operations where the positional String primitives get stuck, and the readers built here are consumed by decide.
• A token whose surface and gloss segment differently, against Rule 2, contributes no GlossedWord: the misalignment is the digitization's to fix, not the reader's to guess.

References

• [CHB08]

def Gloss.toLower (c : Char) : Char

Char.toLower extended over the Latin-1 Supplement and Latin Extended-A capitals by the Unicode case pairings of those blocks, with dotted İ lowered to i; Char.toLower itself only lowers ASCII.

Equations

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

def Gloss.split (seps : List Char) : List Char → List (List Char)

Splits a list of characters at the given separators. Core has List.splitOn, but its body does not reduce across the module boundary under decide, so the recursion is restated here structurally.

Equations

• Gloss.split seps [] = [[]]
• Gloss.split seps (c :: cs) = if c ∈ seps then [] :: Gloss.split seps cs else match Gloss.split seps cs with | r :: rs => (c :: r) :: rs | [] => [[c]]

def Gloss.segments (s : String) : List (List Char)

The morphs of a token, split at the affix boundary - and the clitic boundary = of the Leipzig rules.

Equations

• Gloss.segments s = Gloss.split ['-', '='] s.toList

def Gloss.punct : List Char

The punctuation written around morphs: the brackets of optional material and sentence marks.

Equations

• Gloss.punct = ['(', ')', '[', ']', ',', '.', '!', '?', ';', ':', '\"', '…']

def Gloss.trim (m : List Char) : List Char

A surface morph with its annotation punctuation dropped: the brackets of optional material may sit inside a token, as in (þangað) til.

Equations

• Gloss.trim m = List.filter (fun (x : Char) => decide (x ∉ Gloss.punct)) m

def Gloss.tokens (s : String) : List (List Char)

The words of an orthographic sentence: split at spaces, annotation punctuation dropped, decapitalized. For a language whose sources print no gloss line, the words are matched against the forms the language's fragment declares or realizes, which play the gloss line's role.

Equations

• Gloss.tokens s = List.filter (fun (x : List Char) => !x.isEmpty) (List.map (fun (x : List Char) => List.map Gloss.toLower x) (List.map Gloss.trim (Gloss.split [' '] s.toList)))

def Gloss.formTokens (f : String) : List (List Char)

A declared, possibly multiword, form as the normalized tokens a row's stream shows. The fragments keep their forms raw; normalization happens here, where a reader meets a row.

Equations

• Gloss.formTokens f = Gloss.tokens f

def Gloss.lookup? {α : Type u_1} (lex : List (String × α)) : List (List Char) → Option α

The entry of lex whose declared form starts earliest in the stream, the first listed where several start together.

Equations

• One or more equations did not get rendered due to their size.
• Gloss.lookup? lex [] = none

def Gloss.containsForm (ts : List (List Char)) (f : String) : Bool

The stream shows the declared form f.

Equations

• Gloss.containsForm ts f = (Gloss.lookup? [(f, ())] ts).isSome

def Gloss.IsLabel (g : List Char) : Prop

A gloss is a category label, as the Leipzig rules write PST or 3SG.DF, when it has no lower-case letter; otherwise it is a lexical gloss.

Equations

• Gloss.IsLabel g = ∀ c ∈ g, ¬c.isLower = true

@[instance_reducible]

instance Gloss.instDecidableIsLabel (g : List Char) : Decidable (IsLabel g)

Equations

• Gloss.instDecidableIsLabel g = Gloss.instDecidableIsLabel._aux_1 g

def Gloss.elements (g : List Char) : List (List Char)

The elements of a morph's gloss: an object-language element rendered by several metalanguage elements, words or category labels, has them separated by periods (Rule 4), as come.out or left.SG.MASC.

Equations

• Gloss.elements g = Gloss.split ['.'] g

def Gloss.labels (g : String) : List (List Char)

The category labels of a gloss: the elements of its morphs written without lower-case letters (Rules 2–4), as PST and 3SG in be-PST.3SG.

Equations

• Gloss.labels g = List.filter (fun (l : List Char) => decide (Gloss.IsLabel l) && !l.isEmpty) (List.flatMap Gloss.elements (Gloss.segments g))

structure GlossedWord : Type

A token of the gloss line as the Leipzig rules structure it: each surface morph beside its gloss, in order.

• morphs : List (List Char × List Char)

  The surface morphs with their glosses.

@[instance_reducible]

instance instDecidableEqGlossedWord : DecidableEq GlossedWord

Equations

• instDecidableEqGlossedWord = instDecidableEqGlossedWord.decEq

def instDecidableEqGlossedWord.decEq (x✝ x✝¹ : GlossedWord) : Decidable (x✝ = x✝¹)

Equations

• instDecidableEqGlossedWord.decEq { morphs := a } { morphs := b } = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯

def instReprGlossedWord.repr : GlossedWord → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance instReprGlossedWord : Repr GlossedWord

Equations

• instReprGlossedWord = { reprPrec := instReprGlossedWord.repr }

def GlossedWord.stem (w : GlossedWord) : List Char

The word's first surface morph, decapitalized: the form that a lexicon keys.

Equations

• w.stem = List.map Gloss.toLower (w.morphs.headD ([], [])).1

def GlossedWord.labels (w : GlossedWord) : List (List Char)

The category labels among the elements of the word's glosses.

Equations

• w.labels = List.filter (fun (l : List Char) => decide (Gloss.IsLabel l) && !l.isEmpty) (List.flatMap (fun (m : List Char × List Char) => Gloss.elements m.2) w.morphs)

def GlossedWord.lexicalGloss? (w : GlossedWord) : Option (List Char)

The word's first lexical gloss, where it has one.

Equations

• w.lexicalGloss? = List.find? (fun (g : List Char) => !decide (Gloss.IsLabel g)) (List.map (fun (x : List Char × List Char) => x.2) w.morphs)

def GlossedWord.lexicalMorph? (w : GlossedWord) : Option (List Char)

The surface morph of the word's first lexical gloss, decapitalized: the form that a lexicon of roots keys.

Equations

• w.lexicalMorph? = Option.map (fun (x : List Char × List Char) => List.map Gloss.toLower x.1) (List.find? (fun (m : List Char × List Char) => !decide (Gloss.IsLabel m.2)) w.morphs)

def GlossedWord.wordform (w : GlossedWord) : List Char

The word's surface form: its morphs joined, decapitalized.

Equations

• w.wordform = List.map Gloss.toLower (List.flatMap (fun (x : List Char × List Char) => x.1) w.morphs)

def Datum.glossedWords (e : Datum) : List GlossedWord

The row's tokens whose surface and gloss segment alike, each as a GlossedWord, its surface morphs trimmed of surrounding punctuation.

Equations

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

def Datum.glossStream (e : Datum) : List (List Char)

The row's gloss-line stream: each glossed word's form, split at its internal spaces, the stream that declared forms are matched against.

Equations

• e.glossStream = List.flatMap (fun (w : GlossedWord) => List.filter (fun (x : List Char) => !x.isEmpty) (Gloss.split [' '] w.wordform)) e.glossedWords