-----------------------------------------------------------------------------
-- |
-- Module      :  Mezzo.Model.Rules.Classical
-- 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.Classical
    ( ValidMelConcat
    , ValidHarmConcat
    , ValidHomConcat
    , ValidPitch
    , ValidMotion
    ) where

import Mezzo.Model.Types
import Mezzo.Model.Prim
import Mezzo.Model.Harmony
import Mezzo.Model.Errors

import GHC.TypeLits
import Data.Kind

-------------------------------------------------------------------------------
-- Melodic constraints
-------------------------------------------------------------------------------

-- | Ensures that melodic intervals are valid.
--
-- A melodic interval is invalid if it is
--
--  * any seventh interval.
class ValidMelInterval (e :: PitchPair) (i :: IntervalType)
instance {-# OVERLAPPING #-} PitchPairError "Major sevenths are not permitted in melody: " e
                                => ValidMelInterval e (Interval Maj Seventh)
instance {-# OVERLAPPING #-} PitchPairError "Compound intervals are not permitted in melody: " e
                                => ValidMelInterval e Compound
instance {-# OVERLAPPABLE #-}      ValidMelInterval 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 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 '(a, b) (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 (e :: PitchPair) (i :: IntervalType)
instance {-# OVERLAPPING #-} PitchPairError "Minor seconds are not permitted in harmony: " e
                                => ValidHarmInterval e (Interval Aug Unison)
instance {-# OVERLAPPING #-} PitchPairError "Minor seconds are not permitted in harmony: " e
                                => ValidHarmInterval e (Interval Min Second)
instance {-# OVERLAPPING #-} PitchPairError "Major sevenths are not permitted in harmony: " e
                                => ValidHarmInterval e (Interval Maj Seventh)
instance {-# OVERLAPPING #-} PitchPairError "Major sevenths are not permitted in harmony: " e
                                => ValidHarmInterval e (Interval Dim Octave)
instance {-# OVERLAPPING #-} PitchPairError "Augmented octaves are not permitted in harmony: " e
                                => ValidHarmInterval e (Interval Aug Octave)
instance {-# OVERLAPPABLE #-}      ValidHarmInterval e 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 '(a, b) (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)

-- | 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 ValidHomConcat (ps :: (Partiture n1 l, Partiture n2 l))
instance {-# OVERLAPPING #-}       ValidHomConcat '(None, vs)
instance {-# OVERLAPPABLE #-} ( ValidHomConcat '(vs, us)
                              , AllSatisfyAll '[ValidHarmDyadsInVectors v] us)
                                => ValidHomConcat '((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 (DyPair p1 p2 q1 q2) (MakeInterval p1 p2) (MakeInterval q1 q2))
                        (ContraryMotion (MakeInterval p1 p2) (MakeInterval q1 q2)))
                    (If (p2 <<? q2)
                        (ContraryMotion (MakeInterval p1 p2) (MakeInterval q1 q2))
                        (DirectMotion (DyPair p1 p2 q1 q2) (MakeInterval p1 p2) (MakeInterval q1 q2))))

-- | 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)

-------------------------------------------------------------------------------
-- Note constraints
-------------------------------------------------------------------------------

class ValidPitch (p :: PitchType)
instance PitchError "Note can't be lower than C natural of octave -1: " (Pitch C Flat Oct_1)
                                => ValidPitch (Pitch C Flat Oct_1)
instance PitchError "Note can't be higher than B natural of octave 8: " (Pitch B Sharp Oct8)
                                => ValidPitch (Pitch B Sharp Oct8)
instance {-# OVERLAPPABLE #-} ValidPitch p