Last active
September 30, 2018 18:14
-
-
Save ctford/2f685238dd91ce9a8e4c3fae4fd9c3f7 to your computer and use it in GitHub Desktop.
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
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 |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment