Morphs

A morph is a minimal segmental form together with its attachment kind: root, prefix, suffix, proclitic, enclitic, or free form — the form side of [Has20]'s form–content pairing. Morphs are never zero and never discontinuous.

inductive Morphology.Morph.Side : Type

The side of its host on which a bound morph attaches.

• before : Side

  Before the host: prefixes and proclitics.

• after : Side

  After the host: suffixes and enclitics.

@[implicit_reducible]

instance Morphology.Morph.instDecidableEqSide : DecidableEq Side

Equations

• Morphology.Morph.instDecidableEqSide x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Morphology.Morph.instReprSide.repr : Side → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Morphology.Morph.instReprSide : Repr Side

Equations

• Morphology.Morph.instReprSide = { reprPrec := Morphology.Morph.instReprSide.repr }

@[implicit_reducible]

instance Morphology.Morph.instFintypeSide : Fintype Side

Equations

• Morphology.Morph.instFintypeSide = { elems := { val := ↑Morphology.Morph.Side.enumList, nodup := Morphology.Morph.Side.enumList_nodup }, complete := Morphology.Morph.instFintypeSide._proof_1 }

inductive Morphology.Morph.Attachment : Type

How tightly a bound morph attaches to its host.

• affix : Attachment

  An affix, written with -.

• clitic : Attachment

  A clitic, written with =.

@[implicit_reducible]

instance Morphology.Morph.instDecidableEqAttachment : DecidableEq Attachment

Equations

• Morphology.Morph.instDecidableEqAttachment x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Morphology.Morph.instReprAttachment : Repr Attachment

Equations

• Morphology.Morph.instReprAttachment = { reprPrec := Morphology.Morph.instReprAttachment.repr }

def Morphology.Morph.instReprAttachment.repr : Attachment → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Morphology.Morph.instFintypeAttachment : Fintype Attachment

Equations

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

inductive Morphology.Morph.Kind : Type

The ways a morph attaches.

• bound (side : Side) (attachment : Attachment) : Kind

  A bound morph attaches on a side of its host, as an affix or a clitic.

• root : Kind

  A root morph.

• free : Kind

  A free non-root morph, such as a particle or an auxiliary.

@[implicit_reducible]

instance Morphology.Morph.instDecidableEqKind : DecidableEq Kind

Equations

• Morphology.Morph.instDecidableEqKind = Morphology.Morph.instDecidableEqKind.decEq

def Morphology.Morph.instDecidableEqKind.decEq (x✝ x✝¹ : Kind) : Decidable (x✝ = x✝¹)

Equations

• One or more equations did not get rendered due to their size.
• Morphology.Morph.instDecidableEqKind.decEq (Morphology.Morph.Kind.bound side attachment) Morphology.Morph.Kind.root = isFalse ⋯
• Morphology.Morph.instDecidableEqKind.decEq (Morphology.Morph.Kind.bound side attachment) Morphology.Morph.Kind.free = isFalse ⋯
• Morphology.Morph.instDecidableEqKind.decEq Morphology.Morph.Kind.root (Morphology.Morph.Kind.bound side attachment) = isFalse ⋯
• Morphology.Morph.instDecidableEqKind.decEq Morphology.Morph.Kind.root Morphology.Morph.Kind.root = isTrue ⋯
• Morphology.Morph.instDecidableEqKind.decEq Morphology.Morph.Kind.root Morphology.Morph.Kind.free = isFalse Morphology.Morph.instDecidableEqKind.decEq._proof_7
• Morphology.Morph.instDecidableEqKind.decEq Morphology.Morph.Kind.free (Morphology.Morph.Kind.bound side attachment) = isFalse ⋯
• Morphology.Morph.instDecidableEqKind.decEq Morphology.Morph.Kind.free Morphology.Morph.Kind.root = isFalse Morphology.Morph.instDecidableEqKind.decEq._proof_9
• Morphology.Morph.instDecidableEqKind.decEq Morphology.Morph.Kind.free Morphology.Morph.Kind.free = isTrue ⋯

