Yet another GreekScript approach in Agda

GreekScript3.agda

module GreekScript3 where

data Empty : Set where

Not : Set → Set
Not x = x → Empty

data _And_ (A B : Set) : Set where
  _and_ : (a : A) → (b : B) → A And B

data _Or_ (A B : Set) : Set where
  left : (a : A) → A Or B
  right : (b : B) → A Or B


data Entity : Set where
  α β γ δ ε ζ η θ ι κ λ′ μ ν ξ ο π ρ σ τ υ φ χ ψ ω : Entity
  acute grave circumflex : Entity
  smooth rough : Entity
  diaeresis : Entity

data _Letter : Entity → Set where
  α : α Letter
  β : β Letter
  γ : γ Letter
  δ : δ Letter
  ε : ε Letter
  ζ : ζ Letter
  η : η Letter
  θ : θ Letter
  ι : ι Letter
  κ : κ Letter
  λ′ : λ′ Letter
  μ : μ Letter
  ν : ν Letter
  ξ : ξ Letter
  ο : ο Letter
  π : π Letter
  ρ : ρ Letter
  σ : σ Letter
  τ : τ Letter
  υ : υ Letter
  φ : φ Letter
  χ : χ Letter
  ψ : ψ Letter
  ω : ω Letter

data _Consonant : Entity → Set where
  β : β Consonant
  γ : γ Consonant
  δ : δ Consonant
  ζ : ζ Consonant
  θ : θ Consonant
  κ : κ Consonant
  λ′ : λ′ Consonant
  μ : μ Consonant
  ν : ν Consonant
  ξ : ξ Consonant
  π : π Consonant
  ρ : ρ Consonant
  σ : σ Consonant
  τ : τ Consonant
  φ : φ Consonant
  χ : χ Consonant
  ψ : ψ Consonant

data _Vowel : Entity → Set where
  α : α Vowel
  ε : ε Vowel
  η : η Vowel
  ι : ι Vowel
  ο : ο Vowel
  υ : υ Vowel
  ω : ω Vowel

Vowel→NotConsonant : ∀ {x} → x Vowel → Not (x Consonant)
Vowel→NotConsonant α ()
Vowel→NotConsonant ε ()
Vowel→NotConsonant η ()
Vowel→NotConsonant ι ()
Vowel→NotConsonant ο ()
Vowel→NotConsonant υ ()
Vowel→NotConsonant ω ()

Letter→VowelOrConsonant : ∀ {x} → x Letter → (x Vowel) Or (x Consonant)
Letter→VowelOrConsonant α = left α
Letter→VowelOrConsonant β = right β
Letter→VowelOrConsonant γ = right γ
Letter→VowelOrConsonant δ = right δ
Letter→VowelOrConsonant ε = left ε
Letter→VowelOrConsonant ζ = right ζ
Letter→VowelOrConsonant η = left η
Letter→VowelOrConsonant θ = right θ
Letter→VowelOrConsonant ι = left ι
Letter→VowelOrConsonant κ = right κ
Letter→VowelOrConsonant λ′ = right λ′
Letter→VowelOrConsonant μ = right μ
Letter→VowelOrConsonant ν = right ν
Letter→VowelOrConsonant ξ = right ξ
Letter→VowelOrConsonant ο = left ο
Letter→VowelOrConsonant π = right π
Letter→VowelOrConsonant ρ = right ρ
Letter→VowelOrConsonant σ = right σ
Letter→VowelOrConsonant τ = right τ
Letter→VowelOrConsonant υ = left υ
Letter→VowelOrConsonant φ = right φ
Letter→VowelOrConsonant χ = right χ
Letter→VowelOrConsonant ψ = right ψ
Letter→VowelOrConsonant ω = left ω


data Diphthong : ∀ {v₁ v₂} → v₁ Vowel → v₂ Vowel → Set where
  αι : Diphthong α ι
  ει : Diphthong ε ι
  οι : Diphthong ο ι
  αυ : Diphthong α υ
  ευ : Diphthong ε υ
  ου : Diphthong ο υ
  ηυ : Diphthong η υ
  ωυ : Diphthong ω υ
  υι : Diphthong υ ι

data _Subscript : ∀ {v} → v Vowel → Set where
  ι-subscript : ι Subscript

data ImproperDiphthong : ∀ {v} → v Vowel → ι Subscript → Set where
  ᾳ : ImproperDiphthong α ι-subscript
  ῃ : ImproperDiphthong η ι-subscript
  ῳ : ImproperDiphthong ω ι-subscript

data Length : Set where
  short long : Length

data Long_ : ∀ {v} → v Vowel → Set where
  α : Long α
  η : Long η
  ι : Long ι
  υ : Long υ
  ω : Long ω

data Short_ : ∀ {v} → v Vowel → Set where
  α : Short α
  ε : Short ε
  ι : Short ι
  ο : Short ο
  υ : Short υ

Vowel→ShortOrLong : ∀ {e} → (v : e Vowel) → (Short v) Or (Long v)
Vowel→ShortOrLong α = left α
Vowel→ShortOrLong ε = left ε
Vowel→ShortOrLong η = right η
Vowel→ShortOrLong ι = left ι
Vowel→ShortOrLong ο = left ο
Vowel→ShortOrLong υ = left υ
Vowel→ShortOrLong ω = right ω