-----------------------------------------------------------------------------
-- |
-- 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 (..)
    , Signature (..)
    -- * Constraints
    , ValidNote
    , ValidRest
    , ValidChord
    , ValidProg
    , ValidHom
    , ValidMel
    , ValidHarm
    , ValidTripl
    ) 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
import Mezzo.Model.Rules.RuleSet

infixl 3 :|:
infixl 4 :-:

-------------------------------------------------------------------------------
-- The 'Music' datatype
-------------------------------------------------------------------------------

-- | Properties of a musical piece: the time signature, the key signature and rule set.
data Signature (t :: TimeSignature) (k :: KeyType) (ruleset :: Type) = Sig

-- | 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 t k r. Signature t k r -> Partiture n l -> Type where
    -- | Sequential or melodic composition of music.
    (:|:) :: ValidMel s m1 m2  => Music s m1 -> Music s m2 -> Music s (m1 +|+ m2)
    -- | Parallel or harmonic composition of music.
    (:-:) :: ValidHarm s m1 m2 => Music s m1 -> Music s m2 -> Music s (m1 +-+ m2)
    -- | A note specified by a pitch and a duration.
    Note :: ValidNote s r d => Root r -> Dur d -> Music s (FromRoot r d)
    -- | A rest specified by a duration.
    Rest :: ValidRest s d => Dur d -> Music s (FromSilence d)
    -- | A chord specified by a chord type and a duration.
    Chord :: ValidChord s c d => Cho c -> Dur d -> Music s (FromChord c d)
    -- | A progression specified by a time signature, and its progression schema.
    Progression :: ValidProg r t p => Prog p -> Music (Sig :: Signature t k r) (FromProg p t)
    -- | A homophonic composition with a melody line and an accompaniment.
    Homophony :: ValidHom s m a => Music s m -> Music s a -> Music s (m +-+ a)
    -- | A triplet with a nominal duration and three pitches.
    Triplet :: ValidTripl s d r1 r2 r3 => Dur d -> Root r1 -> Root r2 -> Root r3 -> Music s (FromTriplet d r1 r2 r3)

-------------------------------------------------------------------------------
-- Musical constraints
-- Specifications of the rules that valid musical terms have to follow.
-------------------------------------------------------------------------------

-- | Select the active rule set.
type ActRuleSet = Classical

-- | Ensures that two pieces of music can be composed sequentially.
type ValidMel (s :: Signature t k r) m1 m2 =
    MelConstraints r m1 m2

-- | Ensures that two pieces of music can be composed in parallel.
type ValidHarm (s :: Signature t k r) m1 m2 =
    HarmConstraints r m1 m2

-- | Ensures that the note is valid.
type ValidNote (s :: Signature t k r) ro d =
    (NoteConstraints r ro d, IntRep ro, Primitive d)

-- | Ensures that the rest is valid.
type ValidRest (s :: Signature t k r) d =
    (RestConstraints r d, Primitive d)

-- | Ensures that the chord is valid.
type ValidChord (s :: Signature t k r) (c :: ChordType n) d =
    (ChordConstraints r c d, IntListRep c, Primitive n, Primitive d)

-- | Ensures that a progression is valid.
type ValidProg r t p =
    (ProgConstraints r t p, IntLListRep p, IntRep t, KnownNat t)

-- | Ensures that a homophonic composition is valid.
type ValidHom (s :: Signature t k r) m a =
    HomConstraints r m a

-- | Ensures that a triplet is valid.
type ValidTripl (s :: Signature t k r) d r1 r2 r3 =
    ( TriplConstraints r d r1 r2 r3, IntRep r1, IntRep r2, IntRep r3, Primitive d
    , Primitive (HalfOf d), NoteConstraints r r1 d, NoteConstraints r r2 (HalfOf d)
    , NoteConstraints r r3 (HalfOf d))

-------------------------------------------------------------------------------
-- Pretty-printing
-------------------------------------------------------------------------------

instance Show (Music s m) where show = render . ppMusic

-- | Pretty-print a 'Music' value.
ppMusic :: Music s 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
ppMusic (Progression p) = text "Prog:" <+> doc p

-- | Convert a showable value into a pretty-printed box.
doc :: Show a => a -> Box
doc = text . show