content: 
  -----------------------------------------------------------------------------
  -- |
  -- Module      :  Mezzo.Model.Rules.Strict
  -- Description :  MIDI exporting
  -- Copyright   :  (c) Dima Szamozvancev
  -- License     :  MIT
  --
  -- Maintainer  :  ds709@cam.ac.uk
  -- Stability   :  experimental
  -- Portability :  portable
  --
  -- Types and constraints encoding the rules of classical music.
  --
  -----------------------------------------------------------------------------
  
  module Mezzo.Model.Rules.Strict
      ( ValidMelConcatStrict
      , ValidMelIntervalStrict
      , ValidHarmConcat
      , ValidHomConcat
      , ValidMelMatrixMotion
      , ValidChordType
      ) where
  
  import Mezzo.Model.Types
  import Mezzo.Model.Prim
  import Mezzo.Model.Harmony
  import Mezzo.Model.Errors
  import Mezzo.Model.Rules.Classical
  
  import GHC.TypeLits
  import Data.Kind
  
  
  -- | 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 ValidMelIntervalStrict (e :: PitchPair) (i :: IntervalType)
  instance {-# OVERLAPPING #-}       ValidMelIntervalStrict e (Interval Aug Unison)
  instance {-# OVERLAPS #-} PitchPairError "Augmented melodic intervals are not permitted: " e
                                  => ValidMelIntervalStrict e (Interval Aug a)
  instance {-# OVERLAPS #-} PitchPairError "Diminished melodic intervals are not permitted: " e
                                  => ValidMelIntervalStrict e (Interval Dim a)
  instance {-# OVERLAPPING #-} PitchPairError "Seventh intervals are not permitted in melody: " e
                                  => ValidMelIntervalStrict e (Interval a Seventh)
  instance {-# OVERLAPPING #-} PitchPairError "Compound intervals are not permitted in melody: " e
                                  => ValidMelIntervalStrict e Compound
  instance {-# OVERLAPPABLE #-}      ValidMelIntervalStrict e 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 ValidMelLeapStrict (p1 :: PitchType) (p2 :: PitchType)
  instance {-# OVERLAPPING #-}  ValidMelLeapStrict Silence Silence
  instance {-# OVERLAPPING #-}  ValidMelLeapStrict Silence (Pitch pc acc oct)
  instance {-# OVERLAPPING #-}  ValidMelLeapStrict (Pitch pc acc oct) Silence
  instance {-# OVERLAPPABLE #-} ValidMelIntervalStrict '(a, b) (MakeInterval a b) => ValidMelLeapStrict 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 ValidMelAppendStrict (a :: Voice l1) (b :: Voice l2)
  instance {-# OVERLAPPING #-}  ValidMelAppendStrict End a
  instance {-# OVERLAPPING #-}  ValidMelAppendStrict a End
  instance {-# OVERLAPPABLE #-} ValidMelLeapStrict (Last vs1) (Head vs2) => ValidMelAppendStrict 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 ValidMelConcatStrict (ps1 :: Partiture n l1) (ps2 :: Partiture n l2)
  instance {-# OVERLAPPING #-}       ValidMelConcatStrict None None
  instance {-# OVERLAPPABLE #-} (ValidMelAppendStrict v1 v2, ValidMelConcatStrict vs1 vs2)
                                  => ValidMelConcatStrict (v1 :-- vs1) (v2 :-- vs2)
  
  -------------------------------------------------------------------------------
  -- Voice leading constraints
  -------------------------------------------------------------------------------
  
  -- | 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)
  
  -------------------------------------------------------------------------------
  -- Chord constraints
  -------------------------------------------------------------------------------
  
  -- | Ensures that the chord is not a major seventh chord.
  class ValidChordType (c :: ChordType n)
  instance ValidChordType (Dyad r t i)
  instance ValidChordType (Triad r t i)
  instance {-# OVERLAPPING #-} ChordError "Major seventh chords are not permitted: " r " Maj7"
                                  => ValidChordType (Tetrad r MajSeventh i)
  instance {-# OVERLAPPABLE #-} ValidChordType (Tetrad r t i)
  