def Morphology.Morph.instReprKind.repr : Kind → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Morphology.Morph.instReprKind : Repr Kind

Equations

• Morphology.Morph.instReprKind = { reprPrec := Morphology.Morph.instReprKind.repr }

@[implicit_reducible]

instance Morphology.Morph.instFintypeKind : Fintype Kind

Equations

• Morphology.Morph.instFintypeKind = Fintype.ofEquiv ((_ : Morphology.Morph.Side) × Morphology.Morph.Attachment ⊕ Unit ⊕ Unit) Morphology.Morph.Kind.proxyTypeEquiv

structure Morphology.Morph : Type

A morph is a minimal segmental form with its attachment kind.

• kind : Kind

  How the morph attaches.

• form : String

  The bare segmental material, with no boundary notation.

@[implicit_reducible]

instance Morphology.instDecidableEqMorph : DecidableEq Morph

Equations

• Morphology.instDecidableEqMorph = Morphology.instDecidableEqMorph.decEq

def Morphology.instDecidableEqMorph.decEq (x✝ x✝¹ : Morph) : Decidable (x✝ = x✝¹)

Equations

• Morphology.instDecidableEqMorph.decEq { kind := a, form := a_1 } { kind := b, form := b_1 } = if h : a = b then h ▸ if h : a_1 = b_1 then h ▸ isTrue ⋯ else isFalse ⋯ else isFalse ⋯

@[implicit_reducible]

instance Morphology.instReprMorph : Repr Morph

Equations

• Morphology.instReprMorph = { reprPrec := Morphology.instReprMorph.repr }

def Morphology.instReprMorph.repr : Morph → ℕ → Std.Format

Equations

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

def Morphology.Morph.pref (s : String) : Morph

A prefix morph.

Equations

• Morphology.Morph.pref s = { kind := Morphology.Morph.Kind.bound Morphology.Morph.Side.before Morphology.Morph.Attachment.affix, form := s }

def Morphology.Morph.suff (s : String) : Morph

A suffix morph.

Equations

• Morphology.Morph.suff s = { kind := Morphology.Morph.Kind.bound Morphology.Morph.Side.after Morphology.Morph.Attachment.affix, form := s }

def Morphology.Morph.procl (s : String) : Morph

A proclitic morph.

Equations

• Morphology.Morph.procl s = { kind := Morphology.Morph.Kind.bound Morphology.Morph.Side.before Morphology.Morph.Attachment.clitic, form := s }

def Morphology.Morph.encl (s : String) : Morph

An enclitic morph.

Equations

• Morphology.Morph.encl s = { kind := Morphology.Morph.Kind.bound Morphology.Morph.Side.after Morphology.Morph.Attachment.clitic, form := s }

def Morphology.Morph.free (s : String) : Morph

A free non-root morph.

Equations

• Morphology.Morph.free s = { kind := Morphology.Morph.Kind.free, form := s }

def Morphology.Morph.root (s : String) : Morph

A root morph.

Equations

• Morphology.Morph.root s = { kind := Morphology.Morph.Kind.root, form := s }

def Morphology.Morph.attachment? : Morph → Option Attachment

The attachment of a bound morph; none for roots and free forms.

Equations

• { kind := Morphology.Morph.Kind.bound side a, form := form }.attachment? = some a
• x✝.attachment? = none

def Morphology.Morph.side? : Morph → Option Side

The side a bound morph attaches on; none for roots and free forms.

Equations

• { kind := Morphology.Morph.Kind.bound side a, form := form }.side? = some side
• x✝.side? = none

@[implicit_reducible]

instance Morphology.Morph.instToString : ToString Morph

Equations

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

@[implicit_reducible]

instance Morphology.instToStringListMorph : ToString (List Morph)

Equations

• Morphology.instToStringListMorph = { toString := fun (x : List Morphology.Morph) => match x with | [] => "∅" | ms => "…".intercalate (List.map toString ms) }