Encoding rules of Greek Accents from book by D. A. Carson

GreekAccents.agda

{-# OPTIONS --exact-split #-}

-- adapted from Greek Accents by D.A.Carson
module GreekAccents where

data Consonant : Set where
  β γ δ ζ θ κ ƛ μ ν ξ π ρ ῥ σ τ φ χ ψ [ : Consonant

data SingleVowel : Set where
  α ε η ι ο υ ω : SingleVowel

data IotaSubscriptVowel : Set where
  ᾳ ῃ ῳ : IotaSubscriptVowel

data Diphthong : Set where
  αι αυ ει ευ ηυ οι ου υι : Diphthong

data VowelSoundS : Set where
  V : SingleVowel → VowelSoundS
  I : IotaSubscriptVowel → VowelSoundS
  D : Diphthong → VowelSoundS

data VowelSound : Set where
  α ε η ι ο υ ω : VowelSound
  ᾳ ῃ ῳ : VowelSound
  αι αυ ει ευ ηυ οι ου υι : VowelSound

data AccentPosition : Set where
  ultima penult antepenult : AccentPosition

data Length : Set where
  short long : Length

data VowelSoundLen : VowelSound → Length → Set where
  ᾰ : VowelSoundLen α short
  ᾱ : VowelSoundLen α long
  ε : VowelSoundLen ε short
  η : VowelSoundLen η long
  ῐ : VowelSoundLen ι short
  ῑ : VowelSoundLen ι long
  ο : VowelSoundLen ο short
  ῠ : VowelSoundLen υ short
  ῡ : VowelSoundLen υ long
  ω : VowelSoundLen ω long
  ᾳ : VowelSoundLen ᾳ long
  ῃ : VowelSoundLen ῃ long
  ῳ : VowelSoundLen ῳ long
  αι͝ : VowelSoundLen αι short
  αι͞ : VowelSoundLen αι long
  αυ : VowelSoundLen αυ long
  ει : VowelSoundLen ει long
  ευ : VowelSoundLen ευ long
  ηυ : VowelSoundLen ηυ long
  οι͝ : VowelSoundLen οι short
  οι͞ : VowelSoundLen οι long
  ου : VowelSoundLen ου long
  υι : VowelSoundLen υι long

data Accent : Set where
  acute circumflex : Accent

open import Agda.Builtin.Nat using (Nat; suc)

infixl 5 _:<_
data RList (A : Set) : Set where
  [] : RList A
  _:<_ : RList A → A → RList A

data RVec (A : Set) : Nat → Set where
  [] : RVec A 0
  _:<_ : ∀ {n} → RVec A n → A → RVec A (suc n)

data Position : Nat → Set where
  zero : {n : Nat} → Position (suc n)
  suc : {n : Nat} → Position n → Position (suc n)

Meter = RVec Length

record Syllable : Set where
  constructor syll
  field
    {consonants-count} : Nat
    consonants : RVec Consonant consonants-count
    {vowel-sound} : VowelSound
    {length} : Length
    vowel-sound-length : VowelSoundLen vowel-sound length

βαλλω : RVec Syllable _
βαλλω = [] :< syll ([] :< β) ᾰ :< syll ([] :< ƛ :< ƛ) ω

data WordAccent : Accent → AccentPosition → Set where
  oxytone : WordAccent acute ultima
  paroxytone : WordAccent acute penult
  proparoxytone : WordAccent acute antepenult
  perispomenon : WordAccent circumflex ultima
  properispomenon : WordAccent circumflex penult

data WordMeter : Accent → AccentPosition → ∀ {n} → Meter n → Set where
  acute-ultima        : ∀ {n} → (m : Meter n) → (u : Length)     → WordMeter acute      ultima     (           m      :< u)
  acute-penult-short  : ∀ {n} → (m : Meter n) → (u : Length)     → WordMeter acute      penult     (     m   :< short :< u)
  acute-penult-long   : ∀ {n} → (m : Meter n)                    → WordMeter acute      penult     (     m   :< short :< long)
  acute-antepenult    : ∀ {n} → (m : Meter n) → (ap pu : Length) → WordMeter acute      antepenult (m :< ap  :< pu    :< short)
  acute-antepenult-εω : ∀ {n} → (m : Meter n) → (ap : Length)    → WordMeter acute      antepenult (m :< ap  :< short :< long)
  circumflex-ultima   : ∀ {n} → (m : Meter n)                    → WordMeter circumflex ultima     (            m     :< long)
  circumflex-penult   : ∀ {n} → (m : Meter n)                    → WordMeter circumflex penult     (       m :< long  :< short)

data ShortUltimaAccent : Accent → AccentPosition → Set where
  acute-ultima           : ShortUltimaAccent acute ultima
  acute-short-penult     : ShortUltimaAccent acute penult
  circumflex-long-penult : ShortUltimaAccent circumflex penult
  acute-antepenult       : ShortUltimaAccent acute antepenult

smyth167 : ∀ {n} → (m : Meter n) → ∀ a ap → WordMeter a ap (m :< short) → ShortUltimaAccent a ap
smyth167 m                .acute      .ultima (acute-ultima .m .short) = acute-ultima
smyth167 .(m :< short)    .acute      .penult (acute-penult-short m .short) = acute-short-penult
smyth167 .(m :< long)     .circumflex .penult (circumflex-penult m) = circumflex-long-penult
smyth167 .(m :< ap :< pu) .acute      .antepenult (acute-antepenult m ap pu) = acute-antepenult

data LongUltimaAccent : Accent → AccentPosition → Set where
  either-ultima : (a : Accent) → LongUltimaAccent a ultima
  acute-penult : LongUltimaAccent acute penult
  acute-antepenult-εω : LongUltimaAccent acute antepenult

smyth168 : ∀ {n} → (m : Meter n) → ∀ a ap → WordMeter a ap (m :< long) → LongUltimaAccent a ap
smyth168 m                   .acute      .ultima     (acute-ultima .m .long) = either-ultima acute
smyth168 m                   .circumflex .ultima     (circumflex-ultima .m) = either-ultima circumflex
smyth168 .(m :< short)       .acute      .penult     (acute-penult-short m .long) = acute-penult
smyth168 .(m :< short)       .acute      .penult     (acute-penult-long m) = acute-penult
smyth168 .(m :< ap :< short) .acute      .antepenult (acute-antepenult-εω m ap) = acute-antepenult-εω