mezzo 0.2.0.2 → 0.3.0.0

raw patch · 35 files changed

+2959/−847 lines, 35 filesdep +HUnitdep +deepseqdep +ghc-primPVP ok

version bump matches the API change (PVP)

Dependencies added: HUnit, deepseq, ghc-prim

API changes (from Hackage documentation)

Files

• CHANGELOG.md +21/−0
• LICENSE +0/−21
• LICENSE.md +21/−0
• README.md +282/−29
• mezzo.cabal +30/−4
• src/Mezzo.hs +2/−1
• src/Mezzo/Compose.hs +2/−1
• src/Mezzo/Compose/Basic.hs +6/−6
• src/Mezzo/Compose/Builder.hs +8/−4
• src/Mezzo/Compose/Chords.hs +82/−0
• src/Mezzo/Compose/Combine.hs +80/−30
• src/Mezzo/Compose/Harmonic.hs +0/−74
• src/Mezzo/Compose/Harmony.hs +167/−0
• src/Mezzo/Compose/Intervals.hs +179/−0
• src/Mezzo/Compose/Templates.hs +99/−32
• src/Mezzo/Compose/Types.hs +50/−56
• src/Mezzo/Model.hs +17/−1
• src/Mezzo/Model/Errors.hs +97/−0
• src/Mezzo/Model/Harmony.hs +23/−0
• src/Mezzo/Model/Harmony/Chords.hs +143/−59
• src/Mezzo/Model/Harmony/Functional.hs +300/−131
• src/Mezzo/Model/Harmony/Motion.hs +16/−11
• src/Mezzo/Model/Music.hs +56/−216
• src/Mezzo/Model/Prim.hs +0/−3
• src/Mezzo/Model/Reify.hs +6/−2
• src/Mezzo/Model/Rules/Classical.hs +202/−0
• src/Mezzo/Model/Rules/RuleSet.hs +97/−0
• src/Mezzo/Model/Rules/Strict.hs +131/−0
• src/Mezzo/Model/Types.hs +269/−39
• src/Mezzo/Render.hs +1/−0
• src/Mezzo/Render/MIDI.hs +68/−31
• src/Mezzo/Render/Score.hs +170/−0
• test/PrimSpec.hs +219/−82
• test/TestUtils.hs +30/−0
• test/TypeSpec.hs +85/−14

@@ -0,0 +1,21 @@+# Changelog+All notable changes to this project will be documented in this file.++The format is based on [Keep a Changelog](http://keepachangelog.com/)+and this project adheres to [Semantic Versioning](http://semver.org/).++## 0.3.0 - 2017-06-10+### Added+- Chord progressions: create chord progressions following the conventions of functional harmony.+- Dyads: 2-note chords (thirds, fourths, fifths and octaves), together with their doubled versions.+- Scores: break up a piece into sections that can be compiled and combined separately, and specify various attributes of the music, such as tempo, title, key and time signature.+- Triplets: play three notes in the time of two.+- Rule sets: customise the musical rules checked by the library. Includes three strictness levels, from no rule-checking to strict counterpoint.+- Several small and large examples.++### Changed+- Better error messages, showing the pitches that cause errors.+- Faster rule-checking performance.++## 0.2.0 - 2017-03-17+Initial [Hackage](https://hackage.haskell.org/package/mezzo) release.

@@ -1,21 +0,0 @@-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.

@@ -0,0 +1,21 @@+MIT License++Copyright (c) 2017 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.

