FSM.Entropy.idr

module Data.FSM.Entropy
%default total

data Solfege = Do | Re | Mi | Fa | So | La | Ti

entropy : Solfege -> Solfege -> Nat
entropy Do Do = 1
entropy Do Re = 2
entropy Re Do = 2
entropy Re Re = 1
entropy Re Mi = 2
entropy Mi Re = 2
entropy Mi Mi = 1
entropy Mi Fa = 2
entropy Fa Mi = 2
entropy Fa Fa = 1
entropy Fa So = 2
entropy So Fa = 2
entropy So So = 1
entropy So La = 2
entropy La So = 2
entropy La La = 1
entropy La Ti = 2
entropy Ti La = 2
entropy Ti Ti = 1
entropy _ _ = 4

data Series : (t : Type) -> (t -> t -> Nat) -> (x : t) -> (y : t) -> Nat -> Type where
  End : Series t cost x x bits
  Then : (y : t) -> Series t cost x y (cost x y)
  (>>=) : Series t cost x y bits -> ((bits : Nat) -> Series t cost y z bits') -> Series t cost x z (bits + bits')

Melody : Solfege -> Solfege -> Nat -> Type
Melody = Series Solfege entropy

conventional : Melody Do So 10 -- Actually only needs 8, but the `End` makes up the total.
conventional = do Then Re
                  Then Mi
                  Then Fa
                  Then So
                  End

unconventional : Melody Do So 12 -- Needs the whole 12, as it's an odder melody.
unconventional = do Then Ti
                    Then Mi
                    Then Fa
                    Then So
                    End