lens-fin-rot13.hs

{-# LANGUAGE DataKinds #-}
-- cabal install fin lens

import Data.Char (toLower, isUpper, ord, chr)
import qualified Data.Fin as F
import qualified Data.Type.Nat as N
import Control.Lens

type Nat13 = N.Plus N.Nat4 N.Nat9
type Nat26 = N.Plus Nat13 Nat13
type Fin26 = F.Fin Nat26

alphaOf :: Char -> Maybe (Bool, Fin26)
alphaOf 'a' = Just (False,  0); alphaOf 'A' = Just (True,  0)
alphaOf 'b' = Just (False,  1); alphaOf 'B' = Just (True,  1)
alphaOf 'c' = Just (False,  2); alphaOf 'C' = Just (True,  2)
alphaOf 'd' = Just (False,  3); alphaOf 'D' = Just (True,  3)
alphaOf 'e' = Just (False,  4); alphaOf 'E' = Just (True,  4)
alphaOf 'f' = Just (False,  5); alphaOf 'F' = Just (True,  5)
alphaOf 'g' = Just (False,  6); alphaOf 'G' = Just (True,  6)
alphaOf 'h' = Just (False,  7); alphaOf 'H' = Just (True,  7)
alphaOf 'i' = Just (False,  8); alphaOf 'I' = Just (True,  8)
alphaOf 'j' = Just (False,  9); alphaOf 'J' = Just (True,  9)
alphaOf 'k' = Just (False, 10); alphaOf 'K' = Just (True, 10)
alphaOf 'l' = Just (False, 11); alphaOf 'L' = Just (True, 11)
alphaOf 'm' = Just (False, 12); alphaOf 'M' = Just (True, 12)
alphaOf 'n' = Just (False, 13); alphaOf 'N' = Just (True, 13)
alphaOf 'o' = Just (False, 14); alphaOf 'O' = Just (True, 14)
alphaOf 'p' = Just (False, 15); alphaOf 'P' = Just (True, 15)
alphaOf 'q' = Just (False, 16); alphaOf 'Q' = Just (True, 16)
alphaOf 'r' = Just (False, 17); alphaOf 'R' = Just (True, 17)
alphaOf 's' = Just (False, 18); alphaOf 'S' = Just (True, 18)
alphaOf 't' = Just (False, 19); alphaOf 'T' = Just (True, 19)
alphaOf 'u' = Just (False, 20); alphaOf 'U' = Just (True, 20)
alphaOf 'v' = Just (False, 21); alphaOf 'V' = Just (True, 21)
alphaOf 'w' = Just (False, 22); alphaOf 'W' = Just (True, 22)
alphaOf 'x' = Just (False, 23); alphaOf 'X' = Just (True, 23)
alphaOf 'y' = Just (False, 24); alphaOf 'Y' = Just (True, 24)
alphaOf 'z' = Just (False, 25); alphaOf 'Z' = Just (True, 25)
alphaOf _ = Nothing

alphabet :: Prism' Char (Bool, Fin26)
alphabet = prism (\(u, n) -> chr (fromEnum n + ord (if u then 'A' else 'a')))
                 (\c -> maybe (Left c) Right (alphaOf c))