{-# LANGUAGE ViewPatterns #-}

-----------------------------------------------------------------------------
-- |
-- 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
    (
    -- * Types and operations
      Quality (..)
    , DegreeC (..)
    , TimeSignature
    , TimeSig (..)
    , KeyToQual
    , KeyToOtherQual
    , IsMajor
    , IsMinor
    -- * Functional harmony
    -- ** Types and constructors
    , ProgType (..)
    , Phrase (..)
    , Cadence (..)
    , Tonic (..)
    , Dominant (..)
    , Subdominant (..)
    , ChordsToPartiture
    , ProgTypeToChords
    , FromProg
    -- ** Singletons
    , Prog (..)
    , Ton (..)
    , Dom (..)
    , Sub (..)
    , Cad (..)
    , Phr (..)
    )
    where

import Mezzo.Model.Reify
import Mezzo.Model.Types hiding (IntervalClass (..))
import Mezzo.Model.Prim
import Mezzo.Model.Harmony.Chords

import GHC.TypeLits
import Data.Kind (Type)

infix 5 :=

-------------------------------------------------------------------------------
-- Types and operations
-------------------------------------------------------------------------------

-- | 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 and octave.
data DegreeC (d :: ScaleDegree) (q :: Quality) (k :: KeyType) (i :: Inversion) (o :: OctaveNum) where
    DegChord :: DegreeC d q k i o

-- | The number of beats in a bar.
type TimeSignature = Nat

-- | Singleton for 'TimeSignature'.
data TimeSig (t :: TimeSignature) = TimeSig

-- | Convert the key mode to the corresponding chord quality (i.e., major mode into a major chord).
type family KeyToQual (k :: KeyType) where
    KeyToQual (Key _ _ MajorMode) = MajQ
    KeyToQual (Key _ _ MinorMode) = MinQ

-- | Convert the key mode to the opposite chord quality (i.e., major mode into a minor chord).
type family KeyToOtherQual (k :: KeyType) where
    KeyToOtherQual (Key _ _ MajorMode) = MinQ
    KeyToOtherQual (Key _ _ MinorMode) = MajQ

-- | Convert a quality to a seventh chord type.
type family QualToType (q :: Quality) :: TetradType where
    QualToType MajQ = DoubledT MajTriad
    QualToType MinQ = DoubledT MinTriad
    QualToType DomQ = MajMinSeventh
    QualToType DimQ = DimSeventh

-- | Enforce that the key is in major mode.
class IsMajor (k :: KeyType) (s :: Symbol)
instance IsMajor (Key pc acc MajorMode) s
instance TypeError (Text "Can't have a " :<>: Text s :<>: Text " in minor mode.")
    => IsMajor (Key pc acc MinorMode) s

-- | Enforce that the key is in minor mode.
class IsMinor (k :: KeyType) (s :: Symbol)
instance IsMinor (Key pc acc MinorMode) s
instance TypeError (Text "Can't have a " :<>: Text s :<>: Text " in minor mode.")
    => IsMinor (Key pc acc MajorMode) s

-------------------------------------------------------------------------------
-- Functional harmony
-------------------------------------------------------------------------------

-- | A functionally described piece of music, built from multiple phrases.
data ProgType (k :: KeyType) (l :: Nat) where
    -- | A cadential phrase, ending the progression.
    CadPhrase :: Cadence k l -> ProgType k l
    -- | Add a new phrase to the beginning of the progression.
    (:=) :: Phrase k l -> ProgType k (n - l) -> ProgType k n

-- | A phrase matching a specific functional progression.
data Phrase (k :: KeyType) (l :: Nat) where
    -- | A tonic-dominant-tonic phrase.
    PhraseIVI :: Tonic k (l2 - l1) -> Dominant k l1 -> Tonic k (l - l2) -> Phrase k l
    -- | A dominant-tonic phrase.
    PhraseVI  :: Dominant k l1 -> Tonic k (l - l1) -> Phrase k l
    -- | A tonic phrase.
    PhraseI  :: Tonic k l -> 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    :: DegreeC V MajQ k Inv1 (OctPred o) -> DegreeC I q k Inv0 o -> Cadence k 2
    -- | Authentic cadence with dominant seventh fifth chord.
    AuthCad7   :: DegreeC V DomQ k Inv2 (OctPred o) -> DegreeC I q k Inv0 o -> Cadence k 2
    -- | Authentic cadence with diminished seventh chord.
    AuthCadVii :: DegreeC VII DimQ k Inv1 (OctPred o) -> DegreeC I q k Inv0 o -> Cadence k 2
    -- | Authentic cadence with a cadential 6-4 chord
    AuthCad64  :: DegreeC I q k Inv2 o -> DegreeC V DomQ k Inv3 (OctPred o) -> DegreeC I q k Inv1 o -> Cadence k 3
    -- | Deceptive cadence from a dominant fifth to a sixth.
    DeceptCad  :: DegreeC V DomQ k Inv2 o -> DegreeC VI q k Inv1 o -> Cadence k 2
    -- | Full cadence from subdominant to dominant to tonic.
    FullCad    :: Subdominant k l1 -> Cadence k (l - l1) -> Cadence k l
    -- | No cadence.
    NoCad      :: Cadence k 0

-- | A tonic chord.
data Tonic (k :: KeyType) (l :: Nat) where
    -- | A major tonic chord.
    TonT   :: DegreeC I (KeyToQual k) k Inv0 o -> Tonic k 1
    -- | Doubled tonics.
    TonTT  :: Tonic k l1 -> Tonic k (l - l1) -> Tonic k l

-- | A dominant chord progression.
data Dominant (k :: KeyType) (l :: Nat) where
    -- | Major fifth dominant.
    DomVM   :: DegreeC V MajQ k Inv2 o -> Dominant k 1
    -- | Seventh chord fifth degree dominant.
    DomV7   :: DegreeC V DomQ k Inv2 o -> Dominant k 1
    -- | Diminished seventh degree dominant.
    DomVii0 :: DegreeC VII DimQ k i o -> Dominant k 1
    -- | Secondary dominant followed by dominant.
    DomSecD :: DegreeC II DomQ k Inv0 o -> DegreeC V DomQ k Inv2 (OctPred o) -> Dominant k 2
    -- | Subdominant followed by dominant.
    DomSD   :: Subdominant k l1 -> Dominant k (l - l1) -> Dominant k l
    -- | Doubled dominants.
    DomDD   :: Dominant k l1 -> Dominant k (l - l1) -> Dominant k l

-- | A subdominant chord progression.
data Subdominant (k :: KeyType) (l :: Nat) where
    -- | Major fourth subdominant.
    SubIV      :: DegreeC IV (KeyToQual k) k i o -> Subdominant k 1
    -- | Minor second subdominant.
    SubIIm     :: DegreeC II MinQ k i o -> Subdominant k 1
    -- | Minor third followed by major fourth subdominant.
    SubIIImIVM :: DegreeC III MinQ k i1 o -> DegreeC IV MajQ k i2 (OctPred o) -> Subdominant k 2
    -- | Doubled subdominants.
    SubSS      :: Subdominant k l1 -> Subdominant k (l - l1) -> Subdominant k l

-- | Convert a degree chord to a tetrad.
type DegToChord (dc :: DegreeC d q k i o) = Tetrad (DegreeRoot k (Degree d Natural o)) (QualToType q) i

-- | Convert a cadence to chords.
type family CadToChords (l :: Nat) (c :: Cadence k l) :: Vector (ChordType 4) l where
    CadToChords 2 (AuthCad d1 d2)      = DegToChord d1 :-- DegToChord d2 :-- None
    CadToChords 2 (AuthCad7 d1 d2)     = DegToChord d1 :-- DegToChord d2 :-- None
    CadToChords 2 (AuthCadVii d1 d2)   = DegToChord d1 :-- DegToChord d2 :-- None
    CadToChords 2 (DeceptCad d1 d2)    = DegToChord d1 :-- DegToChord d2 :-- None
    CadToChords 3 (AuthCad64 d1 d2 d3) = DegToChord d1 :-- DegToChord d2 :-- DegToChord d3 :-- None
    CadToChords l (FullCad (s :: Subdominant k l1) c) = SubdomToChords l1 s ++. CadToChords (l - l1) c
    CadToChords 0 NoCad                = None

-- | Convert a tonic to chords.
type family TonToChords (l :: Nat) (t :: Tonic k l) :: Vector (ChordType 4) l where
    TonToChords 1 (TonT d) = DegToChord d :-- None
    TonToChords l (TonTT (t1 :: Tonic k l1) t2) = TonToChords l1 t1 ++. TonToChords (l - l1) t2

-- | 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 2 (DomSecD d1 d2) = DegToChord d1 :-- DegToChord d2 :-- None
    DomToChords l (DomSD (s :: Subdominant k l1) d) =
        SubdomToChords l1 s ++. DomToChords (l - l1) d
    DomToChords l (DomDD (d1 :: Dominant k l1) d2)  =
        DomToChords l1 d1 ++. DomToChords (l - l1) d2

-- | Convert a subdominant to chords.
type family SubdomToChords (l :: Nat) (t :: Subdominant k l) :: Vector (ChordType 4) l where
    SubdomToChords 1 (SubIIm d)         = DegToChord d :-- None
    SubdomToChords 1 (SubIV d)          = DegToChord d :-- None
    SubdomToChords 2 (SubIIImIVM d1 d2) = DegToChord d1 :-- DegToChord d2 :-- None
    SubdomToChords l (SubSS (s1 :: Subdominant k l1) s2) =
        SubdomToChords l1 s1 ++. SubdomToChords (l - l1) s2

-- | Convert a phrase to chords.
type family PhraseToChords (l :: Nat) (p :: Phrase k l) :: Vector (ChordType 4) l where
    PhraseToChords l (PhraseIVI (t1 :: Tonic k (l2 - dl)) (d :: Dominant k dl)
                                (t2 :: Tonic k (l - l2))) =
        TonToChords (l2 - dl) t1 ++. DomToChords dl d ++. TonToChords (l - l2) t2
    PhraseToChords l (PhraseVI (d :: Dominant k dl) t) =
        DomToChords dl d ++. TonToChords (l - dl) t
    PhraseToChords l (PhraseI t) =
        TonToChords l t

-- | Convert a piece to chords.
type family ProgTypeToChords (l :: Nat) (p :: ProgType k l) :: Vector (ChordType 4) l where
    ProgTypeToChords l (CadPhrase (c :: Cadence k l)) = CadToChords l c
    ProgTypeToChords l ((p :: Phrase k l1) := ps) =
        PhraseToChords l1 p ++. ProgTypeToChords (l - l1) ps

-- | Convert a vector of chords ("chord progression") into a 'Partiture'.
type family ChordsToPartiture (v :: Vector (ChordType n) l) (t :: TimeSignature) :: Partiture n (l * t * 8) where
    ChordsToPartiture None _ = (End :-- End :-- End :-- End :-- None)
    ChordsToPartiture (c :-- cs) l = FromChord c (l * 8) +|+ ChordsToPartiture cs l

-- | Convert a progression with a time signature into a 'Partiture'.
type family FromProg (p :: ProgType k l) (t :: TimeSignature) :: Partiture 4 (l * t * 8) where
    FromProg (p :: ProgType k l) t = ChordsToPartiture (ProgTypeToChords l p) t


-- Singletons

-- | The singleton type for 'Tonic'.
data Ton (t :: Tonic k d) = Ton

-- | The singleton type for 'Tonic'.
data Dom (d :: Dominant k d) = Dom

-- | The singleton type for 'Tonic'.
data Sub (s :: Subdominant k d) = Sub

-- | The singleton type for 'Tonic'.
data Cad (c :: Cadence k d) = Cad

-- | The singleton type for 'Tonic'.
data Phr (p :: Phrase k d) = Phr

-- | The singleton type for 'Tonic'.
data Prog (p :: ProgType k l) = Prog

-------------------------------------------------------------------------------
-- Primitive instances
-------------------------------------------------------------------------------

-- Tonic

instance (ch ~ DegToChord d, IntListRep ch) => Primitive (TonT d) where
    type Rep (TonT d) = [[Int]]
    prim _ = [prim (Cho @4 @ch)]
    pretty _ = "Ton"

instance (IntLListRep t1, IntLListRep t2) => Primitive (TonTT (t1 :: Tonic k dur1) (t2 :: Tonic k (l - dur1)) :: Tonic k l) where
    type Rep (TonTT t1 t2) = [[Int]]
    prim _ = prim (Ton @k @dur1 @t1) ++ prim (Ton @k @(l - dur1) @t2)
    pretty _ = pretty (Ton @k @dur1 @t1) ++ " | " ++ pretty (Ton @k @(l - dur1) @t2)

-- Dominant

instance (ch ~ DegToChord d, IntListRep ch) => Primitive (DomVM d) where
    type Rep (DomVM d) = [[Int]]
    prim _ = [prim (Cho @4 @ch)]
    pretty _ = "Dom Maj"

instance (ch ~ DegToChord d, IntListRep ch) => Primitive (DomV7 d) where
    type Rep (DomV7 d) = [[Int]]
    prim _ = [prim (Cho @4 @ch)]
    pretty _ = "Dom Maj7"

instance (ch ~ DegToChord d, IntListRep ch) => Primitive (DomVii0 d) where
    type Rep (DomVii0 d) = [[Int]]
    prim _ = [prim (Cho @4 @ch)]
    pretty _ = "Dom VII0"

instance (ch1 ~ DegToChord d1, IntListRep ch1, ch2 ~ DegToChord d2, IntListRep ch2) => Primitive (DomSecD d1 d2) where
    type Rep (DomSecD d1 d2) = [[Int]]
    prim _ = [prim (Cho @4 @ch1)] ++ [prim (Cho @4 @ch2)]
    pretty _ = "Dom SecD"

instance (IntLListRep sd, IntLListRep d) => Primitive (DomSD (sd :: Subdominant k sdur) (d :: Dominant k (l - sdur)) :: Dominant k l) where
    type Rep (DomSD sd d) = [[Int]]
    prim _ = prim (Sub @k @sdur @sd) ++ prim (Dom @k @(l - sdur) @d)
    pretty _ = pretty (Sub @k @sdur @sd) ++ " | " ++ pretty (Dom @k @(l - sdur) @d)

instance (IntLListRep d1, IntLListRep d2) => Primitive (DomDD (d1 :: Dominant k dur1) (d2 :: Dominant k (l - dur1)) :: Dominant k l) where
    type Rep (DomDD d1 d2) = [[Int]]
    prim _ = prim (Dom @k @dur1 @d1) ++ prim (Dom @k @(l - dur1) @d2)
    pretty _ = pretty (Dom @k @dur1 @d1) ++ " | " ++ pretty (Dom @k @(l - dur1) @d2)

-- Subdominant

instance (ch ~ DegToChord d, IntListRep ch) => Primitive (SubIIm d) where
    type Rep (SubIIm d) = [[Int]]
    prim _ = [prim (Cho @4 @ch)]
    pretty _ = "Sub ii"

instance (ch ~ DegToChord d, IntListRep ch) => Primitive (SubIV d) where
    type Rep (SubIV d) = [[Int]]
    prim _ = [prim (Cho @4 @ch)]
    pretty _ = "Sub IV"

instance (ch1 ~ DegToChord d1, IntListRep ch1, ch2 ~ DegToChord d2, IntListRep ch2) => Primitive (SubIIImIVM d1 d2) where
    type Rep (SubIIImIVM d1 d2) = [[Int]]
    prim _ = [prim (Cho @4 @ch1), prim (Cho @4 @ch2)]
    pretty _ = "Sub iii IV"

instance (IntLListRep s1, IntLListRep s2) => Primitive (SubSS (s1 :: Subdominant k dur1) (s2 :: Subdominant k (l - dur1)) :: Subdominant k l) where
    type Rep (SubSS s1 s2) = [[Int]]
    prim _ = prim (Sub @k @dur1 @s1) ++ prim (Sub @k @(l - dur1) @s2)
    pretty _ = pretty (Sub @k @dur1 @s1) ++ " | " ++ pretty (Sub @k @(l - dur1) @s2)


-- Cadences

instance (ch1 ~ DegToChord d1, IntListRep ch1, ch2 ~ DegToChord d2, IntListRep ch2) => Primitive (AuthCad d1 d2) where
    type Rep (AuthCad d1 d2) = [[Int]]
    prim _ = [prim (Cho @4 @ch1), prim (Cho @4 @ch2)]
    pretty _ = "AuthCad V"

instance (ch1 ~ DegToChord d1, IntListRep ch1, ch2 ~ DegToChord d2, IntListRep ch2) => Primitive (AuthCad7 d1 d2) where
    type Rep (AuthCad7 d1 d2) = [[Int]]
    prim _ = [prim (Cho @4 @ch1), prim (Cho @4 @ch2)]
    pretty _ = "AuthCad V7"

instance (ch1 ~ DegToChord d1, IntListRep ch1, ch2 ~ DegToChord d2, IntListRep ch2) => Primitive (AuthCadVii d1 d2) where
    type Rep (AuthCadVii d1 d2) = [[Int]]
    prim _ = [prim (Cho @4 @ch1), prim (Cho @4 @ch2)]
    pretty _ = "AuthCad vii"

instance (ch1 ~ DegToChord d1, IntListRep ch1, ch2 ~ DegToChord d2, IntListRep ch2, ch3 ~ DegToChord d3, IntListRep ch3) => Primitive (AuthCad64 d1 d2 d3) where
    type Rep (AuthCad64 d1 d2 d3) = [[Int]]
    prim _ = [prim (Cho @4 @ch1), prim (Cho @4 @ch2), prim (Cho @4 @ch3)]
    pretty _ = "AuthCad 6-4"

instance (ch1 ~ DegToChord d1, IntListRep ch1, ch2 ~ DegToChord d2, IntListRep ch2) => Primitive (DeceptCad d1 d2) where
    type Rep (DeceptCad d1 d2) = [[Int]]
    prim _ = [prim (Cho @4 @ch1), prim (Cho @4 @ch2)]
    pretty _ = "DeceptCad"

instance (IntLListRep sd, IntLListRep c) => Primitive (FullCad (sd :: Subdominant k sdur) (c :: Cadence k (l - sdur)) :: Cadence k l) where
    type Rep (FullCad sd c) = [[Int]]
    prim _ = prim (Sub @k @sdur @sd) ++ prim (Cad @k @(l - sdur) @c)
    pretty _ = pretty (Sub @k @sdur @sd) ++ " | " ++ pretty (Cad @k @(l - sdur) @c)

instance Primitive NoCad where
    type Rep NoCad = [[Int]]
    prim _ = []
    pretty _ = "NoCad"

-- Phrases

instance (IntLListRep t1, IntLListRep d, IntLListRep t2) => Primitive (PhraseIVI (t1 :: Tonic k (l2 - l1)) (d :: Dominant k l1) (t2 :: Tonic k (l - l2)) :: Phrase k l) where
    type Rep (PhraseIVI t1 d t2) = [[Int]]
    prim _ = prim (Ton @k @(l2 - l1) @t1) ++ prim (Dom @k @l1 @d) ++ prim (Ton @k @(l - l2) @t2)
    pretty _ = pretty (Ton @k @(l2 - l1) @t1) ++ " | " ++ pretty (Dom @k @l1 @d) ++ " | " ++ pretty (Ton @k @(l - l2) @t2)

instance (IntLListRep d, IntLListRep t) => Primitive (PhraseVI (d :: Dominant k l1) (t :: Tonic k (l - l1)) :: Phrase k l) where
    type Rep (PhraseVI d t) = [[Int]]
    prim _ = prim (Dom @k @l1 @d) ++ prim (Ton @k @(l - l1) @t)
    pretty _ = pretty (Dom @k @l1 @d) ++ " | " ++ pretty (Ton @k @(l - l1) @t)

instance (IntLListRep t) => Primitive (PhraseI (t :: Tonic k l) :: Phrase k l) where
    type Rep (PhraseI t) = [[Int]]
    prim _ = prim (Ton @k @l @t)
    pretty _ = pretty (Ton @k @l @t)

-- Progressions

instance (IntLListRep c) => Primitive (CadPhrase c :: ProgType k l) where
    type Rep (CadPhrase c) = [[Int]]
    prim _ = prim (Cad @k @l @c)
    pretty _ = pretty (Cad @k @l @c)

instance (IntLListRep ph, IntLListRep pr) => Primitive ((ph :: Phrase k l) := (pr :: ProgType k (n - l)) :: ProgType k n) where
    type Rep (ph := pr) = [[Int]]
    prim _ = prim (Phr @k @l @ph) ++ prim (Prog @k @(n - l) @pr)
    pretty _ = pretty (Phr @k @l @ph) ++ " || " ++ pretty (Prog @k @(n - l) @pr)