Syntax of Roman numerals, checked on type level with Agda's dependent types and instance arguments

RomanNumerals.agda

module RomanNumerals where

open import Data.List
open import Data.Unit using (⊤; tt)
open import Data.Empty using (⊥)

data Literal : Set where
  𝐼 𝑉 𝑋 𝐿 𝐶 𝐷 𝑀 : Literal

infix 4 ones_
ones_ : List Literal → Set
ones [] = ⊤
ones 𝐼 ∷ [] = ⊤
ones 𝐼 ∷ 𝐼 ∷ [] = ⊤ 
ones 𝐼 ∷ 𝐼 ∷ 𝐼 ∷ [] = ⊤ 
ones 𝐼 ∷ 𝑉 ∷ [] = ⊤
ones 𝑉 ∷ [] = ⊤
ones 𝑉 ∷ 𝐼 ∷ [] = ⊤
ones 𝑉 ∷ 𝐼 ∷ 𝐼 ∷ [] = ⊤
ones 𝑉 ∷ 𝐼 ∷ 𝐼 ∷ 𝐼 ∷ [] = ⊤
ones 𝐼 ∷ 𝑋 ∷ [] = ⊤
ones _ = ⊥

infix 4 tens_
tens_ : List Literal → Set
tens 𝐿 ∷ 𝑋 ∷ 𝑋 ∷ 𝑋 ∷ ℓ = ones ℓ
tens 𝑋 ∷ 𝑋 ∷ 𝑋 ∷ ℓ = ones ℓ
tens 𝐿 ∷ 𝑋 ∷ 𝑋 ∷ ℓ = ones ℓ
tens 𝑋 ∷ 𝑋 ∷ ℓ = ones ℓ
tens 𝑋 ∷ 𝐿 ∷ ℓ = ones ℓ
tens 𝐿 ∷ 𝑋 ∷ ℓ = ones ℓ
tens 𝑋 ∷ 𝐶 ∷ ℓ = ones ℓ
tens 𝑋 ∷ ℓ = ones ℓ
tens 𝐿 ∷ ℓ = ones ℓ
tens ls = ones ls

infix 4 hundreds_
hundreds_ : List Literal → Set
hundreds 𝐷 ∷ 𝐶 ∷ 𝐶 ∷ 𝐶 ∷ ℓ = tens ℓ 
hundreds 𝐶 ∷ 𝐶 ∷ 𝐶 ∷ ℓ = tens ℓ
hundreds 𝐷 ∷ 𝐶 ∷ 𝐶 ∷ ℓ = tens ℓ
hundreds 𝐶 ∷ 𝐶 ∷ ℓ = tens ℓ
hundreds 𝐶 ∷ 𝐷 ∷ ℓ = tens ℓ
hundreds 𝐷 ∷ 𝐶 ∷ ℓ = tens ℓ
hundreds 𝐶 ∷ 𝑀 ∷ ℓ = tens ℓ
hundreds 𝐶 ∷ ℓ = tens ℓ
hundreds 𝐷 ∷ ℓ = tens ℓ
hundreds ℓ = tens ℓ

infix 4 thousands_
thousands_ : List Literal → Set
thousands 𝑀  ∷ 𝑀  ∷ 𝑀  ∷ ℓ = hundreds ℓ
thousands 𝑀  ∷ 𝑀  ∷ ℓ = hundreds ℓ
thousands 𝑀  ∷ ℓ = hundreds ℓ
thousands ℓ = hundreds ℓ

infix 4 validRoman_
validRoman_ : List Literal → Set
validRoman ℓ = thousands ℓ

infixl 5 _I _V _X _L _C _D _M
data Numeral : {r : List Literal} → Set where
  _I : ∀ {r} {{ _ : validRoman r ∷ʳ 𝐼 }} → Numeral {r} → Numeral { r ∷ʳ 𝐼 }
  _V : ∀ {r} {{ _ : validRoman r ∷ʳ 𝑉 }} → Numeral {r} → Numeral { r ∷ʳ 𝑉 }
  _X : ∀ {r} {{ _ : validRoman r ∷ʳ 𝑋 }} → Numeral {r} → Numeral { r ∷ʳ 𝑋 }
  _L : ∀ {r} {{ _ : validRoman r ∷ʳ 𝐿 }} → Numeral {r} → Numeral { r ∷ʳ 𝐿 }
  _C : ∀ {r} {{ _ : validRoman r ∷ʳ 𝐶 }} → Numeral {r} → Numeral { r ∷ʳ 𝐶 }
  _D : ∀ {r} {{ _ : validRoman r ∷ʳ 𝐷 }} → Numeral {r} → Numeral { r ∷ʳ 𝐷 }
  _M : ∀ {r} {{ _ : validRoman r ∷ʳ 𝑀 }} → Numeral {r} → Numeral { r ∷ʳ 𝑀 }
  ᵣ : Numeral {[]}

-- 112
cvii : Numeral
cvii = ᵣ C V I I

-- 3054
mmmciv : Numeral
mmmciv = ᵣ M M M C I V

-- 999
cmxcix : Numeral
cmxcix = ᵣ C M X C I X

-- Will not typecheck - I before M
-- im : Numeral
-- im = ᵣ I M

-- Will not type typecheck - more than three I in a row
-- iiii : Numeral
-- iiii = ᵣ I I I I

-- Will not typecheck - additives after substractive
-- ivii : Numeral
-- ivii = ᵣ I V I I