packages feed

mezzo (empty) → 0.1.0.0

raw patch · 24 files changed

+3583/−0 lines, 24 filesdep +HCodecsdep +QuickCheckdep +basesetup-changed

Dependencies added: HCodecs, QuickCheck, base, boxes, ghc-typelits-natnormalise, hspec, mezzo, should-not-typecheck, template-haskell

Files

+ LICENSE view
@@ -0,0 +1,21 @@+MIT License++Copyright (c) 2016 Dima Szamozvancev++Permission is hereby granted, free of charge, to any person obtaining a copy+of this software and associated documentation files (the "Software"), to deal+in the Software without restriction, including without limitation the rights+to use, copy, modify, merge, publish, distribute, sublicense, and/or sell+copies of the Software, and to permit persons to whom the Software is+furnished to do so, subject to the following conditions:++The above copyright notice and this permission notice shall be included in all+copies or substantial portions of the Software.++THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR+IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,+FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE+AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER+LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM,+OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE+SOFTWARE.
+ Setup.hs view
@@ -0,0 +1,2 @@+import Distribution.Simple+main = defaultMain
+ app/Main.hs view
@@ -0,0 +1,6 @@+module Main where++import Lib++main :: IO ()+main = someFunc
+ mezzo.cabal view
@@ -0,0 +1,72 @@+name:                mezzo+version:             0.1.0.0+synopsis:            Typesafe music composition+description:         A Haskell music composition library that enforces common+                     musical rules in the type system.+homepage:            https://github.com/DimaSamoz/mezzo#readme+license:             BSD3+license-file:        LICENSE+author:              Dima Szamozvancev+maintainer:          ds709@cam.ac.uk+copyright:           2016 Dima Samozvancev+category:            Music+build-type:          Simple+-- extra-source-files:+cabal-version:       >=1.10++library+  hs-source-dirs:      src+  exposed-modules:     Lib+                     , Mezzo+                     , Mezzo.Model+                     , Mezzo.Model.Prim+                     , Mezzo.Model.Music+                     , Mezzo.Model.Types+                     , Mezzo.Model.Harmony.Motion+                     , Mezzo.Model.Harmony.Chords+                     , Mezzo.Model.Harmony.Functional+                     , Mezzo.Model.Reify++                     , Mezzo.Compose.Types+                     , Mezzo.Compose.Builder+                     , Mezzo.Compose.Templates+                     , Mezzo.Compose.Basic+                     , Mezzo.Compose.Harmonic+                     , Mezzo.Compose.Combine++                     , Mezzo.Render.MIDI++  build-depends:       base >= 4.7 && < 5+                     , ghc-typelits-natnormalise+                     , template-haskell+                     , HCodecs+                     , boxes+  default-language:    Haskell2010++executable mezzo-exe+  hs-source-dirs:      app+  main-is:             Main.hs+  ghc-options:         -threaded -rtsopts -with-rtsopts=-N+  build-depends:       base+                     , mezzo+  default-language:    Haskell2010++test-suite mezzo-test+  type:                exitcode-stdio-1.0+  hs-source-dirs:      test+  main-is:             Main.hs+  other-modules:       Main+                     , PrimSpec+                     , TypeSpec+  build-depends:       base+                     , mezzo+                     , hspec+                     , QuickCheck+                    --  , deepseq+                     , should-not-typecheck+  ghc-options:         -threaded -rtsopts -with-rtsopts=-N+  default-language:    Haskell2010++source-repository head+  type:     git+  location: https://github.com/DimaSamoz/mezzo
+ src/Lib.hs view
@@ -0,0 +1,6 @@+module Lib+    ( someFunc+    ) where++someFunc :: IO ()+someFunc = putStrLn "someFunc"
+ src/Mezzo.hs view
@@ -0,0 +1,6 @@+module Mezzo+    ( someFunc+    ) where++someFunc :: IO ()+someFunc = putStrLn "someFunc"
+ src/Mezzo/Compose/Basic.hs view
@@ -0,0 +1,94 @@+{-# LANGUAGE TypeInType, TypeApplications, TemplateHaskell, RankNTypes, FlexibleContexts, GADTs #-}++-----------------------------------------------------------------------------+-- |+-- Module      :  Mezzo.Compose.Basic+-- Description :  Basic composition units+-- Copyright   :  (c) Dima Szamozvancev+-- License     :  MIT+--+-- Maintainer  :  ds709@cam.ac.uk+-- Stability   :  experimental+-- Portability :  portable+--+-- Literals for pitches, notes, durations, etc.+--+-----------------------------------------------------------------------------++module Mezzo.Compose.Basic where++import GHC.TypeLits+import Data.Kind+import Control.Monad++import Mezzo.Model+import Mezzo.Compose.Types+import Mezzo.Compose.Builder+import Mezzo.Compose.Templates++-- * Atomic literals++-- ** Pitch class literals+pitchClassLits++-- ** Accidental literals+accidentalLits++-- ** Octave literals+octaveLits++-- ** Duration literals and terminators+join <$> traverse mkDurLits [''Whole, ''Half, ''Quarter, ''Eighth, ''Sixteenth]++mk32ndLits++-- * Pitches++-- ** Constructor++-- | Create a new pitch with the given class, accidental and octave.+pitch :: Primitive (Pitch pc acc oct) => PC pc -> Acc acc -> Oct oct -> Pit (Pitch pc acc oct)+pitch pc acc oct = Pit++-- | Value representing silence, the "pitch" of rests.+silence :: Pit Silence+silence = Pit++-- ** Concrete literals+mkPitchLits++-- ** Pitch specifiers (admitting continuations)+mkPitchSpecs++r :: RestS+r dur = dur Pit+-- | Raise a pitch by a semitone.+sharp :: RootM r (Sharpen r)+sharp = constConv Root++-- | Lower a pitch by a semitone.+flat :: RootM r (Flatten r)+flat = constConv Root++-- * Notes++-- ** Constructors+-- | Create a new root from a pitch.+rootP :: IntRep p => Pit p -> Root (PitchRoot p)+rootP p = Root++-- | Create a new root from a key and a scale degree.+rootS :: Primitive (DegreeRoot k d) => KeyS k -> ScaDeg d -> Root (DegreeRoot k d)+rootS k d = Root++-- | Create a new note from a root and duration.+noteP :: (Primitive d, IntRep p) => Pit p -> Dur d -> Music (FromRoot (PitchRoot p) d)+noteP p = Note (rootP p)++noteS :: (Primitive d, IntRep (DegreeRoot k sd))+      => KeyS k -> ScaDeg sd -> Dur d -> Music (FromRoot (DegreeRoot k sd) d)+noteS k sd = Note (rootS k sd)++-- | Create a rest from a duration.+rest :: Primitive d => Dur d -> Music (FromSilence d)+rest = Rest
+ src/Mezzo/Compose/Builder.hs view
@@ -0,0 +1,203 @@+{-# LANGUAGE TypeInType, RankNTypes, ExistentialQuantification, GADTs #-}++-----------------------------------------------------------------------------+-- |+-- Module      :  Mezzo.Compose.Builder+-- Description :  Music builder+-- Copyright   :  (c) Dima Szamozvancev+-- License     :  MIT+--+-- Maintainer  :  ds709@cam.ac.uk+-- Stability   :  experimental+-- Portability :  portable+--+-- Pattern of combinatorially building musical terms of various types.+--+-----------------------------------------------------------------------------++module Mezzo.Compose.Builder+    (+    -- * General builder types+      Spec+    , Conv+    , Mut+    , Term+    , AConv+    , AMut+    , Mut'+    , spec+    , constConv+    -- * Music-specific builder types+    , RootS+    , RestS+    , ChorS+    , RootM+    , ChorM+    , ChorC+    , ChorC'+    , RootT+    , RestT+    , ChorT+    )+    where++import Mezzo.Model++import GHC.TypeLits++-------------------------------------------------------------------------------+-- General types+-------------------------------------------------------------------------------++-- | Specifier: specifies a value of some type which starts the building.+type Spec t = forall m. (t -> m) -> m++-- | Converter: converts a value of type s to a value of type t.+type Conv s t = s -> Spec t++-- | Mutator: mutates a value of type t.+type Mut t = Conv t t++-- | Terminator: finishes building a value of type t and returns a result of type r.+type Term t r = t -> r++-- | Converter with argument: converts a value of type s to a value of type t, consuming an argument of type a.+type AConv a s t = s -> a -> Spec t++-- | Mutator with argument: mutates a value of type t, consuming an argument of type a.+type AMut a t = AConv a t t++-- | Flexible mutator: mutator that allows slight changes in the type (otherwise use 'Conv').+type Mut' t t' = Conv t t'++-- | Returns a new specifier for the given value.+spec :: t -> Spec t+spec i c = c i++-- | A converter that ignores its argument and returns the given constant value.+constConv :: t -> Conv s t+constConv = const . spec++-- | A mutator that does nothing.+nop :: Mut t+nop = spec++-------------------------------------------------------------------------------+-- Music specific types+-------------------------------------------------------------------------------++-- | Root specifier.+type RootS r = Primitive r => Spec (Root r)++-- | Rest specifier.+type RestS = Spec (Pit Silence)++-- | Chord specifier.+type ChorS c = Primitive c => Spec (Cho c)++-- | Root mutator.+type RootM r r' = (Primitive r, Primitive r') => Mut' (Root r) (Root r')++-- | Chord mutator.+type ChorM c c' = (Primitive c, Primitive c') => Mut' (Cho c) (Cho c')++-- | Converter from roots to chords.+type ChorC' c r t i = (Primitive r, Primitive t, Primitive i) => AConv (Inv i) (Root r) (Cho (c r t i))++-- | Converter from roots to chords, using the default inversion.+type ChorC c r t = (Primitive r, Primitive t) => Conv (Root r) (Cho (c r t Inv0))++-- | Note terminator.+type RootT r d = Primitive r => Term (Root r) (Music (FromRoot r d))++--  | Rest terminator.+type RestT d = Term (Pit Silence) (Music (FromSilence d))++-- | Chord terminator.+type ChorT c d = Primitive c => Term (Cho c) (Music (FromChord c d))++-- inKey :: KeyS key -> a -> a+-- inKey key cont = let ?k = key in cont+--+--+-- i :: (?k :: KeyS key) => RootS (DegreeRoot key I)+-- i = spec Root+--+-- c :: RootS (PitchRoot (Pitch C Natural Oct3))+-- c = spec Root+--+-- sharp :: RootM r (Sharpen r)+-- sharp = constConv Root+--+-- maj :: ChorC Triad r MajTriad+-- maj = constConv Cho+--+-- qn :: RootT r 8+-- qn p = Note p Dur+--+-- qc :: KnownNat n => ChorT (c :: ChordType n) 8+-- qc c = Chord c Dur+++-------------------------------------------------------------------------------+-- Silly examples+-- Most of these are quite pointless, but show that the pattern enables us to+-- write DSLs with a very fluent feel.+-------------------------------------------------------------------------------++inc :: Mut Int+inc i = spec (succ i)++toString :: Conv Int String+toString n = spec (show n)++ex :: Mut String+ex s = spec (s ++ "!")++smile :: Term String String+smile s = s ++ " :)"++say :: String -> Spec String+say = spec++add :: Int -> Spec Int+add = spec++and' :: Mut t+and' = nop++to :: Int -> Mut Int+to y x = spec (x + y)++display :: Conv Int String+display = spec . show++result :: Term String String+result = ("result: " ++)++compute :: Double -> Spec Double+compute = spec++plus :: AMut Double Double+plus i p = spec (i + p)++please :: Term Double Double+please = id++percent :: Mut Double+percent = nop++of' :: Double -> Mut Double+of' d p = spec (d * (p / 100))++stack :: Spec [Int]+stack = spec []++push :: AMut Int [Int]+push s v = spec (v : s)++pop :: Mut [Int]+pop = spec . tail++end :: Term [Int] [Int]+end = id
+ src/Mezzo/Compose/Combine.hs view
@@ -0,0 +1,120 @@+{-# LANGUAGE TypeInType, TypeApplications, TypeOperators, FlexibleContexts, RankNTypes,+    FlexibleInstances, ScopedTypeVariables, GADTs, TypeFamilies #-}+{-# OPTIONS_GHC -fplugin GHC.TypeLits.Normalise #-}++-----------------------------------------------------------------------------+-- |+-- Module      :  Mezzo.Compose.Combine+-- Description :  Music combinators+-- Copyright   :  (c) Dima Szamozvancev+-- License     :  MIT+--+-- Maintainer  :  ds709@cam.ac.uk+-- Stability   :  experimental+-- Portability :  portable+--+-- Properties and combinators for 'Music' values.+--+-----------------------------------------------------------------------------++module Mezzo.Compose.Combine+    (+    -- * Music properties and padding+      musicDur+    , durToInt+    , duration+    , voices+    , pad+    -- * Melody composition+    , play+    ) where++import Mezzo.Model+import Mezzo.Compose.Basic+import Mezzo.Compose.Builder+import Mezzo.Compose.Types+import Mezzo.Model.Prim+import Mezzo.Model.Types+import Mezzo.Model.Music++import GHC.TypeLits++-------------------------------------------------------------------------------+-- Music properties+-------------------------------------------------------------------------------++-- | Get the duration of a piece of music.+musicDur :: Primitive l => Music (m :: Partiture n l) -> Dur l+musicDur _ = Dur++-- | Convert a duration to an integer.+durToInt :: Primitive d => Dur d -> Int+durToInt = prim++-- | Get the numeric duration of a piece of music.+duration :: Primitive l => Music (m :: Partiture n l) -> Int+duration = durToInt . musicDur++-- | Get the number of voices in a piece of music.+voices :: Music m -> Int+voices (Note r d) = 1+voices (Rest d) = 1+voices (m1 :|: m2) = voices m1+voices (m1 :-: m2) = voices m1 + voices m2+voices (Chord c d) = chordVoices c++-- | Get the number of voices in a chord.+-- Thanks to Michael B. Gale+chordVoices :: forall (n :: Nat) (c :: ChordType n) . Primitive n => Cho c -> Int+chordVoices _ = prim (undefined :: ChordType n) -- Need to get a kind-level variable to the term level++-- | Add an empty voice to the end of a piece of music.+pad :: (HarmConstraints m (FromSilence b), Primitive b) => Music (m :: Partiture (a - 1) b) -> Music ((m +-+ FromSilence b) :: Partiture a b)+pad m = m :-: rest (musicDur m)++-------------------------------------------------------------------------------+-- Melodies+-------------------------------------------------------------------------------++-- | Convert a melody (a sequence of notes and rests) to `Music`.+play :: (Primitive d) => Melody m d -> Music m+play m@(ps :| p)    = case ps of Melody -> mkMelNote m p ; ps' -> play ps' :|: mkMelNote m p+play m@(ps :<<< p)  = case ps of Melody -> mkMelNote m p ; ps' -> play ps' :|: mkMelNote m p+play m@(ps :<< p)   = case ps of Melody -> mkMelNote m p ; ps' -> play ps' :|: mkMelNote m p+play m@(ps :< p)    = case ps of Melody -> mkMelNote m p ; ps' -> play ps' :|: mkMelNote m p+play m@(ps :^ p)    = case ps of Melody -> mkMelNote m p ; ps' -> play ps' :|: mkMelNote m p+play m@(ps :> p)    = case ps of Melody -> mkMelNote m p ; ps' -> play ps' :|: mkMelNote m p+play m@(ps :>> p)   = case ps of Melody -> mkMelNote m p ; ps' -> play ps' :|: mkMelNote m p+play m@(ps :<<. p)  = case ps of Melody -> mkMelNote m p ; ps' -> play ps' :|: mkMelNote m p+play m@(ps :<. p)   = case ps of Melody -> mkMelNote m p ; ps' -> play ps' :|: mkMelNote m p+play m@(ps :^. p)   = case ps of Melody -> mkMelNote m p ; ps' -> play ps' :|: mkMelNote m p+play m@(ps :>. p)   = case ps of Melody -> mkMelNote m p ; ps' -> play ps' :|: mkMelNote m p+play m@(ps :>>. p)  = case ps of Melody -> mkMelNote m p ; ps' -> play ps' :|: mkMelNote m p+play m@(ps :~| p)   = case ps of Melody -> mkMelRest m ; ps' -> play ps'   :|: mkMelRest m+play m@(ps :~<<< p) = case ps of Melody -> mkMelRest m ; ps' -> play ps'   :|: mkMelRest m+play m@(ps :~<< p)  = case ps of Melody -> mkMelRest m ; ps' -> play ps'   :|: mkMelRest m+play m@(ps :~< p)   = case ps of Melody -> mkMelRest m ; ps' -> play ps'   :|: mkMelRest m+play m@(ps :~^ p)   = case ps of Melody -> mkMelRest m ; ps' -> play ps'   :|: mkMelRest m+play m@(ps :~> p)   = case ps of Melody -> mkMelRest m ; ps' -> play ps'   :|: mkMelRest m+play m@(ps :~>> p)  = case ps of Melody -> mkMelRest m ; ps' -> play ps'   :|: mkMelRest m+play m@(ps :~<<. p) = case ps of Melody -> mkMelRest m ; ps' -> play ps'   :|: mkMelRest m+play m@(ps :~<. p)  = case ps of Melody -> mkMelRest m ; ps' -> play ps'   :|: mkMelRest m+play m@(ps :~^. p)  = case ps of Melody -> mkMelRest m ; ps' -> play ps'   :|: mkMelRest m+play m@(ps :~>. p)  = case ps of Melody -> mkMelRest m ; ps' -> play ps'   :|: mkMelRest m+play m@(ps :~>>. p) = case ps of Melody -> mkMelRest m ; ps' -> play ps'   :|: mkMelRest m++-- | Make a note of suitable duration from a root specifier.+mkMelNote :: (IntRep r, Primitive d) => Melody m d -> RootS r -> Music (FromRoot r d)+mkMelNote m p = p (\r -> Note r (melDur m))++-- | Make a rest of suitable duration from a rest specifier.+mkMelRest :: Primitive d => Melody m d -> Music (FromSilence d)+mkMelRest m = r (\_ -> Rest (melDur m))++-- | Alias for the start of the melody.+melody :: Melody (End :-- None) Quarter+melody = Melody++-- | Get the duration of the notes in a melody.+melDur :: Primitive d => Melody m d -> Dur d+melDur _ = Dur
+ src/Mezzo/Compose/Harmonic.hs view
@@ -0,0 +1,74 @@+{-# LANGUAGE TypeInType, TypeApplications, TemplateHaskell, RankNTypes,+    GADTs, ImplicitParams, FlexibleContexts #-}++-----------------------------------------------------------------------------+-- |+-- Module      :  Mezzo.Compose.Harmonic+-- Description :  Harmonic composition units+-- Copyright   :  (c) Dima Szamozvancev+-- License     :  MIT+--+-- Maintainer  :  ds709@cam.ac.uk+-- Stability   :  experimental+-- Portability :  portable+--+-- Literals for chords and progressions.+--+-----------------------------------------------------------------------------++module Mezzo.Compose.Harmonic where++import Mezzo.Model+import Mezzo.Compose.Types+import Mezzo.Compose.Builder+import Mezzo.Compose.Templates+import Mezzo.Compose.Basic++-- * Atomic literals++-- ** Scale degree literals+scaleDegreeLits++-- ** Mode literals+modeLits++-- ** Triad type literals+triTyLits++-- ** Seventh type literals+sevTyLits++_dbl :: TriType t -> SevType (Doubled t)+_dbl t = SevType++-- ** Inversion literals+invLits++-- ** Constructors++-- | Create a new key from a pitch class, accidental and mode.+key :: PC p -> Acc a -> Mod m -> KeyS (Key p a m)+key p a m = KeyS++-- | Create a triad from a root, a triad type and an inversion.+triad :: Root r -> TriType t -> Inv i -> Cho (Triad r t i)+triad r t i = Cho++-- | Create a seventh chord from a root, a triad type and an inversion.+seventh :: Root r -> SevType t -> Inv i -> Cho (SeventhChord r t i)+seventh r t i = Cho++-- * Chord builders++-- ** Triad converters+mkTriConvs++-- ** Seventh chord converters+mkSevConvs++-- ** Doubled triad converters+mkDoubledConvs++-- ** Inversion mutators+inv :: ChorM c (InvertChord c)+inv = constConv Cho
+ src/Mezzo/Compose/Templates.hs view
@@ -0,0 +1,344 @@+{-# LANGUAGE TypeInType, TemplateHaskell, ExplicitForAll, ViewPatterns #-}++-----------------------------------------------------------------------------+-- |+-- Module      :  Mezzo.Compose.Templates+-- Description :  TH templates+-- Copyright   :  (c) Dima Szamozvancev+-- License     :  MIT+--+-- Maintainer  :  ds709@cam.ac.uk+-- Stability   :  experimental+-- Portability :  portable+--+-- Template Haskell functions to generate music literals.+--+-----------------------------------------------------------------------------++module Mezzo.Compose.Templates+    ( pitchClassLits+    , accidentalLits+    , octaveLits+    , mkDurLits+    , mk32ndLits+    , mkPitchLits+    , mkPitchSpecs+    , scaleDegreeLits+    , modeLits+    , triTyLits+    , sevTyLits+    , invLits+    , mkTriConvs+    , mkSevConvs+    , mkDoubledConvs+    ) where++import Mezzo.Model+import Mezzo.Compose.Types+import Mezzo.Compose.Builder++import Language.Haskell.TH+import Language.Haskell.TH.Syntax (sequenceQ)+import Data.Char+import Control.Monad (join)+++-------------------------------------------------------------------------------+-- Literal templates+-------------------------------------------------------------------------------++-- | Generate pitch class literal declarations.+pitchClassLits :: DecsQ+pitchClassLits = genLitDecs pcFormatter "PC" ''PitchClass++-- | Generate accidental literal declarations.+accidentalLits :: DecsQ+accidentalLits = genLitDecs accFormatter "Acc" ''Accidental++-- | Generate octave literal declarations.+octaveLits :: DecsQ+octaveLits = genLitDecs octFormatter "Oct" ''OctaveNum++-- | Generate scale degree literal declarations.+scaleDegreeLits :: DecsQ+scaleDegreeLits = genLitDecs scaDegFormatter "ScaDeg" ''ScaleDegree++-- | Generate mode literal declarations.+modeLits :: DecsQ+modeLits = genLitDecs modeFormatter "Mod" ''Mode -- Might want to extend modes later++-- | Generate triad type literal declarations.+triTyLits :: DecsQ+triTyLits = genLitDecs choTyFormatter "TriType" ''TriadType++-- | Generate seventh type literal declarations.+sevTyLits :: DecsQ+sevTyLits = do+    dcs <- filter (\n -> nameBase n /= "Doubled") <$> getDataCons ''SeventhType+    join <$> traverse (mkSingLit choTyFormatter "SevType") dcs++invLits :: DecsQ+invLits = genLitDecs invFormatter "Inv" ''Inversion++-------------------------------------------------------------------------------+-- Templates and generators+-------------------------------------------------------------------------------++-- | Make a literal value declaration for a singleton with the given format string,+-- singleton name and data constructor.+mkSingLit :: Formatter -> String -> Name -> DecsQ+mkSingLit format sing dataName = do+        tySig <- sigD valName $ appT pcTyCon ty+        dec <- [d| $(valPat) = $(pcDataCon) |]+        return $ tySig : dec+    where+        valName = mkName (format dataName)+        valPat = varP valName+        pcTyCon = conT $ mkName sing+        ty = promotedT dataName+        pcDataCon = conE $ mkName sing++-- | Generate concrete pitch literals for each pitch class, accidental and octave.+mkPitchLits :: DecsQ+mkPitchLits = do+    pcNames <- getDataCons ''PitchClass+    accNames <- getDataCons ''Accidental+    octNames <- getDataCons ''OctaveNum+    let declareVal pc acc oct = do  -- Generates a type signature and value declaration for the specified pitch+            let pcStr = pcFormatter pc+                accStr = shortAccFormatter acc+                octStr = shortOctFormatter oct+                valName = mkName $ pcStr ++ accStr ++ octStr+            tySig <- sigD valName $ [t| Pit (Pitch $(conT pc) $(conT acc) $(conT oct)) |]+            dec <- [d| $(varP valName) = pitch $(varE $ mkName pcStr) $(varE $ mkName (accFormatter acc)) $(varE $ mkName (octFormatter oct)) |]+            return $ tySig : dec+    join <$> sequence (declareVal <$> pcNames <*> accNames <*> octNames)    -- Every combination of PCs, Accs and Octs++mkDurLits :: Name -> DecsQ+mkDurLits name = do+    let litName = mkName $ durLitFormatter name+        litName' = mkName $ (durLitFormatter name ++ "\'")+    literal <- do+            tySig1 <- sigD litName $ [t| Dur $(conT name) |]+            dec1 <- [d| $(varP litName) = Dur |]+            tySig1' <- sigD litName' $ [t| Dur (Dot $(conT name)) |]+            dec1' <- [d| $(varP litName') = Dur |]+            return $ tySig1 : dec1 ++ tySig1' : dec1'+    noteTerm <- do+            let valName = mkName $ head (durLitFormatter name) : "n"+            tySig2 <- sigD valName $ [t| forall r. IntRep r => RootT r $(conT name) |]+            dec2 <- [d| $(varP valName) = \p -> Note p $(varE litName) |]+            let valName' = mkName $ head (durLitFormatter name) : "n\'"+            tySig2' <- sigD valName' $ [t| forall r. IntRep r => RootT r (Dot $(conT name)) |]+            dec2' <- [d| $(varP valName') = \p -> Note p $(varE litName') |]+            return $ tySig2 : dec2 ++ tySig2' : dec2'+    restTerm <- do+            let valName = mkName $ head (durLitFormatter name) : "r"+            tySig2 <- sigD valName $ [t| RestT $(conT name) |]+            dec2 <- [d| $(varP valName) = const (Rest $(varE litName)) |]+            let valName' = mkName $ head (durLitFormatter name) : "r\'"+            tySig2' <- sigD valName' $ [t| RestT (Dot $(conT name)) |]+            dec2' <- [d| $(varP valName') = const (Rest $(varE litName')) |]+            return $ tySig2 : dec2 ++ tySig2' : dec2'+    chordTerm <- do+            let valName = mkName $ head (durLitFormatter name) : "c"+            tySig2 <- sigD valName $ [t| forall n r. (Primitive n, IntListRep r) => ChorT (r :: ChordType n) $(conT name) |]+            dec2 <- [d| $(varP valName) = \c -> Chord c $(varE litName) |]+            let valName' = mkName $ head (durLitFormatter name) : "c\'"+            tySig2' <- sigD valName' $ [t| forall n r. (Primitive n, IntListRep r) => ChorT (r :: ChordType n) (Dot $(conT name)) |]+            dec2' <- [d| $(varP valName') = \c -> Chord c $(varE litName') |]+            return $ tySig2 : dec2 ++ tySig2' : dec2'+    return $ literal ++ noteTerm ++ restTerm ++ chordTerm++mk32ndLits :: DecsQ -- Don't want to make dotted literals for thirty second notes.+mk32ndLits = do+    let litName = mkName $ "th"+    literal <- do+            tySig1 <- sigD litName $ [t| Dur $(conT ''ThirtySecond) |]+            dec1 <- [d| $(varP litName) = Dur |]+            return $ tySig1 : dec1+    noteTerm <- do+            let valName = mkName $ "tn"+            tySig2 <- sigD valName $ [t| forall r. IntRep r => RootT r $(conT ''ThirtySecond) |]+            dec2 <- [d| $(varP valName) = \p -> Note p $(varE litName) |]+            return $ tySig2 : dec2+    restTerm <- do+            let valName = mkName $ "tr"+            tySig2 <- sigD valName $ [t| RestT $(conT ''ThirtySecond) |]+            dec2 <- [d| $(varP valName) = const (Rest $(varE litName)) |]+            return $ tySig2 : dec2+    chordTerm <- do+            let valName = mkName $ "tc"+            tySig2 <- sigD valName $ [t| forall n r. (Primitive n, IntListRep r) => ChorT (r :: ChordType n) $(conT ''ThirtySecond) |]+            dec2 <- [d| $(varP valName) = \c -> Chord c $(varE litName)  |]+            return $ tySig2 : dec2+    return $ literal ++ noteTerm ++ restTerm ++ chordTerm++-- | Generate pitch root specifiers for earch pitch class, accidental and octave.+-- These allow for combinatorial input with CPS-style durations and modifiers.+mkPitchSpecs :: DecsQ+mkPitchSpecs = do+    pcNames <- getDataCons ''PitchClass+    accNames <- getDataCons ''Accidental+    octNames <- getDataCons ''OctaveNum+    let declareVal pc acc oct = do+            let pcStr = tail $ pcFormatter pc+                accStr = shorterAccFormatter acc+                octStr = shortOctFormatter oct+                valName = mkName $ pcStr ++ accStr ++ octStr+            tySig <- sigD valName $+                [t| RootS (PitchRoot (Pitch $(conT pc) $(conT acc) $(conT oct) )) |]+            dec <- [d| $(varP valName) = spec Root |]+            return $ tySig : dec+    join <$> sequence (declareVal <$> pcNames <*> accNames <*> octNames)++-- | Generate converters from roots to triads, for each triad type.+mkTriConvs :: DecsQ+mkTriConvs = do+    triTyNames <- getDataCons ''TriadType+    let declareFun choTy = do+            let choStr = tail (choTyFormatter choTy)+                valName1 = mkName $ choStr ++ "'"+                valName2 = mkName $ choStr+            tySig1 <- sigD valName1 $+                [t| forall r i. ChorC' Triad r $(conT choTy) i |]+            dec1 <- [d| $(varP valName1) = \i -> constConv Cho |]+            tySig2 <- sigD valName2 $+                [t| forall r. ChorC Triad r $(conT choTy) |]+            dec2 <- [d| $(varP valName2) = constConv Cho |]+            return $ (tySig1 : dec1) ++ (tySig2 : dec2)+    join <$> traverse declareFun triTyNames++-- | Generate converters from roots to seventh chords, for each seventh type.+mkSevConvs :: DecsQ+mkSevConvs = do+    sevTyNames <- filter (\n -> nameBase n /= "Doubled") <$> getDataCons ''SeventhType+    let declareFun choTy = do+            let choStr = tail (choTyFormatter choTy)+                valName1 = mkName $ choStr ++ "'"+                valName2 = mkName $ choStr+            tySig1 <- sigD valName1 $+                [t| forall r i. ChorC' SeventhChord r $(conT choTy) i |]+            dec1 <- [d| $(varP valName1) = \i -> constConv Cho |]+            tySig2 <- sigD valName2 $+                [t| forall r. ChorC SeventhChord r $(conT choTy) |]+            dec2 <- [d| $(varP valName2) = constConv Cho |]+            return $ (tySig1 : dec1) ++ (tySig2 : dec2)+    join <$> traverse declareFun sevTyNames++-- | Generate converters from roots to doubled seventh chords, for each triad type.+mkDoubledConvs :: DecsQ+mkDoubledConvs = do+    triTyNames <- getDataCons ''TriadType+    let declareFun choTy = do+            let choStr = tail (choTyFormatter choTy)+                valName1 = mkName $ choStr ++ "D'"+                valName2 = mkName $ choStr ++ "D"+            tySig1 <- sigD valName1 $+                [t| forall r i. ChorC' SeventhChord r (Doubled $(conT choTy)) i |]+            dec1 <- [d| $(varP valName1) = \i -> constConv Cho |]+            tySig2 <- sigD valName2 $+                [t| forall r. ChorC SeventhChord r (Doubled $(conT choTy)) |]+            dec2 <- [d| $(varP valName2) = constConv Cho |]+            return $ (tySig1 : dec1) ++ (tySig2 : dec2)+    join <$> traverse declareFun triTyNames+++++-------------------------------------------------------------------------------+-- Formatters+-------------------------------------------------------------------------------++-- | Type synonym for a formatter, that specifies how a data constructor name is+-- diplayed as a literal value.+type Formatter = Name -> String++-- | 'PitchClass' formatter.+pcFormatter :: Formatter+pcFormatter pc = '_' : map toLower (nameBase pc)++-- | 'Accidental' formatter.+accFormatter :: Formatter+accFormatter = map toLower . take 2 . nameBase++-- | 'OctaveNum' formatter.+octFormatter :: Formatter+octFormatter oct = 'o' : drop 3 (nameBase oct)++-- | One letter accidental with explicit 'Naturals'.+shortAccFormatter :: Formatter+shortAccFormatter (accFormatter -> "fl") = "f"+shortAccFormatter (accFormatter -> name) = [head name]++-- | One letter accidental with implicit 'Naturals'.+shorterAccFormatter :: Formatter+shorterAccFormatter (shortAccFormatter -> "n") = ""+shorterAccFormatter (shortAccFormatter -> name) = name++-- | Symbolic suffix format for octaves.+shortOctFormatter :: Formatter+shortOctFormatter name = case nameBase name of+    "Oct_1" -> "_5"+    "Oct0"  -> "_4"+    "Oct1"  -> "_3"+    "Oct2"  -> "__"+    "Oct3"  -> "_"+    "Oct4"  -> ""+    "Oct5"  -> "'"+    "Oct6"  -> "''"+    "Oct7"  -> "'3"+    "Oct8"  -> "'4"++-- | Formatter for duration literals.+durLitFormatter :: Formatter+durLitFormatter = map toLower . take 2 . nameBase++-- | Formatter for pitch literals.+pitchLitFormatter :: Name -> Name -> Name -> String+pitchLitFormatter pc acc oct = pcFormatter pc ++ shortAccFormatter acc ++ shortOctFormatter oct++-- | Formatter for scale degrees.+scaDegFormatter :: Formatter+scaDegFormatter name = "_" ++ map toLower (nameBase name)++-- | Formatter for key modes.+modeFormatter :: Formatter+modeFormatter (nameBase -> name) = map toLower (take 3 name) ++ dropWhile isLower (tail name)++-- | Formatter for chords types.+choTyFormatter :: Formatter+choTyFormatter n = case nameBase n of+    "MajTriad"       -> "_maj"+    "MinTriad"       -> "_min"+    "AugTriad"       -> "_aug"+    "DimTriad"       -> "_dim"+    "MajSeventh"     -> "_maj7"+    "MajMinSeventh"  -> "_sev"+    "MinSeventh"     -> "_min7"+    "HalfDimSeventh" -> "_hdim7"+    "DimSeventh"     -> "_dim7"++-- | Formatter for inversions.+invFormatter :: Formatter+invFormatter (nameBase -> name) = "i" ++ [last name]++-------------------------------------------------------------------------------+-- Auxiliary functions+-------------------------------------------------------------------------------++-- | Get the data constructors of a type.+getDataCons :: Name -> Q [Name]+getDataCons tyName = do+    TyConI (DataD _ _ _ _ dcs _) <- reify tyName+    return $ reverse $ map (\(NormalC pc _) -> pc) dcs++-- | Map a function generating declarations from a data constructor to all+-- data constructors of a type.+mapToDataCons :: (Name -> DecsQ) -> Name -> DecsQ+mapToDataCons f tyName = do+    dcNames <- getDataCons tyName+    join <$> traverse f dcNames++genLitDecs :: Formatter -> String -> Name -> DecsQ+genLitDecs format singName name = mapToDataCons (mkSingLit format singName) name
+ src/Mezzo/Compose/Types.hs view
@@ -0,0 +1,172 @@+{-# LANGUAGE TypeInType, TypeOperators, GADTs, TypeFamilies, MultiParamTypeClasses,+    FlexibleInstances, UndecidableInstances, ScopedTypeVariables, FlexibleContexts, RankNTypes #-}++{-# OPTIONS_GHC -fplugin GHC.TypeLits.Normalise #-}++-----------------------------------------------------------------------------+-- |+-- Module      :  Mezzo.Compose.Types+-- Description :  Common types+-- Copyright   :  (c) Dima Szamozvancev+-- License     :  MIT+--+-- Maintainer  :  ds709@cam.ac.uk+-- Stability   :  experimental+-- Portability :  portable+--+-- Types used by the composition library.+--+-----------------------------------------------------------------------------++module Mezzo.Compose.Types+    (+    -- * Duration type synonyms+      Whole+    , Half+    , Quarter+    , Eighth+    , Sixteenth+    , ThirtySecond+    -- * Melody+    , Melody (..)+    )+    where++import Mezzo.Model+import Mezzo.Model.Prim++import Mezzo.Compose.Builder++import Data.Kind+import GHC.TypeLits++infixl 5 :|+infixl 5 :<<<+infixl 5 :<<+infixl 5 :<+infixl 5 :^+infixl 5 :>+infixl 5 :>>+infixl 5 :<<.+infixl 5 :<.+infixl 5 :^.+infixl 5 :>.+infixl 5 :>>.+infixl 5 :~|+infixl 5 :~<<<+infixl 5 :~<<+infixl 5 :~<+infixl 5 :~^+infixl 5 :~>+infixl 5 :~>>+infixl 5 :~<<.+infixl 5 :~<.+infixl 5 :~^.+infixl 5 :~>.+infixl 5 :~>>.++-------------------------------------------------------------------------------+-- Duration type synonyms+-------------------------------------------------------------------------------++-- | Whole note duration.+type Whole = 32++-- | Half note duration.+type Half = 16++-- | Quarter note duration.+type Quarter = 8++-- | Eighth note duration.+type Eighth = 4++-- | Sixteenth note duration.+type Sixteenth = 2++-- | Thirty-second note duration.+type ThirtySecond = 1++-------------------------------------------------------------------------------+-- Musical lists+-------------------------------------------------------------------------------++-- | Single-voice melody: gives an easy way to input notes and rests of different lengths.+data Melody :: forall l. Partiture 1 l -> Nat -> Type where+    -- | Start a new melody. If the first note duration is not specified ('(:|)' is used),+    -- the default duration is a quarter.+    Melody  :: Melody (End :-- None) Quarter+    -- | Add a note with the same duration as the previous one.+    (:|)    :: (MelConstraints ms (FromRoot r d), IntRep r, Primitive d)+           => Melody ms d -> RootS r -> Melody (ms +|+ FromRoot r d) d+    -- | Add a thirty-second note.+    (:<<<)  :: (MelConstraints ms (FromRoot r ThirtySecond), IntRep r, Primitive d)+           => Melody ms d -> RootS r -> Melody (ms +|+ FromRoot r ThirtySecond) ThirtySecond+    -- | Add a sixteenth note.+    (:<<)   :: (MelConstraints ms (FromRoot r Sixteenth), IntRep r, Primitive d)+           => Melody ms d -> RootS r -> Melody (ms +|+ FromRoot r Sixteenth) Sixteenth+    -- | Add an eighth note.+    (:<)    :: (MelConstraints ms (FromRoot r Eighth), IntRep r, Primitive d)+           => Melody ms d -> RootS r -> Melody (ms +|+ FromRoot r Eighth) Eighth+    -- | Add a quarter note.+    (:^)    :: (MelConstraints ms (FromRoot r Quarter), IntRep r, Primitive d)+           => Melody ms d -> RootS r -> Melody (ms +|+ FromRoot r Quarter) Quarter+    -- | Add a half note.+    (:>)    :: (MelConstraints ms (FromRoot r Half), IntRep r, Primitive d)+           => Melody ms d -> RootS r -> Melody (ms +|+ FromRoot r Half) Half+    -- | Add a whole note.+    (:>>)   :: (MelConstraints ms (FromRoot r Whole), IntRep r, Primitive d)+           => Melody ms d -> RootS r -> Melody (ms +|+ FromRoot r Whole) Whole+    -- | Add a dotted sixteenth note.+    (:<<.)  :: (MelConstraints ms (FromRoot r (Dot Sixteenth)), IntRep r, Primitive d)+           => Melody ms d -> RootS r -> Melody (ms +|+ FromRoot r (Dot Sixteenth)) (Dot Sixteenth)+    -- | Add a dotted eighth note.+    (:<.)   :: (MelConstraints ms (FromRoot r (Dot Eighth)), IntRep r, Primitive d)+           => Melody ms d -> RootS r -> Melody (ms +|+ FromRoot r (Dot Eighth)) (Dot Eighth)+    -- | Add a dotted quarter note.+    (:^.)   :: (MelConstraints ms (FromRoot r (Dot Quarter)), IntRep r, Primitive d)+           => Melody ms d -> RootS r -> Melody (ms +|+ FromRoot r (Dot Quarter)) (Dot Quarter)+    -- | Add a dotted half note.+    (:>.)   :: (MelConstraints ms (FromRoot r (Dot Half)), IntRep r, Primitive d)+           => Melody ms d -> RootS r -> Melody (ms +|+ FromRoot r (Dot Half)) (Dot Half)+    -- | Add a dotted whole note.+    (:>>.)  :: (MelConstraints ms (FromRoot r (Dot Whole)), IntRep r, Primitive d)+           => Melody ms d -> RootS r -> Melody (ms +|+ FromRoot r (Dot Whole)) (Dot Whole)+    -- | Add a rest with the same duration as the previous one.+    (:~|)   :: (MelConstraints ms (FromSilence d), Primitive d)+           => Melody ms d -> RestS -> Melody (ms +|+ FromSilence d) d+    -- | Add a thirty-second rest.+    (:~<<<) :: (MelConstraints ms (FromSilence ThirtySecond), Primitive d)+           => Melody ms d -> RestS -> Melody (ms +|+ FromSilence ThirtySecond) ThirtySecond+    -- | Add a sixteenth rest.+    (:~<<)  :: (MelConstraints ms (FromSilence Sixteenth), Primitive d)+           => Melody ms d -> RestS -> Melody (ms +|+ FromSilence Sixteenth) Sixteenth+    -- | Add an eighth rest.+    (:~<)   :: (MelConstraints ms (FromSilence Eighth), Primitive d)+           => Melody ms d -> RestS -> Melody (ms +|+ FromSilence Eighth) Eighth+    -- | Add a quarter rest.+    (:~^)   :: (MelConstraints ms (FromSilence Quarter), Primitive d)+           => Melody ms d -> RestS -> Melody (ms +|+ FromSilence Quarter) Quarter+    -- | Add a half rest.+    (:~>)   :: (MelConstraints ms (FromSilence Half), Primitive d)+           => Melody ms d -> RestS -> Melody (ms +|+ FromSilence Half) Half+    -- | Add a whole rest.+    (:~>>)  :: (MelConstraints ms (FromSilence Whole), Primitive d)+           => Melody ms d -> RestS -> Melody (ms +|+ FromSilence Whole) Whole+    -- | Add a dotted sixteenth rest.+    (:~<<.) :: (MelConstraints ms (FromSilence (Dot Sixteenth)), Primitive d)+           => Melody ms d -> RestS -> Melody (ms +|+ FromSilence (Dot Sixteenth)) (Dot Sixteenth)+    -- | Add a dotted eighth rest.+    (:~<.)  :: (MelConstraints ms (FromSilence (Dot Eighth)), Primitive d)+           => Melody ms d -> RestS -> Melody (ms +|+ FromSilence (Dot Eighth)) (Dot Eighth)+    -- | Add a dotted quarter rest.+    (:~^.)  :: (MelConstraints ms (FromSilence (Dot Quarter)), Primitive d)+           => Melody ms d -> RestS -> Melody (ms +|+ FromSilence (Dot Quarter)) (Dot Quarter)+    -- | Add a dotted half rest.+    (:~>.)  :: (MelConstraints ms (FromSilence (Dot Half)), Primitive d)+           => Melody ms d -> RestS -> Melody (ms +|+ FromSilence (Dot Half)) (Dot Half)+    -- | Add a dotted whole rest.+    (:~>>.) :: (MelConstraints ms (FromSilence (Dot Whole)), Primitive d)+           => Melody ms d -> RestS -> Melody (ms +|+ FromSilence (Dot Whole)) (Dot Whole)++-- raiseByOct :: Melody m d -> Melody (RaiseAllByOct m) d
+ src/Mezzo/Model.hs view
@@ -0,0 +1,55 @@++-----------------------------------------------------------------------------+-- |+-- Module      :  Mezzo.Model+-- Description :  Mezzo music model+-- Copyright   :  (c) Dima Szamozvancev+-- License     :  MIT+--+-- Maintainer  :  ds709@cam.ac.uk+-- Stability   :  experimental+-- Portability :  portable+--+-- Module providing the external interface to the Mezzo type-level music model.+--+-----------------------------------------------------------------------------++module Mezzo.Model (module X) where++-- Uses import/export shortcut as suggested by HLint.++import Mezzo.Model.Types as X+    (+      PitchClass (..)+    , Accidental (..)+    , OctaveNum (..)+    , Duration (..)+    , PC (..)+    , Acc (..)+    , Oct (..)+    , Dur (..)+    , PitchType (..)+    , Pit (..)+    , Mode (..)+    , ScaleDegree (..)+    , KeyType (..)+    , RootType (..)+    , Mod (..)+    , ScaDeg (..)+    , KeyS (..)+    , Root (..)+    , RootToPitch+    , PitchToNat+    , Sharpen+    , Flatten+    , Dot+    , FromRoot+    , FromSilence+    , Voice+    , Partiture+    , RaiseAllByOct+    )+import Mezzo.Model.Harmony.Chords as X+import Mezzo.Model.Harmony.Functional as X+import Mezzo.Model.Music as X+import Mezzo.Model.Reify as X
+ src/Mezzo/Model/Harmony/Chords.hs view
@@ -0,0 +1,242 @@+{-# LANGUAGE  TypeInType, UndecidableInstances, GADTs, TypeOperators,+    TypeApplications, TypeFamilies, ScopedTypeVariables, FlexibleInstances #-}+{-# OPTIONS_GHC -fplugin GHC.TypeLits.Normalise #-}++-----------------------------------------------------------------------------+-- |+-- Module      :  Mezzo.Model.Harmony.Chords+-- Description :  Models of chords+-- Copyright   :  (c) Dima Szamozvancev+-- License     :  MIT+--+-- Maintainer  :  ds709@cam.ac.uk+-- Stability   :  experimental+-- Portability :  portable+--+-- Types and type functions modelling harmonic chords.+--+-----------------------------------------------------------------------------++module Mezzo.Model.Harmony.Chords+    (+    -- * Chords+      TriadType (..)+    , SeventhType (..)+    , Inversion (..)+    , TriType (..)+    , SevType (..)+    , Inv (..)+    , InvertChord+    , ChordType (..)+    , Cho (..)+    , FromChord+    , ChordsToPartiture+    ) where++import GHC.TypeLits+import Data.Kind (Type)++import Mezzo.Model.Types+import Mezzo.Model.Prim+import Mezzo.Model.Reify++-------------------------------------------------------------------------------+-- Chords+-------------------------------------------------------------------------------++-- | The type of a triad.+data TriadType = MajTriad | MinTriad | AugTriad | DimTriad++-- | The type of a seventh chord.+data SeventhType = MajSeventh | MajMinSeventh | MinSeventh | HalfDimSeventh | DimSeventh | Doubled TriadType++-- | The inversion of a chord.+data Inversion = Inv0 | Inv1 | Inv2 | Inv3++-- | The singleton type for 'TriadType'.+data TriType (t :: TriadType) = TriType++-- | The singleton type for 'SeventhType'.+data SevType (t :: SeventhType) = SevType++-- | The singleton type for 'Inversion'.+data Inv (t :: Inversion) = Inv++-- | A chord type, indexed by the number of notes.+data ChordType :: Nat -> Type where+    Triad :: RootType -> TriadType   -> Inversion -> ChordType 3+    SeventhChord :: RootType -> SeventhType -> Inversion -> ChordType 4++data Cho (c :: ChordType n) = Cho++-- | Convert a triad type to a list of intervals between the individual pitches.+type family TriadTypeToIntervals (t :: TriadType) :: Vector IntervalType 3 where+    TriadTypeToIntervals MajTriad =+                Interval Perf Unison :-- Interval Maj Third :-- Interval Perf Fifth :-- None+    TriadTypeToIntervals MinTriad =+                Interval Perf Unison :-- Interval Min Third :-- Interval Perf Fifth :-- None+    TriadTypeToIntervals AugTriad =+                Interval Perf Unison :-- Interval Maj Third :-- Interval Aug Fifth  :-- None+    TriadTypeToIntervals DimTriad =+                Interval Perf Unison :-- Interval Min Third :-- Interval Dim Fifth  :-- None++-- | Convert a seventh chord type to a list of intervals between the individual pitches.+type family SeventhTypeToIntervals (s :: SeventhType) :: Vector IntervalType 4 where+    SeventhTypeToIntervals MajSeventh     = TriadTypeToIntervals MajTriad :-| Interval Maj Seventh+    SeventhTypeToIntervals MajMinSeventh  = TriadTypeToIntervals MajTriad :-| Interval Min Seventh+    SeventhTypeToIntervals MinSeventh     = TriadTypeToIntervals MinTriad :-| Interval Min Seventh+    SeventhTypeToIntervals HalfDimSeventh = TriadTypeToIntervals DimTriad :-| Interval Min Seventh+    SeventhTypeToIntervals DimSeventh     = TriadTypeToIntervals DimTriad :-| Interval Dim Seventh+    SeventhTypeToIntervals (Doubled tt)   = TriadTypeToIntervals tt       :-| Interval Perf Octave++-- | Apply an inversion to a list of pitches.+type family Invert (i :: Inversion) (n :: Nat) (ps :: Vector PitchType n) :: Vector PitchType n where+    Invert Inv0 n ps         = ps+    -- Need awkward workarounds because of #12564.+    Invert Inv1 n (p :-- ps) = ps :-| RaiseByOct p+    Invert Inv2 n (p :-- ps) = Invert Inv1 (n - 1) (p :-- Tail' ps) :-| RaiseByOct (Head' ps)+    Invert Inv3 n (p :-- ps) = Invert Inv2 (n - 1) (p :-- (Head' (Tail' ps)) :-- (Tail' (Tail' (ps)))) :-| RaiseByOct (Head' ps)++-- | Invert a doubled triad chord.+type family InvertDoubled (i :: Inversion) (ps :: Vector PitchType 4) :: Vector PitchType 4 where+    InvertDoubled Inv0 ps = ps+    InvertDoubled Inv1 ps = Invert Inv1 3 (Init' ps) :-| (RaiseByOct (Head' (Tail' ps)))+    InvertDoubled Inv2 ps = Invert Inv2 3 (Init' ps) :-| (RaiseByOct (Head' (Tail' (Tail' ps))))+    InvertDoubled Inv3 ps = RaiseAllBy' ps (Interval Perf Octave)++type family InvSucc (i :: Inversion) :: Inversion where+    InvSucc Inv0 = Inv1+    InvSucc Inv1 = Inv2+    InvSucc Inv2 = Inv3+    InvSucc Inv3 = Inv0++type family InvertChord (c :: ChordType n) :: ChordType n where+    InvertChord (Triad r t Inv2) = Triad r t Inv0+    InvertChord (Triad r t i) = Triad r t (InvSucc i)+    InvertChord (SeventhChord r t i) = SeventhChord r t (InvSucc i)++-- | Build a list of pitches with the given intervals starting from a root.+type family BuildOnRoot (r :: RootType) (is :: Vector IntervalType n) :: Vector PitchType n where+    BuildOnRoot (PitchRoot Silence) _    = TypeError (Text "Can't build a chord on a rest.")+    BuildOnRoot r None       = None+    BuildOnRoot r (i :-- is) = RaiseBy (RootToPitch r) i :-- BuildOnRoot r is++-- | Convert a chord to a list of constituent pitches.+type family ChordToPitchList (c :: ChordType n) :: Vector PitchType n  where+    ChordToPitchList (Triad        r t i) = Invert i 3 (BuildOnRoot r (TriadTypeToIntervals t))+    ChordToPitchList (SeventhChord r (Doubled tt) i)+                                          = InvertDoubled i (BuildOnRoot r (SeventhTypeToIntervals (Doubled tt)))+    ChordToPitchList (SeventhChord r t i) = Invert i 4 (BuildOnRoot r (SeventhTypeToIntervals t))++-- | Convert a chord to a partiture with the given length (one voice for each pitch).+type family FromChord (c :: ChordType n) (l :: Nat) :: Partiture n l where+    FromChord c l = VectorToColMatrix (ChordToPitchList c) l++type family ChordsToPartiture (v :: Vector (ChordType n) l) (d :: Nat) :: Partiture n (l * d) where+    ChordsToPartiture None l = None+    ChordsToPartiture (c :-- cs) d = FromChord c d +|+ ChordsToPartiture cs d++-------------------------------------------------------------------------------+-- Primitive instances+-------------------------------------------------------------------------------++-- Chord types+instance Primitive MajTriad where+    type Rep MajTriad = Int -> [Int]+    prim t = \r -> [r, r + 4, r + 7]+    pretty t = "Maj"++instance Primitive MinTriad where+    type Rep MinTriad = Int -> [Int]+    prim t = \r -> [r, r + 3, r + 7]+    pretty t = "min"++instance Primitive AugTriad where+    type Rep AugTriad = Int -> [Int]+    prim t = \r -> [r, r + 4, r + 8]+    pretty t = "aug"++instance Primitive DimTriad where+    type Rep DimTriad = Int -> [Int]+    prim t = \r -> [r, r + 3, r + 6]+    pretty t = "dim"++instance Primitive MajSeventh where+    type Rep MajSeventh = Int -> [Int]+    prim t = \r -> [r, r + 4, r + 7, r + 11]+    pretty t = "Maj7"++instance Primitive MajMinSeventh where+    type Rep MajMinSeventh = Int -> [Int]+    prim t = \r -> [r, r + 4, r + 7, r + 10]+    pretty t = "7"++instance Primitive MinSeventh where+    type Rep MinSeventh = Int -> [Int]+    prim t = \r -> [r, r + 3, r + 7, r + 10]+    pretty t = "min7"++instance Primitive HalfDimSeventh where+    type Rep HalfDimSeventh = Int -> [Int]+    prim t = \r -> [r, r + 3, r + 6, r + 10]+    pretty t = "hdim7"++instance Primitive DimSeventh where+    type Rep DimSeventh = Int -> [Int]+    prim t = \r -> [r, r + 3, r + 6, r + 9]+    pretty t = "dim7"++instance FunRep Int [Int] c => Primitive (Doubled c) where+    type Rep (Doubled c) = Int -> [Int]+    prim t = \r -> prim (TriType @c) r ++ [r + 12]+    pretty t = pretty (TriType @c) ++ "D"++-- Inversions+-- Places the first element of the list on its end.+invChord :: [Int] -> [Int]+invChord [] = []+invChord (x : xs) = xs ++ [x + 12]++instance Primitive Inv0 where+    type Rep Inv0 = [Int] -> [Int]+    prim i = id+    pretty i = "I0"++instance Primitive Inv1 where+    type Rep Inv1 = [Int] -> [Int]+    prim i = invChord+    pretty i = "I1"++instance Primitive Inv2 where+    type Rep Inv2 = [Int] -> [Int]+    prim i = invChord . invChord+    pretty i = "I2"++instance Primitive Inv3 where+    type Rep Inv3 = [Int] -> [Int]+    prim i = invChord . invChord . invChord+    pretty i = "I3"++instance (IntRep r, FunRep Int [Int] t, FunRep [Int] [Int] i)+        => Primitive (Triad r t i) where+    type Rep (Triad r t i) = [Int]+    prim c = prim (Inv @i) . prim (TriType @t) $ prim (Root @r)+    pretty c = pc ++ " " ++ pretty (TriType @t) ++ " " ++ pretty (Inv @i)+        where pc = takeWhile (\c -> c /= ' ' && c /= '\'' && c /= '_') $ pretty (Root @r)++instance (IntRep r, FunRep Int [Int] tt, FunRep [Int] [Int] i)+        => Primitive (SeventhChord r (Doubled tt) i) where+    type Rep (SeventhChord r (Doubled tt) i) = [Int]+    prim c = inverted ++ [head inverted + 12]+        where rootPos = prim (TriType @tt) $ prim (Root @r)+              inverted = prim (Inv @i) rootPos+    pretty c = pc ++ " " ++ pretty (TriType @tt) ++ "D " ++ pretty (Inv @i)+        where pc = takeWhile (\c -> c /= ' ' && c /= '\'' && c /= '_') $ pretty (Root @r)+++instance {-# OVERLAPPABLE #-} (IntRep r, FunRep Int [Int] t, FunRep [Int] [Int] i)+        => Primitive (SeventhChord r t i) where+    type Rep (SeventhChord r t i) = [Int]+    prim c = prim (Inv @i) . prim (SevType @t) $ prim (Root @r)+    pretty c = pc ++ " " ++ pretty (SevType @t) ++ " " ++ pretty (Inv @i)+        where pc = takeWhile (\c -> c /= ' ' && c /= '\'' && c /= '_') $ pretty (Root @r)
+ src/Mezzo/Model/Harmony/Functional.hs view
@@ -0,0 +1,217 @@+{-# LANGUAGE  TypeInType, MultiParamTypeClasses, FlexibleInstances,+    UndecidableInstances, GADTs, TypeOperators, TypeFamilies, FlexibleContexts #-}+{-# OPTIONS_GHC -fplugin GHC.TypeLits.Normalise #-}++-----------------------------------------------------------------------------+-- |+-- Module      :  Mezzo.Model.Harmony.Functional+-- Description :  Models of functional harmony+-- Copyright   :  (c) Dima Szamozvancev+-- License     :  MIT+--+-- Maintainer  :  ds709@cam.ac.uk+-- Stability   :  experimental+-- Portability :  portable+--+-- Types and type functions modelling principles of functional harmony.+--+-----------------------------------------------------------------------------++module Mezzo.Model.Harmony.Functional+    (+      Quality (..)+    , Degree (..)+    , Piece (..)+    , Phrase (..)+    , Cadence (..)+    , Tonic (..)+    , Dominant (..)+    , Subdominant (..)+    , PieceToChords+    )+    where++import GHC.TypeLits+import Data.Kind++import Mezzo.Model.Types hiding (IntervalClass (..))+import Mezzo.Model.Prim+import Mezzo.Model.Harmony.Chords++-- | The quality of a scale degree chord.+data Quality = MajQ | MinQ | DomQ | DimQ++-- | A scale degree chord in given key, on the given scale, with the given quality.+data Degree (d :: ScaleDegree) (q :: Quality) (k :: KeyType) (i :: Inversion) where+    DegChord :: Degree d q k i++-- | Ensure that the degree and quality match the mode.+class DiatonicDegree (d :: ScaleDegree) (q :: Quality) (k :: KeyType)+instance MajDegQuality d q => DiatonicDegree d q (Key pc acc MajorMode)+instance MinDegQuality d q => DiatonicDegree d q (Key pc acc MinorMode)++-- | Ensure that the degree and quality are valid in major mode.+class MajDegQuality (d :: ScaleDegree) (q :: Quality)+instance {-# OVERLAPPING #-} MajDegQuality I MajQ+instance {-# OVERLAPPING #-} MajDegQuality II MinQ+instance {-# OVERLAPPING #-} MajDegQuality II DomQ  -- Secondary dominant+instance {-# OVERLAPPING #-} MajDegQuality III MinQ+instance {-# OVERLAPPING #-} MajDegQuality IV MajQ+instance {-# OVERLAPPING #-} MajDegQuality V MajQ+instance {-# OVERLAPPING #-} MajDegQuality V DomQ+instance {-# OVERLAPPING #-} MajDegQuality VI MinQ+instance {-# OVERLAPPING #-} MajDegQuality VII DimQ+instance {-# OVERLAPPABLE #-} TypeError (Text "Can't have a "+                                    :<>: ShowQual q+                                    :<>: ShowDeg d+                                    :<>: Text " degree chord in major mode.")+                                => MajDegQuality d q++-- | Ensure that the degree and quality are valid in minor mode.+class MinDegQuality (d :: ScaleDegree) (q :: Quality)+instance {-# OVERLAPPING #-} MinDegQuality I MinQ+instance {-# OVERLAPPING #-} MinDegQuality II DimQ+instance {-# OVERLAPPING #-} MinDegQuality II DomQ  -- Secondary dominant+instance {-# OVERLAPPING #-} MinDegQuality III MajQ+instance {-# OVERLAPPING #-} MinDegQuality IV MinQ+instance {-# OVERLAPPING #-} MinDegQuality V MajQ+instance {-# OVERLAPPING #-} MinDegQuality V DomQ+instance {-# OVERLAPPING #-} MinDegQuality VI MajQ+instance {-# OVERLAPPING #-} MinDegQuality VII MajQ+instance {-# OVERLAPPABLE #-} TypeError (Text "Can't have a "+                                    :<>: ShowType q :<>: Text " "+                                    :<>: ShowType d+                                    :<>: Text " degree chord in minor mode.")+                                => MinDegQuality d q++-- | A functionally described piece of music, built from multiple phrases.+data Piece (k :: KeyType) (l :: Nat) where+    Cad :: Cadence k l -> Piece k l+    (:=) :: Phrase k l -> Piece k (n - l) -> Piece k n++-- | A phrase matching a specific functional progression.+data Phrase (k :: KeyType) (l :: Nat) where+    -- | A tonic-dominant-tonic progression.+    PhraseIVI :: Tonic k (l2 - l1) -> Dominant k l1 -> Tonic k (l - l2) -> Phrase k l+    -- | A dominant-tonic progression.+    PhraseVI  :: Dominant k l1 -> Tonic k (l - l1) -> Phrase k l++-- | A cadence in a specific key with a specific length.+data Cadence (k :: KeyType) (l :: Nat) where+    -- | Authentic cadence with major fifth chord.+    AuthCad    :: Degree V MajQ k Inv1 -> Degree I q k Inv0 -> Cadence k 2+    -- | Authentic cadence with dominant seventh fifth chord.+    AuthCad7   :: Degree V DomQ k Inv2 -> Degree I q k Inv0 -> Cadence k 2+    -- | Authentic cadence with diminished seventh chord.+    AuthCadVii :: Degree VII DimQ k Inv0 -> Degree I q k Inv0 -> Cadence k 2+    -- | Authentic cadence with a cadential 6-4 chord+    AuthCad64  :: Degree I MajQ k Inv2 -> Degree V DomQ k Inv3 -> Degree I MajQ k Inv1 -> Cadence k 3+    -- | Half cadence ending with a major fifth chord.+    HalfCad    :: Degree d q k i -> Degree V MajQ k Inv0 -> Cadence k 2+    -- | Deceptive cadence from a dominant fifth to a sixth.+    DeceptCad  :: Degree V DomQ k Inv0 -> Degree VI q k Inv2 -> Cadence k 2++-- | A tonic chord.+data Tonic (k :: KeyType) (l :: Nat) where+    -- | A major tonic chord.+    TonMaj :: Degree I MajQ k Inv0 -> Tonic k 1 -- Temporarily (?) allow only no inversion+    -- | A minor tonic chord.+    TonMin :: Degree I MinQ k Inv0 -> Tonic k 1++class NotInv2 (i :: Inversion)+instance NotInv2 Inv0+instance TypeError (Text "Can't have a tonic in second inversion.") => NotInv2 Inv2+instance NotInv2 Inv1+instance NotInv2 Inv3++-- | A dominant chord progression.+data Dominant (k :: KeyType) (l :: Nat) where+    -- | Major fifth dominant.+    DomVM   :: Degree V MajQ k i -> Dominant k 1+    -- | Seventh chord fifth degree dominant.+    DomV7   :: Degree V DomQ k i -> Dominant k 1+    -- | Diminished seventh degree dominant.+    DomVii0 :: Degree VII DimQ k i -> Dominant k 1+    -- | Subdominant followed by dominant.+    DomSD   :: Subdominant k l1 -> Dominant k (l - l1) -> Dominant k l+    -- | Secondary dominant followed by dominant.+    DomSecD :: Degree II DomQ k Inv0 -> Degree V DomQ k Inv2 -> Dominant k 2++-- | A subdominant chord progression.+data Subdominant (k :: KeyType) (l :: Nat) where+    -- | Minor second subdominant.+    SubIIm     :: Degree II MinQ k i -> Subdominant k 1+    -- | Major fourth subdominant.+    SubIVM     :: Degree IV MajQ k i -> Subdominant k 1+    -- | Minor third followed by major fourth subdominant+    SubIIImIVM :: Degree III MinQ k i1 -> Degree IV MajQ k i2 -> Subdominant k 2+    -- | Minor fourth dominant.+    SubIVm     :: Degree IV MinQ k i -> Subdominant k 1++-- | Convert a scale degree to a chord.+type family DegToChord (d :: Degree d q k i) :: ChordType 4 where+    DegToChord (DegChord :: Degree d q k i) = SeventhChord (DegreeRoot k d) (QualToType q) i++-- | Convert a quality to a seventh chord type.+type family QualToType (q :: Quality) :: SeventhType where+    QualToType MajQ = Doubled MajTriad+    QualToType MinQ = Doubled MinTriad+    QualToType DomQ = MajMinSeventh+    QualToType DimQ = DimSeventh++-- | Convert a cadence to chords.+type family CadToChords (c :: Cadence k l) :: Vector (ChordType 4) l where+    CadToChords (AuthCad  d1 d2) = DegToChord d1 :-- DegToChord d2 :-- None+    CadToChords (AuthCad7 d1 d2) = DegToChord d1 :-- DegToChord d2 :-- None+    CadToChords (AuthCadVii d1 d2) = DegToChord d1 :-- DegToChord d2 :-- None+    CadToChords (AuthCad64 d1 d2 d3) = DegToChord d1 :-- DegToChord d2 :-- DegToChord d3 :-- None+    CadToChords (HalfCad d1 d2) = DegToChord d1 :-- DegToChord d2 :-- None+    CadToChords (DeceptCad d1 d2) = DegToChord d1 :-- DegToChord d2 :-- None++-- | Convert a tonic to chords.+type family TonToChords (t :: Tonic k l) :: Vector (ChordType 4) l where+    TonToChords (TonMaj d) = DegToChord d :-- None+    TonToChords (TonMin d) = DegToChord d :-- None++-- | Convert a dominant to chords.+type family DomToChords (l :: Nat) (t :: Dominant k l) :: Vector (ChordType 4) l where+    DomToChords 1 (DomVM d) = DegToChord d :-- None+    DomToChords 1 (DomV7 d) = DegToChord d :-- None+    DomToChords 1 (DomVii0 d) = DegToChord d :-- None+    DomToChords l (DomSD (s :: Subdominant k l1) d) =+                    SubdomToChords s ++. DomToChords (l - l1) d+    DomToChords 2 (DomSecD d1 d2) = DegToChord d1 :-- DegToChord d2 :-- None++-- | Convert a subdominant to chords.+type family SubdomToChords (t :: Subdominant k l) :: Vector (ChordType 4) l where+    SubdomToChords (SubIIm d) = DegToChord d :-- None+    SubdomToChords (SubIVM d) = DegToChord d :-- None+    SubdomToChords (SubIIImIVM d1 d2) = DegToChord d1 :-- DegToChord d2 :-- None+    SubdomToChords (SubIVm d) = DegToChord d :-- None++-- | Convert a phrase to chords.+type family PhraseToChords (l :: Nat) (p :: Phrase k l) :: Vector (ChordType 4) l where+    PhraseToChords l (PhraseIVI t1 (d :: Dominant k dl) t2) = TonToChords t1 ++. DomToChords dl d ++. TonToChords t2+    PhraseToChords l (PhraseVI (d :: Dominant k dl) t) = DomToChords dl d ++. TonToChords t++-- | Convert a piece to chords.+type family PieceToChords (l :: Nat) (p :: Piece k l) :: Vector (ChordType 4) l where+    PieceToChords l (Cad (c :: Cadence k l)) = CadToChords c+    PieceToChords l ((p :: Phrase k l1) := ps) = PhraseToChords l1 p ++. PieceToChords (l - l1) ps++-- | Convert a quality to text.+type family ShowQual (q :: Quality) :: ErrorMessage where+    ShowQual MajQ = Text "major "+    ShowQual MinQ = Text "minor "+    ShowQual DomQ = Text "dominant "+    ShowQual DimQ = Text "diminished "++-- | Convert a degree to text.+type family ShowDeg (d :: ScaleDegree) :: ErrorMessage where+    ShowDeg I = Text "1st"+    ShowDeg II = Text "2nd"+    ShowDeg III = Text "3rd"+    ShowDeg IV = Text "4th"+    ShowDeg V = Text "5th"+    ShowDeg VI = Text "6th"+    ShowDeg VII = Text "7th"
+ src/Mezzo/Model/Harmony/Motion.hs view
@@ -0,0 +1,92 @@+{-# LANGUAGE  TypeInType, MultiParamTypeClasses, FlexibleInstances,+    UndecidableInstances #-}++-----------------------------------------------------------------------------+-- |+-- Module      :  Mezzo.Model.Harmony.Motion+-- Description :  Models of harmonic motion+-- Copyright   :  (c) Dima Szamozvancev+-- License     :  MIT+--+-- Maintainer  :  ds709@cam.ac.uk+-- Stability   :  experimental+-- Portability :  portable+--+-- Classes modelling consonance, dissonance and harmonic motion.+--+-----------------------------------------------------------------------------++module Mezzo.Model.Harmony.Motion+    (+    -- * Consonant and dissonant intervals+      PerfConsonantInterval+    , ImperfConsonantInterval+    , DissonantInterval+    -- * Harmonic motion+    , DirectMotion+    , ContraryMotion+    , ObliqueMotion+    ) where++import GHC.TypeLits++import Mezzo.Model.Types+import Mezzo.Model.Prim++-------------------------------------------------------------------------------+-- Consonant and dissonant intervals+-------------------------------------------------------------------------------++-- | Classifies perfect consonant intervals:+--+--  * Perfect unisons+--  * Perfect fifths+--  * Perfect octaves+class PerfConsonantInterval (i :: IntervalType)+instance PerfConsonantInterval (Interval Perf Unison)+instance PerfConsonantInterval (Interval Perf Fifth)+instance PerfConsonantInterval (Interval Perf Octave)++-- | Classifies imperfect consonant intervals:+--+--  * Major and minor thirds+--  * Major and minor sixths+class ImperfConsonantInterval (i :: IntervalType)+instance ImperfConsonantInterval (Interval Maj Third)+instance ImperfConsonantInterval (Interval Min Third)+instance ImperfConsonantInterval (Interval Maj Sixth)+instance ImperfConsonantInterval (Interval Min Sixth)++-- | Classifies dissonant intervals:+--+--  * Perfect fourth (by common practice convention)+--  * Augmented and diminished intervals+--  * Second and seventh intervals+class DissonantInterval (i :: IntervalType)+instance DissonantInterval (Interval Perf Fourth)+instance DissonantInterval (Interval Aug is)+instance DissonantInterval (Interval Dim is)+instance DissonantInterval (Interval ic Second)+instance DissonantInterval (Interval ic Seventh)++-------------------------------------------------------------------------------+-- Harmonic motion+-------------------------------------------------------------------------------++-- | Ensures that direct motion is permitted between the two intervals.+class DirectMotion (i1 :: IntervalType) (i2 :: IntervalType)+instance {-# OVERLAPPING #-} TypeError (Text "Direct motion into a perfect unison is forbidden.")+                                => DirectMotion i1 (Interval Perf Unison)+instance {-# OVERLAPPING #-} TypeError (Text "Direct motion into a perfect fifth is forbidden.")+                                => DirectMotion i1 (Interval Perf Fifth)+instance {-# OVERLAPPING #-} TypeError (Text "Direct motion into a perfect octave is forbidden.")+                                => DirectMotion i1 (Interval Perf Octave)+instance {-# OVERLAPPABLE #-}      DirectMotion i1 i2++-- | Ensures that contrary motion is permitted between the two intervals.+class ContraryMotion (i1 :: IntervalType) (i2 :: IntervalType)+instance ContraryMotion i1 i2++-- | Ensures that oblique motion is permitted between the two intervals.+class ObliqueMotion (i1 :: IntervalType) (i2 :: IntervalType)+instance ObliqueMotion i1 i2
+ src/Mezzo/Model/Music.hs view
@@ -0,0 +1,303 @@+{-# LANGUAGE TypeInType, RankNTypes, TypeOperators, GADTs, ConstraintKinds,+    FlexibleContexts, MultiParamTypeClasses, TypeFamilies, UndecidableInstances,+    FlexibleInstances #-}+{-# OPTIONS_GHC -fplugin GHC.TypeLits.Normalise #-}++-----------------------------------------------------------------------------+-- |+-- Module      :  Mezzo.Model.Music+-- Description :  Mezzo music algebra+-- Copyright   :  (c) Dima Szamozvancev+-- License     :  MIT+--+-- Maintainer  :  ds709@cam.ac.uk+-- Stability   :  experimental+-- Portability :  portable+--+-- Algebraic description of music with type-level constraints.+--+-----------------------------------------------------------------------------++module Mezzo.Model.Music+    (+    -- * Music+      Music (..)+    , Score (..)+    -- * Harmonic constructs+    , Progression+    -- * Constraints+    , MelConstraints+    , HarmConstraints+    , ChordConstraints+    ) where++import Data.Kind+import GHC.TypeLits+import Text.PrettyPrint.Boxes++import Mezzo.Model.Prim+import Mezzo.Model.Harmony.Motion+import Mezzo.Model.Harmony.Chords+import Mezzo.Model.Harmony.Functional+import Mezzo.Model.Types+import Mezzo.Model.Reify++infixl 4 :|:+infixl 4 :-:++-------------------------------------------------------------------------------+-- The 'Music' datatype+-------------------------------------------------------------------------------++-- | A piece of music consisting of parallel and sequential composition of notes+-- and rests, subject to constraints.+--+-- Currently enforced constraints are:+--+--  * Height (number of voices) of two sequentially composed pieces must be equal.+--  * Width (number of temporal units) of two parallelly composed pieces must be equal.+--  * Sequentially composed voices cannot have any augmented, diminished or seventh leaps.+--  * Parallelly composed pieces cannot have any minor second or major seventh harmonic intervals.+--  * Music must not contain parallel or concealed unisons, fifths or octaves.+--+data Music :: forall n l. Partiture n l -> Type where+    -- | A note specified by a pitch and a duration.+    Note :: NoteConstraints r d => Root r -> Dur d -> Music (FromRoot r d)+    -- | A rest specified by a duration.+    Rest :: RestConstraints d => Dur d -> Music (FromSilence d)+    -- | Sequential or melodic composition of music.+    (:|:) :: MelConstraints m1 m2  => Music m1 -> Music m2 -> Music (m1 +|+ m2)+    -- | Parallel or harmonic composition of music.+    (:-:) :: HarmConstraints m1 m2 => Music m1 -> Music m2 -> Music (m1 +-+ m2)+    -- | A chord specified by a chord type and a duration.+    Chord :: ChordConstraints c d => Cho c -> Dur d -> Music (FromChord c d)+    -- Progression :: ProgressionConstraints p => Prog p -> Music (FromProg p)++-- | A type encapsulating every 'Music' composition.+data Score = forall m. Score (Music m)++-------------------------------------------------------------------------------+-- Harmonic constructs+-- Types and type synonyms constructing 'Music' instances from harmonic types.+-------------------------------------------------------------------------------++-- | A chord progression with the given scheme and chord length.+type Progression (p :: Piece k l) (d :: Nat) = Music (ChordsToPartiture (PieceToChords l p) d)++-------------------------------------------------------------------------------+-- Musical constraints+-- Specifications of the rules that valid musical terms have to follow.+-------------------------------------------------------------------------------++-- | Enable or disable music correctness checking.+type Strict = True++-- | Applies the constraint c if strict checking is enabled.+type IfStrict c = If Strict c Valid++-- | Ensures that the note is valid.+type NoteConstraints r d = (IntRep r, Primitive d)++-- | Ensures that the rest is valid.+type RestConstraints d = (Primitive d)++-- | Ensures that two pieces of music can be composed sequentially.+type MelConstraints (m1 :: Partiture n l1) (m2 :: Partiture n l2) =+        IfStrict (ValidMelConcat m1 m2)++-- | Ensures that two pieces of music can be composed in parallel.+type HarmConstraints m1 m2 = IfStrict (ValidHarmConcat (Align m1 m2))++-- | Ensures that the chord is valid.+type ChordConstraints (c :: ChordType n) d = (IntListRep c, Primitive n, Primitive d)++-- | Ensures that a progression is valid.+type ProgressionConstraints p = Valid++---- Melodic constraints++-- | Ensures that melodic intervals are valid.+--+-- A melodic interval is invalid if it is+--+--  * any augmented interval or+--  * any diminished interval or+--  * any seventh interval.+class ValidMelInterval (i :: IntervalType)+instance {-# OVERLAPPING #-}       ValidMelInterval (Interval Aug Unison)+instance {-# OVERLAPS #-} TypeError (Text "Augmented melodic intervals are not permitted.")+                                => ValidMelInterval (Interval Aug a)+instance {-# OVERLAPS #-} TypeError (Text "Diminished melodic intervals are not permitted.")+                                => ValidMelInterval (Interval Dim a)+instance {-# OVERLAPPING #-} TypeError (Text "Seventh intervals are not permitted in melody.")+                                => ValidMelInterval (Interval a Seventh)+instance {-# OVERLAPPABLE #-}      ValidMelInterval i++-- | Ensures that two pitches form valid melodic leaps.+--+-- Two pitches form valid melodic leaps if+--+--  * at least one of them is silent (i.e. it is a rest) or+--  * they form a valid melodic interval.+class ValidMelLeap (p1 :: PitchType) (p2 :: PitchType)+instance {-# OVERLAPPING #-}  ValidMelLeap Silence Silence+instance {-# OVERLAPPING #-}  ValidMelLeap Silence (Pitch pc acc oct)+instance {-# OVERLAPPING #-}  ValidMelLeap (Pitch pc acc oct) Silence+instance {-# OVERLAPPABLE #-} ValidMelInterval (MakeInterval a b) => ValidMelLeap a b++-- | Ensures that two voices can be appended.+--+-- Two voices can be appended if+--+--  * at least one of them is empty or+--  * the last pitch of the first vector forms a valid melodic leap+--    with the first pitch of the second vector.+class ValidMelAppend (a :: Voice l1) (b :: Voice l2)+instance {-# OVERLAPPING #-}  ValidMelAppend End a+instance {-# OVERLAPPING #-}  ValidMelAppend a End+instance {-# OVERLAPPABLE #-} ValidMelLeap (Last vs1) (Head vs2) => ValidMelAppend vs1 vs2++-- | Ensures that two partitures can be horizontally concatenated.+--+-- Two part lists can be horizontally concatenated if+--+--  * both of them are empty or+--  * all of the voices can be appended.+class ValidMelConcat (ps1 :: Partiture n l1) (ps2 :: Partiture n l2)+instance {-# OVERLAPPING #-}       ValidMelConcat None None+instance {-# OVERLAPPABLE #-} (ValidMelAppend v1 v2, ValidMelConcat vs1 vs2)+                                => ValidMelConcat (v1 :-- vs1) (v2 :-- vs2)+++---- Harmonic constraints++-- | Ensures that harmonic intervals are valid.+--+-- A harmonic interval is invalid if it is+--+--  * a minor second or+--  * a major seventh or+--  * an augmented octave.+class ValidHarmInterval (i :: IntervalType)+instance {-# OVERLAPPING #-} TypeError (Text "Can't have minor seconds in chords.")+                                => ValidHarmInterval (Interval Aug Unison)+instance {-# OVERLAPPING #-} TypeError (Text "Can't have minor seconds in chords.")+                                => ValidHarmInterval (Interval Min Second)+instance {-# OVERLAPPING #-} TypeError (Text "Can't have major sevenths in chords.")+                                => ValidHarmInterval (Interval Maj Seventh)+instance {-# OVERLAPPING #-} TypeError (Text "Can't have major sevenths in chords.")+                                => ValidHarmInterval (Interval Dim Octave)+instance {-# OVERLAPPING #-} TypeError (Text "Can't have augmented octaves in chords.")+                                => ValidHarmInterval (Interval Aug Octave)+instance {-# OVERLAPPABLE #-}      ValidHarmInterval i++-- | Ensures that two pitches form valid harmonic dyad (interval).+--+-- Two pitches form valid harmonic dyads if+--+--  * at least one of them is silent (i.e. it is a rest) or+--  * they form a valid harmonic interval.+class ValidHarmDyad (p1 :: PitchType) (p2 :: PitchType)+instance {-# OVERLAPPING #-}  ValidHarmDyad Silence Silence+instance {-# OVERLAPPING #-}  ValidHarmDyad (Pitch pc acc oct) Silence+instance {-# OVERLAPPING #-}  ValidHarmDyad Silence (Pitch pc acc oct)+instance {-# OVERLAPPABLE #-} ValidHarmInterval (MakeInterval a b) => ValidHarmDyad a b++-- | Ensures that two voices form pairwise valid harmonic dyads.+class ValidHarmDyadsInVectors (v1 :: Voice l) (v2 :: Voice l)+instance AllPairsSatisfy ValidHarmDyad v1 v2 => ValidHarmDyadsInVectors v1 v2++-- | Ensures that two partitures can be vertically concatenated.+--+-- Two partitures can be vertically concatenated if+--+--  * the top one is empty or+--  * all but the first voice can be concatenated, and the first voice+--    forms valid harmonic dyads with every other voice and follows the rules+--    of valid harmonic motion.+class ValidHarmConcat (ps :: (Partiture n1 l, Partiture n2 l))+instance {-# OVERLAPPING #-}       ValidHarmConcat '(None, vs)+instance {-# OVERLAPPABLE #-} ( ValidHarmConcat '(vs, us)+                              , AllSatisfyAll [ ValidHarmDyadsInVectors v+                                              , ValidHarmMotionInVectors v] us)+                                => ValidHarmConcat '((v :-- vs), us)+++---- Voice leading constraints++-- | Ensures that four pitches (representing two consequent intervals) follow+-- the rules for valid harmonic motion.+--+-- Harmonic motion is not permitted if+--+--  * it is direct motion into a perfect interval (this covers parallel and+--    concealed fifths, octaves and unisons).+type family ValidMotion (p1 :: PitchType) (p2 :: PitchType)+                        (q1 :: PitchType) (q2 :: PitchType)+                            :: Constraint where+    ValidMotion Silence _ _ _ = Valid+    ValidMotion _ Silence _ _ = Valid+    ValidMotion _ _ Silence _ = Valid+    ValidMotion _ _ _ Silence = Valid+    ValidMotion p1 p2 q1 q2   =+            If ((p1 .~. q1) .||. (p2 .~. q2))+                (ObliqueMotion (MakeInterval p1 p2) (MakeInterval q1 q2))+                (If (p1 <<? q1)+                    (If (p2 <<? q2)+                        (DirectMotion (MakeInterval p1 p2) (MakeInterval q1 q2))+                        (ContraryMotion (MakeInterval p1 p2) (MakeInterval q1 q2)))+                    (If (p2 <<? q2)+                        (ContraryMotion (MakeInterval p1 p2) (MakeInterval q1 q2))+                        (DirectMotion (MakeInterval p1 p2) (MakeInterval q1 q2))))++-- | Ensures that the interval formed by the first pitch and the last element+-- of the first voice can move to the interval formed by the second+-- pitch and the first element of the second voice.+class ValidMelPitchVectorMotion (p1 :: PitchType) (p2 :: PitchType) (v1 :: Voice l1) (v2 :: Voice l2)+instance {-# OVERLAPPING #-}    ValidMelPitchVectorMotion p1 p2 End End+instance {-# OVERLAPPABLE #-} ValidMotion p1 (Last v1) p2 (Head v2)+                            =>  ValidMelPitchVectorMotion p1 p2 v1 v2+-- Can't have v1 be End and v2 be not End, since if v1 under p1 is not nil, there+-- must be an accompanying voice under p2++-- | Ensures that two partitures follow the rules of motion when+-- horizontally concatenated.+--+-- Two horizontally concatenated partitures follow the rules of harmonic motion if+--+--  * both are empty or+--  * their lower voices can be concatenated and the joining elements of the+--    top voice form intervals with the joining elements of the other voices+--    which follow the rules of harmonic motion.+class ValidMelMatrixMotion (ps1 :: Partiture n l1) (ps2 :: Partiture n l2)+instance {-# OVERLAPPING #-}       ValidMelMatrixMotion None None+instance {-# OVERLAPPABLE #-} ( ValidMelMatrixMotion vs1 vs2+                              , AllPairsSatisfy' (ValidMelPitchVectorMotion (Last v1) (Head v2)) vs1 vs2)+                                => ValidMelMatrixMotion (v1 :-- vs1) (v2 :-- vs2)++-- | Ensures that two voices form pairwise intervals which follow the+-- rules of harmonic motion.+class ValidHarmMotionInVectors (v1 :: Voice l) (v2 :: Voice p)+instance {-# OVERLAPPING #-}       ValidHarmMotionInVectors End End+instance {-# OVERLAPPING #-} ValidHarmMotionInVectors (p :* d1 :- End) (q :* d2 :- End)+instance {-# OVERLAPPABLE #-} ( ValidMotion p q (Head ps) (Head qs)+                              , ValidHarmMotionInVectors ps qs)+                                => ValidHarmMotionInVectors (p :* d1 :- ps) (q :* d2 :- qs)++-------------------------------------------------------------------------------+-- Pretty-printing+-------------------------------------------------------------------------------++instance Show (Music m) where show = render . ppMusic++-- | Pretty-print a 'Music' value.+ppMusic :: Music m -> Box+ppMusic (Note r d) = char '|' <+> doc r <+> doc d+ppMusic (Rest d) = char '|' <+> text "~~~~" <+> doc d+ppMusic (m1 :|: m2) = ppMusic m1 <> emptyBox 1 1 <> ppMusic m2+ppMusic (m1 :-: m2) = ppMusic m1 // ppMusic m2+ppMusic (Chord c d) = char '|' <+> doc c <+> doc d++-- | Convert a showable value into a pretty-printed box.+doc :: Show a => a -> Box+doc = text . show
+ src/Mezzo/Model/Prim.hs view
@@ -0,0 +1,302 @@+{-# LANGUAGE TypeInType, TypeOperators, TypeFamilies, GADTs,+    UndecidableInstances, ConstraintKinds #-}+{-# OPTIONS_GHC -fplugin GHC.TypeLits.Normalise #-}++-----------------------------------------------------------------------------+-- |+-- Module      :  Mezzo.Model.Prim+-- Description :  Mezzo type primitives+-- Copyright   :  (c) Dima Szamozvancev+-- License     :  MIT+--+-- Maintainer  :  ds709@cam.ac.uk+-- Stability   :  experimental+-- Portability :  portable+--+-- Primitive types that make up the base for the Mezzo type model.+--+-----------------------------------------------------------------------------++module Mezzo.Model.Prim+    (+    -- * Vectors and matrices+      Vector (..)+    , Times (..)+    , Elem (..)+    , type (**)+    , OptVector (..)+    , Head+    , Head'+    , Last+    , Tail'+    , Init'+    , Length+    , Length'+    , Matrix+    , type (++)+    , type (++.)+    , type (:-|)+    , type (+*+)+    , type (+|+)+    , type (+-+)+    , Align+    , VectorToColMatrix+    -- * Logic and arithmetic+    , If+    , Not+    , type (.&&.)+    , type (.||.)+    , type (.~.)+    , MaxN+    , MinN+    -- * Constraints+    , Valid+    , Invalid+    , AllSatisfy+    , AllPairsSatisfy+    , AllPairsSatisfy'+    , SatisfiesAll+    , AllSatisfyAll+    ) where++import Data.Kind+import GHC.TypeLits++infixr 7 :*+infixr 7 **+infixr 6 :-+infixr 5 :--+infixl 4 +++infixl 4 +*++infixl 4 +|++infixl 4 +-++infixl 3 .&&.+infixl 3 .||.+infixl 5 .~.++-------------------------------------------------------------------------------+-- Type-level vectors and matrices+-------------------------------------------------------------------------------++-- | Simple length-indexed vector.+data Vector :: Type -> Nat -> Type where+    None :: Vector t 0+    (:--) :: t -> Vector t (n - 1) -> Vector t n++-- | Singleton type for the number of repetitions of an element.+data Times (n :: Nat) where+    T :: Times n++-- | An element of a "run-length encoded" vector, containing the value and+-- the number of repetitions+data Elem :: Type -> Nat -> Type where+    (:*) :: t -> Times n -> Elem t n++-- | Replicate a value the specified number of times to create a new 'Elem'.+type family (v :: t) ** (d :: Nat) :: Elem t d where+    v ** d = v :* (T :: Times d)++-- | A length-indexed vector, optimised for repetitions.+data OptVector :: Type -> Nat -> Type where+    End  :: OptVector t 0+    (:-) :: Elem t l -> OptVector t (n - l) -> OptVector t n++-- | Get the first element of an optimised vector.+type family Head (v :: OptVector t n) :: t where+    Head End           = TypeError (Text "Vector has no head element.")+    Head (v :* _ :- _) = v++-- | Get the first element of a simple vector.+type family Head' (v :: Vector t n) :: t where+    Head' None      = TypeError (Text "Vector has no head element.")+    Head' (v :-- _) = v++-- | Get the last element of the vector.+type family Last (v :: OptVector t n) :: t where+    Last End             = TypeError (Text "Vector has no last element.")+    Last (v :* _ :- End) = v+    Last (_ :- vs)       = Last vs++-- | Get the tail of the vector.+type family Tail' (v :: Vector t n) :: Vector t (n - 1) where+    Tail' None = TypeError (Text "Vector has no tail.")+    Tail' (_ :-- vs) = vs++-- | Get everything but the last element of the vector.+type family Init' (v :: Vector t n) :: Vector t (n - 1) where+    Init' None = TypeError (Text "Vector is empty.")+    Init' (p :-- None) = None+    Init' (p :-- ps) = p :-- Init' ps++-- | Get the length of an optimised vector.+type family Length (v :: OptVector t n) :: Nat where+    Length (v :: OptVector t n) = n++-- | Get the length of a vector.+type family Length' (v :: Vector t n) :: Nat where+    Length' (v :: Vector t n) = n++-- | Append two optimised vectors.+type family (x :: OptVector t n) ++ (y :: OptVector t m) :: OptVector t (n + m) where+    ys        ++ End = ys+    End       ++ ys = ys+    (x :- xs) ++ ys = x :- (xs ++ ys)++-- | Append two simple vectors.+type family (x :: Vector t n) ++. (y :: Vector t m) :: Vector t (n + m) where+    None       ++. ys = ys+    (x :-- xs) ++. ys = x :-- (xs ++. ys)++-- | Add an element to the end of a simple vector.+type family (v :: Vector t n) :-| (e :: t) :: Vector t (n + 1) where+    v :-| e = v ++. (e :-- None)++-- | Repeat the value the specified number of times to create a new 'OptVector'.+type family (a :: t) +*+ (n :: Nat) :: OptVector t n where+    x +*+ 0 = End+    x +*+ n = x ** n :- End++-- | A dimension-indexed matrix.+type Matrix t p q = Vector (OptVector t q) p++-- | Horizontal concatenation of type-level matrices.+-- Places the first matrix to the left of the second.+type family (a :: Matrix t p q) +|+ (b :: Matrix t p r) :: Matrix t p (q + r) where+    None         +|+ None         = None+    (r1 :-- rs1) +|+ (r2 :-- rs2) = (r1 ++ r2) :-- (rs1 +|+ rs2)++-- | Vertical concatenation of type-level matrices.+-- Places the first matrix on top of the second.+type family (a :: Matrix t p r) +-+ (b :: Matrix t q r) :: Matrix t (p + q) r where+    m1 +-+ m2 = ConcatPair (Align m1 m2)++-- | Concatenates a type-level pair of vectors.+type family ConcatPair (vs :: (Vector t p, Vector t q)) :: Vector t (p + q) where+    ConcatPair '(v1, v2) = v1 ++. v2++-- | Vertically aligns two matrices by separating elements so that the element+-- boundaries line up.+type family Align (a :: Matrix t p r) (b :: Matrix t q r) :: (Matrix t p r, Matrix t q r) where+    Align None m = '(None, m)+    Align m None = '(m, None)+    Align (r1 :-- rs1) (r2 :-- rs2) =+            '(FragmentMatByVec (r1 :-- rs1) r2, FragmentMatByVec (r2 :-- rs2) r1)++-- | Fragments a matrix by a vector: all the element boundaries in the vector must+-- also appear in the fragmented matrix.+type family FragmentMatByVec (m :: Matrix t q p) (v :: OptVector t p) :: Matrix t q p where+    FragmentMatByVec None       _ = None+    FragmentMatByVec (r :-- rs) v = FragmentVecByVec r v :-- FragmentMatByVec rs v++-- | Fragments a vector by another vector: all the element boundaries in the second+-- vector must also appear in the first.+type family FragmentVecByVec (v :: OptVector t p) (u :: OptVector t p) :: OptVector t p where+    FragmentVecByVec End _ = End+    -- If the lengths of the first element match up, they are not fragmented.+    FragmentVecByVec (v :* (T :: Times k) :- vs) (u :* (T :: Times k) :- us) =+            v ** k :- (FragmentVecByVec vs us)+    -- If the lengths of the first elements don't match up, we fragment the element+    -- by the shortest of the two lengths, and add the remainder as a separate element.+    FragmentVecByVec (v :* (T :: Times k) :- vs) (u :* (T :: Times l) :- us) =+        If (k <=? l)+            ((v ** k) :- (FragmentVecByVec vs (u ** (l - k) :- us)))+            ((v ** l) :- (FragmentVecByVec (v ** (k - l) :- vs) us))++-- | Convert a simple vector to a column matrix.+type family VectorToColMatrix (v :: Vector t n) (l :: Nat) :: Matrix t n l where+    VectorToColMatrix None _ = None+    VectorToColMatrix (v :-- vs) l = (VectorToColMatrix vs l) ++. (v ** l :- End :-- None)++-------------------------------------------------------------------------------+-- Type-level logic and arithmetic+-------------------------------------------------------------------------------++-- | Conditional expression at the type level.+type family If (b :: Bool) (t :: k) (e :: k) :: k where+    If True  t e = t+    If False t e = e++-- | Negation of type-level Booleans.+type family Not (a :: Bool) :: Bool where+    Not True  = False+    Not False = True++-- | Conjunction of type-level Booleans.+type family (b1 :: Bool) .&&. (b2 :: Bool) :: Bool where+    b1 .&&. b2 = If b1 b2 False++-- | Disjunction of type-level Booleans.+type family (b1 :: Bool) .||. (b2 :: Bool) :: Bool where+    b1 .||. b2 = If b1 True b2++-- | Equality of types.+type family (a :: k) .~. (b :: k) :: Bool where+    a .~. a = True+    a .~. b = False++-- | Returns the maximum of two natural numbers.+type family MaxN (n1 :: Nat) (n2 :: Nat) :: Nat where+    MaxN 0 n2 = n2+    MaxN n1 0 = n1+    MaxN n n = n+    MaxN n1 n2 = If (n1 <=? n2) (n2) (n1)++-- | Returns the minimum of two natural numbers.+type family MinN (n1 :: Nat) (n2 :: Nat) :: Nat where+    MinN 0 n2 = 0+    MinN n1 0 = 0+    MinN n n = n+    MinN n1 n2 = If (n1 <=? n2) (n1) (n2)++-------------------------------------------------------------------------------+-- Constraints+-------------------------------------------------------------------------------++-- | Valid base constraint.+type Valid = (() :: Constraint)++-- | Invalid base constraint.+type Invalid = True ~ False++-- | Create a new constraint which is valid only if every element in the given+-- vector satisfies the given unary constraint.+-- Analogue of 'map' for constraints and vectors.+type family AllSatisfy (c  :: a -> Constraint)+                       (xs :: OptVector a n)+                           :: Constraint where+    AllSatisfy c End            = Valid+    AllSatisfy c (x :* _ :- xs) = ((c x), AllSatisfy c xs)++-- | Create a new constraint which is valid only if every pair of elements in+-- the given optimised vectors satisfy the given binary constraint.+-- Analogue of 'zipWith' for constraints and optimised vectors.+type family AllPairsSatisfy (c  :: a -> b -> Constraint)+                            (xs :: OptVector a n) (ys :: OptVector b n)+                                :: Constraint where+    AllPairsSatisfy c End            End            = Valid+    AllPairsSatisfy c (x :* _ :- xs) (y :* _ :- ys) = ((c x y), AllPairsSatisfy c xs ys)++-- | Create a new constraint which is valid only if every pair of elements in+-- the given vectors satisfy the given binary constraint.+-- Analogue of 'zipWith' for constraints and vectors.+type family AllPairsSatisfy' (c  :: a -> b -> Constraint)+                            (xs :: Vector a n) (ys :: Vector b n)+                                :: Constraint where+    AllPairsSatisfy' c None       None       = Valid+    AllPairsSatisfy' c (x :-- xs) (y :-- ys) = ((c x y), AllPairsSatisfy' c xs ys)++-- | Create a new constraint which is valid only if the given value satisfies+-- every unary constraint in the given list.+type family SatisfiesAll (cs :: [a -> Constraint])+                         (xs :: a)+                             :: Constraint where+    SatisfiesAll '[]      a = Valid+    SatisfiesAll (c : cs) a = (c a, SatisfiesAll cs a)++-- | Create a new constraint which is valid only if every element in the given+-- vector satisfies every unary constraint in the given list.+type family AllSatisfyAll (c1 :: [a -> Constraint])+                          (xs :: Vector a n)+                              :: Constraint where+    AllSatisfyAll _ None        = Valid+    AllSatisfyAll cs (v :-- vs) = (SatisfiesAll cs v, AllSatisfyAll cs vs)
+ src/Mezzo/Model/Reify.hs view
@@ -0,0 +1,42 @@+{-# LANGUAGE TypeInType, ScopedTypeVariables, TypeFamilies, FlexibleInstances,+    UndecidableInstances, ConstraintKinds #-}++-----------------------------------------------------------------------------+-- |+-- Module      :  Mezzo.Model.Reify+-- Description :  MIDI exporting+-- Copyright   :  (c) Dima Szamozvancev+-- License     :  MIT+--+-- Maintainer  :  ds709@cam.ac.uk+-- Stability   :  experimental+-- Portability :  portable+--+-- Class of types which can be reified at the term level.+--+-----------------------------------------------------------------------------++module Mezzo.Model.Reify where++import Data.Kind++-- | Class of types which can have a primitive representation at runtime.+class Primitive (a :: k) where+    -- | The type of the primitive representation.+    type Rep a+    -- | Convert a singleton of the type into its primitive representation.+    prim :: sing a -> Rep a+    -- | Pretty print a singleton of the type.+    pretty :: sing a -> String++instance {-# OVERLAPPABLE #-} Primitive t => Show (sing t) where+    show = pretty++-- | Primitive types with integer representations.+type IntRep t = (Primitive t, Rep t ~ Int)++-- | Primitive types with integer list representations.+type IntListRep t = (Primitive t, Rep t ~ [Int])++-- | Primitive types with function representations from type a to type b.+type FunRep a b t = (Primitive t, Rep t ~ (a -> b))
+ src/Mezzo/Model/Types.hs view
@@ -0,0 +1,698 @@+{-# LANGUAGE TypeInType, GADTs, TypeOperators, TypeFamilies, UndecidableInstances,+    TypeApplications, ScopedTypeVariables, FlexibleInstances, StandaloneDeriving, ViewPatterns #-}+{-# OPTIONS_GHC -fplugin GHC.TypeLits.Normalise #-}++-----------------------------------------------------------------------------+-- |+-- Module      :  Mezzo.Model.Types+-- Description :  Mezzo music types+-- Copyright   :  (c) Dima Szamozvancev+-- License     :  MIT+--+-- Maintainer  :  ds709@cam.ac.uk+-- Stability   :  experimental+-- Portability :  portable+--+-- Types modeling basic musical constructs at the type level.+--+-----------------------------------------------------------------------------++module Mezzo.Model.Types+    (+    -- * Note properties+      PitchClass (..)+    , Accidental (..)+    , OctaveNum (..)+    , Duration (..)+    -- ** Singleton types for note properties+    , PC (..)+    , Acc (..)+    , Oct (..)+    , Dur (..)+    -- * Pitches+    , PitchType (..)+    , Pit (..)+    , type (=?=)+    , type (<<=?)+    , type (<<?)+    -- * Harmonic types+    , Mode (..)+    , ScaleDegree (..)+    , KeyType (..)+    , RootType (..)+    , Mod (..)+    , ScaDeg (..)+    , KeyS (..)+    , Root (..)+    , RootToPitch+    , PitchToNat+    , Sharpen+    , Flatten+    , Dot+    , FromRoot+    , FromSilence+    -- * Specialised musical vector types+    , Voice+    , Partiture+    -- * Intervals+    , IntervalSize (..)+    , IntervalClass (..)+    , IntervalType (..)+    , MakeInterval+    , HalfStepsUpBy+    , HalfStepsDownBy+    , RaiseBy+    , LowerBy+    , RaiseAllBy'+    , LowerAllBy'+    , RaiseByOct+    , LowerByOct+    , RaiseAllByOct+    ) where++import GHC.TypeLits+import Data.Proxy++import Mezzo.Model.Prim+import Mezzo.Model.Reify++infixl 3 <<=?+infixl 3 <<?++-------------------------------------------------------------------------------+-- Note properties+-- The "minimum complete definition" for musical notes and rests.+-------------------------------------------------------------------------------++-- | The diatonic pitch class of the note.+data PitchClass = C | D | E | F | G | A | B++-- | The accidental applied to a note.+data Accidental = Natural | Flat | Sharp++-- | The octave where the note resides (middle C is Oct4).+data OctaveNum =+    Oct_1 | Oct0 | Oct1 | Oct2 | Oct3 | Oct4 | Oct5 | Oct6 | Oct7 | Oct8++-- | The duration of the note (a whole note has duration 32).+type Duration = Nat++---- Singleton types for note properties++-- | The singleton type for 'PitchClass'.+data PC (pc :: PitchClass) where+    PC :: Primitive pc => PC pc++-- | The singleton type for 'Accidental'.+data Acc (acc :: Accidental) where+    Acc :: Primitive acc => Acc acc++-- | The singleton type for 'Octave'.+data Oct (oct :: OctaveNum) where+    Oct :: Primitive oct => Oct oct++-- | The singleton type for 'Duration'.+data Dur (dur :: Duration) where+    Dur :: Primitive dur => Dur dur++-------------------------------------------------------------------------------+-- Pitches+-- Encapsulates the pitch class, accidental and octave of a note.+-------------------------------------------------------------------------------++-- | The type of pitches.+data PitchType where+    -- | A pitch made up of a pitch class, an accidental and an octave.+    Pitch :: PitchClass -> Accidental -> OctaveNum -> PitchType+    -- | Silence, the pitch of rests.+    Silence :: PitchType++-- | The singleton type for pitches.+data Pit (p :: PitchType) where+    Pit :: Primitive p => Pit p++-------------------------------------------------------------------------------+-- Harmonic types+-------------------------------------------------------------------------------++-- | The mode of a key: major or minor.+data Mode = MajorMode | MinorMode++-- | The seven scale degrees.+data ScaleDegree = I | II | III | IV | V | VI | VII++-- | The of a scale, chord or piece.+data KeyType = Key PitchClass Accidental Mode++-- | The root of a chord.+data RootType where+    -- | A pitch constructs a diatonic root.+    PitchRoot :: PitchType -> RootType+    -- | A key and a scale degree constructs a scalar root.+    DegreeRoot :: KeyType -> ScaleDegree -> RootType++-- | The singleton type for 'Mode'.+data Mod (m :: Mode) = Mod++-- | The singleton type for 'ScaleDegree'+data ScaDeg (sd :: ScaleDegree) = ScaDeg++-- | The singleton type for 'KeyType'.+data KeyS (k :: KeyType) = KeyS++-- | The singleton type for 'Root'.+data Root (r :: RootType) where+    Root :: Primitive r => Root r++-- | Convert a root to a pitch.+--+-- Note: the default octave for scalar roots is 'Oct2'.+type family RootToPitch (dr :: RootType) :: PitchType where+    RootToPitch (PitchRoot p) = p+    RootToPitch (DegreeRoot (Key pc acc m) d) =+                    HalfStepsUpBy (Pitch pc acc Oct2) (DegreeOffset m d)++-- | Calculate the semitone offset of a scale degree in a given mode.+type family DegreeOffset (m :: Mode) (d :: ScaleDegree) where+    DegreeOffset MajorMode I   = 0+    DegreeOffset MajorMode II  = 2+    DegreeOffset MajorMode III = 4+    DegreeOffset MajorMode IV  = 5+    DegreeOffset MajorMode V   = 7+    DegreeOffset MajorMode VI  = 9+    DegreeOffset MajorMode VII = 11+    DegreeOffset MinorMode I   = 0+    DegreeOffset MinorMode II  = 2+    DegreeOffset MinorMode III = 3+    DegreeOffset MinorMode IV  = 5+    DegreeOffset MinorMode V   = 7+    DegreeOffset MinorMode VI  = 8+    DegreeOffset MinorMode VII = 10++-- | Sharpen a root.+type family Sharpen (r :: RootType) :: RootType where+    Sharpen r = PitchRoot (HalfStepUp (RootToPitch r))++-- | Flatten a root.+type family Flatten (r :: RootType) :: RootType where+    Flatten r = PitchRoot (HalfStepDown (RootToPitch r))++-- | Halve a type-level natural.+type family HalfOf (n :: Nat) :: Nat where+    HalfOf 0 = 0+    HalfOf 1 = 0+    HalfOf 8 = 4+    HalfOf 32 = 16+    HalfOf n = 1 + (HalfOf (n - 2))++-- | Form a dotted duration.+type family Dot (d :: Duration) :: Duration where+    Dot 1 = TypeError (Text "Can't have dotted thirty-seconds.")+    Dot n = n + HalfOf n++-- | Create a new partiture with one voice of the given pitch.+type family FromRoot (r :: RootType) (d :: Nat) :: Partiture 1 d where+    FromRoot r d = ((RootToPitch r) +*+ d) :-- None++-- | Create a new partiture with one voice of silence.+type family FromSilence (d :: Nat) :: Partiture 1 d where+    FromSilence d = (Silence +*+ d) :-- None++-------------------------------------------------------------------------------+-- Type specialisations+-------------------------------------------------------------------------------++-- | A 'Voice' is made up of a sequence of pitch repetitions.+type Voice l = OptVector PitchType l++-- | A 'Partiture' is made up of a fixed number of voices.+type Partiture n l = Matrix PitchType n l++-------------------------------------------------------------------------------+-- Intervals+-------------------------------------------------------------------------------++-- | The size of the interval.+data IntervalSize =+    Unison | Second | Third | Fourth | Fifth | Sixth | Seventh | Octave++-- | The class of the interval.+data IntervalClass = Maj | Perf | Min | Aug | Dim++-- | The type of intervals.+data IntervalType where+    -- | An interval smaller than 13 semitones, where musical rules+    -- can still be enforced.+    Interval :: IntervalClass -> IntervalSize -> IntervalType+    -- | An interval larger than 13 semitones, which is large enough+    -- so that dissonance effects are not significant.+    Compound :: IntervalType++-------------------------------------------------------------------------------+-- Interval construction+-------------------------------------------------------------------------------++-- | Make an interval from two arbitrary pitches.+type family MakeInterval (p1 :: PitchType) (p2 :: PitchType) :: IntervalType where+    MakeInterval Silence Silence = TypeError (Text "Can't make intervals from rests.")+    MakeInterval Silence p2      = TypeError (Text "Can't make intervals from rests.")+    MakeInterval p1      Silence = TypeError (Text "Can't make intervals from rests.")+    MakeInterval p1 p2 =+        If  (p1 <<=? p2)+            (MakeIntervalOrd p1 p2)+            (MakeIntervalOrd p2 p1)++-- | Make an interval from two ordered pitches.+type family MakeIntervalOrd (p1 :: PitchType) (p2 :: PitchType) :: IntervalType where+    -- Handling base cases.+    MakeIntervalOrd p p = Interval Perf Unison+    MakeIntervalOrd (Pitch C Natural o) (Pitch C Sharp o) = Interval Aug Unison+    MakeIntervalOrd (Pitch C Natural o) (Pitch D Flat o) = Interval Min Second+    MakeIntervalOrd (Pitch C acc o)     (Pitch D acc o)   = Interval Maj Second+    MakeIntervalOrd (Pitch C acc o)     (Pitch E acc o)   = Interval Maj Third+    MakeIntervalOrd (Pitch C acc o)     (Pitch F acc o)   = Interval Perf Fourth+    MakeIntervalOrd (Pitch C acc o)     (Pitch G acc o)   = Interval Perf Fifth+    MakeIntervalOrd (Pitch C acc o)     (Pitch A acc o)   = Interval Maj Sixth+    MakeIntervalOrd (Pitch C acc o)     (Pitch B acc o)   = Interval Maj Seventh+    -- Handling perfect and augmented octaves.+    MakeIntervalOrd (Pitch C acc o1) (Pitch C acc o2) =+            If (OctSucc o1 .~. o2) (Interval Perf Octave) Compound+    MakeIntervalOrd (Pitch C Natural o1) (Pitch C Sharp o2) =+            If (OctSucc o1 .~. o2) (Interval Aug Octave) Compound+    MakeIntervalOrd (Pitch C Flat o1) (Pitch C Natural o2) =+            If (OctSucc o1 .~. o2) (Interval Aug Octave) Compound+    -- Handling accidental first pitch.+    MakeIntervalOrd (Pitch C Flat o) (Pitch pc2 acc o) =+            Expand (MakeIntervalOrd (Pitch C Natural o) (Pitch pc2 acc o))+    MakeIntervalOrd (Pitch C Sharp o) (Pitch pc2 acc o) =+            Shrink (MakeIntervalOrd (Pitch C Natural o) (Pitch pc2 acc o))+    -- Handling accidental second pitch.+    MakeIntervalOrd (Pitch C Natural o) (Pitch pc2 Sharp o) =+            Expand (MakeIntervalOrd (Pitch C Natural o) (Pitch pc2 Natural o))+    MakeIntervalOrd (Pitch C Natural o) (Pitch pc2 Flat o) =+            Shrink (MakeIntervalOrd (Pitch C Natural o) (Pitch pc2 Natural o))+    -- Handling the general case.+    MakeIntervalOrd (Pitch pc1 acc1 o1) (Pitch pc2 acc2 o2) =+            If  (o1 .~. o2 .||. OctSucc o1 .~. o2)+                (MakeIntervalOrd (HalfStepDown (Pitch pc1 acc1 o1)) (HalfStepDown (Pitch pc2 acc2 o2)))+                Compound+    -- Handling erroneous construction (shouldn't happen).+    MakeIntervalOrd _ _ = TypeError (Text "Invalid interval.")++-- | Shrink an interval.+type family Shrink (i :: IntervalType) :: IntervalType where+    Shrink (Interval Perf Unison) = TypeError (Text "Can't diminish unisons.")+    Shrink (Interval Perf is)     = Interval Dim is+    Shrink (Interval Min  is)     = Interval Dim is+    Shrink (Interval Maj  is)     = Interval Min is+    Shrink (Interval Aug  Unison) = Interval Perf Unison+    Shrink (Interval Aug  Fourth) = Interval Perf Fourth+    Shrink (Interval Aug  Fifth)  = Interval Perf Fifth+    Shrink (Interval Aug  Octave) = Interval Perf Octave+    Shrink (Interval Aug  is)     = Interval Maj is+    Shrink (Interval Dim  Unison) = TypeError (Text "Can't diminish unisons.")+    Shrink (Interval Dim  Second) = TypeError (Text "Can't diminish unisons.")+    Shrink (Interval Dim  Fifth)  = Interval Perf Fourth+    Shrink (Interval Dim  Sixth)  = Interval Dim Fifth+    Shrink (Interval Dim  is)     = Interval Min (IntSizePred is)+    Shrink  Compound              = Compound++-- | Expand an interval.+type family Expand (i :: IntervalType) :: IntervalType where+    Expand (Interval Perf Octave)  = Interval Aug Octave+    Expand (Interval Perf is)      = Interval Aug is+    Expand (Interval Maj  is)      = Interval Aug is+    Expand (Interval Min  is)      = Interval Maj is+    Expand (Interval Dim  Unison)  = TypeError (Text "Can't diminish unisons.")+    Expand (Interval Dim  Fourth)  = Interval Perf Fourth+    Expand (Interval Dim  Fifth)   = Interval Perf Fifth+    Expand (Interval Dim  Octave)  = Interval Perf Octave+    Expand (Interval Dim  is)      = Interval Min is+    Expand (Interval Aug  Third)   = Interval Aug Fourth+    Expand (Interval Aug  Fourth)  = Interval Perf Fifth+    Expand (Interval Aug  Seventh) = Interval Aug Octave+    Expand (Interval Aug  Octave)  = Compound+    Expand (Interval Aug  is)      = Interval Maj (IntSizeSucc is)+    Expand  Compound               = Compound++-------------------------------------------------------------------------------+-- Enumerations and orderings+-- Implementation of enumerators and ordering relations for applicable types.+-------------------------------------------------------------------------------++-- | Convert a pitch to a natural number (equal to its MIDI code).+type family PitchToNat (p :: PitchType) :: Nat where+    PitchToNat Silence = TypeError (Text "Can't convert a rest to a number.")+    PitchToNat (Pitch C Natural Oct_1) = 0+    PitchToNat (Pitch C Sharp Oct_1)   = 1+    PitchToNat (Pitch D Flat Oct_1)    = 1+    PitchToNat (Pitch C Natural Oct1)  = 24+    PitchToNat (Pitch C Natural Oct2)  = 36+    PitchToNat (Pitch C Natural Oct3)  = 48+    PitchToNat (Pitch C Natural Oct4)  = 60+    PitchToNat (Pitch C Natural Oct5)  = 72+    PitchToNat (Pitch C Natural Oct6)  = 84+    PitchToNat p                       = 1 + PitchToNat (HalfStepDown p)++-- | Convert a natural number to a suitable pitch.+-- Not a functional relation, so usage is not recommended.+type family NatToPitch (n :: Nat) where+    NatToPitch 0 = Pitch C Natural Oct_1+    NatToPitch 1 = Pitch C Sharp Oct_1+    NatToPitch n = HalfStepUp (NatToPitch (n - 1))++-- | Greater than or equal to for pitches.+type family (p1 :: PitchType) <<=? (p2 :: PitchType) where+    p1 <<=? p2 = PitchToNat p1 <=? PitchToNat p2++-- | Greater than for pitches.+type family (p1 :: PitchType) <<? (p2 :: PitchType) where+    p1 <<? p2 = (p1 <<=? p2) .&&. Not (p1 .~. p2)++-- | Enharmonic equality of pitches.+type family (p :: PitchType) =?= (q :: PitchType) :: Bool where+    Silence             =?= Silence             = True+    Silence             =?= _                   = False+    _                   =?= Silence             = False+    Pitch pc acc oct    =?= Pitch pc acc oct    = True+    Pitch C Flat o1     =?= Pitch B Natural o2  = o1 .~. OctSucc o2+    Pitch C Natural o1  =?= Pitch B Sharp o2    = o1 .~. OctSucc o2+    Pitch E Natural oct =?= Pitch F Flat oct    = True+    Pitch E Sharp oct   =?= Pitch F Natural oct = True+    Pitch F Flat oct    =?= Pitch E Natural oct = True+    Pitch F Natural oct =?= Pitch E Sharp oct   = True+    Pitch B Natural o1  =?= Pitch C Flat o2     = OctSucc o1 .~. o2+    Pitch B Sharp o1    =?= Pitch C Natural o2  = OctSucc o1 .~. o2+    Pitch pc1 Sharp oct =?= Pitch pc2 Flat oct  = ClassSucc pc1 .~. pc2+    Pitch pc1 Flat oct  =?= Pitch pc2 Sharp oct = pc1 .~. ClassSucc pc2+    _                   =?= _                   = False++-- | Convert an octave to a natural number.+type family OctToNat (o :: OctaveNum) :: Nat where+    OctToNat Oct_1 = 0+    OctToNat Oct0  = 1+    OctToNat Oct1  = 2+    OctToNat Oct2  = 3+    OctToNat Oct3  = 4+    OctToNat Oct4  = 5+    OctToNat Oct5  = 6+    OctToNat Oct6  = 7+    OctToNat Oct7  = 8+    OctToNat Oct8  = 9++-- | Convert a natural number to an octave.+type family NatToOct (n :: Nat) :: OctaveNum where+    NatToOct 0 = Oct_1+    NatToOct 1 = Oct0+    NatToOct 2 = Oct1+    NatToOct 3 = Oct2+    NatToOct 4 = Oct3+    NatToOct 5 = Oct4+    NatToOct 6 = Oct5+    NatToOct 7 = Oct6+    NatToOct 8 = Oct7+    NatToOct 9 = Oct8+    NatToOct _ = TypeError (Text "Invalid octave.")++-- | Increase the octave by the given number.+type family IncreaseOctave (o :: OctaveNum) (n :: Nat) :: OctaveNum where+    IncreaseOctave o n = NatToOct (OctToNat o + n)++-- | Decrease the octave by the given number.+type family DecreaseOctave (o :: OctaveNum) (n :: Nat) :: OctaveNum where+    DecreaseOctave o n = NatToOct (OctToNat o - n)++-- | Increment an octave.+type family OctSucc (o :: OctaveNum) :: OctaveNum where+    OctSucc o = IncreaseOctave o 1++-- | Decrement an octave.+type family OctPred (o :: OctaveNum) :: OctaveNum where+    OctPred o = DecreaseOctave o 1++-- | Convert a pitch class to a natural number.+type family ClassToNat (pc :: PitchClass) :: Nat where+    ClassToNat C = 0+    ClassToNat D = 1+    ClassToNat E = 2+    ClassToNat F = 3+    ClassToNat G = 4+    ClassToNat A = 5+    ClassToNat B = 6++-- | Convert a natural number to a pitch class.+-- Numbers are taken modulo 7: e.g. 8 corresponds to the pitch 8 mod 7 = 1 = D+type family NatToClass (n :: Nat) :: PitchClass where+    NatToClass 0 = C+    NatToClass 1 = D+    NatToClass 2 = E+    NatToClass 3 = F+    NatToClass 4 = G+    NatToClass 5 = A+    NatToClass 6 = B+    NatToClass n = NatToClass (n - 7)++-- | Increase the pitch class by a given number.+type family IncreaseClass (pc :: PitchClass) (n :: Nat) :: PitchClass where+    IncreaseClass pc n = NatToClass (ClassToNat pc + n)++-- | Decrease the pitch class by a given number.+type family DecreaseClass (pc :: PitchClass) (n :: Nat) :: PitchClass where+    DecreaseClass pc n = NatToClass (ClassToNat pc - n)++-- | Increment a pitch class.+type family ClassSucc (pc :: PitchClass) :: PitchClass where+    ClassSucc pc = IncreaseClass pc 1++-- | Decrement a pitch class.+type family ClassPred (pc :: PitchClass) :: PitchClass where+    ClassPred pc = DecreaseClass pc 1++-- | Convert an interval size to a natural number.+type family IntSizeToNat (is :: IntervalSize) :: Nat where+    IntSizeToNat Unison  = 0+    IntSizeToNat Second  = 1+    IntSizeToNat Third   = 2+    IntSizeToNat Fourth  = 3+    IntSizeToNat Fifth   = 4+    IntSizeToNat Sixth   = 5+    IntSizeToNat Seventh = 6+    IntSizeToNat Octave  = 7++-- | Convert a natural number to an interval size.+type family NatToIntSize (n :: Nat) :: IntervalSize where+    NatToIntSize 0 = Unison+    NatToIntSize 1 = Second+    NatToIntSize 2 = Third+    NatToIntSize 3 = Fourth+    NatToIntSize 4 = Fifth+    NatToIntSize 5 = Sixth+    NatToIntSize 6 = Seventh+    NatToIntSize 7 = Octave+    NatToIntSize _ = TypeError (Text "Invalid interval size.")++-- | Increase the interval size by a given number.+type family IncreaseIntSize (is :: IntervalSize) (n :: Nat) :: IntervalSize where+    IncreaseIntSize is n = NatToIntSize (IntSizeToNat is + n)++-- | Decrease the interval size by a given number.+type family DecreaseIntSize (is :: IntervalSize) (n :: Nat) :: IntervalSize where+    DecreaseIntSize is n = NatToIntSize (IntSizeToNat is - n)++-- | Increment an interval size.+type family IntSizeSucc (is :: IntervalSize) :: IntervalSize where+    IntSizeSucc is = IncreaseIntSize is 1++-- | Decrement an interval size.+type family IntSizePred (is :: IntervalSize) :: IntervalSize where+    IntSizePred is = DecreaseIntSize is 1++-- | Calculate the width of an interval in half-steps.+type family IntervalWidth (i :: IntervalType) :: Nat where+    IntervalWidth (Interval Dim Unison)  = TypeError (Text "Can't diminish unisons.")+    IntervalWidth (Interval Perf Unison) = 0+    IntervalWidth (Interval Aug Unison)  = 1+    IntervalWidth (Interval Dim Fourth)  = 4+    IntervalWidth (Interval Perf Fourth) = 5+    IntervalWidth (Interval Aug Fourth)  = 6+    IntervalWidth (Interval Dim Fifth)   = 6+    IntervalWidth (Interval Perf Fifth)  = 7+    IntervalWidth (Interval Aug Fifth)   = 8+    IntervalWidth (Interval Dim Octave)  = 11+    IntervalWidth (Interval Perf Octave) = 12+    IntervalWidth (Interval Aug Octave)  = 13+    IntervalWidth (Interval Maj Second)  = 2+    IntervalWidth (Interval Maj Third)   = 4+    IntervalWidth (Interval Maj Sixth)   = 9+    IntervalWidth (Interval Maj Seventh) = 11+    IntervalWidth (Interval Aug is)      = IntervalWidth (Interval Maj is) + 1+    IntervalWidth (Interval Min is)      = IntervalWidth (Interval Maj is) - 1+    IntervalWidth (Interval Dim is)      = IntervalWidth (Interval Maj is) - 2++-- | Move a pitch up by a semitone.+type family HalfStepUp (p :: PitchType) :: PitchType where+    HalfStepUp Silence              = Silence+    HalfStepUp (Pitch B  Flat    o) = Pitch B Natural o+    HalfStepUp (Pitch B  acc     o) = Pitch C acc (OctSucc o)+    HalfStepUp (Pitch E  Flat    o) = Pitch E Natural o+    HalfStepUp (Pitch E  acc     o) = Pitch F acc o+    HalfStepUp (Pitch pc Flat    o) = Pitch pc Natural o+    HalfStepUp (Pitch pc Natural o) = Pitch pc Sharp o+    HalfStepUp (Pitch pc Sharp   o) = Pitch (ClassSucc pc) Natural o++-- | Move a pitch down by a semitone.+type family HalfStepDown (p :: PitchType) :: PitchType where+    HalfStepDown Silence              = Silence+    HalfStepDown (Pitch C  Sharp   o) = Pitch C Natural o+    HalfStepDown (Pitch C  acc     o) = Pitch B acc (OctPred o)+    HalfStepDown (Pitch F  Sharp   o) = Pitch F Natural o+    HalfStepDown (Pitch F  acc     o) = Pitch E acc o+    HalfStepDown (Pitch pc Flat    o) = Pitch (ClassPred pc) Natural o+    HalfStepDown (Pitch pc Natural o) = Pitch pc Flat o+    HalfStepDown (Pitch pc Sharp   o) = Pitch pc Natural o++-- | Move a pitch up by the specified number of semitones.+type family HalfStepsUpBy (p :: PitchType) (n :: Nat) :: PitchType where+    HalfStepsUpBy p 0 = p+    HalfStepsUpBy p n = HalfStepUp (HalfStepsUpBy p (n - 1))++-- | Move a pitch down by the specified number of semitones.+type family HalfStepsDownBy (p :: PitchType) (n :: Nat) :: PitchType where+    HalfStepsDownBy p 0 = p+    HalfStepsDownBy p n = HalfStepDown (HalfStepsDownBy p (n - 1))++-- | Raise a pitch by an interval.+type family RaiseBy (p :: PitchType) (i :: IntervalType) :: PitchType where+    RaiseBy Silence _           = Silence+    RaiseBy _ Compound          = TypeError (Text "Can't shift by compound interval")+    RaiseBy p (Interval Min is) = HalfStepDown (HalfStepsUpBy p (IntervalWidth (Interval Min is) + 1))+    RaiseBy p (Interval Dim is) = HalfStepDown (HalfStepsUpBy p (IntervalWidth (Interval Dim is) + 1))+    RaiseBy p i                 = HalfStepsUpBy p (IntervalWidth i)++-- | Lower a pitch by an interval.+type family LowerBy (p :: PitchType) (i :: IntervalType) :: PitchType where+    LowerBy Silence _           = Silence+    LowerBy _ Compound          = TypeError (Text "Can't shift by compound interval")+    LowerBy p (Interval Maj is) = HalfStepUp (HalfStepsDownBy p (IntervalWidth (Interval Maj is) + 1))+    LowerBy p (Interval Aug is) = HalfStepUp (HalfStepsDownBy p (IntervalWidth (Interval Aug is) + 1))+    LowerBy p i                 = HalfStepsDownBy p (IntervalWidth i)++-- | Raise all pitches in a voice by an interval.+type family RaiseAllBy (ps :: Voice l) (i :: IntervalType) :: Voice l where+    RaiseAllBy End _ = End+    RaiseAllBy (p :* d :- ps) i = RaiseBy p i :* d :- RaiseAllBy ps i++-- | Raise multiple pitches by an interval.+type family RaiseAllBy' (ps :: Vector PitchType n) (i :: IntervalType) :: Vector PitchType n where+    RaiseAllBy' None _ = None+    RaiseAllBy' (p :-- ps) i = RaiseBy p i :-- RaiseAllBy' ps i++-- | Lower all pitches in a voice by an interval.+type family LowerAllBy (ps :: Voice l) (i :: IntervalType) :: Voice l where+    LowerAllBy End _ = End+    LowerAllBy (p :* d :- ps) i = LowerBy p i :* d :- LowerAllBy ps i++-- | Lower multiple pitches by an interval.+type family LowerAllBy' (ps :: Vector PitchType n) (i :: IntervalType) :: Vector PitchType n where+    LowerAllBy' None _ = None+    LowerAllBy' (p :-- ps) i = LowerBy p i :-- LowerAllBy' ps i++-- | Raise a pitch by an octave.+type family RaiseByOct (p :: PitchType) :: PitchType where+    RaiseByOct p = RaiseBy p (Interval Perf Octave)++-- | Lower a pitch by an octave.+type family LowerByOct (p :: PitchType) :: PitchType where+    LowerByOct p = LowerBy p (Interval Perf Octave)++type family RaiseAllByOct (ps :: Voice l) :: Voice l where+    RaiseAllByOct v = RaiseAllBy v (Interval Perf Octave)++-------------------------------------------------------------------------------+-- Primitive instances+-------------------------------------------------------------------------------++instance Primitive Oct_1 where type Rep Oct_1 = Int ; prim o = 0 ; pretty o = "_5"+instance Primitive Oct0 where type Rep Oct0 = Int ; prim o = 12 ; pretty o = "_4"+instance Primitive Oct1 where type Rep Oct1 = Int ; prim o = 24 ; pretty o = "_3"+instance Primitive Oct2 where type Rep Oct2 = Int ; prim o = 36 ; pretty o = "__"+instance Primitive Oct3 where type Rep Oct3 = Int ; prim o = 48 ; pretty o = "_ "+instance Primitive Oct4 where type Rep Oct4 = Int ; prim o = 60 ; pretty o = "  "+instance Primitive Oct5 where type Rep Oct5 = Int ; prim o = 72 ; pretty o = "' "+instance Primitive Oct6 where type Rep Oct6 = Int ; prim o = 84 ; pretty o = "''"+instance Primitive Oct7 where type Rep Oct7 = Int ; prim o = 96 ; pretty o = "'3"+instance Primitive Oct8 where type Rep Oct8 = Int ; prim o = 108; pretty o = "'4"++instance Primitive C where type Rep C = Int ; prim p = 0 ; pretty p = "C"+instance Primitive D where type Rep D = Int ;  prim p = 2 ; pretty p = "D"+instance Primitive E where type Rep E = Int ;  prim p = 4 ; pretty p = "E"+instance Primitive F where type Rep F = Int ;  prim p = 5 ; pretty p = "F"+instance Primitive G where type Rep G = Int ;  prim p = 7 ; pretty p = "G"+instance Primitive A where type Rep A = Int ;  prim p = 9 ; pretty p = "A"+instance Primitive B where type Rep B = Int ;  prim p = 11; pretty p = "B"++instance Primitive Natural where type Rep Natural = Int ; prim a = 0 ; pretty a = " "+instance Primitive Flat where type Rep Flat = Int ; prim a = -1 ; pretty a = "b"+instance Primitive Sharp where type Rep Sharp = Int ; prim a = 1 ; pretty a = "#"++-- "Equality constraints are literally magic."+--                                  - Michael Gale, 2017+instance (IntRep pc, IntRep acc, IntRep oct)+        => Primitive (Pitch pc acc oct) where+    type Rep (Pitch pc acc oct) = Int+    prim p = prim (PC @pc) + prim (Acc @acc) + prim (Oct @oct)+    pretty p = pretty (PC @pc) ++ pretty (Acc @acc) ++ pretty (Oct @oct)++instance Primitive Silence where type Rep Silence = Int ; prim s = 60 ; pretty s = "~~~~"++instance IntRep p => Primitive (Root (PitchRoot p)) where+    type Rep (Root (PitchRoot p)) = Int+    prim r = prim (Pit @p)+    pretty r = pretty (Pit @p)++-- Modes+instance Primitive MajorMode where type Rep MajorMode = Bool ; prim m = True ; pretty m = "Major"+instance Primitive MinorMode where type Rep MinorMode = Bool ; prim m = False ; pretty m = "minor"++-- Scale degrees+instance Primitive I    where type Rep I    = Int ; prim d = 0 ; pretty d = "I"+instance Primitive II   where type Rep II   = Int ; prim d = 1 ; pretty d = "II"+instance Primitive III  where type Rep III  = Int ; prim d = 2 ; pretty d = "III"+instance Primitive IV   where type Rep IV   = Int ; prim d = 3 ; pretty d = "IV"+instance Primitive V    where type Rep V    = Int ; prim d = 4 ; pretty d = "V"+instance Primitive VI   where type Rep VI   = Int ; prim d = 5 ; pretty d = "VI"+instance Primitive VII  where type Rep VII  = Int ; prim d = 6 ; pretty d = "VII"+++instance (IntRep pc, IntRep acc, IntRep mo) => Primitive (Key pc acc mo) where+    type Rep (Key pc acc mo) = Int+    prim k = 0 -- to be changed+    pretty k = pretty (PC @pc) ++ pretty (Acc @acc) ++ " " ++ pretty (Mod @mo)+++instance (IntRep p, RootToPitch (DegreeRoot k sd) ~ p, Primitive sd)+        => Primitive (Root (DegreeRoot k sd)) where+    type Rep (Root (DegreeRoot k sd)) = Int+    prim r = prim (Pit @p)+    pretty r = pretty (ScaDeg @sd)++instance IntRep p => Primitive (PitchRoot p) where+    type Rep (PitchRoot p) = Int+    prim p = prim (Pit @p)+    pretty p = pretty (Pit @p)++instance KnownNat n => Primitive n where+    type Rep n = Int+    prim = fromInteger . natVal+    pretty (natVal -> 1) = "Th"+    pretty (natVal -> 2) = "Si"+    pretty (natVal -> 3) = "Si."+    pretty (natVal -> 4) = "Ei"+    pretty (natVal -> 6) = "Ei."+    pretty (natVal -> 8) = "Qu"+    pretty (natVal -> 12) = "Qu."+    pretty (natVal -> 16) = "Ha"+    pretty (natVal -> 24) = "Ha."+    pretty (natVal -> 32) = "Wh"+    pretty (natVal -> 48) = "Wh."+    pretty (natVal -> n) = ":" ++ show n
+ src/Mezzo/Render/MIDI.hs view
@@ -0,0 +1,116 @@+{-# LANGUAGE TypeInType, GADTs #-}++-----------------------------------------------------------------------------+-- |+-- Module      :  Mezzo.Render.MIDI+-- Description :  MIDI exporting+-- Copyright   :  (c) Dima Szamozvancev+-- License     :  MIT+--+-- Maintainer  :  ds709@cam.ac.uk+-- Stability   :  experimental+-- Portability :  portable+--+-- Functions for exporting Mezzo compositions into MIDI files.+-- Skeleton code by Stephen Lavelle.+--+-----------------------------------------------------------------------------++module Mezzo.Render.MIDI+    ( renderMusic, musicToMidi )+    where++import Mezzo.Model++import Codec.Midi++-------------------------------------------------------------------------------+-- Types+-------------------------------------------------------------------------------++-- | A MIDI representation of a musical note.+data MidiNote = MidiNote+    { noteNum :: Int        -- ^ MIDI number of a note (middle C is 60).+    , vel     :: Velocity   -- ^ Performance velocity of the note.+    , start   :: Ticks      -- ^ Relative start time of the note.+    , noteDur :: Ticks      -- ^ Duration of the note.+    } deriving Show++-- | A MIDI event: a MIDI message at a specific timestamp.+type MidiEvent = (Ticks, Message)++-- | A sequence of MIDI events.+type MidiTrack = Track Ticks++-------------------------------------------------------------------------------+-- Operations+-------------------------------------------------------------------------------++-- | Play a MIDI note with the specified duration and default velocity.+midiNote :: Int -> Ticks -> MidiNote+midiNote root dur = MidiNote {noteNum = root, vel = 100, start = 0, noteDur = dur}++midiRest :: Ticks -> MidiNote+midiRest dur = MidiNote {noteNum = 60, vel = 0, start = 0, noteDur = dur}++-- | Start playing the specified 'MidiNote'.+keyDown :: MidiNote -> MidiEvent+keyDown n = (start n, NoteOn {channel = 0, key = noteNum n, velocity = vel n})++-- | Stop playing the specified 'MidiNote'.+keyUp :: MidiNote -> MidiEvent+keyUp n = (start n + noteDur n, NoteOn {channel = 0, key = noteNum n, velocity = 0})++-- | Play the specified 'MidiNote'.+playNote :: Int -> Ticks -> MidiTrack+playNote root dur = map ($ midiNote root dur) [keyDown, keyUp]++-- | Play a rest of the specified duration.+playRest :: Ticks -> MidiTrack+playRest dur = map ($ midiRest dur) [keyDown, keyUp]++-- | Merge two parallel MIDI tracks.+(><) :: MidiTrack -> MidiTrack -> MidiTrack+m1 >< m2 = removeTrackEnds $ m1 `merge` m2++-- | Convert a 'Dur' to 'Ticks'.+durToTicks :: Primitive d => Dur d -> Ticks+durToTicks d = prim d * 60 -- 1 Mezzo tick (a 32nd note) ~ 60 MIDI ticks++-------------------------------------------------------------------------------+-- Rendering+-------------------------------------------------------------------------------++-- | A basic skeleton of a MIDI file.+midiSkeleton :: MidiTrack -> Midi+midiSkeleton mel = Midi+    { fileType = MultiTrack+    , timeDiv = TicksPerBeat 480+    , tracks =+        [ [ (0, ChannelPrefix 0)+          , (0, TrackName " Grand Piano  ")+          , (0, InstrumentName "GM Device  1")+          , (0, TimeSignature 4 2 24 8)+          , (0, KeySignature 0 0)+          ]+        ++ mel+        ++ [ (0, TrackEnd) ]+        ]+    }++-- | Convert a 'Music' piece into a 'MidiTrack'.+musicToMidi :: Music m -> MidiTrack+musicToMidi (Note root dur) = playNote (prim root) (durToTicks dur)+musicToMidi (Rest dur) = playRest (durToTicks dur)+musicToMidi (m1 :|: m2) = musicToMidi m1 ++ musicToMidi m2+musicToMidi (m1 :-: m2) = musicToMidi m1 >< musicToMidi m2+musicToMidi (Chord c d) = foldr1 (><) notes+    where notes = map (`playNote` durToTicks d) $ prim c++-- | Create a MIDI file with the specified name and track.+createMidi :: FilePath -> MidiTrack -> IO ()+createMidi f notes = exportFile f $ midiSkeleton notes++-- | Create a MIDI file with the specified path and composition.+renderMusic :: FilePath -> Music m -> IO ()+renderMusic f m = createMidi f (musicToMidi m)
+ test/Main.hs view
@@ -0,0 +1,13 @@+++module Main where++import Test.Hspec++import PrimSpec+import TypeSpec++main :: IO ()+main = mapM_ hspec [ primSpec+                   , typeSpec+                   ]
+ test/PrimSpec.hs view
@@ -0,0 +1,304 @@+{-# OPTIONS_GHC -fdefer-type-errors #-}+-- {-# OPTIONS_GHC -w #-}+{-# LANGUAGE TypeInType, TypeOperators, GADTs, MultiParamTypeClasses, FlexibleInstances #-}++module PrimSpec where++import Test.Hspec+import GHC.TypeLits+import Control.Exception (evaluate)+import Test.ShouldNotTypecheck (shouldNotTypecheck)++import Mezzo.Model.Prim++primSpec :: Spec+primSpec =+    describe "Mezzo.Model.Prim" $ do+        describe "Vector operations" $ do+            it "should replicate elements" $+                timesReplicate `shouldBe` True+            it "should get the head of an optimised vector" $+                optVectorHead `shouldBe` True+            it "should get the head of a vector" $+                vectorHead `shouldBe` True+            it "should get the last element of an optimised vector" $+                optVectorLast `shouldBe` True+            it "should get the tail of a vector" $+                vectorTail `shouldBe` True+            it "should get the initial elements of a vector" $+                vectorInit `shouldBe` True+            it "should get the length of an optimised vector" $+                optVectorLength `shouldBe` True+            it "should get the length of a vector" $+                vectorLength `shouldBe` True+            it "should append optimised vectors" $+                optVectorAppend `shouldBe` True+            it "should append vectors" $+                vectorAppend `shouldBe` True+            it "should add an element to the end of a vector" $+                snoc `shouldBe` True+            it "should repeat an element to an optimised vector" $+                repeatVec `shouldBe` True++        describe "Matrix operations" $ do+            it "should vertically align matrices" $+                align `shouldBe` True+            it "should horizontally concatenate matrices" $+                matHConcat `shouldBe` True+            it "should vertically concatenate matrices" $+                matVConcat `shouldBe` True+            it "should convert vectors to column matrices" $+                vecToColMatrix `shouldBe` True++        describe "Arithmetic operations" $ do+            it "should calculate maximum of two numbers" $ do+                maxNat `shouldBe` True+            it "should calculate minimum of two numbers" $ do+                minNat `shouldBe` True++        describe "Constraint operations" $ do+            it "should apply a constraint to an optimised vector" $ do+                allSatisfy `shouldBe` True+                -- shouldNotTypecheck allSatisfyInv+            it "should apply a binary constraint to two optimised vectors" $ do+                allPairsSatisfy `shouldBe` True+                shouldNotTypecheck allPairsSatisfyInv+            it "should apply a binary constraint to two vectors" $ do+                allPairsSatisfy' `shouldBe` True+                shouldNotTypecheck allPairsSatisfyInv'+            it "should apply all constraints to a value" $ do+                satisfiesAll `shouldBe` True+                -- shouldNotTypecheck satisfiesAllInv+            it "should apply all constraints to all values" $ do+                allSatisfyAll `shouldBe` True+                -- shouldNotTypecheck allSatisfyAllInv+++timesReplicate :: (True ** 23) ~ (True :* (T :: Times 23)) => Bool+timesReplicate = True++optVectorHead :: (Head (True ** 4 :- End)) ~ True => Bool+optVectorHead = True++vectorHead :: (Head' (True :-- None)) ~ True => Bool+vectorHead = True++optVectorLast :: (Last (True ** 4 :- False ** 9 :- End)) ~ False => Bool+optVectorLast = True++vectorTail :: (Tail' (True :-- False :-- None)) ~ (False :-- None) => Bool+vectorTail = True++vectorInit :: (Init' (True :-- False :-- None)) ~ (True :-- None) => Bool+vectorInit = True++optVectorLength :: (Length (True ** 4 :- False ** 9 :- End)) ~ 13 => Bool+optVectorLength = True++vectorLength :: (Length' (True :-- False :-- None)) ~ 2 => Bool+vectorLength = True++optVectorAppend :: ((True ** 5 :- False ** 2 :- End) ++ End ++ (False ** 9 :- End))+                  ~ (True ** 5 :- False ** 2 :- False ** 9 :- End) => Bool+optVectorAppend = True++vectorAppend :: ((2 :-- 43 :-- None) ++. None ++. (6 :-- None))+                  ~ (2 :-- 43 :-- 6 :-- None) => Bool+vectorAppend = True++snoc :: ((2 :-- 5 :-- None) :-| 6) ~ (2 :-- 5 :-- 6 :-- None) => Bool+snoc = True++repeatVec :: (True +*+ 3) ~ (True ** 3 :- End) => Bool+repeatVec = True++matHConcat ::+          -- Normal matrices+        ( ((True ** 2 :- End :-- False ** 2 :- End :-- None)+           +|+ (False ** 5 :- End :-- True ** 5 :- End :-- None))+          ~ ((True ** 2 :- False ** 5 :- End :-- False ** 2 :- True ** 5 :- End :-- None))+          -- Right empty+        , ((True ** 2 :- End :-- False ** 2 :- End :-- None)+           +|+ (End :-- End :-- None))+          ~ (True ** 2 :- End :-- False ** 2 :- End :-- None)+          -- Left empty+        , ((End :-- End :-- None)+           +|+ (True ** 2 :- End :-- False ** 2 :- End :-- None))+          ~ (True ** 2 :- End :-- False ** 2 :- End :-- None)+          -- Both empty+        , (None +|+ None) ~ None+        ) => Bool+matHConcat = True++align ::+          -- Right fragment+        ( Align (True ** 2 :- False ** 2 :- End :-- None) (True ** 4 :- End :-- None)+          ~ '(True ** 2 :- False ** 2 :- End :-- None, True ** 2 :- True ** 2 :- End :-- None)+          -- Left fragment+        , Align (False ** 18 :- End :-- None) (True ** 8 :- False ** 10 :- End :-- None)+          ~ '(False ** 8 :- False ** 10 :- End :-- None, True ** 8 :- False ** 10 :- End :-- None)+          -- No fragment+        , Align (True ** 4 :- End :-- None) (False ** 4 :- End :-- None)+          ~ '(True ** 4 :- End :-- None, False ** 4 :- End :-- None)+          -- Both fragment+        , Align (False ** 18 :- True ** 3 :- End :-- None) (True ** 8 :- False ** 13 :- End :-- None)+          ~ '(False ** 8 :- False ** 10 :- True ** 3 :- End :-- None, True ** 8 :- False ** 10 :- False ** 3 :- End :-- None)+        ) => Bool+align = True++matVConcat ::+          -- No fragmentation+        (    ((True ** 3 :- False ** 6 :- End :-- None)+          +-+ (False ** 3 :- True ** 6 :- End :-- None))+          ~ (True ** 3 :- False ** 6 :- End :-- False ** 3 :- True ** 6 :- End :-- None)+          -- Top fragment+        ,    ((True ** 9 :- End :-- None)+          +-+ (False ** 3 :- True ** 6 :- End :-- None))+          ~ (True ** 3 :- True ** 6 :- End :-- False ** 3 :- True ** 6 :- End :-- None)+          -- Bottom fragment+        ,    ((True ** 3 :- False ** 6 :- End :-- None)+          +-+ (False ** 9 :- End :-- None))+          ~ (True ** 3 :- False ** 6 :- End :-- False ** 3 :- False ** 6 :- End :-- None)+          -- Both fragment+        ,    ((True ** 3 :- False ** 6 :- End :-- None)+          +-+ (False ** 6 :- True ** 3 :- End :-- None))+          ~ (True ** 3 :- False ** 3 :- False ** 3 :- End :-- False ** 3 :- False ** 3 :- True ** 3 :- End :-- None)+          -- More voices+        ,    ((True ** 2 :- False ** 8 :- End :-- False ** 2 :- True ** 8 :- End :-- None)+          +-+ (False ** 4 :- True ** 6 :- End :-- None)+          +-+ (True ** 1 :- False ** 8 :- True ** 1 :- End :-- False ** 1 :- True ** 8 :- False ** 1 :- End :-- None))+          ~    ((True ** 1 :- True ** 1 :- False ** 2 :- False ** 5 :- False ** 1 :- End)+            :-- (False ** 1 :- False ** 1 :- True ** 2 :- True ** 5 :- True ** 1 :- End)+            :-- (False ** 1 :- False ** 1 :- False ** 2 :- True ** 5 :- True ** 1 :- End)+            :-- (True ** 1 :- False ** 1 :- False ** 2 :- False ** 5 :- True ** 1 :- End)+            :-- (False ** 1 :- True ** 1 :- True ** 2 :- True ** 5 :- False ** 1 :- End) :-- None+            )+        ) => Bool+matVConcat = True++vecToColMatrix ::+        ( (VectorToColMatrix (True :-- False :-- None) 24)+          ~ (False ** 24 :- End :-- True ** 24 :- End :-- None)+        , (VectorToColMatrix None 11) ~ None+        ) => Bool+vecToColMatrix = True+++-- Let's assume that the Boolean functions work...++maxNat :: ((MaxN 5 9) ~ 9, (MaxN 7 4) ~ 7, (MaxN 0 8) ~ 8, (MaxN 1 0) ~ 1, (MaxN 3 3) ~ 3+          , (MaxN (MaxN 133 43) 235) ~ 235) => Bool+maxNat = True++minNat :: ((MinN 5 9) ~ 5, (MinN 7 4) ~ 4, (MinN 0 8) ~ 0, (MinN 1 0) ~ 0, (MinN 3 3) ~ 3+          , (MinN (MinN 133 43) 235) ~ 43) => Bool+minNat = True++allSatisfy :: (AllSatisfy Num (Int ** 1 :- Integer ** 1 :- Double ** 1 :- End)) => Bool+allSatisfy = True++-- allSatisfyInv :: (AllSatisfy Integral (Double ** 1 :- String ** 1 :- Bool ** 1 :- End)) => Bool+-- allSatisfyInv = True++class TestConstraint (a :: Nat) (b :: Nat)+instance (MaxN a b ~ b) => TestConstraint a b++allPairsSatisfy :: (AllPairsSatisfy TestConstraint+                    (1 ** 1 :- 3 ** 1 :- 5 ** 1 :- End) (2 ** 1 :- 4 ** 1 :- 6 ** 1 :- End)) => Bool+allPairsSatisfy = True++allPairsSatisfyInv :: (AllPairsSatisfy TestConstraint (4 ** 1 :- End) (1 ** 1 :- End)) => Bool+allPairsSatisfyInv = True++allPairsSatisfy' :: (AllPairsSatisfy' TestConstraint+                    (1 :-- 3 :-- 5 :-- None) (2 :-- 4 :-- 6 :-- None)) => Bool+allPairsSatisfy' = True++allPairsSatisfyInv' :: (AllPairsSatisfy' TestConstraint (2 :-- None) (1 :-- None)) => Bool+allPairsSatisfyInv' = True++satisfiesAll :: (SatisfiesAll '[Num, Integral, Show] Int) => Bool+satisfiesAll = True++-- Doesn't work unfortunately+-- satisfiesAllInv :: (SatisfiesAll '[Num, Integral, Show] Bool) => Bool+-- satisfiesAllInv = True++allSatisfyAll :: (AllSatisfyAll '[Num, Show] (Double :-- Int :-- Integer :-- None)) => Bool+allSatisfyAll = True++-- allSatisfyAllInv :: (AllSatisfyAll '[Num, Show] (Bool :-- String :-- Integer :-- None)) => Bool+-- allSatisfyAllInv = True++++{- MALFORMED TYPE SIGNATURES: should never typecheck+-- (Comment out line above to expose)++timesReplicateW :: (True ** 23) ~ (True :* (T :: Times 1)) => Bool+optVectorHeadW :: (Head (True ** 4 :- End)) ~ False => Bool+vectorHeadW :: (Head' (True :-- None)) ~ False => Bool+optVectorLastW :: (Last (True ** 4 :- False ** 9 :- End)) ~ True => Bool+vectorTailW :: (Tail' (True :-- False :-- None)) ~ (True :-- None) => Bool+vectorInitW :: (Init' (True :-- False :-- None)) ~ (False :-- None) => Bool+optVectorLengthW :: (Length (True ** 4 :- False ** 9 :- End)) ~ 12 => Bool+vectorLengthW :: (Length' (True :-- False :-- None)) ~ 3 => Bool+optVectorAppendW :: ((True ** 5 :- False ** 2 :- End) ++ (False ** 9 :- End))+                  ~ (True ** 5 :- False ** 11 :- End) => Bool+vectorAppendW :: ((2 :-- 43 :-- None) ++. None ++. (6 :-- None))+                ~ (2 :-- 3 :-- 6 :-- None) => Bool+snocW :: ((2 :-- 5 :-- None) :-| 6) ~ (2 :-- 5 :-- 4 :-- None) => Bool+repeatVecW :: (True +*+ 3) ~ (True ** 4 :- End) => Bool+matHConcatW ::+        (  ((True ** 2 :- End :-- False ** 2 :- End :-- None)+           +|+ (False ** 5 :- End :-- True ** 5 :- End :-- None))+           ~ ((True ** 2 :- False ** 5 :- End :-- True ** 2 :- True ** 5 :- End :-- None))++        ,  ((True ** 2 :- End :-- False ** 2 :- End :-- None)+           +|+ (End :-- None))+           ~ (True ** 2 :- End :-- False ** 2 :- End :-- None)++        , (None +|+ None) ~ (None :-- None)+        )+          => Bool+alignW ::+          -- Right fragment+        ( Align (True ** 2 :- False ** 2 :- End :-- None) (True ** 4 :- End :-- None)+          ~ '(True ** 2 :- False ** 2 :- End :-- None, True ** 1 :- True ** 3 :- End :-- None)+          -- Left fragment+        , Align (False ** 18 :- End :-- None) (True ** 8 :- False ** 10 :- End :-- None)+          ~ '(False ** 7 :- False ** 11 :- End :-- None, True ** 8 :- False ** 10 :- End :-- None)+          -- No fragment+        , Align (True ** 4 :- End :-- None) (False ** 4 :- End :-- None)+          ~ '(True ** 4 :- End :-- None, True ** 4 :- End :-- None)+          -- Both fragment+        , Align (False ** 18 :- True ** 3 :- End :-- None) (True ** 8 :- False ** 13 :- End :-- None)+          ~ '(False ** 8 :- False ** 9 :- True ** 4 :- End :-- None, True ** 8 :- False ** 10 :- False ** 3 :- End :-- None)+        ) => Bool+vecToColMatrixW ::+        ( (VectorToColMatrix (True :-- False :-- None) 24)+          ~ (False ** 24 :- End :-- False ** 24 :- End :-- None)+        , (VectorToColMatrix None 11) ~ (True ** 11 :- End :-- None)+        ) => Bool++allSatisfyW :: (AllSatisfy Num (Int ** 1 :- Bool ** 1 :- Double ** 1 :- End)) => Bool+++timesReplicateW = True+optVectorHeadW = True+vectorHeadW = True+optVectorLastW = True+vectorTailW = True+vectorInitW = True+optVectorLengthW = True+vectorLengthW = True+optVectorAppendW = True+vectorAppendW = True+snocW = True+repeatVecW = True+matHConcatW = True+alignW = True+vecToColMatrixW = True+allSatisfyW = True++-- -}
+ test/TypeSpec.hs view
@@ -0,0 +1,79 @@+{-# OPTIONS_GHC -fdefer-type-errors #-}+-- {-# OPTIONS_GHC -w #-}+{-# LANGUAGE TypeInType, TypeOperators, GADTs, MultiParamTypeClasses, FlexibleInstances #-}++module TypeSpec where++import Test.Hspec+import GHC.TypeLits+import Control.Exception (evaluate)+import Data.Proxy+import Test.ShouldNotTypecheck (shouldNotTypecheck)++import Mezzo.Model.Types++typeSpec :: Spec+typeSpec =+    describe "Mezzo.Model.Types" $ do+        describe "Harmonic types" $ do+            it "should convert roots to pitches" $ do+                rootToPitch `shouldBe` True+                shouldNotTypecheck rootToPitchInv+            it "should sharpen roots" $ do+                sharpen `shouldBe` True+                shouldNotTypecheck sharpenInv+            it "should flatten roots" $ do+                flatten `shouldBe` True+                shouldNotTypecheck flattenInv+            it "should make intervals" $ do+                flatten `shouldBe` True++rootToPitch ::+        ( (RootToPitch (PitchRoot (Pitch C Natural Oct3)) ~ (Pitch C Natural Oct3))+        , (RootToPitch (DegreeRoot (Key D Flat MinorMode) IV) ~ (Pitch F Sharp Oct2))+        ) => Bool+rootToPitch = True++rootToPitchInv :: Proxy (RootToPitch (DegreeRoot (Key D Flat MinorMode) IV))+               -> Proxy (Pitch E Natural Oct2)+rootToPitchInv = id++sharpen :: ( (Sharpen (PitchRoot (Pitch C Natural Oct3))) ~ (PitchRoot (Pitch C Sharp Oct3))+           , (Sharpen (PitchRoot (Pitch E Natural Oct3))) ~ (PitchRoot (Pitch F Natural Oct3))+           , (Sharpen (PitchRoot (Pitch C Flat Oct3))) ~ (PitchRoot (Pitch C Natural Oct3))+           , (Sharpen (PitchRoot (Pitch B Natural Oct3))) ~ (PitchRoot (Pitch C Natural Oct4))+           , (Sharpen (DegreeRoot (Key F Sharp MinorMode) VI)) ~ (PitchRoot (Pitch D Sharp Oct3))+           , (Sharpen (DegreeRoot (Key E Sharp MajorMode) VII)) ~ (PitchRoot (Pitch F Natural Oct3))+           ) => Bool+sharpen = True++sharpenInv :: Proxy '(Sharpen (PitchRoot (Pitch B Flat Oct5)), Sharpen (DegreeRoot (Key C Flat MajorMode) IV))+           -> Proxy '(PitchRoot (Pitch C Flat Oct6), PitchRoot (Pitch F Natural Oct3))+sharpenInv = id++flatten :: ( (Flatten (PitchRoot (Pitch D Natural Oct3))) ~ (PitchRoot (Pitch D Flat Oct3))+           , (Flatten (PitchRoot (Pitch F Natural Oct3))) ~ (PitchRoot (Pitch E Natural Oct3))+           , (Flatten (PitchRoot (Pitch C Sharp Oct3))) ~ (PitchRoot (Pitch C Natural Oct3))+           , (Flatten (PitchRoot (Pitch C Natural Oct3))) ~ (PitchRoot (Pitch B Natural Oct2))+           , (Flatten (DegreeRoot (Key F Sharp MinorMode) VI)) ~ (PitchRoot (Pitch D Flat Oct3))+           , (Flatten (DegreeRoot (Key E Sharp MajorMode) VII)) ~ (PitchRoot (Pitch E Flat Oct3))+           ) => Bool+flatten = True++flattenInv :: Proxy '(Flatten (PitchRoot (Pitch C Sharp Oct5)), Flatten (DegreeRoot (Key C Flat MajorMode) V))+           -> Proxy '(PitchRoot (Pitch B Sharp Oct4), PitchRoot (Pitch E Natural Oct3))+flattenInv = id++makeInterval ::+            ( (MakeInterval (Pitch C Natural Oct3) (Pitch E Natural Oct3)) ~ (Interval Maj Third)+            , (MakeInterval (Pitch E Natural Oct3) (Pitch C Natural Oct3)) ~ (Interval Maj Third)+            , (MakeInterval (Pitch C Natural Oct3) (Pitch B Flat Oct3)) ~ (Interval Min Seventh)+            , (MakeInterval (Pitch E Sharp Oct3) (Pitch E Sharp Oct3)) ~ (Interval Perf Unison)+            , (MakeInterval (Pitch E Natural Oct3) (Pitch F Flat Oct3)) ~ (Interval Perf Unison)+            , (MakeInterval (Pitch E Sharp Oct3) (Pitch F Flat Oct3)) ~ (Interval Min Second)+            , (MakeInterval (Pitch F Sharp Oct3) (Pitch G Flat Oct3)) ~ (Interval Perf Unison)+            , (MakeInterval (Pitch C Natural Oct3) (Pitch C Natural Oct4)) ~ (Interval Perf Octave)+            , (MakeInterval (Pitch E Flat Oct3) (Pitch F Flat Oct4)) ~ Compound+            , (MakeInterval (Pitch E Sharp Oct3) (Pitch F Flat Oct4)) ~ (Interval Maj Seventh)+            ) => Bool+makeInterval = True