@@ -4,8 +4,41 @@  *Mezzo* is a Haskell library and embedded domain-specific language for music description. Its novelty is in the fact that it can enforce various rules of music composition *statically*, that is, at compile-time. This effectively means that if you write "bad" music, your composition will not compile – think of it as a **very** strict spell-checker for music. -Note: the project is still very much work-in-progress.+<!-- TOC depthFrom:2 depthTo:6 withLinks:1 updateOnSave:1 orderedList:0 --> +- [Getting started](#getting-started)+	- [Prerequisites](#prerequisites)+	- [Installation](#installation)+	- [First composition](#first-composition)+- [Composing in Mezzo](#composing-in-mezzo)+	- [Basic concepts](#basic-concepts)+	- [Literal vs. builder style](#literal-vs-builder-style)+	- [Primitives](#primitives)+		- [Notes](#notes)+		- [Rests](#rests)+		- [Chords](#chords)+	- [Composition](#composition)+		- [Harmonic composition](#harmonic-composition)+		- [Melodic composition](#melodic-composition)+	- [Melodies](#melodies)+		- [Examples:](#examples)+	- [Chord progressions](#chord-progressions)+		- [Harmonic regions](#harmonic-regions)+		- [Phrases](#phrases)+- [Scores](#scores)+	- [Score building](#score-building)+- [Rendering and exporting](#rendering-and-exporting)+- [Rule sets](#rule-sets)+	- [The `free` rule set](#the-free-rule-set)+	- [The `classical` rule set](#the-classical-rule-set)+	- [The `strict` rule set](#the-strict-rule-set)+	- [Custom rule sets](#custom-rule-sets)+	- [Other constraints](#other-constraints)+- [License](#license)+- [Acknowledgments](#acknowledgments)++<!-- /TOC -->+ ## Getting started  This section explains how to install Mezzo and start using the library.@@ -27,7 +60,7 @@ If using Stack, you will need to add the package to your `extra-deps` in your `stack.yaml` (as Mezzo is not part of Stackage yet), and then add it normally to your `.cabal` file dependencies:  ```cabal-extra-deps: [ mezzo-0.2.0.2 ]+extra-deps: [ mezzo-0.3.0.0 ]  build-depends: base >= 4.7 && < 5              , mezzo@@ -38,25 +71,25 @@  ### First composition -Create a new project (e.g., with `stack new`) with a `Main` module. Type:+Create a new project (e.g. with `stack new`) with a `Main` module. Type:  ```haskell import Mezzo -comp = play $ melody :| c :| d :| e :| f :>> g+comp = defScore $ play $ melody :| c :| d :| e :| f :>> g  main :: IO () main = renderMusic "comp.mid" comp ``` -Save, build and execute (e.g., with `stack exec <project_name>`). You should get a `.mid` file in the project directory which looks something like this:+Save, build and execute (e.g. with `stack exec <project_name>`). You should get a `.mid` file in the project directory which looks something like this: -![First composition](/docs/comp1.png)+![First composition](https://raw.githubusercontent.com/DimaSamoz/mezzo/master/docs/comp1.png) -To test the correctness checking, change the `d` in `comp` to a `b`. You should see the following when you save the file:+To test the correctness checking, change the `d` note in `comp` to a `b`. You should see the following when you save the file:  ```-• Seventh intervals are not permitted in melody.+• Major sevenths are not permitted in melody: C and B • In the first argument of ‘(:|)’, namely ‘melody :| c :| b’   In the first argument of ‘(:|)’, namely ‘melody :| c :| b :| e’   In the first argument of ‘(:>>)’, namely@@ -69,7 +102,7 @@  ### Basic concepts -*Music description languages* are textual representations of musical pieces, used for note input or transcription. Most MDLs provide ways of inputting notes, rests and ways to combine these into melodies or chords. Mezzo additionally lets users input *chords* in their symbolic representation, as well as *chord progressions* in the future.+*Music description languages* are textual representations of musical pieces, used for note input or transcription. Most MDLs provide ways of inputting notes, rests and ways to combine these into melodies or chords. Mezzo additionally lets users input *chords* in their symbolic representation, as well as *chord progressions* using a schematic description of functional harmony.  ### Literal vs. builder style @@ -87,7 +120,7 @@ Notes are given by their pitch and duration. In builder style, every pitch has an explicit value, consisting of three parts:  * **Pitch class**: one of `c`, `d`, `e`, `f`, `g`, `a` or `b`; determines the position of the note in the octave, a white key on the keyboard.-* **Accidental**: a suffix of the pitch class, one of `f` (flat) or `s` (sharp). Natural accidentals are not specified, so `c` means C natural. Accidentals can also be written out as a separate attribute (`c sharp qn`), or even repeated (for example, double sharps: `c sharp sharp qn` or `cs sharp qn`).+* **Accidental**: a suffix of the pitch class, one of `f` (flat, e.g. `bf qn`) or `s` (sharp, e.g. `fs qn`). Natural accidentals are not specified, so `c` means C natural. Accidentals can also be written out as a separate attribute (`c sharp qn`), or even repeated (for example, double sharps: `c sharp sharp qn` or `cs sharp qn`). * **Octave**: the last component of the value. The default octave is 4, this is unmarked. Lower octaves are marked with `_`, `__`, `_3`, `_4` and `_5`. Higher octaves are marked with `'`, `''`, `'3` and `'4`. A C natural in octave 2 is therefore `c__ qn`, a B flat in octave 7 is `bf'3 qn`.  Durations are written after the pitch. For notes, the value is the first letter of the duration name (eighth, quarter, etc.) followed by `n` for note, e.g., `qn` for quarter note. A dotted duration is specified by following the name with a `'`: `hn'` is a dotted half note, with the length of three quarters.@@ -101,10 +134,11 @@ Chords are given by their root (a pitch), type, inversion and duration: a C major quarter triad in first inversion is `c maj inv qc`.  * **Root**: specified the same way as in a note (`c`, `af''`, etc.).-* **Type**: three classes of chords: triads, doubled triads and seventh chords.+* **Type**: three classes of chords: dyads, triads and tetrads.+    * Dyads: A harmonic interval consisting of 2 notes. 5 types possible: minor thirds (`min3`), major thirds (`maj3`), fourths (`fourth`), fifths (`fifth`) and octaves (`oct`).     * Triads: 3 pitches separated by thirds. 4 types possible: major (`maj`), minor (`min`), augmented (`aug`) and diminished (`dim`), based on the size of the intervals between the pitches.-    * Doubled triads: a triad with the lowermost note doubled an octave above. Same types as the triads, but ending with a `D`, e.g., `majD` or `dimD`.-    * Seventh chords: 4 pitches separated by thirds (the top one is a seventh above the bottom one). 5 types possible: major seventh (`maj7`), major-minor/dominant seventh (`dom7`), minor seventh (`min7`), half-diminished seventh (`hdim7`), diminished seventh (`dim7`).+    * Tetrads: 4 pitches separated by thirds (the top one is a seventh above the bottom one). 5 types possible: major seventh (`maj7`), major-minor/dominant seventh (`dom7`), minor seventh (`min7`), half-diminished seventh (`hdim7`), diminished seventh (`dim7`).+* **Doubling**: dyads and triads can be doubled to become a triad and tetrad respectively. This is done by repeating the bottommost note an octave higher, so a doubled C major third would consist of a C, an E, and another C an octave above. Doubling is specified by a `D` after the chord type, e.g. `fifthD`, `majD` or `augD`. * **Inversion**: all of the types can be followed by a `'` and then a separate attribute `i0`, `i1`, `i2` or `i3` to specify zeroth, first, second or third inversion: `c maj' i2 qc`. Alternatively, the `inv` attribute can be added (any number of times) to invert a chord once (or any number of times): `c maj inv inv qc`.  Chord durations end with a `c` and can be dotted, as before: `c min7 qc`, `f sharp hdim inv wc'`.@@ -123,6 +157,20 @@  For consistency, pieces should be composed from top voice to the bottom: the above example would therefore play a C major triad. The composed pieces can be any musical composition, as long as the durations of the pieces matches. If this is not the case, the shorter voice has to be padded by rests where necessary. +When using `(:-:)`, both harmonic intervals and harmonic motion are checked for correctness, so it is mainly intended for contrapuntal compositions. For homophonic compositions (where the "voices" are not independent, the top one being the main melody and the bottom ones being the accompaniment), you can use the `hom` function which does not enforce rules of harmonic motion. For example,++```haskell+(g qn :|: a qn) :-: (c qn :|: d qn)+```++would not compile due to a parallel fifth (`(:|:)` is melodic composition, described in the next section). However,++```haskell+(g qn :|: a qn) `hom` (c qn :|: d qn)+```++compiles, as `hom` only checks for harmonic dissonance.+ #### Melodic composition  Melodic composition `(:|:)` plays one piece of music after the other:@@ -137,13 +185,13 @@ c qn :|: c maj qc ``` -fails to compile (and produces a very cryptic error message), as the first note is only one voice while the chord is three voices. We can remedy this either by explicitly adding rests, or padding the first piece with silent voices, using the functions `pad`, `pad2`, `pad3` or `pad4`:+fails to compile (and unfortunately produces a very cryptic error message), as the first note is only one voice while the chord is three voices. We can remedy this either by explicitly adding rests, or padding the first piece with silent voices, using the functions `pad`, `pad2`, `pad3` or `pad4`:  ```haskell pad2 (c qn) :|: c maj qc ``` -This adds empty voices below the existing voices, but in some cases (e.g., a contrapuntal composition), we might want to keep the upper and lower voice and keep the middle voice silent. In this case, we can use the `restWhile` function to input a voice of the same length as the argument, but with no notes.+This adds empty voices below the existing voices, but in some cases (e.g. a contrapuntal composition), we might want to keep the upper and lower voice and keep the middle voice silent. In this case, we can use the `restWhile` function to input a voice of the same length as the argument, but with no notes.  ```haskell comp = (top :-: restWhile top :-: bottom) :|: c maj qc@@ -173,8 +221,21 @@ * `(:~<<<)`, `(:~<<)`, `(:~<)`, `(:~^)`, `(:~>)` and `(:~>>)`: as above, but must be followed by a rest. * All constructors that change the duration (except `(:<<<)` and `(:~<<<)`) can be followed by a `.` to make the duration dotted. For example, `melody :^ c :^. d :> e` specifies a melody of a quarter note, a dotted quarter note and a half note. -#### Examples:+Below is a table summarising the melody construction operators. +| Duration      | Note  | Rest  | Dotted note | Dotted rest |+|---------------|-------|-------|-------------|-------------|+| No change     | <code>:&#124;</code> | <code>:~&#124;</code> |  | |+| Thirty-second | `:<<<`  | `:~<<<` |               |               |+| Sixteenth     | `:<< `  | `:~<<`  | `:<<.`        | `:~<<.`       |+| Eighth        | `:<`    | `:~<`   | `:<.`         | `:~<.`        |+| Quarter       | `:^`    | `:~^`   | `:^.`         | `:~^.`        |+| Half          | `:>`    | `:~>`   | `:>.`         | `:~>.`        |+| Whole         | `:>>`   | `:~>>`  | `:>>.`        | `:~>>.`       |+++#### Examples+ * Frère Jacques:  ```haskell@@ -183,7 +244,7 @@ fj3 = play $ melody :< d' :| e' :| d' :| c' :^ b :| g fj4 = play $ melody :| g :| d :> g -fj = fj1 :|: fj1 :|: fj2 :|: fj2 :|: fj3 :|: fj3 :|: fj4 :|: fj4+fj = defScore $ fj1 :|: fj1 :|: fj2 :|: fj2 :|: fj3 :|: fj3 :|: fj4 :|: fj4 ```  * Jingle Bells:@@ -192,34 +253,225 @@ p1 = play $ melody :< e :| e :^ e :< e :| e :^ e :< e :| g :<. c :<< d :>> e p2 = play $ melody :< f :| f :<. f :<< f :< f :| e :<. e :<< e :< e :| d :| d :| e :^ d :| g -jb = p1 :| p2+jb = defScore $ p1 :|: p2 ``` -## Composition rules+### Chord progressions -Mezzo enforces a number of composition rules found in classical (common practice) music theory. These can be expanded in the future.+Mezzo implements a subset of the [functional harmony grammar](http://www.tandfonline.com/doi/abs/10.1080/17459737.2011.573676) of Martin Rohrmeier and is inspired by [HarmTrace](https://hackage.haskell.org/package/HarmTrace). The idea is that chord progressions are described schematically using *functional harmony*, a harmonic system which assigns various roles or *functions* to different chords of a key. For example, the chord of the first degree (called the *tonic*) represents stability and "home", while the fifth degree chord (the *dominant*) creates harmonic tension which has to be resolved into the tonic. The Mezzo EDSL for creating progressions guarantees that harmonic functions are handled and constructed correctly. For example, the following is a I–IV–V–I–IV–V7–I progression, consisting of one tonic-dominant-tonic phrase and a cadence: -### Harmonic intervals+```haskell+p = prog $ ph_IVI ton dom_V ton :+ cadence (full subdom_IV auth_V7_I)+``` -Mezzo disallows very dissonant harmonic intervals like minor seconds, major sevenths and augmented octaves. For example, `c qn :-: b qn` produces a type error. Note that the rule only applies at harmonic composition and not enforced for chords: that is, a major seventh chord (which contains a major seventh) *is* allowed, but only when constructed symbolically. The composition `c maj7 qc :-: d' qn` is allowed, but `c maj qc :-: b qn :-: d' qn` triggers the error.+#### Harmonic regions -### Melodic intervals+*Harmonic regions* are one of more chords of a certain harmonic function. For example, a tonic region can consist of one or more tonic chords. The actual nature of the chords (e.g. key, mode, etc.) is determined by the key signature of the piece, described in the [next section](#scores). The regions are either single values (e.g. `dom_ii_V7` generates a secondary dominant chord followed by a dominant chord) or combinators of regions (e.g. `dom_S_D` creates a dominant region from a subdominant region and a dominant region). The chords generated are sequences of quarter chords in the third octave, with appropriate inversions so the progression sounds as conjunct as possible. -Mezzo disallows augmented and diminished melodic intervals, as well as seventh leaps: these are difficult to sing (a common reason for musical constraints) and don't sound good to the ear. Note that due to enharmonic equivalence, an interval might have several names, and some of these may be forbidden. For example, a distance of 3 semitones can be called a minor third (allowed) or an augmented second (disallowed). The reasoning behind this is that minor intervals often appear in music in minor mode, but an augmented interval is usually a given with an accidental and is therefore more "out of place".+* Tonic regions+    * `ton`: one tonic chord.+    * `ton_T_T t1 t2`: two consecutive tonic regions.+* Dominant regions:+    * `dom_V`: a major fifth degree chord.+    * `dom_V7`: a dominant fifth degree chord.+    * `dom_vii0`: a diminished seventh degree chord.+    * `dom_II_V7`: a secondary dominant (second degree) followed by a dominant (fifth degree) chord.+    * `dom_S_D sd d`: a subdominant region followed by a dominant region.+    * `dom_D_D d1 d2`: two consecutive dominant regions.+* Subdominant regions:+    * `subdom_IV`: a fourth degree chord.+    * `subdom_ii`: a second degree minor chord.+    * `subdom_iii_IV`: a third degree minor chord followed by a fourth degree major chord.+    * `subdom_S_S sd1 sd2`: two consecutive subdominant regions. +#### Phrases+A chord progression is broken up into *phrases*, composed using the `:+` operator. The last phrase must always be a *cadential phrase*, which provides closure to the piece. Phrase constructors (such as `ph_VI`) take tonic and dominant regions as arguments, which are described above. The cadential phrase is constructed using the `cadence` keyword, and followed by a cadential region.++* Phrases:+    * `ph_I t`: a tonic phrase, consisting of a single tonic region.+    * `ph_VI d t`: a dominant-tonic phrase, consisting of a dominant and tonic region+    * `ph_IVI t1 d t2`: a tonic-dominant-tonic phrase, consisting of a tonic, dominant and tonic region.+* Cadential regions:+    * `auth_V_I`: an authentic V–I cadence.+    * `auth_V7_I`: an authentic dominant V7–I cadence.+    * `auth_vii_I`: an authentic leading tone vii–I cadence.+    * `auth_64_V7_I`: an authentic dominant cadence with a cadential 6-4.+    * `decept_V_iv`: a deceptive V-iv cadence.+    * `full sd c`: a full cadence, consisting of a subdominant region and a cadence.++The example above therefore has a tonic-dominant-tonic region, followed by a full cadence with a fourth degree subdominant and authentic dominant cadence. The `prog` keyword converts a schema into a `Music` value.++```haskell+p = prog $ ph_IVI ton dom_V ton :+ cadence (full subdom_IV auth_V7_I)+```++## Scores++`Music` values cannot be immediately exported into MIDI files, as there are various attributes of the piece that need to be specified first (in particular, the [rule set](#rule-sets) used to check the correctness of the composition, without which the pieces will not compile). This is accomplished by constructing a `Score` out of a `Music` value, and specifying the attributes of the piece such as the tempo, time signature or rule set. Scores can also be used to break a larger musical piece into multiple sections which are "pre-rendered": this significantly cuts down on rule-checking time, as the correctness of the sections is checked independently. This also allows tempo or key changes, since each section can have its own set of attributes.++### Score building+Scores are built using the following syntax:++```+score [<attribute_name> <attribute_value>]* withMusic <music>+```++For example, the following creates a new score from a `Music` value `m` for the refrain section of a piece in A minor and quadruple (common) meter, with a tempo of 120 BPM and strict rule-checking:++```haskell+comp = score section "refrain"+             setKeySig a_min+             setTimeSig quadruple+             setTempo 120+             setRuleSet strict+             withMusic m+```++* The `score` keyword starts building a score and must be followed by the keyword `withMusic` with zero or more optional attributes in-between.+* The score attributes are simple name-value pairs written one after the other, with no punctuation (line breaks, as above, are optional). Mezzo currently supports the following attributes:++| Attribute name | Attribute type | Default value   | Description                                                                                                                                                                                                            |+|----------------|----------------|-----------------|------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------|+| `section`      | string         | `"Composition"` | A brief description of the section of the piece that the score describes.  This attribute is only for documentation purposes, to make it clear in the source code which section is where.                              |+| `setKeySig`    | key signature  | `c_maj`         | The key signature of the score, e.g. `c_maj`, `a_min`, `fs_maj`, `bf_min`. This affects the key of the chord progressions.                                                                                             |+| `setTimeSig`   | time signature | `quadruple`     | The time signature of the score, one of `duple`, `triple`, or `quadruple`.  This affects the number of chords played in a bar of a progression  (e.g. three chords for triple meter, four chords for quadruple meter). |+| `setTempo`     | integer        | 120             | The tempo of the piece, in BPM. This affects the tempo of the MIDI file playback.                                                                                                                                      |+| `setRuleSet`   | rule set       | `classical`     | The rule set used to check the correctness of a piece. One of `free`, `classical`, `strict`, or any other user-defined rule set.                                                                                       |++* The `withMusic` keyword finishes building a score from its argument of type `Music`.+* If no attributes are modified (i.e. the default score attributes are used), the shorthand function `defScore m` can be used instead of `score withMusic m` to create a score from the piece `m`.++## Rendering and exporting++Once a score is created from a musical piece, it can be exported as a MIDI file using the `renderScore` function:++```haskell+renderScore :: FilePath -> Title -> Score -> IO ()+```++The function takes a file path (specified as a `String`), the title of the MIDI track (also a `String`) and the score to export. Upon successful rendering, you should see the message `Composition rendered to <filepath>.`.++If a piece is broken up into smaller scores (sections), all of them can be concatenated and rendered using the `renderScores` function:++```haskell+renderScore :: FilePath -> Title -> [Score] -> IO ()+```++This is similar to `renderScore`, but takes a list of `Score`s (in the desired order). Note that this allows for reuse of sections: for example, a refrain (or repeated section) only has to be described once, and the score created from it can be reused without any additional rule-checking. See the Für Elise example for a demonstration.++## Rule sets+As different musical genres enforce different kinds of rules, Mezzo lets users select different levels of strictness (called *rule sets*) or even completely customise the musical rules that are checked. In particular, one rule set turns off correctness checking completely, allowing for complete creative freedom.++Mezzo predefines three rule sets of increasing strictness. These can be specified using the `setRuleSet` score attribute, as described in [Score building](#score-building).++### The `free` rule set+No musical rules enforced, the music is free from restrictions.++### The `classical` rule set+Enforces the common rules of classical music without being too restrictive. In particular:++* Very dissonant harmonic intervals like minor seconds, major sevenths and augmented octaves are forbidden. For example, `c qn :-: b qn` produces a type error. Note that the rule only applies at harmonic composition and is not enforced for chords: that is, a major seventh chord (which contains a major seventh) *is* allowed, but only when constructed symbolically.+* Large melodic intervals such as major sevenths or compound intervals are forbidden. These break up the flow of a melody, making it sound disjunct.+* Rules of harmonic motion, such as parallel and concealed unisons, fifths and octaves, are forbidden for harmonic composition of voices. Two voices singing in parallel a perfect interval apart are very difficult to distinguish: the intervals are so consonant that the voices effectively fuse together, and this does not make for interesting music. These rules are only enforced for contrapuntal harmonic composition (the `(:-:)` operator) of individual voices, so sequential composition of chords (the `(:|:)` operator) or chord progressions *are* allowed: the independence of voices is not important in a sequence of chords.++### The `strict` rule set+Enforces most of the rules of strict contrapuntal compositions, which are often based around vocal performance. This rule set is the most restrictive and is generally leads to longer compile times, but is probably the most useful for students of composition.++* Dissonant harmonic intervals are disallowed, just as in the `classical` rule set. However, major seventh chords are also disallowed.+* Large melodic intervals (sevenths and compound intervals) are disallowed, and so are augmented and diminished melodic intervals. These are difficult to sing and don't sound good to the ear. Note that due to enharmonic equivalence, an interval might have several names, and some of these may be forbidden. For example, a distance of 3 semitones can be called a minor third (allowed) or an augmented second (disallowed). The reasoning behind this is that minor intervals often appear in music in minor mode, but an augmented interval is usually given with an accidental and is therefore more "out of place". A caveat is that Mezzo internally only has three accidentals so it interprets `a flat flat qn` as a G natural. This means that the interval `c qn :|: a flat flat qn` is allowed, even though it is technically a diminished sixth interval.+* Harmonic motion constraints are enforced for harmonic *and* melodic composition (`(:-:)` and `(:|:)`), as well as homophonic composition (`hom`). Symbolic chord progressions are still allowed, even if they violate harmonic motion rules – however, motion rules between a progression accompaniment and a melodic line are enforced. -### Harmonic motion+### Custom rule sets+Users of Mezzo can define their own custom rule sets, albeit adding complex rules can require a closer understanding of the Mezzo internals and type-level computation. Rule sets are a collection of constraints (i.e. Haskell type class constraints), one for all of the ways a `Music` value can be constructed: harmonic composition, melodic composition, homophonic composition, rests, notes, chords, progressions. -Mezzo enforces the common rules of harmonic motion, that is, direct motion into perfect intervals (unison, fifth, octave). Two voices singing in parallel a perfect interval apart are very difficult to distinguish: the intervals are so consonant that the voices effectively fuse together, and this does not make for interesting music.+Any value can be used as a rule set, as long as its type is an instance of the `RuleSet` type class: -This rule only applies and is only enforced when creating contrapuntal compositions, i.e., when composing two or more melodies in parallel. This means that simple chord progressions with parallel octaves *are* allowed, since the independence of voices is not important in a sequence of chords.+```haskell+class RuleSet t where+    type MelConstraints   t (m1 :: Partiture n l1) (m2 :: Partiture n l2) :: Constraint+    type HarmConstraints  t (m1 :: Partiture n1 l) (m2 :: Partiture n2 l) :: Constraint+    type NoteConstraints  t (r :: RootType)        (d :: Duration)        :: Constraint+    type RestConstraints  t                        (d :: Duration)        :: Constraint+    type ChordConstraints t (c :: ChordType n)     (d :: Duration)        :: Constraint+    type ProgConstraints  t (s :: TimeSignature)   (p :: ProgType k l)    :: Constraint+    type HomConstraints   t (m1 :: Partiture n1 l) (m2 :: Partiture n2 l) :: Constraint+``` +The various constraints take as input the arguments of the corresponding `Music` constructor: for example, `HarmConstraints` takes the two type-level composed musical pieces (of type `Partiture`) as arguments, and returns a `Constraint` (see ConstraintKinds extension) expressing whether the pieces can be harmonically composed.++Custom rule sets can be useful even if the exact details of Mezzo's type-level model are not understood. For example, suppose that we want to create a very restrictive rule set for first-species counterpoint: this species only allows for melodic lines containing whole notes and enforces most of the classic rules of harmony, melody and motion. To implement this rule set, we can restrict the constructors that are allowed and delegate the complex rule-checking to the existing Mezzo implementation. To start, we define a new type for our rule set:++```haskell+data FirstSpecies = FirstSpecies+```++Now, we make `FirstSpecies` an instance of the `RuleSet` type class by defining the associated constraint synonyms. In this case, we want to:++* Use the same musical rule-checking methods as the `strict` rule set+* Only allow whole note and rest durations+* Disallow chords and progressions.++To achieve this, we declare the following instance of the `RuleSet` class for `FirstSpecies`:++```haskell+instance RuleSet FirstSpecies where+    type MelConstraints   FirstSpecies m1 m2 = MelConstraints Strict m1 m2+    type HarmConstraints  FirstSpecies m1 m2 = HarmConstraints Strict m1 m2+    type HomConstraints   FirstSpecies m1 m2 = HomConstraints Strict m1 m2+    type NoteConstraints  FirstSpecies r d   = ValidDur d+    type RestConstraints  FirstSpecies d     = ValidDur d+    type ChordConstraints FirstSpecies c d   = InvalidChord+    type ProgConstraints  FirstSpecies t p   = InvalidProg+```++* `MelConstraints`, `HarmConstraints` and `HomConstraints` simply delegate rule-checking to the constraints of the `Strict` rule set.+* `NoteConstraints` and `RestConstraints` are defined using the `ValidDur` class, defined as follows:+```haskell+class ValidDur (d :: Duration)+instance ValidDur Whole+instance {-# OVERLAPPABLE #-}+        TypeError (Text "First species counterpoint only have whole durations.")+        => ValidDur d+```+  This makes use of GHC's [custom type errors](https://ghc.haskell.org/trac/ghc/wiki/Proposal/CustomTypeErrors) feature, with the correspoinding types available in the GHC.TypeLits module. We define the `ValidDur` type class (restricting its argument to a type of kind `Duration`) without any methods. The `Whole` duration is made an instance of `ValidDur`, expressing our intention to make whole durations valid. The overlappable instance for `ValidDur d` is selected only if the previous instance does not fit (i.e. the duration is not `Whole`): in this case, a custom type error is encountered and type-checking fails, displaying our custom error message.+* `ChordConstraints` and `ProgConstraints` are simply equal to the "constant" (nullary) type classes `InvalidChord` and `InvalidProg`, which are defined in a similar manner to `ValidDur`:++```haskell+class InvalidChord+instance TypeError (Text "Chords are not allowed in counterpoint.")+         => InvalidChord++class InvalidProg+instance TypeError (Text "Progressions are not allowed in counterpoint.")+         => InvalidProg+```+  In this case, the constraints always fail (since they have no arguments), displaying the corresponding error message.++Having defined this instance, we can expect to see our custom constraints any time we use the `FirstSpecies` rule set. For example, the following composition fails to compile:++```haskell+comp = score setRuleSet FirstSpecies+             withMusic (c maj qc :-: b qn)+```++The type error messages explain what the problem is, just as we defined them:++```+• Can't have major sevenths in chords: C and B+• Chords are not allowed in counterpoint.+• First species counterpoint only have whole durations.+```++The full file (with the necessary language extensions and module imports needed) can be found in the [examples folder](https://github.com/DimaSamoz/mezzo/blob/master/examples/src/Other/FirstSpecies.hs).+ ### Other constraints -Mezzo "implicitly" enforces other rules, but these are only required to make the internal enforcement system work.+Mezzo "implicitly" enforces other rules, but these are only required to make the internal enforcement system work. These rules are enforced independently of the rule set selected.+ * As discussed above, concatenation of pieces of music requires both to have the same vertical or horizontal dimensions: this can be achieved by padding the shorter one with voices or rests. * The shortest possible duration is a thirty-second: this means that dotted thirty-second notes are not allowed.+* Progressions generally follow the key of the score, but some harmonic regions are only valid in one of the two modes. In particular, the subdominant regions `subdom_ii` `subdom_iii_IV` can only appear in a major mode piece. * The octave limits are -1 to 8 inclusive: the lowest pitch is `c_5`, the highest pitch is `b'4`. For example, `b'4 maj qc` does not type-check, as the third and fifth are out of bounds.  ## License@@ -229,4 +481,5 @@ ## Acknowledgments  * [Michael B. Gale](http://www.github.com/mbg) for constant support, good ideas and encouragement.-* [Richard Eisenberg](http://www.github.com/goldfirere) for always knowing what to do when I got hopelessly stuck (and also making this project possible).+* [Richard Eisenberg](http://www.github.com/goldfirere) for always knowing what to do when I got hopelessly stuck using TypeInType...+* [Simon Peyton Jones](https://github.com/simonpj) for a stimulating discussion about the project and valuable advice on future work.

@@ -1,17 +1,18 @@ name:                mezzo-version:             0.2.0.2+version:             0.3.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 license:             MIT-license-file:        LICENSE+license-file:        LICENSE.md author:              Dima Szamozvancev maintainer:          ds709@cam.ac.uk copyright:           2016 Dima Samozvancev category:            Music build-type:          Simple extra-source-files:  README.md+                   , CHANGELOG.md                    , docs/*.png cabal-version:       >=1.10 @@ -22,29 +23,52 @@                      , Mezzo.Model.Prim                      , Mezzo.Model.Music                      , Mezzo.Model.Types+                     , Mezzo.Model.Harmony                      , Mezzo.Model.Harmony.Motion                      , Mezzo.Model.Harmony.Chords                      , Mezzo.Model.Harmony.Functional                      , Mezzo.Model.Reify+                     , Mezzo.Model.Rules.RuleSet+                     , Mezzo.Model.Rules.Classical+                     , Mezzo.Model.Rules.Strict+                     , Mezzo.Model.Errors                       , Mezzo.Compose                      , Mezzo.Compose.Types                      , Mezzo.Compose.Builder                      , Mezzo.Compose.Templates                      , Mezzo.Compose.Basic-                     , Mezzo.Compose.Harmonic+                     , Mezzo.Compose.Chords+                     , Mezzo.Compose.Harmony                      , Mezzo.Compose.Combine+                     , Mezzo.Compose.Intervals                       , Mezzo.Render                      , Mezzo.Render.MIDI+                     , Mezzo.Render.Score    build-depends:       base >= 4.7 && < 5                      , ghc-typelits-natnormalise                      , template-haskell                      , HCodecs                      , boxes+                     , ghc-prim+  ghc-options:         -fplugin GHC.TypeLits.Normalise   default-language:    Haskell2010+  default-extensions:  TypeInType+                     , TypeApplications+                     , TypeFamilies+                     , GADTs+                     , RankNTypes+                     , ScopedTypeVariables+                     , TypeOperators+                     , MultiParamTypeClasses+                     , FlexibleInstances+                     , FlexibleContexts+                     , UndecidableInstances+                     , ConstraintKinds + test-suite mezzo-test   type:                exitcode-stdio-1.0   hs-source-dirs:      test@@ -52,12 +76,14 @@   other-modules:       Main                      , PrimSpec                      , TypeSpec+                     , TestUtils   build-depends:       base                      , mezzo                      , hspec                      , QuickCheck-                    --  , deepseq+                     , deepseq                      , should-not-typecheck+                     , HUnit   ghc-options:         -threaded -rtsopts -with-rtsopts=-N   default-language:    Haskell2010 

@@ -14,7 +14,7 @@ -- ----------------------------------------------------------------------------- -module Mezzo (module X) where+module Mezzo (module X, ($), (++), concat) where  -- Uses import/export shortcut as suggested by HLint. @@ -24,4 +24,5 @@     ( Music (..)     , Voice (..)     , Partiture (..)+    , RuleSet (..)     )

@@ -22,4 +22,5 @@ import Mezzo.Compose.Builder as X import Mezzo.Compose.Types as X import Mezzo.Compose.Combine as X-import Mezzo.Compose.Harmonic as X+import Mezzo.Compose.Chords as X+import Mezzo.Compose.Harmony as X

@@ -1,4 +1,4 @@-{-# LANGUAGE TypeInType, TypeApplications, TemplateHaskell, RankNTypes, FlexibleContexts, GADTs #-}+{-# LANGUAGE TemplateHaskell #-}  ----------------------------------------------------------------------------- -- |@@ -78,17 +78,17 @@ 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 :: Primitive (DegreeRoot k d) => KeyS k -> Deg 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 :: (Primitive d, IntRep p, ValidNote s (PitchRoot p) d) => Pit p -> Dur d -> Music s (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 :: (Primitive d, IntRep (DegreeRoot k sd), ValidNote (Sig :: Signature t k r) (DegreeRoot k sd) d)+      => KeyS k -> Deg sd -> Dur d -> Music (Sig :: Signature t k r) (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 :: (Primitive d, ValidRest s d) => Dur d -> Music s (FromSilence d) rest = Rest

@@ -1,4 +1,3 @@-{-# LANGUAGE TypeInType, RankNTypes, ExistentialQuantification, GADTs #-}  ----------------------------------------------------------------------------- -- |@@ -24,6 +23,7 @@     , Term     , AConv     , AMut+    , ATerm     , Mut'     , spec     , constConv@@ -67,6 +67,10 @@ -- | Mutator with argument: mutates a value of type t, consuming an argument of type a. type AMut a t = AConv a t t +-- | Terminator with argument: finishes building a value of type t, returning a result of+-- type r, consuming an argument of type a.+type ATerm a t r = t -> a -> r+ -- | Flexible mutator: mutator that allows slight changes in the type (otherwise use 'Conv'). type Mut' t t' = Conv t t' @@ -108,13 +112,13 @@ 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))+type RootT s r d = Primitive r => Term (Root r) (Music s (FromRoot r d))  --  | Rest terminator.-type RestT d = Term (Pit Silence) (Music (FromSilence d))+type RestT s d = Term (Pit Silence) (Music s (FromSilence d))  -- | Chord terminator.-type ChorT c d = Primitive c => Term (Cho c) (Music (FromChord c d))+type ChorT s c d = Primitive c => Term (Cho c) (Music s (FromChord c d))  -- inKey :: KeyS key -> a -> a -- inKey key cont = let ?k = key in cont

@@ -0,0 +1,82 @@+{-# LANGUAGE TemplateHaskell #-}++-----------------------------------------------------------------------------+-- |+-- Module      :  Mezzo.Compose.Chords+-- 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.Chords 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++-- ** Dyad type literals+dyaTyLits++-- ** Triad type literals+triTyLits++-- ** Tetrad type literals+tetTyLits++_dbl :: TriType t -> TetType (DoubledT t)+_dbl t = TetType++-- ** 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 -> TetType t -> Inv i -> Cho (Tetrad r t i)+seventh r t i = Cho++-- * Chord builders++-- ** Dyad converters+mkDyaConvs++-- ** Triad converters+mkTriConvs++-- ** Doubled dyad converters+mkDoubledDConvs++-- ** Tetrad converters+mkTetConvs++-- ** Doubled triad converters+mkDoubledTConvs++-- ** Inversion mutators+inv :: ChorM c (InvertChord c)+inv = constConv Cho

@@ -1,6 +1,4 @@-{-# LANGUAGE TypeInType, TypeApplications, TypeOperators, FlexibleContexts, RankNTypes,-    FlexibleInstances, ScopedTypeVariables, GADTs, TypeFamilies #-}-{-# OPTIONS_GHC -fplugin GHC.TypeLits.Normalise #-}+{-# OPTIONS_GHC -fconstraint-solver-iterations=0 #-}  ----------------------------------------------------------------------------- -- |@@ -32,12 +30,24 @@     -- * Melody composition     , play     , melody+    -- * Textures+    , hom+    , melAccomp+    -- * Triplets+    , _triplet+    , tripletW+    , tripletH+    , tripletQ+    , tripletE+    , tripletS     ) where  import Mezzo.Model import Mezzo.Compose.Basic import Mezzo.Compose.Builder import Mezzo.Compose.Types+import Mezzo.Compose.Harmony+import Mezzo.Compose.Intervals import Mezzo.Model.Prim import Mezzo.Model.Types import Mezzo.Model.Music@@ -49,7 +59,7 @@ -------------------------------------------------------------------------------  -- | Get the duration of a piece of music.-musicDur :: Primitive l => Music (m :: Partiture n l) -> Dur l+musicDur :: Primitive l => Music s (m :: Partiture n l) -> Dur l musicDur _ = Dur  -- | Convert a duration to an integer.@@ -57,16 +67,18 @@ durToInt = prim  -- | Get the numeric duration of a piece of music.-duration :: Primitive l => Music (m :: Partiture n l) -> Int+duration :: Primitive l => Music s (m :: Partiture n l) -> Int duration = durToInt . musicDur  -- | Get the number of voices in a piece of music.-voices :: Music m -> Int+voices :: Music s m -> Int voices (Note r d) = 1 voices (Rest d) = 1+voices (Chord c d) = chordVoices c+voices (Progression _) = 4+voices (Homophony m a) = voices m + voices a 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@@ -74,36 +86,36 @@ chordVoices _ = prim (undefined :: ChordType n) -- Need to get a kind-level variable to the term level  -- | Add an empty voice to the piece of music.-pad :: (HarmConstraints m (FromSilence b), Primitive b)-    => Music (m :: Partiture (a - 1) b) -> Music ((m +-+ FromSilence b) :: Partiture a b)+pad :: (ValidHarm s m (FromSilence b), Primitive b, ValidRest s b)+    => Music s (m :: Partiture (a - 1) b) -> Music s ((m +-+ FromSilence b) :: Partiture a b) pad m = m :-: restWhile m  -- | Add two empty voices to the piece of music.-pad2 :: ( HarmConstraints m (FromSilence b)-        , HarmConstraints (m +-+ FromSilence b) (FromSilence b)-        , Primitive b)-     => Music (m :: Partiture (a - 2) b) -> Music ((m +-+ FromSilence b +-+ FromSilence b) :: Partiture a b)+pad2 :: ( ValidHarm s m (FromSilence b)+        , ValidHarm s (m +-+ FromSilence b) (FromSilence b)+        , Primitive b, ValidRest s b)+     => Music s (m :: Partiture (a - 2) b) -> Music s ((m +-+ FromSilence b +-+ FromSilence b) :: Partiture a b) pad2 m = m :-: restWhile m :-: restWhile m  -- | Add three empty voices to the piece of music.-pad3 :: ( HarmConstraints m (FromSilence b)-        , HarmConstraints (m +-+ FromSilence b) (FromSilence b)-        , HarmConstraints (m +-+ FromSilence b +-+ FromSilence b) (FromSilence b)-        , Primitive b)-     => Music (m :: Partiture (a - 3) b) -> Music ((m +-+ FromSilence b +-+ FromSilence b +-+ FromSilence b) :: Partiture a b)+pad3 :: ( ValidHarm s m (FromSilence b)+        , ValidHarm s (m +-+ FromSilence b) (FromSilence b)+        , ValidHarm s (m +-+ FromSilence b +-+ FromSilence b) (FromSilence b)+        , Primitive b, ValidRest s b)+     => Music s (m :: Partiture (a - 3) b) -> Music s ((m +-+ FromSilence b +-+ FromSilence b +-+ FromSilence b) :: Partiture a b) pad3 m = m :-: restWhile m :-: restWhile m :-: restWhile m  -- | Add four empty voices to the piece of music.-pad4 :: ( HarmConstraints m (FromSilence b)-        , HarmConstraints (m +-+ FromSilence b) (FromSilence b)-        , HarmConstraints (m +-+ FromSilence b +-+ FromSilence b) (FromSilence b)-        , HarmConstraints (m +-+ FromSilence b +-+ FromSilence b +-+ FromSilence b) (FromSilence b)-        , Primitive b)-     => Music (m :: Partiture (a - 4) b) -> Music ((m +-+ FromSilence b +-+ FromSilence b +-+ FromSilence b +-+ FromSilence b) :: Partiture a b)+pad4 :: ( ValidHarm s m (FromSilence b)+        , ValidHarm s (m +-+ FromSilence b) (FromSilence b)+        , ValidHarm s (m +-+ FromSilence b +-+ FromSilence b) (FromSilence b)+        , ValidHarm s (m +-+ FromSilence b +-+ FromSilence b +-+ FromSilence b) (FromSilence b)+        , Primitive b, ValidRest s b)+     => Music s (m :: Partiture (a - 4) b) -> Music s ((m +-+ FromSilence b +-+ FromSilence b +-+ FromSilence b +-+ FromSilence b) :: Partiture a b) pad4 m = m :-: restWhile m :-: restWhile m :-: restWhile m :-: restWhile m  -- | Rest for the duration of the given music piece.-restWhile :: Primitive l =>  Music (m :: Partiture n l) -> Music (FromSilence l)+restWhile :: (Primitive l, ValidRest s l) =>  Music s (m :: Partiture n l) -> Music s (FromSilence l) restWhile m = rest (musicDur m)  -------------------------------------------------------------------------------@@ -111,7 +123,7 @@ -------------------------------------------------------------------------------  -- | Convert a melody (a sequence of notes and rests) to `Music`.-play :: (Primitive d) => Melody m d -> Music m+play :: (Primitive d) => Melody s m d -> Music s 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@@ -138,17 +150,55 @@ 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 :: (IntRep r, Primitive d, ValidNote s r d) => Melody s m d -> RootS r -> Music s (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 :: (Primitive d, ValidRest s d) => Melody s m d -> Music s (FromSilence d) mkMelRest m = r (\_ -> Rest (melDur m))  -- | Alias for the start of the melody.-melody :: Melody (End :-- None) Quarter+melody :: Melody s (End :-- None) Quarter melody = Melody  -- | Get the duration of the notes in a melody.-melDur :: Primitive d => Melody m d -> Dur d+melDur :: Primitive d => Melody s m d -> Dur d melDur _ = Dur++-------------------------------------------------------------------------------+-- Textures+-------------------------------------------------------------------------------++hom :: ValidHom s m a => Music s m -> Music s a -> Music s (m +-+ a)+hom = Homophony++melAccomp :: (s ~ (Sig :: Signature t k r), ValidProg r t p, pm ~ FromProg p t, ValidHom s m pm, Primitive d) => Melody s m d -> InKey k (PhraseList p) -> Music s (m +-+ pm)+melAccomp m p = Homophony (play m) (prog p)++-------------------------------------------------------------------------------+-- Triplets+-------------------------------------------------------------------------------++-- | Create a new triplet with three notes, with 2/3 of the specified duration each.+_triplet :: ValidTripl s d r1 r2 r3 => Dur d -> Root r1 -> Root r2 -> Root r3 -> Music s (FromTriplet d r1 r2 r3)+_triplet = Triplet++-- | Create a new triplet lasting a whole note.+tripletW :: ValidTripl s Half r1 r2 r3 => RootS r1 -> RootS r2 -> RootS r3 -> Music s (FromTriplet Half r1 r2 r3)+tripletW r1 r2 r3 = Triplet _ha (r1 id) (r2 id) (r3 id)++-- | Create a new triplet lasting a half note.+tripletH :: ValidTripl s Quarter r1 r2 r3 => RootS r1 -> RootS r2 -> RootS r3 -> Music s (FromTriplet Quarter r1 r2 r3)+tripletH r1 r2 r3 = Triplet _qu (r1 id) (r2 id) (r3 id)++-- | Create a new triplet lasting a quarter note.+tripletQ :: ValidTripl s Eighth r1 r2 r3 => RootS r1 -> RootS r2 -> RootS r3 -> Music s (FromTriplet Eighth r1 r2 r3)+tripletQ r1 r2 r3 = Triplet _ei (r1 id) (r2 id) (r3 id)++-- | Create a new triplet lasting an eighth note.+tripletE :: ValidTripl s Sixteenth r1 r2 r3 => RootS r1 -> RootS r2 -> RootS r3 -> Music s (FromTriplet Sixteenth r1 r2 r3)+tripletE r1 r2 r3 = Triplet _si (r1 id) (r2 id) (r3 id)++-- | Create a new triplet lasting a sixteenth note.+tripletS :: ValidTripl s ThirtySecond r1 r2 r3 => RootS r1 -> RootS r2 -> RootS r3 -> Music s (FromTriplet ThirtySecond r1 r2 r3)+tripletS r1 r2 r3 = Triplet _th (r1 id) (r2 id) (r3 id)

@@ -1,74 +0,0 @@-{-# 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

@@ -0,0 +1,167 @@+{-# LANGUAGE TemplateHaskell, ScopedTypeVariables #-}++-----------------------------------------------------------------------------+-- |+-- Module      :  Mezzo.Compose.Harmony+-- Description :  Harmony 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.Harmony where++import Mezzo.Model+import Mezzo.Compose.Types+import Mezzo.Compose.Builder+import Mezzo.Compose.Templates+import Mezzo.Compose.Basic++import GHC.TypeLits++infixr 5 :+++-- * Functional harmony terms++-- | Type of harmonic terms in some key.+type InKey k v = KeyS k -> v++toProg :: InKey k (PhraseList p) -> InKey k (Prog p)+toProg _ = const Prog++-- ** Progressions++-- | Create a new musical progression from the given time signature and progression schema.+prog :: ValidProg r t p => InKey k (PhraseList p) -> Music (Sig :: Signature t k r) (FromProg p t)+prog ik = Progression ((toProg ik) KeyS)++-- ** Phrases++-- | List of phrases in a progression parameterised by the key, ending with a cadence.+data PhraseList (p :: ProgType k l) where+    -- | A cadential phrase, ending the progression.+    Cdza :: Cad c -> KeyS k -> PhraseList (CadPhrase c)+    -- | Add a new phrase to the beginning of the progression.+    (:+) :: InKey k (Phr p) -> InKey k (PhraseList ps) -> KeyS k -> PhraseList (p := ps)++-- | Create a new cadential phrase.+cadence :: InKey k (Cad c) -> InKey k (PhraseList (CadPhrase c))+cadence c = \k -> Cdza (c k) k++-- | Dominant-tonic phrase.+ph_I :: InKey k (Ton (t :: Tonic k l)) -> InKey k (Phr (PhraseI t :: Phrase k l))+ph_I _ = const Phr++-- | Dominant-tonic phrase.+ph_VI :: InKey k (Dom (d :: Dominant k l1)) -> InKey k (Ton (t :: Tonic k (l - l1))) -> InKey k (Phr (PhraseVI d t :: Phrase k l))+ph_VI _ _ = const Phr++-- | Tonic-dominant-tonic phrase.+ph_IVI :: InKey k (Ton (t1 :: Tonic k (l2 - l1))) -> InKey k (Dom (d :: Dominant k l1)) -> InKey k (Ton (t2 :: Tonic k (l - l2))) -> InKey k (Phr (PhraseIVI t1 d t2 :: Phrase k l))+ph_IVI _ _ _ = const Phr++-- ** Cadences++-- | Authentic V-I dominant cadence.+auth_V_I :: InKey k (Cad (AuthCad (DegChord :: DegreeC V MajQ k Inv1 Oct2) (DegChord :: DegreeC I (KeyToQual k) k Inv0 Oct3)))+auth_V_I = const Cad++-- | Authentic V7-I dominant seventh cadence.+auth_V7_I :: InKey k (Cad (AuthCad7 (DegChord :: DegreeC V DomQ k Inv2 Oct2) (DegChord :: DegreeC I (KeyToQual k) k Inv0 Oct3)))+auth_V7_I = const Cad++-- | Authentic vii-I leading tone cadence.+auth_vii_I :: InKey k (Cad (AuthCadVii (DegChord :: DegreeC VII DimQ k Inv1 Oct2) (DegChord :: DegreeC I (KeyToQual k) k Inv0 Oct3)))+auth_vii_I = const Cad++-- | Authentic cadential 6-4 cadence.+auth_64_V7_I :: InKey k (Cad (AuthCad64 (DegChord :: DegreeC I (KeyToQual k) k Inv2 Oct3) (DegChord :: DegreeC V DomQ k Inv3 Oct2) (DegChord :: DegreeC I (KeyToQual k) k Inv1 Oct3)))+auth_64_V7_I = const Cad++-- | Deceptive V-iv cadence.+decept_V_iv :: InKey k (Cad (DeceptCad (DegChord :: DegreeC V DomQ k Inv2 Oct2) (DegChord :: DegreeC VI (KeyToOtherQual k) k Inv1 Oct2)))+decept_V_iv = const Cad++-- | Full cadence, starting with a subdominant.+full :: InKey k (Sub s) -> InKey k (Cad c) -> InKey k (Cad (FullCad s c))+full _ _ = const Cad++-- ** Tonic chords++-- | Tonic chord.+ton :: InKey k (Ton (TonT (DegChord :: DegreeC I (KeyToQual k) k Inv0 Oct3)))+ton = const Ton++-- | Doubled tonics.+ton_T_T :: InKey k (Ton ton1) -> InKey k (Ton ton2) -> InKey k (Ton (TonTT ton1 ton2))+ton_T_T _ _ = const Ton+++-- ** Dominants++-- | Dominant (V) chord.+dom_V :: InKey k (Dom (DomVM (DegChord :: DegreeC V MajQ k Inv2 Oct2)))+dom_V = const Dom++-- | Dominant seventh (V7) chord.+dom_V7 :: InKey k (Dom (DomV7 (DegChord :: DegreeC V DomQ k Inv2 Oct2)))+dom_V7 = const Dom++-- | Dominant leading tone (vii) chord.+dom_vii0 :: InKey k (Dom (DomVii0 (DegChord :: DegreeC VII DimQ k Inv1 Oct2)))+dom_vii0 = const Dom++-- | Secondary dominant - dominant (V/V-V7) chord.+dom_II_V7 :: InKey k (Dom (DomSecD (DegChord :: DegreeC II DomQ k Inv0 Oct3) (DegChord :: DegreeC V DomQ k Inv2 Oct2)))+dom_II_V7 = const Dom++-- | Subdominant followed by a dominant.+dom_S_D :: InKey k (Sub subdom) -> InKey k (Dom dom) -> InKey k (Dom (DomSD subdom dom))+dom_S_D _ _ = const Dom++-- | Dominant followed by another dominant.+dom_D_D :: InKey k (Dom dom1) -> InKey k (Dom dom2) -> InKey k (Dom (DomDD dom1 dom2))+dom_D_D _ _ = const Dom++-- ** Subdominants++-- | Subdominant fourth (IV) chord.+subdom_IV :: InKey k (Sub (SubIV (DegChord :: DegreeC IV (KeyToQual k) k Inv2 Oct2)))+subdom_IV = const Sub++-- | Subdominant minor second (ii) chord.+subdom_ii :: IsMajor k "ii subdominant"+    => InKey k (Sub (SubIIm (DegChord :: DegreeC II MinQ k Inv0 Oct3)))+subdom_ii = const Sub++-- | Subdominant third-fourth (iii-IV) progression.+subdom_iii_IV :: IsMajor k "iii-IV subdominant"+    => InKey k (Sub (SubIIImIVM (DegChord :: DegreeC III MinQ k Inv0 Oct3) (DegChord :: DegreeC IV MajQ k Inv3 Oct2)))+subdom_iii_IV = const Sub++-- | Doubled subdominants.+subdom_S_S :: InKey k (Sub sub1) -> InKey k (Sub sub2) -> InKey k (Sub (SubSS sub1 sub2))+subdom_S_S _ _ = const Sub++-- * Time signatures++-- | Duple meter (2/4).+duple :: TimeSig 2+duple = TimeSig++-- | Triple meter (3/4).+triple :: TimeSig 3+triple = TimeSig++-- | Quadruple meter (4/4).+quadruple :: TimeSig 4+quadruple = TimeSig++-- * Key literals+mkKeyLits

@@ -0,0 +1,179 @@++-----------------------------------------------------------------------------+-- |+-- Module      :  Mezzo.Compose.Intervals+-- Description :  Interval literals+-- Copyright   :  (c) Dima Szamozvancev+-- License     :  MIT+--+-- Maintainer  :  ds709@cam.ac.uk+-- Stability   :  experimental+-- Portability :  portable+--+-- Literals and operations involving intervals.+--+-----------------------------------------------------------------------------++module Mezzo.Compose.Intervals where++import Mezzo.Model+import Mezzo.Model.Prim+import Mezzo.Compose.Types+import Mezzo.Compose.Builder+import Mezzo.Compose.Templates++import GHC.TypeLits+import Data.Kind+import Control.Monad+++-- * Atomic literals++-- ** Interval class literals++_iMaj :: IC Maj+_iMaj = IC++_iMin :: IC Min+_iMin = IC++_iPerf :: IC Perf+_iPerf = IC++_iAug :: IC Aug+_iAug = IC++_iDim :: IC Dim+_iDim = IC++-- ** Interval size literals++_i1 :: IS Unison+_i1 = IS++_i2 :: IS Second+_i2 = IS++_i3 :: IS Third+_i3 = IS++_i4 :: IS Fourth+_i4 = IS++_i5 :: IS Fifth+_i5 = IS++_i6 :: IS Sixth+_i6 = IS++_i7 :: IS Seventh+_i7 = IS++_i8 :: IS Octave+_i8 = IS++-- ** Constructor++interval :: IC ic -> IS is -> Intv (Interval ic is)+interval _ _ = Intv++-- * Concrete interval literals++iPerf1 :: Intv (Interval Perf Unison)+iPerf1 = Intv++iAug1 :: Intv (Interval Aug Unison)+iAug1 = Intv+++iDim2 :: Intv (Interval Dim Second)+iDim2 = Intv++iMin2 :: Intv (Interval Min Second)+iMin2 = Intv++iMaj2 :: Intv (Interval Maj Second)+iMaj2 = Intv++iAug2 :: Intv (Interval Aug Second)+iAug2 = Intv+++iDim3 :: Intv (Interval Dim Third)+iDim3 = Intv++iMin3 :: Intv (Interval Min Third)+iMin3 = Intv++iMaj3 :: Intv (Interval Maj Third)+iMaj3 = Intv++iAug3 :: Intv (Interval Aug Third)+iAug3 = Intv+++iDim4 :: Intv (Interval Dim Fourth)+iDim4 = Intv++iPerf4 :: Intv (Interval Perf Fourth)+iPerf4 = Intv++iAug4 :: Intv (Interval Aug Fourth)+iAug4 = Intv+++iDim5 :: Intv (Interval Dim Fifth)+iDim5 = Intv++iPerf5 :: Intv (Interval Perf Fifth)+iPerf5 = Intv++iAug5 :: Intv (Interval Aug Fifth)+iAug5 = Intv+++iDim6 :: Intv (Interval Dim Sixth)+iDim6 = Intv++iMin6 :: Intv (Interval Min Sixth)+iMin6 = Intv++iMaj6 :: Intv (Interval Maj Sixth)+iMaj6 = Intv++iAug6 :: Intv (Interval Aug Sixth)+iAug6 = Intv+++iDim7 :: Intv (Interval Dim Seventh)+iDim7 = Intv++iMin7 :: Intv (Interval Min Seventh)+iMin7 = Intv++iMaj7 :: Intv (Interval Maj Seventh)+iMaj7 = Intv++iAug7 :: Intv (Interval Aug Seventh)+iAug7 = Intv+++iDim8 :: Intv (Interval Dim Octave)+iDim8 = Intv++iPerf8 :: Intv (Interval Perf Octave)+iPerf8 = Intv++iAug8 :: Intv (Interval Aug Octave)+iAug8 = Intv+++-- * Operations++transUp :: (tr ~ (PitchRoot (RaiseBy (RootToPitch r) i)), IntRep tr)+    => Intv i -> RootS r -> RootS tr+transUp i _ = spec Root++transDown :: (tr ~ (PitchRoot (LowerBy (RootToPitch r) i)), IntRep tr)+    => Intv i -> RootS r -> RootS tr+transDown i _ = spec Root

@@ -1,4 +1,4 @@-{-# LANGUAGE TypeInType, TemplateHaskell, ExplicitForAll, ViewPatterns #-}+{-# LANGUAGE TemplateHaskell, ExplicitForAll, ViewPatterns #-}  ----------------------------------------------------------------------------- -- |@@ -22,15 +22,19 @@     , mkDurLits     , mk32ndLits     , mkPitchLits+    , mkKeyLits     , mkPitchSpecs     , scaleDegreeLits     , modeLits+    , dyaTyLits     , triTyLits-    , sevTyLits+    , tetTyLits     , invLits+    , mkDyaConvs     , mkTriConvs-    , mkSevConvs-    , mkDoubledConvs+    , mkDoubledDConvs+    , mkTetConvs+    , mkDoubledTConvs     ) where  import Mezzo.Model@@ -67,15 +71,20 @@ modeLits :: DecsQ modeLits = genLitDecs modeFormatter "Mod" ''Mode -- Might want to extend modes later +dyaTyLits :: DecsQ+dyaTyLits = genLitDecs choTyFormatter "DyaType" ''DyadType+ -- | Generate triad type literal declarations. triTyLits :: DecsQ-triTyLits = genLitDecs choTyFormatter "TriType" ''TriadType+triTyLits = do+    dcs <- filter (\n -> nameBase n /= "DoubledD") <$> getDataCons ''TriadType+    join <$> traverse (mkSingLit choTyFormatter "TriType") dcs  -- | Generate seventh type literal declarations.-sevTyLits :: DecsQ-sevTyLits = do-    dcs <- filter (\n -> nameBase n /= "Doubled") <$> getDataCons ''SeventhType-    join <$> traverse (mkSingLit choTyFormatter "SevType") dcs+tetTyLits :: DecsQ+tetTyLits = do+    dcs <- filter (\n -> nameBase n /= "DoubledT") <$> getDataCons ''TetradType+    join <$> traverse (mkSingLit choTyFormatter "TetType") dcs  invLits :: DecsQ invLits = genLitDecs invFormatter "Inv" ''Inversion@@ -110,7 +119,7 @@                 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)) |]+            dec <- [d| $(varP valName) = Pit |]             return $ tySig : dec     join <$> sequence (declareVal <$> pcNames <*> accNames <*> octNames)    -- Every combination of PCs, Accs and Octs @@ -126,26 +135,26 @@             return $ tySig1 : dec1 ++ tySig1' : dec1'     noteTerm <- do             let valName = mkName $ (durLitFormatter name) !! 1 : "n"-            tySig2 <- sigD valName $ [t| forall r. IntRep r => RootT r $(conT name) |]+            tySig2 <- sigD valName $ [t| forall r s. (ValidNote s r $(conT name), IntRep r) => RootT s r $(conT name) |]             dec2 <- [d| $(varP valName) = \p -> Note p $(varE litName) |]             let valName' = mkName $ (durLitFormatter name) !! 1 : "n\'"-            tySig2' <- sigD valName' $ [t| forall r. IntRep r => RootT r (Dot $(conT name)) |]+            tySig2' <- sigD valName' $ [t| forall r s. (ValidNote s r (Dot $(conT name)), IntRep r) => RootT s r (Dot $(conT name)) |]             dec2' <- [d| $(varP valName') = \p -> Note p $(varE litName') |]             return $ tySig2 : dec2 ++ tySig2' : dec2'     restTerm <- do             let valName = mkName $ (durLitFormatter name) !! 1 : "r"-            tySig2 <- sigD valName $ [t| RestT $(conT name) |]+            tySig2 <- sigD valName $ [t| forall s. (ValidRest s $(conT name)) => RestT s $(conT name) |]             dec2 <- [d| $(varP valName) = const (Rest $(varE litName)) |]             let valName' = mkName $ (durLitFormatter name) !! 1 : "r\'"-            tySig2' <- sigD valName' $ [t| RestT (Dot $(conT name)) |]+            tySig2' <- sigD valName' $ [t| forall s. (ValidRest s (Dot $(conT name))) => RestT s (Dot $(conT name)) |]             dec2' <- [d| $(varP valName') = const (Rest $(varE litName')) |]             return $ tySig2 : dec2 ++ tySig2' : dec2'     chordTerm <- do             let valName = mkName $ (durLitFormatter name) !! 1 : "c"-            tySig2 <- sigD valName $ [t| forall n r. (Primitive n, IntListRep r) => ChorT (r :: ChordType n) $(conT name) |]+            tySig2 <- sigD valName $ [t| forall n r s. (Primitive n, IntListRep r, ValidChord s r $(conT name)) => ChorT s (r :: ChordType n) $(conT name) |]             dec2 <- [d| $(varP valName) = \c -> Chord c $(varE litName) |]             let valName' = mkName $ (durLitFormatter name) !! 1 : "c\'"-            tySig2' <- sigD valName' $ [t| forall n r. (Primitive n, IntListRep r) => ChorT (r :: ChordType n) (Dot $(conT name)) |]+            tySig2' <- sigD valName' $ [t| forall n r s. (Primitive n, IntListRep r, ValidChord s r (Dot $(conT name))) => ChorT s (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@@ -159,21 +168,37 @@             return $ tySig1 : dec1     noteTerm <- do             let valName = mkName $ "tn"-            tySig2 <- sigD valName $ [t| forall r. IntRep r => RootT r $(conT ''ThirtySecond) |]+            tySig2 <- sigD valName $ [t| forall r s. (ValidNote s r $(conT ''ThirtySecond), IntRep r) => RootT s 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) |]+            tySig2 <- sigD valName $ [t| forall s. ValidRest s $(conT ''ThirtySecond) => RestT s $(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) |]+            tySig2 <- sigD valName $ [t| forall n r s. (Primitive n, IntListRep r, ValidChord s r $(conT ''ThirtySecond)) => ChorT s (r :: ChordType n) $(conT ''ThirtySecond) |]             dec2 <- [d| $(varP valName) = \c -> Chord c $(varE litName)  |]             return $ tySig2 : dec2     return $ literal ++ noteTerm ++ restTerm ++ chordTerm +mkKeyLits :: DecsQ+mkKeyLits = do+    pcNames <- getDataCons ''PitchClass+    accNames <- getDataCons ''Accidental+    modeNames <- getDataCons ''Mode+    let declareVal pc acc mode = do  -- Generates a type signature and value declaration for the specified pitch+            let pcStr = tail $ pcFormatter pc+                accStr = shorterAccFormatter acc+                modeStr = shortModeFormatter mode+                valName = mkName $ pcStr ++ accStr ++ modeStr+            tySig <- sigD valName $ [t| KeyS (Key $(conT pc) $(conT acc) $(conT mode)) |]+            dec <- [d| $(varP valName) = KeyS |]+            return $ tySig : dec+    join <$> sequence (declareVal <$> pcNames <*> accNames <*> modeNames)    -- Every combination of PCs, Accs and Octs++ -- | Generate pitch root specifiers for earch pitch class, accidental and octave. -- These allow for combinatorial input with CPS-style durations and modifiers. mkPitchSpecs :: DecsQ@@ -193,9 +218,26 @@     join <$> sequence (declareVal <$> pcNames <*> accNames <*> octNames)  -- | Generate converters from roots to triads, for each triad type.+mkDyaConvs :: DecsQ+mkDyaConvs = do+    triTyNames <- getDataCons ''DyadType+    let declareFun choTy = do+            let choStr = tail (choTyFormatter choTy)+                valName1 = mkName $ choStr ++ "'"+                valName2 = mkName $ choStr+            tySig1 <- sigD valName1 $+                [t| forall r i. ChorC' Dyad r $(conT choTy) i |]+            dec1 <- [d| $(varP valName1) = \i -> constConv Cho |]+            tySig2 <- sigD valName2 $+                [t| forall r. ChorC Dyad r $(conT choTy) |]+            dec2 <- [d| $(varP valName2) = constConv Cho |]+            return $ (tySig1 : dec1) ++ (tySig2 : dec2)+    join <$> traverse declareFun triTyNames++-- | Generate converters from roots to triads, for each triad type. mkTriConvs :: DecsQ mkTriConvs = do-    triTyNames <- getDataCons ''TriadType+    triTyNames <- filter (\n -> nameBase n /= "DoubledD") <$> getDataCons ''TriadType     let declareFun choTy = do             let choStr = tail (choTyFormatter choTy)                 valName1 = mkName $ choStr ++ "'"@@ -209,36 +251,53 @@             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+-- | Generate converters from roots to doubled dyads, for each dyad type.+mkDoubledDConvs :: DecsQ+mkDoubledDConvs = do+    triTyNames <- getDataCons ''DyadType     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' Triad r (DoubledD $(conT choTy)) i |]+            dec1 <- [d| $(varP valName1) = \i -> constConv Cho |]+            tySig2 <- sigD valName2 $+                [t| forall r. ChorC Triad r (DoubledD $(conT choTy)) |]+            dec2 <- [d| $(varP valName2) = constConv Cho |]+            return $ (tySig1 : dec1) ++ (tySig2 : dec2)+    join <$> traverse declareFun triTyNames++-- | Generate converters from roots to tetrads, for each tetrad type.+mkTetConvs :: DecsQ+mkTetConvs = do+    sevTyNames <- filter (\n -> nameBase n /= "DoubledT") <$> getDataCons ''TetradType+    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 |]+                [t| forall r i. ChorC' Tetrad r $(conT choTy) i |]             dec1 <- [d| $(varP valName1) = \i -> constConv Cho |]             tySig2 <- sigD valName2 $-                [t| forall r. ChorC SeventhChord r $(conT choTy) |]+                [t| forall r. ChorC Tetrad 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+-- | Generate converters from roots to doubled triads, for each triad type.+mkDoubledTConvs :: DecsQ+mkDoubledTConvs = do+    triTyNames <- filter (\n -> nameBase n /= "DoubledD") <$> 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 |]+                [t| forall r i. ChorC' Tetrad r (DoubledT $(conT choTy)) i |]             dec1 <- [d| $(varP valName1) = \i -> constConv Cho |]             tySig2 <- sigD valName2 $-                [t| forall r. ChorC SeventhChord r (Doubled $(conT choTy)) |]+                [t| forall r. ChorC Tetrad r (DoubledT $(conT choTy)) |]             dec2 <- [d| $(varP valName2) = constConv Cho |]             return $ (tySig1 : dec1) ++ (tySig2 : dec2)     join <$> traverse declareFun triTyNames@@ -306,9 +365,17 @@ modeFormatter :: Formatter modeFormatter (nameBase -> name) = map toLower (take 3 name) ++ dropWhile isLower (tail name) +shortModeFormatter :: Formatter+shortModeFormatter (modeFormatter -> name) = '_' : take 3 name+ -- | Formatter for chords types. choTyFormatter :: Formatter choTyFormatter n = case nameBase n of+    "MajThird"       -> "_maj3"+    "MinThird"       -> "_min3"+    "PerfFourth"     -> "_fourth"+    "PerfFifth"      -> "_fifth"+    "PerfOct"        -> "_oct"     "MajTriad"       -> "_maj"     "MinTriad"       -> "_min"     "AugTriad"       -> "_aug"

@@ -1,8 +1,4 @@-{-# LANGUAGE TypeInType, TypeOperators, GADTs, TypeFamilies, MultiParamTypeClasses,-    FlexibleInstances, UndecidableInstances, ScopedTypeVariables, FlexibleContexts, RankNTypes #-} -{-# OPTIONS_GHC -fplugin GHC.TypeLits.Normalise #-}- ----------------------------------------------------------------------------- -- | -- Module      :  Mezzo.Compose.Types@@ -92,81 +88,79 @@ -------------------------------------------------------------------------------  -- | 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+data Melody :: forall l t k r. Signature t k r -> 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+    Melody  :: Melody s (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+    (:|)    :: (ValidMel s ms (FromRoot r d), IntRep r, Primitive d, ValidNote s r d)+           => Melody s ms d -> RootS r -> Melody s (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+    (:<<<)  :: (ValidMel s ms (FromRoot r ThirtySecond), IntRep r, Primitive d, ValidNote s r ThirtySecond)+           => Melody s ms d -> RootS r -> Melody s (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+    (:<<)   :: (ValidMel s ms (FromRoot r Sixteenth), IntRep r, Primitive d, ValidNote s r Sixteenth)+           => Melody s ms d -> RootS r -> Melody s (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+    (:<)    :: (ValidMel s ms (FromRoot r Eighth), IntRep r, Primitive d, ValidNote s r Eighth)+           => Melody s ms d -> RootS r -> Melody s (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+    (:^)    :: (ValidMel s ms (FromRoot r Quarter), IntRep r, Primitive d, ValidNote s r Quarter)+           => Melody s ms d -> RootS r -> Melody s (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+    (:>)    :: (ValidMel s ms (FromRoot r Half), IntRep r, Primitive d, ValidNote s r Half)+           => Melody s ms d -> RootS r -> Melody s (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+    (:>>)   :: (ValidMel s ms (FromRoot r Whole), IntRep r, Primitive d, ValidNote s r Whole)+           => Melody s ms d -> RootS r -> Melody s (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)+    (:<<.)  :: (ValidMel s ms (FromRoot r (Dot Sixteenth)), IntRep r, Primitive d, ValidNote s r (Dot Sixteenth))+           => Melody s ms d -> RootS r -> Melody s (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)+    (:<.)   :: (ValidMel s ms (FromRoot r (Dot Eighth)), IntRep r, Primitive d, ValidNote s r (Dot Eighth))+           => Melody s ms d -> RootS r -> Melody s (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)+    (:^.)   :: (ValidMel s ms (FromRoot r (Dot Quarter)), IntRep r, Primitive d, ValidNote s r (Dot Quarter))+           => Melody s ms d -> RootS r -> Melody s (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)+    (:>.)   :: (ValidMel s ms (FromRoot r (Dot Half)), IntRep r, Primitive d, ValidNote s r (Dot Half))+           => Melody s ms d -> RootS r -> Melody s (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)+    (:>>.)  :: (ValidMel s ms (FromRoot r (Dot Whole)), IntRep r, Primitive d, ValidNote s r (Dot Whole))+           => Melody s ms d -> RootS r -> Melody s (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+    (:~|)   :: (ValidMel s ms (FromSilence d), Primitive d, ValidRest s d)+           => Melody s ms d -> RestS -> Melody s (ms +|+ FromSilence d) d     -- | Add a thirty-second rest.-    (:~<<<) :: (MelConstraints ms (FromSilence ThirtySecond), Primitive d)-           => Melody ms d -> RestS -> Melody (ms +|+ FromSilence ThirtySecond) ThirtySecond+    (:~<<<) :: (ValidMel s ms (FromSilence ThirtySecond), Primitive d, ValidRest s ThirtySecond)+           => Melody s ms d -> RestS -> Melody s (ms +|+ FromSilence ThirtySecond) ThirtySecond     -- | Add a sixteenth rest.-    (:~<<)  :: (MelConstraints ms (FromSilence Sixteenth), Primitive d)-           => Melody ms d -> RestS -> Melody (ms +|+ FromSilence Sixteenth) Sixteenth+    (:~<<)  :: (ValidMel s ms (FromSilence Sixteenth), Primitive d, ValidRest s Sixteenth)+           => Melody s ms d -> RestS -> Melody s (ms +|+ FromSilence Sixteenth) Sixteenth     -- | Add an eighth rest.-    (:~<)   :: (MelConstraints ms (FromSilence Eighth), Primitive d)-           => Melody ms d -> RestS -> Melody (ms +|+ FromSilence Eighth) Eighth+    (:~<)   :: (ValidMel s ms (FromSilence Eighth), Primitive d, ValidRest s Eighth)+           => Melody s ms d -> RestS -> Melody s (ms +|+ FromSilence Eighth) Eighth     -- | Add a quarter rest.-    (:~^)   :: (MelConstraints ms (FromSilence Quarter), Primitive d)-           => Melody ms d -> RestS -> Melody (ms +|+ FromSilence Quarter) Quarter+    (:~^)   :: (ValidMel s ms (FromSilence Quarter), Primitive d, ValidRest s Quarter)+           => Melody s ms d -> RestS -> Melody s (ms +|+ FromSilence Quarter) Quarter     -- | Add a half rest.-    (:~>)   :: (MelConstraints ms (FromSilence Half), Primitive d)-           => Melody ms d -> RestS -> Melody (ms +|+ FromSilence Half) Half+    (:~>)   :: (ValidMel s ms (FromSilence Half), Primitive d, ValidRest s Half)+           => Melody s ms d -> RestS -> Melody s (ms +|+ FromSilence Half) Half     -- | Add a whole rest.-    (:~>>)  :: (MelConstraints ms (FromSilence Whole), Primitive d)-           => Melody ms d -> RestS -> Melody (ms +|+ FromSilence Whole) Whole+    (:~>>)  :: (ValidMel s ms (FromSilence Whole), Primitive d, ValidRest s Whole)+           => Melody s ms d -> RestS -> Melody s (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)+    (:~<<.) :: (ValidMel s ms (FromSilence (Dot Sixteenth)), Primitive d, ValidRest s (Dot Sixteenth))+           => Melody s ms d -> RestS -> Melody s (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)+    (:~<.)  :: (ValidMel s ms (FromSilence (Dot Eighth)), Primitive d, ValidRest s (Dot Eighth))+           => Melody s ms d -> RestS -> Melody s (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)+    (:~^.)  :: (ValidMel s ms (FromSilence (Dot Quarter)), Primitive d, ValidRest s (Dot Quarter))+           => Melody s ms d -> RestS -> Melody s (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)+    (:~>.)  :: (ValidMel s ms (FromSilence (Dot Half)), Primitive d, ValidRest s (Dot Half))+           => Melody s ms d -> RestS -> Melody s (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+    (:~>>.) :: (ValidMel s ms (FromSilence (Dot Whole)), Primitive d, ValidRest s (Dot Whole))+           => Melody s ms d -> RestS -> Melody s (ms +|+ FromSilence (Dot Whole)) (Dot Whole)

@@ -32,24 +32,40 @@     , Pit (..)     , Mode (..)     , ScaleDegree (..)+    , DegreeType (..)     , KeyType (..)     , RootType (..)     , Mod (..)     , ScaDeg (..)+    , Deg (..)     , KeyS (..)     , Root (..)+    , IntervalSize (..)+    , IntervalClass (..)+    , IntervalType (..)+    , IS (..)+    , IC (..)+    , Intv (..)     , RootToPitch     , PitchToNat     , Sharpen     , Flatten+    , OctPred+    , OctSucc     , Dot     , FromRoot     , FromSilence     , Voice     , Partiture-    , RaiseAllByOct+    , RaiseBy+    , LowerBy+    , RaiseAllBy+    , LowerAllBy+    , TransposeUpBy+    , TransposeDownBy     ) 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+import Mezzo.Model.Rules.RuleSet as X

@@ -0,0 +1,97 @@++-----------------------------------------------------------------------------+-- |+-- Module      :  Mezzo.Model.Errors+-- Description :  Musical error handling+-- Copyright   :  (c) Dima Szamozvancev+-- License     :  MIT+--+-- Maintainer  :  ds709@cam.ac.uk+-- Stability   :  experimental+-- Portability :  portable+--+-- Types and functions for handling and displaying composition errors.+--+-----------------------------------------------------------------------------++module Mezzo.Model.Errors where++import Mezzo.Model.Types++import GHC.TypeLits++-------------------------------------------------------------------------------+-- Types+-------------------------------------------------------------------------------++-- | A pair of pitches.+type PitchPair = (PitchType, PitchType)++-- | A pair of dyads (pair of pairs of pitches).+data DyadPair = DyP PitchPair PitchPair++-- | Create dyad pair from four pitches.+type family DyPair p1 p2 q1 q2 :: DyadPair where+    DyPair p1 p2 q1 q2 = DyP '(p1, p2) '(q1, q2)++-------------------------------------------------------------------------------+-- Pretty printing+-------------------------------------------------------------------------------++-- | Print pitch class type.+type family PpPC (pc :: PitchClass) :: ErrorMessage where+    PpPC C = Text "C"+    PpPC D = Text "D"+    PpPC E = Text "E"+    PpPC F = Text "F"+    PpPC G = Text "G"+    PpPC A = Text "A"+    PpPC B = Text "B"++-- | Print accidental type.+type family PpAcc (acc :: Accidental) :: ErrorMessage where+    PpAcc Natural = Text ""+    PpAcc Sharp = Text "#"+    PpAcc Flat = Text "b"++-- | Print octave type.+type family PpOct (oct :: OctaveNum) :: ErrorMessage where+    PpOct Oct_1 = Text "_5"+    PpOct Oct0 = Text "_4"+    PpOct Oct1 = Text "_3"+    PpOct Oct2 = Text "__"+    PpOct Oct3 = Text "_"+    PpOct Oct4 = Text ""+    PpOct Oct5 = Text "'"+    PpOct Oct6 = Text "''"+    PpOct Oct7 = Text "'3"+    PpOct Oct8 = Text "'4"++-- | Print pitch type.+type family PpPitch (p :: PitchType) :: ErrorMessage where+    PpPitch (Pitch pc acc oct) = PpPC pc :<>: PpAcc acc :<>: PpOct oct+    PpPitch Silence = Text "Rest"++-- | Print pitch pair.+type family PpPitchPair (pp :: PitchPair) :: ErrorMessage where+    PpPitchPair '(p1, p2) = PpPitch p1 :<>: Text " and " :<>: PpPitch p2++-- | Print dyad pair.+type family PpDyadPair (dp :: DyadPair) :: ErrorMessage where+    PpDyadPair (DyP d1 d2) = PpPitchPair d1 :<>: Text ", then " :<>: PpPitchPair d2++-- | Create an error message with a given text and pitch.+type family PitchError (t :: Symbol) (p :: PitchType) where+    PitchError t p = TypeError (Text t :<>: PpPitch p)++-- | Create an error message with a given text and pair of pitches.+type family PitchPairError (t :: Symbol) (p :: PitchPair) where+    PitchPairError t p = TypeError (Text t :<>: PpPitchPair p)++-- | Create an error message with the given text and pair of dyads.+type family MotionError (t :: Symbol) (d :: DyadPair) where+    MotionError t p = TypeError (Text t :<>: PpDyadPair p)++-- | Create an error message with the given text and chord root.+type family ChordError (t1 :: Symbol) (r :: RootType) (t2 :: Symbol) where+    ChordError t1 r t2 = TypeError (Text t1  :<>: PpPitch (RootToPitch r) :<>: Text t2)

@@ -0,0 +1,23 @@++-----------------------------------------------------------------------------+-- |+-- Module      :  Mezzo.Model.Harmony+-- Description :  Mezzo harmonic constructs+-- Copyright   :  (c) Dima Szamozvancev+-- License     :  MIT+--+-- Maintainer  :  ds709@cam.ac.uk+-- Stability   :  experimental+-- Portability :  portable+--+-- Module providing the external interface to the Mezzo harmonic constructs.+--+-----------------------------------------------------------------------------++module Mezzo.Model.Harmony (module X) where++-- Uses import/export shortcut as suggested by HLint.++import Mezzo.Model.Harmony.Chords as X+import Mezzo.Model.Harmony.Functional as X+import Mezzo.Model.Harmony.Motion as X

@@ -1,6 +1,3 @@-{-# LANGUAGE  TypeInType, UndecidableInstances, GADTs, TypeOperators,-    TypeApplications, TypeFamilies, ScopedTypeVariables, FlexibleInstances #-}-{-# OPTIONS_GHC -fplugin GHC.TypeLits.Normalise #-}  ----------------------------------------------------------------------------- -- |@@ -20,17 +17,18 @@ module Mezzo.Model.Harmony.Chords     (     -- * Chords-      TriadType (..)-    , SeventhType (..)+      DyadType (..)+    , TriadType (..)+    , TetradType (..)     , Inversion (..)+    , DyaType (..)     , TriType (..)-    , SevType (..)+    , TetType (..)     , Inv (..)     , InvertChord     , ChordType (..)     , Cho (..)     , FromChord-    , ChordsToPartiture     ) where  import GHC.TypeLits@@ -44,50 +42,72 @@ -- Chords ------------------------------------------------------------------------------- +-- | The type of a dyad.+data DyadType = MinThird | MajThird | PerfFourth | PerfFifth | PerfOct+ -- | The type of a triad.-data TriadType = MajTriad | MinTriad | AugTriad | DimTriad+data TriadType = MajTriad | MinTriad | AugTriad | DimTriad | DoubledD DyadType --- | The type of a seventh chord.-data SeventhType = MajSeventh | MajMinSeventh | MinSeventh | HalfDimSeventh | DimSeventh | Doubled TriadType+-- | The type of a tetrad.+data TetradType = MajSeventh | MajMinSeventh | MinSeventh | HalfDimSeventh | DimSeventh | DoubledT TriadType  -- | The inversion of a chord. data Inversion = Inv0 | Inv1 | Inv2 | Inv3 +-- | A chord type, indexed by the number of notes.+data ChordType :: Nat -> Type where+    -- | A dyad, consisting of two pitches.+    Dyad   :: RootType -> DyadType -> Inversion -> ChordType 2+    -- | A triad, consisting of three pitches.+    Triad  :: RootType -> TriadType -> Inversion -> ChordType 3+    -- | A tetrad, consisting of four pitches.+    Tetrad :: RootType -> TetradType -> Inversion -> ChordType 4++-- | The singleton type for 'DyadType'+data DyaType (t :: DyadType) = DyaType+ -- | The singleton type for 'TriadType'. data TriType (t :: TriadType) = TriType --- | The singleton type for 'SeventhType'.-data SevType (t :: SeventhType) = SevType+-- | The singleton type for 'TetradType'.+data TetType (t :: TetradType) = TetType  -- | 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-+-- | The singleton type for 'ChordType'. data Cho (c :: ChordType n) = Cho +-- | Convert a dyad type to a list of intervals between the individual pitches.+type family DyadTypeToIntervals (t :: DyadType) :: Vector IntervalType 2 where+    DyadTypeToIntervals MinThird =+                Interval Perf Unison :-- Interval Min Third   :-- None+    DyadTypeToIntervals MajThird =+                Interval Perf Unison :-- Interval Maj Third   :-- None+    DyadTypeToIntervals PerfFourth =+                Interval Perf Unison :-- Interval Perf Fourth :-- None+    DyadTypeToIntervals PerfFifth =+                Interval Perf Unison :-- Interval Perf Fifth  :-- None+    DyadTypeToIntervals PerfOct =+                Interval Perf Unison :-- Interval Perf Octave :-- None+ -- | 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+    TriadTypeToIntervals MajTriad      = DyadTypeToIntervals MajThird :-| Interval Perf Fifth+    TriadTypeToIntervals MinTriad      = DyadTypeToIntervals MinThird :-| Interval Perf Fifth+    TriadTypeToIntervals AugTriad      = DyadTypeToIntervals MajThird :-| Interval Aug Fifth+    TriadTypeToIntervals DimTriad      = DyadTypeToIntervals MinThird :-| Interval Dim Fifth+    TriadTypeToIntervals (DoubledD dt) = DyadTypeToIntervals dt       :-| Interval Perf Octave + -- | 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+type family TetradTypeToIntervals (s :: TetradType) :: Vector IntervalType 4 where+    TetradTypeToIntervals MajSeventh     = TriadTypeToIntervals MajTriad :-| Interval Maj Seventh+    TetradTypeToIntervals MajMinSeventh  = TriadTypeToIntervals MajTriad :-| Interval Min Seventh+    TetradTypeToIntervals MinSeventh     = TriadTypeToIntervals MinTriad :-| Interval Min Seventh+    TetradTypeToIntervals HalfDimSeventh = TriadTypeToIntervals DimTriad :-| Interval Min Seventh+    TetradTypeToIntervals DimSeventh     = TriadTypeToIntervals DimTriad :-| Interval Dim Seventh+    TetradTypeToIntervals (DoubledT 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@@ -95,52 +115,93 @@     -- 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 Inv3 n (p :-- ps) = Invert Inv2 (n - 1) (p :-- (Head' ps) :-- (Tail' (Tail' (ps)))) :-| RaiseByOct (Head' (Tail' 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 InvertDoubledD (i :: Inversion) (ps :: Vector PitchType 3) :: Vector PitchType 3 where+    InvertDoubledD Inv0 ps = ps+    InvertDoubledD Inv1 ps = Invert Inv1 2 (Init' ps) :-| (RaiseByOct (Head' (Tail' ps)))+    InvertDoubledD Inv2 ps = RaiseAllBy' ps (Interval Perf Octave) +-- | Invert a doubled triad chord.+type family InvertDoubledT (i :: Inversion) (ps :: Vector PitchType 4) :: Vector PitchType 4 where+    InvertDoubledT Inv0 ps = ps+    InvertDoubledT Inv1 ps = Invert Inv1 3 (Init' ps) :-| (RaiseByOct (Head' (Tail' ps)))+    InvertDoubledT Inv2 ps = Invert Inv2 3 (Init' ps) :-| (RaiseByOct (Head' (Tail' (Tail' ps))))+    InvertDoubledT Inv3 ps = RaiseAllBy' ps (Interval Perf Octave)++-- | Enumerate inversions. type family InvSucc (i :: Inversion) :: Inversion where     InvSucc Inv0 = Inv1     InvSucc Inv1 = Inv2     InvSucc Inv2 = Inv3     InvSucc Inv3 = Inv0 +-- | Invert a chord once. type family InvertChord (c :: ChordType n) :: ChordType n where+    InvertChord (Dyad r t Inv0) = Dyad r t Inv1+    InvertChord (Dyad r t Inv1) = Dyad r t Inv0     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)+    InvertChord (Tetrad r t i) = Tetrad 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+    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))+    ChordToPitchList (Dyad r t i)+                    = Invert i 2 (BuildOnRoot r (DyadTypeToIntervals t))+    ChordToPitchList (Triad r (DoubledD dt) i)+                    = InvertDoubledD i (BuildOnRoot r (TriadTypeToIntervals (DoubledD dt)))+    ChordToPitchList (Triad r t i)+                    = Invert i 3 (BuildOnRoot r (TriadTypeToIntervals t))+    ChordToPitchList (Tetrad r (DoubledT tt) i)+                    = InvertDoubledT i (BuildOnRoot r (TetradTypeToIntervals (DoubledT tt)))+    ChordToPitchList (Tetrad r t i)+                    = Invert i 4 (BuildOnRoot r (TetradTypeToIntervals 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 MajThird where+    type Rep MajThird = Int -> [Int]+    prim t = \r -> [r, r + 4]+    pretty t = "M3"++instance Primitive MinThird where+    type Rep MinThird = Int -> [Int]+    prim t = \r -> [r, r + 3]+    pretty t = "m3"++instance Primitive PerfFourth where+    type Rep PerfFourth = Int -> [Int]+    prim t = \r -> [r, r + 5]+    pretty t = "P4"++instance Primitive PerfFifth where+    type Rep PerfFifth = Int -> [Int]+    prim t = \r -> [r, r + 7]+    pretty t = "P5"++instance Primitive PerfOct where+    type Rep PerfOct = Int -> [Int]+    prim t = \r -> [r, r + 12]+    pretty t = "P8"++ instance Primitive MajTriad where     type Rep MajTriad = Int -> [Int]     prim t = \r -> [r, r + 4, r + 7]@@ -161,6 +222,12 @@     prim t = \r -> [r, r + 3, r + 6]     pretty t = "dim" +instance FunRep Int [Int] c => Primitive (DoubledD c) where+    type Rep (DoubledD c) = Int -> [Int]+    prim t = \r -> prim (DyaType @c) r ++ [r + 12]+    pretty t = pretty (DyaType @c) ++ "D"++ instance Primitive MajSeventh where     type Rep MajSeventh = Int -> [Int]     prim t = \r -> [r, r + 4, r + 7, r + 11]@@ -186,8 +253,8 @@     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]+instance FunRep Int [Int] c => Primitive (DoubledT c) where+    type Rep (DoubledT c) = Int -> [Int]     prim t = \r -> prim (TriType @c) r ++ [r + 12]     pretty t = pretty (TriType @c) ++ "D" @@ -218,25 +285,42 @@     pretty i = "I3"  instance (IntRep r, FunRep Int [Int] t, FunRep [Int] [Int] i)+        => Primitive (Dyad r t i) where+    type Rep (Dyad r t i) = [Int]+    prim c = prim (Inv @i) . prim (DyaType @t) $ prim (Root @r)+    pretty c = pc ++ " " ++ pretty (DyaType @t) ++ " " ++ pretty (Inv @i)+        where pc = takeWhile (\c -> c /= ' ' && c /= '\'' && c /= '_') $ pretty (Root @r)+++instance (IntRep r, FunRep Int [Int] dt, FunRep [Int] [Int] i)+        => Primitive (Triad r (DoubledD dt) i) where+    type Rep (Triad r (DoubledD dt) i) = [Int]+    prim c = inverted ++ [head inverted + 12]+        where rootPos = prim (DyaType @dt) $ prim (Root @r)+              inverted = prim (Inv @i) rootPos+    pretty c = pc ++ " " ++ pretty (DyaType @dt) ++ "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 (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]+        => Primitive (Tetrad r (DoubledT tt) i) where+    type Rep (Tetrad r (DoubledT 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)+        => Primitive (Tetrad r t i) where+    type Rep (Tetrad r t i) = [Int]+    prim c = prim (Inv @i) . prim (TetType @t) $ prim (Root @r)+    pretty c = pc ++ " " ++ pretty (TetType @t) ++ " " ++ pretty (Inv @i)         where pc = takeWhile (\c -> c /= ' ' && c /= '\'' && c /= '_') $ pretty (Root @r)

@@ -1,6 +1,4 @@-{-# LANGUAGE  TypeInType, MultiParamTypeClasses, FlexibleInstances,-    UndecidableInstances, GADTs, TypeOperators, TypeFamilies, FlexibleContexts #-}-{-# OPTIONS_GHC -fplugin GHC.TypeLits.Normalise #-}+{-# LANGUAGE ViewPatterns #-}  ----------------------------------------------------------------------------- -- |@@ -19,199 +17,370 @@  module Mezzo.Model.Harmony.Functional     (+    -- * Types and operations       Quality (..)-    , Degree (..)-    , Piece (..)+    , DegreeC (..)+    , TimeSignature+    , TimeSig (..)+    , KeyToQual+    , KeyToOtherQual+    , IsMajor+    , IsMinor+    -- * Functional harmony+    -- ** Types and constructors+    , ProgType (..)     , Phrase (..)     , Cadence (..)     , Tonic (..)     , Dominant (..)     , Subdominant (..)-    , PieceToChords+    , ChordsToPartiture+    , ProgTypeToChords+    , FromProg+    -- ** Singletons+    , Prog (..)+    , Ton (..)+    , Dom (..)+    , Sub (..)+    , Cad (..)+    , Phr (..)     )     where -import GHC.TypeLits-import Data.Kind-+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.-data Degree (d :: ScaleDegree) (q :: Quality) (k :: KeyType) (i :: Inversion) where-    DegChord :: Degree d q k i+-- | 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 --- | 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)+-- | The number of beats in a bar.+type TimeSignature = Nat --- | 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+-- | Singleton for 'TimeSignature'.+data TimeSig (t :: TimeSignature) = TimeSig --- | 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+-- | 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 Piece (k :: KeyType) (l :: Nat) where-    Cad :: Cadence k l -> Piece k l-    (:=) :: Phrase k l -> Piece k (n - l) -> Piece k n+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 progression.+    -- | A tonic-dominant-tonic phrase.     PhraseIVI :: Tonic k (l2 - l1) -> Dominant k l1 -> Tonic k (l - l2) -> Phrase k l-    -- | A dominant-tonic progression.+    -- | 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    :: Degree V MajQ k Inv1 -> Degree I q k Inv0 -> Cadence k 2+    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   :: Degree V DomQ k Inv2 -> Degree I q k Inv0 -> Cadence k 2+    AuthCad7   :: DegreeC V DomQ k Inv2 (OctPred o) -> DegreeC I q k Inv0 o -> Cadence k 2     -- | Authentic cadence with diminished seventh chord.-    AuthCadVii :: Degree VII DimQ k Inv0 -> Degree I q k Inv0 -> Cadence k 2+    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  :: 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+    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  :: Degree V DomQ k Inv0 -> Degree VI q k Inv2 -> Cadence k 2+    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  -- | 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+    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   :: Degree V MajQ k i -> Dominant k 1+    DomVM   :: DegreeC V MajQ k Inv2 o -> Dominant k 1     -- | Seventh chord fifth degree dominant.-    DomV7   :: Degree V DomQ k i -> Dominant k 1+    DomV7   :: DegreeC V DomQ k Inv2 o -> Dominant k 1     -- | Diminished seventh degree dominant.-    DomVii0 :: Degree VII DimQ k i -> Dominant k 1+    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-    -- | Secondary dominant followed by dominant.-    DomSecD :: Degree II DomQ k Inv0 -> Degree V DomQ k Inv2 -> Dominant k 2+    -- | Doubled dominants.+    DomDD   :: Dominant k l1 -> Dominant k (l - l1) -> Dominant k l  -- | 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+    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 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 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 (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+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  -- | 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+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 l (DomSD (s :: Subdominant k l1) d) =-                    SubdomToChords s ++. DomToChords (l - l1) d+    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 (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+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 (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+    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 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+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 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 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 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"+-- | 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)++-- 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)

@@ -1,7 +1,5 @@-{-# LANGUAGE  TypeInType, MultiParamTypeClasses, FlexibleInstances,-    UndecidableInstances #-} ------------------------------------------------------------------------------+---------------------------------------------------------------------------- -- | -- Module      :  Mezzo.Model.Harmony.Motion -- Description :  Models of harmonic motion@@ -32,6 +30,7 @@  import Mezzo.Model.Types import Mezzo.Model.Prim+import Mezzo.Model.Errors  ------------------------------------------------------------------------------- -- Consonant and dissonant intervals@@ -74,14 +73,20 @@ -------------------------------------------------------------------------------  -- | 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+class DirectMotion (e :: DyadPair) (i1 :: IntervalType) (i2 :: IntervalType)+instance {-# OVERLAPPING #-} MotionError "Parallel unisons are forbidden: " e+                                => DirectMotion e (Interval Perf Unison) (Interval Perf Unison)+instance {-# OVERLAPS #-} MotionError "Direct motion into a perfect unison is forbidden: " e+                                => DirectMotion e i1 (Interval Perf Unison)+instance {-# OVERLAPPING #-} MotionError "Parallel fifths are forbidden: " e+                                => DirectMotion e (Interval Perf Fifth) (Interval Perf Fifth)+instance {-# OVERLAPS #-} MotionError "Direct motion into a perfect fifth is forbidden: " e+                                => DirectMotion e i1 (Interval Perf Fifth)+instance {-# OVERLAPPING #-} MotionError "Parallel octaves are forbidden: " e+                                => DirectMotion e (Interval Perf Octave) (Interval Perf Octave)+instance {-# OVERLAPS #-} MotionError "Direct motion into a perfect octave is forbidden: " e+                                => DirectMotion e i1 (Interval Perf Octave)+instance {-# OVERLAPPABLE #-}      DirectMotion e i1 i2  -- | Ensures that contrary motion is permitted between the two intervals. class ContraryMotion (i1 :: IntervalType) (i2 :: IntervalType)

@@ -1,7 +1,3 @@-{-# LANGUAGE TypeInType, RankNTypes, TypeOperators, GADTs, ConstraintKinds,-    FlexibleContexts, MultiParamTypeClasses, TypeFamilies, UndecidableInstances,-    FlexibleInstances #-}-{-# OPTIONS_GHC -fplugin GHC.TypeLits.Normalise #-}  ----------------------------------------------------------------------------- -- |@@ -22,13 +18,16 @@     (     -- * Music       Music (..)-    , Score (..)-    -- * Harmonic constructs-    , Progression+    , Signature (..)     -- * Constraints-    , MelConstraints-    , HarmConstraints-    , ChordConstraints+    , ValidNote+    , ValidRest+    , ValidChord+    , ValidProg+    , ValidHom+    , ValidMel+    , ValidHarm+    , ValidTripl     ) where  import Data.Kind@@ -41,14 +40,18 @@ import Mezzo.Model.Harmony.Functional import Mezzo.Model.Types import Mezzo.Model.Reify+import Mezzo.Model.Rules.RuleSet -infixl 4 :|:+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. --@@ -60,243 +63,80 @@ --  * 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)+data Music :: forall n l t k r. Signature t k r -> Partiture n l -> Type where     -- | Sequential or melodic composition of music.-    (:|:) :: MelConstraints m1 m2  => Music m1 -> Music m2 -> Music (m1 +|+ m2)+    (:|:) :: ValidMel s m1 m2  => Music s m1 -> Music s m2 -> Music s (m1 +|+ m2)     -- | Parallel or harmonic composition of music.-    (:-:) :: HarmConstraints m1 m2 => Music m1 -> Music m2 -> Music (m1 +-+ m2)+    (:-:) :: 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 :: 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)+    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. ------------------------------------------------------------------------------- --- | Enable or disable music correctness checking.-type Strict = True+-- | Select the active rule set.+type ActRuleSet = Classical --- | Applies the constraint c if strict checking is enabled.-type IfStrict c = If Strict c Valid+-- | 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 NoteConstraints r d = (IntRep r, Primitive d)+type ValidNote (s :: Signature t k r) ro d =+    (NoteConstraints r ro d, IntRep ro, 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))+type ValidRest (s :: Signature t k r) d =+    (RestConstraints r d, Primitive d)  -- | Ensures that the chord is valid.-type ChordConstraints (c :: ChordType n) d = (IntListRep c, Primitive n, Primitive d)+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 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+type ValidProg r t p =+    (ProgConstraints r t p, IntLListRep p, IntRep t, KnownNat t) --- | 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 a homophonic composition is valid.+type ValidHom (s :: Signature t k r) m a =+    HomConstraints r m a --- | 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)+-- | 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 m) where show = render . ppMusic+instance Show (Music s m) where show = render . ppMusic  -- | Pretty-print a 'Music' value.-ppMusic :: Music m -> Box+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

@@ -1,6 +1,3 @@-{-# LANGUAGE TypeInType, TypeOperators, TypeFamilies, GADTs,-    UndecidableInstances, ConstraintKinds #-}-{-# OPTIONS_GHC -fplugin GHC.TypeLits.Normalise #-}  ----------------------------------------------------------------------------- -- |

@@ -1,5 +1,3 @@-{-# LANGUAGE TypeInType, ScopedTypeVariables, TypeFamilies, FlexibleInstances,-    UndecidableInstances, ConstraintKinds #-}  ----------------------------------------------------------------------------- -- |@@ -32,11 +30,17 @@ instance {-# OVERLAPPABLE #-} Primitive t => Show (sing t) where     show = pretty +-- | Primitive types with Boolean representations.+type BoolRep t = (Primitive t, Rep t ~ Bool)+ -- | 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 list of integer list representations.+type IntLListRep 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))

@@ -0,0 +1,202 @@++-----------------------------------------------------------------------------+-- |+-- 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

@@ -0,0 +1,97 @@++-----------------------------------------------------------------------------+-- |+-- Module      :  Mezzo.Model.Rules.RuleSet+-- Description :  MIDI exporting+-- Copyright   :  (c) Dima Szamozvancev+-- License     :  MIT+--+-- Maintainer  :  ds709@cam.ac.uk+-- Stability   :  experimental+-- Portability :  portable+--+-- Encapsulation of various musical rule sets that Mezzo can use.+--+-----------------------------------------------------------------------------++module Mezzo.Model.Rules.RuleSet where++import Mezzo.Model.Types+import Mezzo.Model.Harmony+import Mezzo.Model.Reify+import Mezzo.Model.Prim++import qualified Mezzo.Model.Rules.Classical as CR+import qualified Mezzo.Model.Rules.Strict as SR++import Data.Kind+import GHC.TypeLits++-- * Rule sets++-- | The types of rule sets implemented.+-- data RuleSetType =+--       Free          -- ^ No composition rules.+--     | Classical     -- ^ Classical rules.+--     | Strict        -- ^ Strict rules.++data Free = Free+data Classical = Classical+data Strict = Strict++-- | Class of rule sets for a given rule type.+class RuleSet t where+    type MelConstraints   t (m1 :: Partiture n l1) (m2 :: Partiture n l2) :: Constraint+    type HarmConstraints  t (m1 :: Partiture n1 l) (m2 :: Partiture n2 l) :: Constraint+    type NoteConstraints  t (r :: RootType)        (d :: Duration)        :: Constraint+    type RestConstraints  t                        (d :: Duration)        :: Constraint+    type ChordConstraints t (c :: ChordType n)     (d :: Duration)        :: Constraint+    type ProgConstraints  t (s :: TimeSignature)   (p :: ProgType k l)    :: Constraint+    type HomConstraints   t (m1 :: Partiture n1 l) (m2 :: Partiture n2 l) :: Constraint+    type TriplConstraints t (d :: Duration) (r1 :: RootType) (r2 :: RootType) (r3 :: RootType) :: Constraint++    -- Defaults+    type NoteConstraints t r d = CR.ValidPitch (RootToPitch r)+    type RestConstraints t d = Valid+    type ChordConstraints t c d = Valid+    type ProgConstraints t s p = Valid+    type TriplConstraints t d r1 r2 r3 = Valid+++-- | No rules.+instance RuleSet Free where+    type MelConstraints Free m1 m2 = Valid+    type HarmConstraints Free m1 m2 = Valid+    type HomConstraints Free m1 m2 = Valid++-- | Classical rules.+--+-- Forbids+--+-- * seventh melodic intervals,+-- * minor second, major seventh and augmented octave harmonic intervals, and+-- * direct motion into perfect intervals on harmonic composition.+instance RuleSet Classical where+    type MelConstraints Classical m1 m2 = CR.ValidMelConcat m1 m2+    type HarmConstraints Classical m1 m2 = CR.ValidHarmConcat (Align m1 m2)+    type HomConstraints Classical m1 m2 = CR.ValidHomConcat (Align m1 m2)++-- | Strict rules.+--+-- Forbids all of the above ('Classical'), as well as+--+-- * diminished and augmented melodic intervals,+-- * direct motion into perfect intervals on melodic and homophonic composition, and+-- * major seventh chords.+instance RuleSet Strict where+    type MelConstraints Strict m1 m2 = (SR.ValidMelConcatStrict m1 m2, SR.ValidMelMatrixMotion m1 m2)+    type HarmConstraints Strict m1 m2 = SR.ValidHarmConcat (Align m1 m2)+    type HomConstraints Strict m1 m2 = SR.ValidHarmConcat (Align m1 m2)+    type ChordConstraints Strict c d = (SR.ValidChordType c)+    type TriplConstraints Strict d r1 r2 r3 = ( MelConstraints Strict (FromRoot r1 d) (FromRoot r2 d)+                                              , MelConstraints Strict (FromRoot r2 d) (FromRoot r3 d))++-- * Literal values++-- | The proxy type for 'RuleSetType'.+-- data RuleS (r :: RuleSetType) = RuleS

@@ -0,0 +1,131 @@++-----------------------------------------------------------------------------+-- |+-- 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)

@@ -1,6 +1,4 @@-{-# LANGUAGE TypeInType, GADTs, TypeOperators, TypeFamilies, UndecidableInstances,-    TypeApplications, ScopedTypeVariables, FlexibleInstances, StandaloneDeriving, ViewPatterns #-}-{-# OPTIONS_GHC -fplugin GHC.TypeLits.Normalise #-}+{-# LANGUAGE StandaloneDeriving, ViewPatterns #-}  ----------------------------------------------------------------------------- -- |@@ -38,19 +36,23 @@     -- * Harmonic types     , Mode (..)     , ScaleDegree (..)+    , DegreeType (..)     , KeyType (..)     , RootType (..)     , Mod (..)     , ScaDeg (..)     , KeyS (..)+    , Deg (..)     , Root (..)     , RootToPitch     , PitchToNat     , Sharpen     , Flatten     , Dot+    , HalfOf     , FromRoot     , FromSilence+    , FromTriplet     -- * Specialised musical vector types     , Voice     , Partiture@@ -59,15 +61,26 @@     , IntervalClass (..)     , IntervalType (..)     , MakeInterval+    -- ** Singleton types for interval properties+    , IC (..)+    , IS (..)+    , Intv (..)+    -- * Operations+    , OctPred+    , OctSucc     , HalfStepsUpBy     , HalfStepsDownBy     , RaiseBy     , LowerBy+    , RaiseAllBy+    , LowerAllBy     , RaiseAllBy'     , LowerAllBy'     , RaiseByOct     , LowerByOct     , RaiseAllByOct+    , TransposeUpBy+    , TransposeDownBy     ) where  import GHC.TypeLits@@ -141,6 +154,8 @@ -- | The seven scale degrees. data ScaleDegree = I | II | III | IV | V | VI | VII +data DegreeType = Degree ScaleDegree Accidental OctaveNum+ -- | The of a scale, chord or piece. data KeyType = Key PitchClass Accidental Mode @@ -149,7 +164,7 @@     -- | A pitch constructs a diatonic root.     PitchRoot :: PitchType -> RootType     -- | A key and a scale degree constructs a scalar root.-    DegreeRoot :: KeyType -> ScaleDegree -> RootType+    DegreeRoot :: KeyType -> DegreeType -> RootType  -- | The singleton type for 'Mode'. data Mod (m :: Mode) = Mod@@ -160,6 +175,8 @@ -- | The singleton type for 'KeyType'. data KeyS (k :: KeyType) = KeyS +data Deg (d :: DegreeType) = Deg+ -- | The singleton type for 'Root'. data Root (r :: RootType) where     Root :: Primitive r => Root r@@ -169,25 +186,27 @@ -- 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)+    RootToPitch (DegreeRoot (Key pc acc m) (Degree sd dacc oct)) =+                    HalfStepsUpBy (Pitch pc acc oct) (DegreeOffset m sd dacc)  -- | 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+type family DegreeOffset (m :: Mode) (d :: ScaleDegree) (a :: Accidental) where+    DegreeOffset MajorMode I   Natural = 0+    DegreeOffset MajorMode II  Natural = 2+    DegreeOffset MajorMode III Natural = 4+    DegreeOffset MajorMode IV  Natural = 5+    DegreeOffset MajorMode V   Natural = 7+    DegreeOffset MajorMode VI  Natural = 9+    DegreeOffset MajorMode VII Natural = 11+    DegreeOffset MinorMode I   Natural = 0+    DegreeOffset MinorMode II  Natural = 2+    DegreeOffset MinorMode III Natural = 3+    DegreeOffset MinorMode IV  Natural = 5+    DegreeOffset MinorMode V   Natural = 7+    DegreeOffset MinorMode VI  Natural = 8+    DegreeOffset MinorMode VII Natural = 10+    DegreeOffset m         sd  Flat    = (DegreeOffset m sd Natural) - 1+    DegreeOffset m         sd  Sharp   = (DegreeOffset m sd Natural) + 1  -- | Sharpen a root. type family Sharpen (r :: RootType) :: RootType where@@ -218,6 +237,11 @@ type family FromSilence (d :: Nat) :: Partiture 1 d where     FromSilence d = (Silence +*+ d) :-- None +-- | Create a new partiture with a triplet of three notes.+type family FromTriplet (d :: Nat) (r1 :: RootType) (r2 :: RootType) (r3 :: RootType)+            :: Partiture 1 (d + HalfOf d + HalfOf d) where+    FromTriplet d r1 r2 r3 = FromRoot r1 d +|+ FromRoot r2 (HalfOf d) +|+ FromRoot r3 (HalfOf d)+ ------------------------------------------------------------------------------- -- Type specialisations -------------------------------------------------------------------------------@@ -248,6 +272,15 @@     -- so that dissonance effects are not significant.     Compound :: IntervalType +-- | The singleton type for 'IntervalSize'.+data IS (is :: IntervalSize) = IS++-- | The singleton type for 'IntervalClass'.+data IC (ic :: IntervalClass) = IC++-- | The singleton type for 'IntervalType'.+data Intv (i :: IntervalType) = Intv+ ------------------------------------------------------------------------------- -- Interval construction -------------------------------------------------------------------------------@@ -266,6 +299,8 @@ type family MakeIntervalOrd (p1 :: PitchType) (p2 :: PitchType) :: IntervalType where     -- Handling base cases.     MakeIntervalOrd p p = Interval Perf Unison+    ---- Base cases from C.+    MakeIntervalOrd (Pitch C Flat o) (Pitch C Natural o) = Interval Aug 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@@ -274,26 +309,87 @@     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+    ---- Base cases from F.+    MakeIntervalOrd (Pitch F Flat o) (Pitch F Natural o) = Interval Aug Unison+    MakeIntervalOrd (Pitch F Natural o) (Pitch F Sharp o) = Interval Aug Unison+    MakeIntervalOrd (Pitch F Natural o) (Pitch G Flat o) = Interval Min Second+    MakeIntervalOrd (Pitch F acc o)     (Pitch G acc o)   = Interval Maj Second+    MakeIntervalOrd (Pitch F acc o)     (Pitch A acc o)   = Interval Maj Third+    MakeIntervalOrd (Pitch F acc o)     (Pitch B acc o)   = Interval Aug Fourth+    MakeIntervalOrd (Pitch F acc o1)     (Pitch C acc o2)   =+            IntervalOrCompound o1 o2 (Interval Perf Fifth)+    MakeIntervalOrd (Pitch F acc o1)     (Pitch D acc o2)   =+            IntervalOrCompound o1 o2 (Interval Maj Sixth)+    MakeIntervalOrd (Pitch F acc o1)     (Pitch E acc o2)   =+            IntervalOrCompound o1 o2 (Interval Maj Seventh)+    ---- Base cases from A.+    MakeIntervalOrd (Pitch A Flat o) (Pitch A Natural o) = Interval Aug Unison+    MakeIntervalOrd (Pitch A Natural o) (Pitch A Sharp o) = Interval Aug Unison+    MakeIntervalOrd (Pitch A Natural o) (Pitch B Flat o) = Interval Min Second+    MakeIntervalOrd (Pitch A acc o)     (Pitch B acc o)   = Interval Maj Second+    MakeIntervalOrd (Pitch A acc o1)     (Pitch C acc o2)   =+            IntervalOrCompound o1 o2 (Interval Min Third)+    MakeIntervalOrd (Pitch A acc o1)     (Pitch D acc o2)   =+            IntervalOrCompound o1 o2 (Interval Perf Fourth)+    MakeIntervalOrd (Pitch A acc o1)     (Pitch E acc o2)   =+            IntervalOrCompound o1 o2 (Interval Perf Fifth)+    MakeIntervalOrd (Pitch A acc o1)     (Pitch F acc o2)   =+        IntervalOrCompound o1 o2 (Interval Min Sixth)+    MakeIntervalOrd (Pitch A acc o1)     (Pitch G acc o2)   =+        IntervalOrCompound o1 o2 (Interval Min Seventh)     -- Handling perfect and augmented octaves.     MakeIntervalOrd (Pitch C acc o1) (Pitch C acc o2) =-            If (OctSucc o1 .~. o2) (Interval Perf Octave) Compound+            IntervalOrCompound o1 o2 (Interval Perf Octave)     MakeIntervalOrd (Pitch C Natural o1) (Pitch C Sharp o2) =-            If (OctSucc o1 .~. o2) (Interval Aug Octave) Compound+            IntervalOrCompound o1 o2 (Interval Aug Octave)     MakeIntervalOrd (Pitch C Flat o1) (Pitch C Natural o2) =-            If (OctSucc o1 .~. o2) (Interval Aug Octave) Compound+            IntervalOrCompound o1 o2 (Interval Aug Octave)+    MakeIntervalOrd (Pitch F acc o1) (Pitch F acc o2) =+            IntervalOrCompound o1 o2 (Interval Perf Octave)+    MakeIntervalOrd (Pitch F Natural o1) (Pitch F Sharp o2) =+            IntervalOrCompound o1 o2 (Interval Aug Octave)+    MakeIntervalOrd (Pitch F Flat o1) (Pitch F Natural o2) =+            IntervalOrCompound o1 o2 (Interval Aug Octave)+    MakeIntervalOrd (Pitch A acc o1) (Pitch A acc o2) =+            IntervalOrCompound o1 o2 (Interval Perf Octave)+    MakeIntervalOrd (Pitch A Natural o1) (Pitch A Sharp o2) =+            IntervalOrCompound o1 o2 (Interval Aug Octave)+    MakeIntervalOrd (Pitch A Flat o1) (Pitch A Natural o2) =+            IntervalOrCompound o1 o2 (Interval Aug Octave)     -- 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))+    MakeIntervalOrd (Pitch F Flat o) (Pitch E Sharp o) = Interval Min Second+    MakeIntervalOrd (Pitch F Flat o) (Pitch E Natural o) = Interval Dim Second+    MakeIntervalOrd (Pitch E Natural o) (Pitch F Flat o) = Interval Dim Second+    MakeIntervalOrd (Pitch F Flat o) (Pitch pc2 acc o) =+            Expand (MakeIntervalOrd (Pitch F Natural o) (Pitch pc2 acc o))+    MakeIntervalOrd (Pitch F Sharp o) (Pitch pc2 acc o) =+            Shrink (MakeIntervalOrd (Pitch F Natural o) (Pitch pc2 acc o))+    MakeIntervalOrd (Pitch A Flat o) (Pitch pc2 acc o) =+            Expand (MakeIntervalOrd (Pitch A Natural o) (Pitch pc2 acc o))+    MakeIntervalOrd (Pitch A Sharp o) (Pitch pc2 acc o) =+            Shrink (MakeIntervalOrd (Pitch A 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))+    MakeIntervalOrd (Pitch F Natural o) (Pitch pc2 Sharp o) =+            Expand (MakeIntervalOrd (Pitch F Natural o) (Pitch pc2 Natural o))+    MakeIntervalOrd (Pitch F Natural o) (Pitch pc2 Flat o) =+            Shrink (MakeIntervalOrd (Pitch F Natural o) (Pitch pc2 Natural o))+    MakeIntervalOrd (Pitch A Natural o) (Pitch pc2 Sharp o) =+            Expand (MakeIntervalOrd (Pitch A Natural o) (Pitch pc2 Natural o))+    MakeIntervalOrd (Pitch A Natural o) (Pitch pc2 Flat o) =+            Shrink (MakeIntervalOrd (Pitch A Natural o) (Pitch pc2 Natural o))     -- Handling the general case.+    MakeIntervalOrd (Pitch pc1 acc1 o) (Pitch pc2 acc2 o) =+            MakeIntervalOrd (HalfStepDown (Pitch pc1 acc1 o)) (HalfStepDown (Pitch pc2 acc2 o))     MakeIntervalOrd (Pitch pc1 acc1 o1) (Pitch pc2 acc2 o2) =-            If  (o1 .~. o2 .||. OctSucc o1 .~. o2)+            If  (NextOct o1 o2)                 (MakeIntervalOrd (HalfStepDown (Pitch pc1 acc1 o1)) (HalfStepDown (Pitch pc2 acc2 o2)))                 Compound     -- Handling erroneous construction (shouldn't happen).@@ -301,7 +397,7 @@  -- | Shrink an interval. type family Shrink (i :: IntervalType) :: IntervalType where-    Shrink (Interval Perf Unison) = TypeError (Text "Can't diminish unisons.")+    Shrink (Interval Perf Unison) = TypeError (Text "Can't diminish unisons.1")     Shrink (Interval Perf is)     = Interval Dim is     Shrink (Interval Min  is)     = Interval Dim is     Shrink (Interval Maj  is)     = Interval Min is@@ -310,8 +406,8 @@     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  Unison) = TypeError (Text "Can't diminish unisons.2")+    Shrink (Interval Dim  Second) = TypeError (Text "Can't diminish unisons.3")     Shrink (Interval Dim  Fifth)  = Interval Perf Fourth     Shrink (Interval Dim  Sixth)  = Interval Dim Fifth     Shrink (Interval Dim  is)     = Interval Min (IntSizePred is)@@ -323,7 +419,7 @@     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  Unison)  = TypeError (Text "Can't diminish unisons.4")     Expand (Interval Dim  Fourth)  = Interval Perf Fourth     Expand (Interval Dim  Fifth)   = Interval Perf Fifth     Expand (Interval Dim  Octave)  = Interval Perf Octave@@ -362,12 +458,27 @@     NatToPitch n = HalfStepUp (NatToPitch (n - 1))  -- | Greater than or equal to for pitches.-type family (p1 :: PitchType) <<=? (p2 :: PitchType) where+type family (p1 :: PitchType) <<=? (p2 :: PitchType) :: Bool where+    p <<=? p = True+    (Pitch pc1 acc oct) <<=? (Pitch pc2 acc oct) = ClassToNat pc1 <=? ClassToNat pc2+    (Pitch pc acc oct) <<=? (Pitch pc Sharp oct) = True+    (Pitch pc Sharp oct) <<=? (Pitch pc acc oct) = False+    (Pitch pc Flat oct) <<=? (Pitch pc acc oct) = True+    (Pitch pc acc oct) <<=? (Pitch pc Flat oct) = False+    (Pitch E Sharp oct) <<=? (Pitch F Flat oct) = False+    (Pitch F Flat oct) <<=? (Pitch E Sharp oct) = True+    (Pitch B Sharp oct) <<=? (Pitch C Flat oct') =+            If (NextOct oct oct') False ((Pitch B Natural oct) <<=? (Pitch C Flat oct'))+    (Pitch C Flat oct) <<=? (Pitch B Sharp oct') =+            If (NextOct oct' oct) True ((Pitch C Natural oct) <<=? (Pitch B Sharp oct'))+    (Pitch pc1 acc1 oct) <<=? (Pitch pc2 acc2 oct) = ClassToNat pc1 <=? ClassToNat pc2+    (Pitch pc1 acc1 oct1) <<=? (Pitch pc2 acc2 oct2) = OctToNat oct1 <=? OctToNat oct2     p1 <<=? p2 = PitchToNat p1 <=? PitchToNat p2  -- | Greater than for pitches. type family (p1 :: PitchType) <<? (p2 :: PitchType) where-    p1 <<? p2 = (p1 <<=? p2) .&&. Not (p1 .~. p2)+    p <<? p = False+    p1 <<? p2 = (p1 <<=? p2)  -- | Enharmonic equality of pitches. type family (p :: PitchType) =?= (q :: PitchType) :: Bool where@@ -430,6 +541,24 @@ type family OctPred (o :: OctaveNum) :: OctaveNum where     OctPred o = DecreaseOctave o 1 +-- | Returns True if the successor of o1 is o2.+type family NextOct (o1 :: OctaveNum) (o2 :: OctaveNum) :: Bool where+    NextOct Oct_1 Oct0 = True+    NextOct Oct0 Oct1 = True+    NextOct Oct1 Oct2 = True+    NextOct Oct2 Oct3 = True+    NextOct Oct3 Oct4 = True+    NextOct Oct4 Oct5 = True+    NextOct Oct5 Oct6 = True+    NextOct Oct6 Oct7 = True+    NextOct Oct7 Oct8 = True+    NextOct _    _    = False++-- | Returns i if o2 is after o2, otherwise returns Compound.+type family IntervalOrCompound (o1 :: OctaveNum) (o2 :: OctaveNum) (i :: IntervalType)+            :: IntervalType where+    IntervalOrCompound o1 o2 int = If (NextOct o1 o2) int Compound+ -- | Convert a pitch class to a natural number. type family ClassToNat (pc :: PitchClass) :: Nat where     ClassToNat C = 0@@ -608,6 +737,18 @@ type family RaiseAllByOct (ps :: Voice l) :: Voice l where     RaiseAllByOct v = RaiseAllBy v (Interval Perf Octave) +-- | Transpose a partiture up by the given interval.+type family TransposeUpBy (p :: Partiture n l) (i :: IntervalType) :: Partiture n l where+    TransposeUpBy _ Compound = TypeError (Text "Can't transpose by compound interval.")+    TransposeUpBy None i = None+    TransposeUpBy (v :-- vs) i = RaiseAllBy v i :-- TransposeUpBy vs i++-- | Transpose a partiture down by the given interval.+type family TransposeDownBy (p :: Partiture n l) (i :: IntervalType) :: Partiture n l where+    TransposeDownBy _ Compound = TypeError (Text "Can't transpose by compound interval.")+    TransposeDownBy None i = None+    TransposeDownBy (v :-- vs) i = LowerAllBy v i :-- TransposeDownBy vs i+ ------------------------------------------------------------------------------- -- Primitive instances -------------------------------------------------------------------------------@@ -643,6 +784,11 @@     prim p = prim (PC @pc) + prim (Acc @acc) + prim (Oct @oct)     pretty p = pretty (PC @pc) ++ pretty (Acc @acc) ++ pretty (Oct @oct) +instance (IntRep sd, IntRep acc, IntRep oct) => Primitive (Degree sd acc oct) where+    type Rep (Degree sd acc oct) = Int+    prim _ = prim (ScaDeg @sd) + prim (Acc @acc) + prim (Oct @oct)+    pretty _ = pretty (ScaDeg @sd) ++ 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@@ -664,17 +810,19 @@ 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+instance (IntRep pc, IntRep acc, BoolRep mo) => Primitive (Key pc acc mo) where+    type Rep (Key pc acc mo) = [Int]+    prim k = (+ (prim (PC @pc) + prim (Acc @acc))) <$> baseScale+        where baseScale = if (prim (Mod @ mo))+                            then [0, 2, 4, 5, 7, 9, 11]+                            else [0, 2, 3, 5, 7, 8, 10]     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+instance (IntRep p, RootToPitch (DegreeRoot k deg) ~ p, Primitive deg, Primitive k)+        => Primitive (DegreeRoot k deg) where+    type Rep (DegreeRoot k deg) = Int     prim r = prim (Pit @p)-    pretty r = pretty (ScaDeg @sd)+    pretty r = pretty (Deg @deg)  instance IntRep p => Primitive (PitchRoot p) where     type Rep (PitchRoot p) = Int@@ -696,3 +844,85 @@     pretty (natVal -> 32) = "Wh"     pretty (natVal -> 48) = "Wh."     pretty (natVal -> n) = ":" ++ show n++-- Intervals++---- Interval classes++instance Primitive Maj where+    type Rep Maj = Int -> Int+    prim _ = id+    pretty _ = "Maj"++instance Primitive Min where+    type Rep Min = Int -> Int+    prim _ = pred+    pretty _ = "Min"++instance Primitive Perf where+    type Rep Perf = Int -> Int+    prim _ = id+    pretty _ = "Perf"++instance Primitive Aug where+    type Rep Aug = Int -> Int+    prim _ = (+ 1)+    pretty _ = "Aug"++instance Primitive Dim where+    type Rep Dim = Int -> Int+    prim _ 2 = 0+    prim _ 4 = 2+    prim _ 5 = 4+    prim _ 7 = 6+    prim _ 9 = 7+    prim _ 11 = 9+    prim _ 12 = 11+    pretty _ = "Dim"++---- Interval sizes++instance Primitive Unison where+    type Rep Unison = Int+    prim _ = 0+    pretty _ = "1"++instance Primitive Second where+    type Rep Second = Int+    prim _ = 2+    pretty _ = "2"++instance Primitive Third where+    type Rep Third = Int+    prim _ = 4+    pretty _ = "3"++instance Primitive Fourth where+    type Rep Fourth = Int+    prim _ = 5+    pretty _ = "4"++instance Primitive Fifth where+    type Rep Fifth = Int+    prim _ = 7+    pretty _ = "5"++instance Primitive Sixth where+    type Rep Sixth = Int+    prim _ = 9+    pretty _ = "6"++instance Primitive Seventh where+    type Rep Seventh = Int+    prim _ = 11+    pretty _ = "7"++instance Primitive Octave where+    type Rep Octave = Int+    prim _ = 12+    pretty _ = "8"++instance (FunRep Int Int ic, IntRep is) => Primitive (Interval ic is) where+    type Rep (Interval ic is) = Int+    prim _ = prim (IC @ic) (prim (IS @ is))+    pretty _ = pretty (IC @ic) ++ " " ++ pretty (IS @is)

@@ -19,3 +19,4 @@ -- Uses import/export shortcut as suggested by HLint.  import Mezzo.Render.MIDI as X+import Mezzo.Render.Score as X

@@ -1,4 +1,4 @@-{-# LANGUAGE TypeInType, GADTs #-}+{-# LANGUAGE ScopedTypeVariables #-}  ----------------------------------------------------------------------------- -- |@@ -17,13 +17,18 @@ -----------------------------------------------------------------------------  module Mezzo.Render.MIDI-    ( renderMusic, musicToMidi )+    (renderScore, renderScores, withMusic, defScore )     where  import Mezzo.Model+import Mezzo.Compose (_th, _si, _ei, _qu, _ha, _wh)+import Mezzo.Render.Score+import Mezzo.Compose.Builder -import Codec.Midi +import Codec.Midi hiding (key, Key)+import qualified Codec.Midi as CM (key, Key)+ ------------------------------------------------------------------------------- -- Types -------------------------------------------------------------------------------@@ -42,6 +47,9 @@ -- | A sequence of MIDI events. type MidiTrack = Track Ticks +-- | A musical score.+type Score = MidiTrack+ ------------------------------------------------------------------------------- -- Operations -------------------------------------------------------------------------------@@ -55,62 +63,91 @@  -- | Start playing the specified 'MidiNote'. keyDown :: MidiNote -> MidiEvent-keyDown n = (start n, NoteOn {channel = 0, key = noteNum n, velocity = vel n})+keyDown n = (start n, NoteOn {channel = 0, CM.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})+keyUp n = (start n + noteDur n, NoteOn {channel = 0, CM.key = noteNum n, velocity = 0})  -- | Play the specified 'MidiNote'. playNote :: Int -> Ticks -> MidiTrack-playNote root dur = map ($ midiNote root dur) [keyDown, keyUp]+playNote root dur = map ($ midiNote root (dur * 60)) [keyDown, keyUp]  -- | Play a rest of the specified duration. playRest :: Ticks -> MidiTrack-playRest dur = map ($ midiRest dur) [keyDown, keyUp]+playRest dur = map ($ midiRest (dur * 60)) [keyDown, keyUp] +-- | Play the specified 'MidiNote'.+playTriplet :: [Int] -> Ticks -> MidiTrack+playTriplet ts dur = concatMap playShortNote ts+    where playShortNote root = map ($ midiNote root (dur * 40)) [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 ------------------------------------------------------------------------------- +-- | Title of a composition+type Title = String++-- | Convert a 'Music' piece into a 'MidiTrack'.+musicToMidi :: forall t k m r. Music (Sig :: Signature t k r) m -> Score+musicToMidi (m1 :|: m2) = musicToMidi m1 ++ musicToMidi m2+musicToMidi (m1 :-: m2) = musicToMidi m1 >< musicToMidi m2+musicToMidi (Note root dur) = playNote (prim root) (prim dur)+musicToMidi (Rest dur) = playRest (prim dur)+musicToMidi (Chord c d) = foldr1 (><) notes+    where notes = map (`playNote` prim d) $ prim c+musicToMidi (Progression p) = foldr1 (++) chords+    where chords = (toChords <$> init (prim p)) ++ [cadence (last (prim p))]+          toChords :: [Int] -> Score+          toChords = concat . replicate (prim (TimeSig @t)) . foldr1 (><) . map (`playNote` prim _qu)+          cadence :: [Int] -> Score+          cadence = foldr1 (><) . map (`playNote` prim _wh)+musicToMidi (Homophony m a) = musicToMidi m >< musicToMidi a+musicToMidi (Triplet d r1 r2 r3) = playTriplet [prim r1, prim r2, prim r3] (prim d)++-- | Sets the music content of the score.+withMusic :: ATerm (Music (Sig :: Signature t k r) m) (Attributes t k r) Score+withMusic atts m = [ (0, getTimeSig atts)+                    , (0, getKeySig atts)+                    , (0, TempoChange (60000000 `div` tempo atts))+                    ] ++ musicToMidi m++-- | Shorthand for quickly creating a score with the default attributes.+defScore :: Music (Sig :: Signature 4 (Key C Natural MajorMode) Classical) m -> Score+defScore = score withMusic+ -- | A basic skeleton of a MIDI file.-midiSkeleton :: MidiTrack -> Midi-midiSkeleton mel = Midi-    { fileType = MultiTrack+midiSkeleton :: Title -> Score -> Midi+midiSkeleton trName mel = Midi+    { fileType = SingleTrack     , timeDiv = TicksPerBeat 480     , tracks =         [ [ (0, ChannelPrefix 0)-          , (0, TrackName " Grand Piano  ")+          , (0, TrackName trName)           , (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+exportMidi :: FilePath -> Title -> Score -> IO ()+exportMidi f trName notes = do+    exportFile f $ midiSkeleton trName notes+    putStrLn $ "Composition rendered to " ++ f ++ "." --- | Create a MIDI file with the specified path and composition.-renderMusic :: FilePath -> Music m -> IO ()-renderMusic f m = createMidi f (musicToMidi m)++-- | Create a MIDI file with the specified path, title and score.+renderScore :: FilePath -> Title -> Score -> IO ()+renderScore f compTitle sc = exportMidi f compTitle sc+++-- | Create a MIDI file with the specified path, title and list of scores.+renderScores :: FilePath -> Title -> [Score] -> IO ()+renderScores f compTitle ts = renderScore f compTitle (concat ts)

@@ -0,0 +1,170 @@+{-# LANGUAGE RecordWildCards #-}++-----------------------------------------------------------------------------+-- |+-- Module      :  Mezzo.Render.Score+-- Description :  Score building+-- Copyright   :  (c) Dima Szamozvancev+-- License     :  MIT+--+-- Maintainer  :  ds709@cam.ac.uk+-- Stability   :  experimental+-- Portability :  portable+--+-- Combinators for building scores: 'Music' values with global composition+-- attributes such as tempo or key signature.+--+-----------------------------------------------------------------------------++module Mezzo.Render.Score+    ( -- * Scores and attributes+      Attributes (..)+    , defAttributes+    , getTimeSig+    , getKeySig+      -- * Score builders+    , score+    , section+    , setTempo+    , setTimeSig+    , setKeySig+    , setRuleSet+      -- * Rule sets+    , free+    , classical+    , strict+    )+    where++import Mezzo.Model+import Mezzo.Compose.Harmony+import Mezzo.Compose.Builder++import Codec.Midi hiding (key, Key)+import qualified Codec.Midi as CM (key, Key)+import qualified GHC.TypeLits as GT++-------------------------------------------------------------------------------+-- Attributes+-------------------------------------------------------------------------------++-- | Datatype containing MIDI attributes of a Mezzo composition.+data Attributes t k r =+    (Primitive t, Primitive k, ScoreAtt t, ScoreAtt k)+    => Attributes+    { title :: String               -- ^ The title of the composition.+    , tempo :: Tempo                -- ^ The tempo of the composition in BPM.+    , timeSignature :: TimeSig t    -- ^ The time signature of the composition.+    , keySignature :: KeyS k        -- ^ The key signature of the composition.+    , ruleSet :: r+    }++-- | Default attributes: "Composition" in C major in common time, with tempo 120 BPM.+defAttributes :: Attributes 4 (Key C Natural MajorMode) Classical+defAttributes = Attributes+    { title = "Composition"+    , tempo = 120+    , timeSignature = quadruple+    , keySignature = c_maj+    , ruleSet = classical+    }++-------------------------------------------------------------------------------+-- Builders+-------------------------------------------------------------------------------++-- Score attribute specifier: uses the default attributes.+score :: Spec (Attributes 4 (Key C Natural MajorMode) Classical)+score = spec defAttributes++-- | Sets the title of the composition.+section :: AMut String (Attributes t k r)+section atts titl = spec (atts {title = titl})++-- | Sets the tempo of the composition.+setTempo :: AMut Tempo (Attributes t k r)+setTempo atts temp = spec (atts {tempo = temp})++-- | Sets the time signature of the composition.+setTimeSig :: (Primitive t', ScoreAtt t') => AConv (TimeSig t') (Attributes t k r) (Attributes t' k r)+setTimeSig Attributes{..} ts = spec (Attributes title tempo ts keySignature ruleSet)++-- | Sets the key signature of the composition.+setKeySig :: (Primitive k', ScoreAtt k') => AConv (KeyS k') (Attributes t k r) (Attributes t k' r)+setKeySig Attributes{..} ks = spec (Attributes title tempo timeSignature ks ruleSet)++-- | Sets the key signature of the composition.+setRuleSet :: AConv r' (Attributes t k r) (Attributes t k r')+setRuleSet Attributes{..} rs = spec (Attributes title tempo timeSignature keySignature rs)+++-- | Get the time signature MIDI message.+getTimeSig :: Attributes t k r -> Message+getTimeSig Attributes{timeSignature = t} = getAtt t++-- | Get the key signature MIDI message.+getKeySig :: Attributes t k r -> Message+getKeySig Attributes{keySignature = k} = getAtt k++-------------------------------------------------------------------------------+-- Rule sets+-------------------------------------------------------------------------------++-- | No enforced rules.+free :: Free+free = Free++-- | Classical rules.+classical :: Classical+classical = Classical++-- | Strict rules+strict :: Strict+strict = Strict++++-- | Class for types that can be converted into score attribute MIDI messages.+class ScoreAtt a where+    -- | Get the MIDI message corresponding to a type-level attribute.+    getAtt :: proxy a -> Message++instance ScoreAtt 2 where getAtt t = TimeSignature 2 2 24 8+instance ScoreAtt 3 where getAtt t = TimeSignature 3 2 24 8+instance ScoreAtt 4 where getAtt t = TimeSignature 4 2 24 8++instance ScoreAtt (Key C Flat    MajorMode) where getAtt k = KeySignature (-7) 0+instance ScoreAtt (Key G Flat    MajorMode) where getAtt k = KeySignature (-6) 0+instance ScoreAtt (Key D Flat    MajorMode) where getAtt k = KeySignature (-5) 0+instance ScoreAtt (Key A Flat    MajorMode) where getAtt k = KeySignature (-4) 0+instance ScoreAtt (Key E Flat    MajorMode) where getAtt k = KeySignature (-3) 0+instance ScoreAtt (Key B Flat    MajorMode) where getAtt k = KeySignature (-2) 0+instance ScoreAtt (Key F Natural MajorMode) where getAtt k = KeySignature (-1) 0+instance ScoreAtt (Key C Natural MajorMode) where getAtt k = KeySignature  0 0+instance ScoreAtt (Key G Natural MajorMode) where getAtt k = KeySignature  1 0+instance ScoreAtt (Key D Natural MajorMode) where getAtt k = KeySignature  2 0+instance ScoreAtt (Key A Natural MajorMode) where getAtt k = KeySignature  3 0+instance ScoreAtt (Key E Natural MajorMode) where getAtt k = KeySignature  4 0+instance ScoreAtt (Key B Natural MajorMode) where getAtt k = KeySignature  5 0+instance ScoreAtt (Key F Sharp   MajorMode) where getAtt k = KeySignature  6 0+instance ScoreAtt (Key C Sharp   MajorMode) where getAtt k = KeySignature  7 0++instance ScoreAtt (Key A Flat    MinorMode) where getAtt k = KeySignature (-7) 1+instance ScoreAtt (Key E Flat    MinorMode) where getAtt k = KeySignature (-6) 1+instance ScoreAtt (Key B Flat    MinorMode) where getAtt k = KeySignature (-5) 1+instance ScoreAtt (Key F Natural MinorMode) where getAtt k = KeySignature (-4) 1+instance ScoreAtt (Key C Natural MinorMode) where getAtt k = KeySignature (-3) 1+instance ScoreAtt (Key G Natural MinorMode) where getAtt k = KeySignature (-2) 1+instance ScoreAtt (Key D Natural MinorMode) where getAtt k = KeySignature (-1) 1+instance ScoreAtt (Key A Natural MinorMode) where getAtt k = KeySignature  0 1+instance ScoreAtt (Key E Natural MinorMode) where getAtt k = KeySignature  1 1+instance ScoreAtt (Key B Natural MinorMode) where getAtt k = KeySignature  2 1+instance ScoreAtt (Key F Sharp   MinorMode) where getAtt k = KeySignature  3 1+instance ScoreAtt (Key C Sharp   MinorMode) where getAtt k = KeySignature  4 1+instance ScoreAtt (Key G Sharp   MinorMode) where getAtt k = KeySignature  5 1+instance ScoreAtt (Key D Sharp   MinorMode) where getAtt k = KeySignature  6 1+instance ScoreAtt (Key A Sharp   MinorMode) where getAtt k = KeySignature  7 1++instance {-# OVERLAPPABLE #-} GT.TypeError (GT.Text "The key signature is invalid.")+    => ScoreAtt (Key pc acc mode) where+    getAtt = undefined

@@ -1,5 +1,5 @@-{-# OPTIONS_GHC -fdefer-type-errors #-}--- {-# OPTIONS_GHC -w #-}+{-# OPTIONS_GHC -fdefer-type-errors  #-}+{-# OPTIONS_GHC -Wno-deferred-type-errors #-} {-# LANGUAGE TypeInType, TypeOperators, GADTs, MultiParamTypeClasses, FlexibleInstances #-}  module PrimSpec where@@ -8,127 +8,264 @@ import GHC.TypeLits import Control.Exception (evaluate) import Test.ShouldNotTypecheck (shouldNotTypecheck)+import TestUtils  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+            it "should replicate elements" $ do+                shouldTypecheck timesReplicate+                shouldNotTypecheck timesReplicate'+                shouldNotTypecheck timesReplicate'' +            it "should get the head of an optimised vector" $ do+                shouldTypecheck optVectorHead+                shouldNotTypecheck optVectorHead'++            it "should get the head of a vector" $ do+                shouldTypecheck vectorHead+                shouldNotTypecheck vectorHead'++            it "should get the last element of an optimised vector" $ do+                shouldTypecheck optVectorLast+                shouldNotTypecheck optVectorLast'++            it "should get the tail of a vector" $ do+                shouldTypecheck vectorTail+                shouldNotTypecheck vectorTail'+                shouldNotTypecheck vectorTail''++            it "should get the initial elements of a vector" $ do+                shouldTypecheck vectorInit+                shouldNotTypecheck vectorInit'+                shouldNotTypecheck vectorInit'++            it "should get the length of an optimised vector" $ do+                shouldTypecheck optVectorLength+                shouldNotTypecheck optVectorLength'++            it "should get the length of a vector" $ do+                shouldTypecheck vectorLength+                shouldNotTypecheck vectorLength'++            it "should append optimised vectors" $ do+                shouldTypecheck optVectorAppend+                shouldNotTypecheck optVectorAppend'+                shouldNotTypecheck optVectorAppend''++            it "should append vectors" $ do+                shouldTypecheck vectorAppend+                shouldNotTypecheck vectorAppend'+                shouldNotTypecheck vectorAppend''++            it "should add an element to the end of a vector" $ do+                shouldTypecheck snoc+                shouldNotTypecheck snoc'+                shouldNotTypecheck snoc''++            it "should repeat an element to an optimised vector" $ do+                shouldTypecheck repeatVec+                shouldNotTypecheck repeatVec'+                shouldNotTypecheck repeatVec''+         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+            it "should horizontally concatenate matrices" $ do+                shouldTypecheck matHConcatNorm+                shouldNotTypecheck matHConcatNorm'+                shouldNotTypecheck matHConcatNorm''+                shouldTypecheck matHConcatRE+                shouldNotTypecheck matHConcatRE'+                shouldTypecheck matHConcatLE+                shouldNotTypecheck matHConcatLE'+                -- shouldTypecheck matHConcatBE +            it "should vertically concatenate matrices" $ do+                shouldTypecheck matVConcat+            it "should vertically align matrices" $ do+                shouldTypecheck align+            it "should convert vectors to column matrices" $ do+                shouldTypecheck vecToColMatrix+         describe "Arithmetic operations" $ do             it "should calculate maximum of two numbers" $ do-                maxNat `shouldBe` True+                shouldTypecheck maxNat             it "should calculate minimum of two numbers" $ do-                minNat `shouldBe` True+                shouldTypecheck minNat          describe "Constraint operations" $ do             it "should apply a constraint to an optimised vector" $ do-                allSatisfy `shouldBe` True+                shouldTypecheck allSatisfy                 -- shouldNotTypecheck allSatisfyInv             it "should apply a binary constraint to two optimised vectors" $ do-                allPairsSatisfy `shouldBe` True+                shouldTypecheck allPairsSatisfy                 shouldNotTypecheck allPairsSatisfyInv             it "should apply a binary constraint to two vectors" $ do-                allPairsSatisfy' `shouldBe` True+                shouldTypecheck allPairsSatisfy'                 shouldNotTypecheck allPairsSatisfyInv'             it "should apply all constraints to a value" $ do-                satisfiesAll `shouldBe` True+                shouldTypecheck satisfiesAll                 -- shouldNotTypecheck satisfiesAllInv             it "should apply all constraints to all values" $ do-                allSatisfyAll `shouldBe` True+                shouldTypecheck allSatisfyAll                 -- shouldNotTypecheck allSatisfyAllInv +---------------------+-- Vector operations+--------------------- -timesReplicate :: (True ** 23) ~ (True :* (T :: Times 23)) => Bool-timesReplicate = True+timesReplicate :: (True ** 23) :~: (True :* (T :: Times 23))+timesReplicate = Refl+timesReplicate' :: (True ** 23) :~: (False :* (T :: Times 23))+timesReplicate' = Refl+timesReplicate'' :: (True ** 23) :~: (True :* (T :: Times 13))+timesReplicate'' = Refl -optVectorHead :: (Head (True ** 4 :- End)) ~ True => Bool-optVectorHead = True+optVectorHead :: (Head (True ** 4 :- End)) :~: True+optVectorHead = Refl+optVectorHead' :: (Head (True ** 4 :- End)) :~: False+optVectorHead' = Refl -vectorHead :: (Head' (True :-- None)) ~ True => Bool-vectorHead = True+vectorHead :: (Head' (True :-- None)) :~: True+vectorHead = Refl+vectorHead' :: (Head' (True :-- None)) :~: False+vectorHead' = Refl -optVectorLast :: (Last (True ** 4 :- False ** 9 :- End)) ~ False => Bool-optVectorLast = True+optVectorLast :: (Last (True ** 4 :- False ** 9 :- End)) :~: False+optVectorLast = Refl+optVectorLast' :: (Last (True ** 4 :- False ** 9 :- End)) :~: True+optVectorLast' = Refl -vectorTail :: (Tail' (True :-- False :-- None)) ~ (False :-- None) => Bool-vectorTail = True+vectorTail :: (Tail' (True :-- False  :-- True :-- None)) :~: (False :-- True :-- None)+vectorTail = Refl+vectorTail' :: (Tail' (True :-- False  :-- True :-- None)) :~: (False :-- False :-- None)+vectorTail' = Refl+vectorTail'' :: (Tail' (True :-- False  :-- True :-- None)) :~: (False :-- None)+vectorTail'' = Refl -vectorInit :: (Init' (True :-- False :-- None)) ~ (True :-- None) => Bool-vectorInit = True+vectorInit :: (Init' (True :-- False  :-- True :-- None)) :~: (True :-- False :-- None)+vectorInit = Refl+vectorInit' :: (Init' (True :-- False  :-- True :-- None)) :~: (False :-- False :-- None)+vectorInit' = Refl+vectorInit'' :: (Init' (True :-- False  :-- True :-- None)) :~: (False :-- None)+vectorInit'' = Refl -optVectorLength :: (Length (True ** 4 :- False ** 9 :- End)) ~ 13 => Bool-optVectorLength = True+optVectorLength :: (Length (True ** 4 :- False ** 9 :- End)) :~: 13+optVectorLength = Refl+optVectorLength' :: (Length (True ** 4 :- False ** 9 :- End)) :~: 6+optVectorLength' = Refl -vectorLength :: (Length' (True :-- False :-- None)) ~ 2 => Bool-vectorLength = True+vectorLength :: (Length' (True :-- False :-- None)) :~: 2+vectorLength = Refl+vectorLength' :: (Length' (True :-- False :-- None)) :~: 5+vectorLength' = Refl  optVectorAppend :: ((True ** 5 :- False ** 2 :- End) ++ End ++ (False ** 9 :- End))-                  ~ (True ** 5 :- False ** 2 :- False ** 9 :- End) => Bool-optVectorAppend = True+                :~: (True ** 5 :- False ** 2 :- False ** 9 :- End)+optVectorAppend = Refl+optVectorAppend' :: ((True ** 5 :- False ** 2 :- End) ++ End ++ (False ** 9 :- End))+                 :~: (True ** 5 :- True ** 2 :- False ** 9 :- End)+optVectorAppend' = Refl+optVectorAppend'' :: ((True ** 5 :- False ** 2 :- End) ++ End ++ (False ** 9 :- End))+                  :~: (True ** 5 :- False ** 1 :- False ** 9 :- End)+optVectorAppend'' = Refl+optVectorAppend''' :: ((True ** 5 :- False ** 2 :- End) ++ End ++ (False ** 9 :- End))+                   :~: (True ** 5 :- False ** 11 :- End)+optVectorAppend''' = Refl  vectorAppend :: ((2 :-- 43 :-- None) ++. None ++. (6 :-- None))-                  ~ (2 :-- 43 :-- 6 :-- None) => Bool-vectorAppend = True+             :~: (2 :-- 43 :-- 6 :-- None)+vectorAppend = Refl+vectorAppend' :: ((2 :-- 43 :-- None) ++. None ++. (6 :-- None))+              :~: (2 :-- 43 :-- 1 :-- None)+vectorAppend' = Refl+vectorAppend'' :: ((2 :-- 43 :-- None) ++. None ++. (6 :-- None))+               :~: (2 :-- 1 :-- None)+vectorAppend'' = Refl -snoc :: ((2 :-- 5 :-- None) :-| 6) ~ (2 :-- 5 :-- 6 :-- None) => Bool-snoc = True+snoc :: ((2 :-- 5 :-- None) :-| 6) :~: (2 :-- 5 :-- 6 :-- None)+snoc = Refl+snoc' :: ((2 :-- 5 :-- None) :-| 2) :~: (2 :-- 5 :-- 6 :-- None)+snoc' = Refl+snoc'' :: ((2 :-- 5 :-- None) :-| 2) :~: (2 :-- 4 :-- 5 :-- 6 :-- None)+snoc'' = Refl -repeatVec :: (True +*+ 3) ~ (True ** 3 :- End) => Bool-repeatVec = True+repeatVec :: (True +*+ 3) :~: (True ** 3 :- End)+repeatVec = Refl+repeatVec' :: (True +*+ 3) :~: (False ** 3 :- End)+repeatVec' = Refl+repeatVec'' :: (True +*+ 3) :~: (True ** 2 :- End)+repeatVec'' = Refl -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+---------------------+-- Matrix operations+---------------------+-- Harmonic concatenation++matHConcatNorm :: ((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))+matHConcatNorm = Refl+matHConcatNorm' :: ((True ** 2 :- End :-- False ** 2 :- End :-- None)+               +|+ (False ** 5 :- End :-- False ** 5 :- End :-- None))+            :~: ((True ** 2 :- False ** 5 :- End :-- False ** 2 :- True ** 5 :- End :-- None))+matHConcatNorm' = Refl+matHConcatNorm'' :: ((True ** 2 :- End :-- False ** 2 :- End :-- None)+              +|+ (False ** 5 :- End :-- True ** 5 :- End :-- None))+            :~: ((True ** 5 :- False ** 2 :- End :-- False ** 2 :- True ** 5 :- End :-- None))+matHConcatNorm'' = Refl++matHConcatRE :: ((True ** 2 :- End :-- False ** 2 :- End :-- None)+             +|+ (End :-- End :-- None))+            :~: (True ** 2 :- End :-- False ** 2 :- End :-- None)+matHConcatRE = Refl+matHConcatRE' :: ((True ** 2 :- End :-- False ** 2 :- End :-- None)+              +|+ (End :-- End :-- None))+            :~: (True ** 2 :- End :-- True ** 2 :- End :-- None)+matHConcatRE' = Refl++matHConcatLE :: ((True ** 2 :- End :-- False ** 2 :- End :-- None)+             +|+ (End :-- End :-- None))+            :~: (True ** 2 :- End :-- False ** 2 :- End :-- None)+matHConcatLE = Refl+matHConcatLE' :: ((True ** 2 :- End :-- False ** 2 :- End :-- None)+              +|+ (End :-- End :-- None))+            :~: (True ** 2 :- End :-- True ** 2 :- End :-- None)+matHConcatLE' = Refl++matHConcatBE :: ((None :: Matrix t 0 0) +|+ None) :~: None+matHConcatBE = Refl++-- Vertical concatenation+matVConcatNF :: ((True ** 3 :- False ** 6 :- End :-- None)+             +-+ (False ** 3 :- True ** 6 :- End :-- None))+        :~: (True ** 3 :- False ** 6 :- End :-- False ** 3 :- True ** 6 :- End :-- None)+matVConcatNF = Refl+matVConcatNF' :: ((True ** 3 :- False ** 6 :- End :-- None)+              +-+ (False ** 3 :- True ** 6 :- End :-- None))+        :~: (True ** 3 :- False ** 6 :- End :-- True ** 3 :- True ** 6 :- End :-- None)+matVConcatNF' = Refl+matVConcatNF'' :: ((True ** 3 :- False ** 6 :- End :-- None)+             +-+ (False ** 3 :- True ** 6 :- End :-- None))+        :~: (True ** 2 :- False ** 7 :- End :-- False ** 3 :- True ** 6 :- End :-- None)+matVConcatNF'' = Refl++matVConcatTF :: ((True ** 9 :- End :-- None)+             +-+ (False ** 3 :- True ** 6 :- End :-- None))+        :~: (True ** 3 :- True ** 6 :- End :-- False ** 3 :- True ** 6 :- End :-- None)+matVConcatTF = Refl+matVConcatTF' :: ((True ** 9 :- End :-- None)+             +-+ (False ** 3 :- True ** 6 :- End :-- None))+        :~: (True ** 3 :- True ** 6 :- End :-- True ** 3 :- True ** 6 :- End :-- None)+matVConcatTF' = Refl+matVConcatTF'' :: ((True ** 9 :- End :-- None)+             +-+ (False ** 3 :- True ** 6 :- End :-- None))+        :~: (True ** 3 :- True ** 6 :- End :-- False ** 2 :- True ** 7 :- End :-- None)+matVConcatTF'' = Refl+  align ::           -- Right fragment

@@ -0,0 +1,30 @@+{-# LANGUAGE TypeInType, RankNTypes, GADTs, TypeOperators #-}++-- Opposite of the 'shouldNotTypecheck' function from+-- https://github.com/CRogers/should-not-typecheck+--++module TestUtils where++import Control.DeepSeq (force, NFData (..))+import Control.Exception (evaluate, try, TypeError (..))+import Test.HUnit.Lang (Assertion, assertFailure)++-- | Hetero-kinded propositional type equality.+-- If the type (a :~: b) is inhabited by Refl, a and b must be equal+data (a :: k1) :~: (b :: k2) where+  Refl :: a :~: a++-- | Instance which makes+instance NFData (a :~: b) where+    rnf Refl = ()++-- | Takes one argument, an expression that should  typecheck.+-- It will fail the test if the expression does not typecheck.+-- Requires Deferred Type Errors to be enabled for the file it is called in.+shouldTypecheck :: NFData a => (() ~ () => a) -> Assertion+shouldTypecheck a = do+  result <- try (evaluate $ force a)+  case result of+    Right _ -> return ()+    Left (TypeError msg) -> assertFailure $ "Expected expression to compile but it did not compile: \n" ++ msg

@@ -9,32 +9,40 @@ import Control.Exception (evaluate) import Data.Proxy import Test.ShouldNotTypecheck (shouldNotTypecheck)+import TestUtils  import Mezzo.Model.Types+import Mezzo.Model.Prim+import Mezzo.Model.Harmony  typeSpec :: Spec typeSpec =     describe "Mezzo.Model.Types" $ do         describe "Harmonic types" $ do             it "should convert roots to pitches" $ do-                rootToPitch `shouldBe` True+                shouldTypecheck rootToPitch                 shouldNotTypecheck rootToPitchInv             it "should sharpen roots" $ do-                sharpen `shouldBe` True+                shouldTypecheck sharpen                 shouldNotTypecheck sharpenInv             it "should flatten roots" $ do-                flatten `shouldBe` True+                shouldTypecheck flatten                 shouldNotTypecheck flattenInv             it "should make intervals" $ do-                flatten `shouldBe` True+                shouldTypecheck makeInterval+            it "should shift pitches by an interval" $+                shouldTypecheck shift+        describe "Chords" $ do+            it "should convert chords to Music" $+                shouldTypecheck fromChord  rootToPitch ::         ( (RootToPitch (PitchRoot (Pitch C Natural Oct3)) ~ (Pitch C Natural Oct3))-        , (RootToPitch (DegreeRoot (Key D Flat MinorMode) IV) ~ (Pitch F Sharp Oct2))+        , (RootToPitch (DegreeRoot (Key D Flat MinorMode) (Degree IV Natural Oct2)) ~ (Pitch F Sharp Oct2))         ) => Bool rootToPitch = True -rootToPitchInv :: Proxy (RootToPitch (DegreeRoot (Key D Flat MinorMode) IV))+rootToPitchInv :: Proxy (RootToPitch (DegreeRoot (Key D Flat MinorMode) (Degree IV Natural Oct2)))                -> Proxy (Pitch E Natural Oct2) rootToPitchInv = id @@ -42,12 +50,12 @@            , (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))+           , (Sharpen (DegreeRoot (Key F Sharp MinorMode) (Degree VI Natural Oct3))) ~ (PitchRoot (Pitch D Sharp Oct4))+           , (Sharpen (DegreeRoot (Key E Sharp MajorMode) (Degree VII Natural Oct3))) ~ (PitchRoot (Pitch F Natural Oct4))            ) => Bool sharpen = True -sharpenInv :: Proxy '(Sharpen (PitchRoot (Pitch B Flat Oct5)), Sharpen (DegreeRoot (Key C Flat MajorMode) IV))+sharpenInv :: Proxy '(Sharpen (PitchRoot (Pitch B Flat Oct5)), Sharpen (DegreeRoot (Key C Flat MajorMode) (Degree IV Natural Oct3)))            -> Proxy '(PitchRoot (Pitch C Flat Oct6), PitchRoot (Pitch F Natural Oct3)) sharpenInv = id @@ -55,12 +63,12 @@            , (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))+           , (Flatten (DegreeRoot (Key F Sharp MinorMode) (Degree VI Natural Oct3))) ~ (PitchRoot (Pitch D Flat Oct4))+           , (Flatten (DegreeRoot (Key E Sharp MajorMode) (Degree VII Natural Oct3))) ~ (PitchRoot (Pitch E Flat Oct4))            ) => Bool flatten = True -flattenInv :: Proxy '(Flatten (PitchRoot (Pitch C Sharp Oct5)), Flatten (DegreeRoot (Key C Flat MajorMode) V))+flattenInv :: Proxy '(Flatten (PitchRoot (Pitch C Sharp Oct5)), Flatten (DegreeRoot (Key C Flat MajorMode) (Degree V Natural Oct3)))            -> Proxy '(PitchRoot (Pitch B Sharp Oct4), PitchRoot (Pitch E Natural Oct3)) flattenInv = id @@ -69,11 +77,74 @@             , (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 Natural Oct3) (Pitch F Flat Oct3)) ~ (Interval Dim Second)             , (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 F Sharp Oct3) (Pitch G Flat Oct3)) ~ (Interval Dim Second)             , (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)+            , (MakeInterval (Pitch C Natural Oct3) (Pitch F Sharp Oct3)) ~ (Interval Aug Fourth)+            , (MakeInterval (Pitch C Natural Oct3) (Pitch G Flat Oct3)) ~ (Interval Dim Fifth)+            , (MakeInterval (Pitch D Natural Oct3) (Pitch B Flat Oct3)) ~ (Interval Min Sixth)+            -- , (MakeInterval (Pitch D Natural Oct3) (Pitch A Sharp Oct3)) ~ (Interval Aug Fifth)+            , (MakeInterval (Pitch F Sharp Oct3) (Pitch A Natural Oct3)) ~ (Interval Min Third)+            -- , (MakeInterval (Pitch G Flat Oct3) (Pitch A Natural Oct3)) ~ (Interval Aug Second)+            , (MakeInterval (Pitch C Sharp Oct3) (Pitch B Natural Oct3)) ~ (Interval Min Seventh)+            -- , (MakeInterval (Pitch D Flat Oct3) (Pitch B Natural Oct3)) ~ (Interval Aug Sixth)+            -- , (MakeInterval (Pitch B Natural Oct3) (Pitch D Flat Oct3)) ~ (Interval Aug Sixth)+            -- , (MakeInterval (Pitch C Sharp Oct3) (Pitch C Flat Oct4)) ~ (Interval Dim Octave)+            , (MakeInterval (Pitch G Sharp Oct3) (Pitch E Natural Oct4)) ~ (Interval Min Sixth)+            -- , (MakeInterval (Pitch A Flat Oct3) (Pitch E Natural Oct4)) ~ (Interval Aug Fifth)+            , (MakeInterval (Pitch A Flat Oct3) (Pitch F Flat Oct4)) ~ (Interval Min Sixth)             ) => Bool makeInterval = True++shift ::+            ( (RaiseBy (Pitch C Natural Oct3) (Interval Maj Third) ~ (Pitch E Natural Oct3))+            , (LowerBy (Pitch E Natural Oct3) (Interval Maj Third)) ~ (Pitch C Natural Oct3)+            , (RaiseBy (Pitch C Natural Oct3) (Interval Min Seventh)) ~ (Pitch B Flat Oct3)+            , (RaiseBy (Pitch E Sharp Oct3) (Interval Perf Unison)) ~ (Pitch E Sharp Oct3)+            , (RaiseBy (Pitch E Natural Oct3) (Interval Min Second)) ~ (Pitch F Natural Oct3)+            , (LowerBy (Pitch F Natural Oct3) (Interval Min Second)) ~ (Pitch E Natural Oct3)+            , (RaiseBy (Pitch C Natural Oct3) (Interval Perf Octave)) ~ (Pitch C Natural Oct4)+            , (LowerBy (Pitch C Natural Oct4) (Interval Perf Octave)) ~ (Pitch C Natural Oct3)+            , (RaiseBy (Pitch E Sharp Oct3) (Interval Maj Seventh)) ~ (Pitch E Natural Oct4)+            , (RaiseBy (Pitch C Natural Oct3) (Interval Aug Fourth)) ~ (Pitch F Sharp Oct3)+            , (LowerBy (Pitch F Natural Oct4) (Interval Aug Fourth)) ~ (Pitch B Natural Oct3)+            , (RaiseBy (Pitch C Natural Oct3) (Interval Dim Fifth)) ~ (Pitch G Flat Oct3)+            , (LowerBy (Pitch F Natural Oct4) (Interval Dim Fifth)) ~ (Pitch B Natural Oct3)+            ) => Bool+shift = True+++fromChord ::+            ( (FromChord (Triad (PitchRoot (Pitch C Natural Oct4)) MajTriad Inv0) 8)+                ~ ( Pitch G Natural Oct4 ** 8 :- End+                :-- Pitch E Natural Oct4 ** 8 :- End+                :-- Pitch C Natural Oct4 ** 8 :- End :-- None)+            , (FromChord (Triad (PitchRoot (Pitch A Flat Oct4)) DimTriad Inv2) 8)+                ~ ( Pitch B Natural Oct5 ** 8 :- End+                :-- Pitch G Sharp Oct5 ** 8 :- End+                :-- Pitch D Natural Oct5 ** 8 :- End :-- None)+            , (FromChord (Tetrad (PitchRoot (Pitch G Natural Oct4)) MajMinSeventh Inv0) 8)+                ~ ( Pitch F Natural Oct5 ** 8 :- End+                :-- Pitch D Natural Oct5 ** 8 :- End+                :-- Pitch B Natural Oct4 ** 8 :- End+                :-- Pitch G Natural Oct4 ** 8 :- End :-- None)+            , (FromChord (Tetrad (PitchRoot (Pitch B Sharp Oct3)) HalfDimSeventh Inv3) 8)+                ~ ( Pitch F Sharp Oct5 ** 8 :- End+                :-- Pitch D Sharp Oct5 ** 8 :- End+                :-- Pitch C Natural Oct5 ** 8 :- End+                :-- Pitch B Flat Oct4 ** 8 :- End :-- None)+            , (FromChord (Tetrad (PitchRoot (Pitch C Natural Oct4)) (DoubledT MajTriad) Inv0) 8)+                ~ ( Pitch C Natural Oct5 ** 8 :- End+                :-- Pitch G Natural Oct4 ** 8 :- End+                :-- Pitch E Natural Oct4 ** 8 :- End+                :-- Pitch C Natural Oct4 ** 8 :- End :-- None)+            , (FromChord (Tetrad (PitchRoot (Pitch C Sharp Oct4)) (DoubledT AugTriad) Inv1) 8)+                ~ ( Pitch F Natural Oct5 ** 8 :- End+                :-- Pitch C Sharp Oct5 ** 8 :- End+                :-- Pitch A Natural Oct4 ** 8 :- End+                :-- Pitch F Natural Oct4 ** 8 :- End :-- None)+            ) => Bool+fromChord = True