Mezzo.Model.Prim

Primitive types that make up the base for the Mezzo type model.

Vectors and matrices

data Vector :: Type -> Nat -> Type where

Simple length-indexed vector.

Constructors

None :: Vector t 0

(:--) :: t -> Vector t (n - 1) -> Vector t n infixr 5

Instances

(ValidHomConcat ((-) n1 1) n2 l ((,) (Partiture ((-) n1 1) l) (Partiture n2 l) vs us), AllSatisfyAll n2 (Voice l) ((:) (Voice l -> Constraint) (ValidHarmDyadsInVectors l v) ([] (Voice l -> Constraint))) us) => ValidHomConcat n1 n2 l ((,) (Vector (Voice l) n1) (Partiture n2 l) ((:--) (Voice l) n1 v vs) us)

ValidHomConcat 0 n2 l ((,) (Vector (OptVector PitchType l) 0) (Partiture n2 l) (None (OptVector PitchType l)) vs)

(ValidHarmConcat ((-) n1 1) n2 l ((,) (Partiture ((-) n1 1) l) (Partiture n2 l) vs us), AllSatisfyAll n2 (Voice l) ((:) (Voice l -> Constraint) (ValidHarmDyadsInVectors l v) ((:) (Voice l -> Constraint) (ValidHarmMotionInVectors l l v) ([] (Voice l -> Constraint)))) us) => ValidHarmConcat n1 n2 l ((,) (Vector (Voice l) n1) (Partiture n2 l) ((:--) (Voice l) n1 v vs) us)

ValidHarmConcat 0 n2 l ((,) (Vector (OptVector PitchType l) 0) (Partiture n2 l) (None (OptVector PitchType l)) vs)

data Times n where

Singleton type for the number of repetitions of an element.

Constructors

T :: Times n

data Elem :: Type -> Nat -> Type where

An element of a "run-length encoded" vector, containing the value and the number of repetitions

Constructors

(:*) :: t -> Times n -> Elem t n infixr 7

type family (v :: t) ** (d :: Nat) :: Elem t d where ... infixr 7

Replicate a value the specified number of times to create a new Elem.

Equations

v ** d = v :* (T :: Times d)

data OptVector :: Type -> Nat -> Type where

A length-indexed vector, optimised for repetitions.

Constructors

End :: OptVector t 0

(:-) :: Elem t l -> OptVector t (n - l) -> OptVector t n infixr 6

Instances

ValidMelConcat l2 0 l1 (None (OptVector PitchType l1)) (None (OptVector PitchType l2))

ValidMelMatrixMotion l2 0 l1 (None (OptVector PitchType l1)) (None (OptVector PitchType l2))

ValidMelConcatStrict l2 0 l1 (None (OptVector PitchType l1)) (None (OptVector PitchType l2))

(ValidHomConcat ((-) n1 1) n2 l ((,) (Partiture ((-) n1 1) l) (Partiture n2 l) vs us), AllSatisfyAll n2 (Voice l) ((:) (Voice l -> Constraint) (ValidHarmDyadsInVectors l v) ([] (Voice l -> Constraint))) us) => ValidHomConcat n1 n2 l ((,) (Vector (Voice l) n1) (Partiture n2 l) ((:--) (Voice l) n1 v vs) us)

ValidHomConcat 0 n2 l ((,) (Vector (OptVector PitchType l) 0) (Partiture n2 l) (None (OptVector PitchType l)) vs)

(ValidHarmConcat ((-) n1 1) n2 l ((,) (Partiture ((-) n1 1) l) (Partiture n2 l) vs us), AllSatisfyAll n2 (Voice l) ((:) (Voice l -> Constraint) (ValidHarmDyadsInVectors l v) ((:) (Voice l -> Constraint) (ValidHarmMotionInVectors l l v) ([] (Voice l -> Constraint)))) us) => ValidHarmConcat n1 n2 l ((,) (Vector (Voice l) n1) (Partiture n2 l) ((:--) (Voice l) n1 v vs) us)

ValidHarmConcat 0 n2 l ((,) (Vector (OptVector PitchType l) 0) (Partiture n2 l) (None (OptVector PitchType l)) vs)

(ValidMelAppend l2 l1 v1 v2, ValidMelConcat l2 ((-) n 1) l1 vs1 vs2) => ValidMelConcat l2 n l1 ((:--) (Voice l1) n v1 vs1) ((:--) (Voice l2) n v2 vs2)

(ValidMelMatrixMotion l2 ((-) n 1) l1 vs1 vs2, AllPairsSatisfy' ((-) n 1) (Voice l2) (Voice l1) (ValidMelPitchVectorMotion l2 l1 (Last PitchType l1 v1) (Head PitchType l2 v2)) vs1 vs2) => ValidMelMatrixMotion l2 n l1 ((:--) (OptVector PitchType l1) n v1 vs1) ((:--) (OptVector PitchType l2) n v2 vs2)

(ValidMelAppendStrict l2 l1 v1 v2, ValidMelConcatStrict l2 ((-) n 1) l1 vs1 vs2) => ValidMelConcatStrict l2 n l1 ((:--) (Voice l1) n v1 vs1) ((:--) (Voice l2) n v2 vs2)

type family Head (v :: OptVector t n) :: t where ...

Get the first element of an optimised vector.

Equations

Head End = TypeError (Text "Vector has no head element.")

Head ((v :* _) :- _) = v

type family Head' (v :: Vector t n) :: t where ...

Get the first element of a simple vector.

Equations

Head' None = TypeError (Text "Vector has no head element.")

Head' (v :-- _) = v

type family Last (v :: OptVector t n) :: t where ...

Get the last element of the vector.

Equations

Last End = TypeError (Text "Vector has no last element.")

Last ((v :* _) :- End) = v

Last (_ :- vs) = Last vs

type family Tail' (v :: Vector t n) :: Vector t (n - 1) where ...

Get the tail of the vector.

Equations

Tail' None = TypeError (Text "Vector has no tail.")

Tail' (_ :-- vs) = vs

type family Init' (v :: Vector t n) :: Vector t (n - 1) where ...

Get everything but the last element of the vector.

Equations

Init' None = TypeError (Text "Vector is empty.")

Init' (p :-- None) = None

Init' (p :-- ps) = p :-- Init' ps

type family Length (v :: OptVector t n) :: Nat where ...

Get the length of an optimised vector.

Equations

Length (v :: OptVector t n) = n

type family Length' (v :: Vector t n) :: Nat where ...

Get the length of a vector.

Equations

Length' (v :: Vector t n) = n

type Matrix t p q = Vector (OptVector t q) p

A dimension-indexed matrix.

type family (x :: OptVector t n) ++ (y :: OptVector t m) :: OptVector t (n + m) where ... infixl 4

Append two optimised vectors.

Equations

ys ++ End = ys

End ++ ys = ys

(x :- xs) ++ ys = x :- (xs ++ ys)

type family (x :: Vector t n) ++. (y :: Vector t m) :: Vector t (n + m) where ...

Append two simple vectors.

Equations

None ++. ys = ys

(x :-- xs) ++. ys = x :-- (xs ++. ys)

type family (v :: Vector t n) :-| (e :: t) :: Vector t (n + 1) where ...

Add an element to the end of a simple vector.

Equations

v :-| e = v ++. (e :-- None)

type family (a :: t) +*+ (n :: Nat) :: OptVector t n where ... infixl 4

Repeat the value the specified number of times to create a new OptVector.

Equations

x +*+ 0 = End

x +*+ n = (x ** n) :- End

type family (a :: Matrix t p q) +|+ (b :: Matrix t p r) :: Matrix t p (q + r) where ... infixl 4

Horizontal concatenation of type-level matrices. Places the first matrix to the left of the second.

Equations

None +|+ None = None

(r1 :-- rs1) +|+ (r2 :-- rs2) = (r1 ++ r2) :-- (rs1 +|+ rs2)

type family (a :: Matrix t p r) +-+ (b :: Matrix t q r) :: Matrix t (p + q) r where ... infixl 4

Vertical concatenation of type-level matrices. Places the first matrix on top of the second.

Equations

m1 +-+ m2 = ConcatPair (Align m1 m2)

type family Align (a :: Matrix t p r) (b :: Matrix t q r) :: (Matrix t p r, Matrix t q r) where ...

Vertically aligns two matrices by separating elements so that the element boundaries line up.

Equations

Align None m = '(None, m)

Align m None = '(m, None)

Align (r1 :-- rs1) (r2 :-- rs2) = '(FragmentMatByVec (r1 :-- rs1) r2, FragmentMatByVec (r2 :-- rs2) r1)

type family VectorToColMatrix (v :: Vector t n) (l :: Nat) :: Matrix t n l where ...

Convert a simple vector to a column matrix.

Equations

VectorToColMatrix None _ = None

VectorToColMatrix (v :-- vs) l = VectorToColMatrix vs l ++. (((v ** l) :- End) :-- None)

Logic and arithmetic

type family If (b :: Bool) (t :: k) (e :: k) :: k where ...

Conditional expression at the type level.

Equations

If True t e = t

If False t e = e

type family Not (a :: Bool) :: Bool where ...

Negation of type-level Booleans.

Equations

Not True = False

Not False = True

type family (b1 :: Bool) .&&. (b2 :: Bool) :: Bool where ... infixl 3

Conjunction of type-level Booleans.

Equations

b1 .&&. b2 = If b1 b2 False

type family (b1 :: Bool) .||. (b2 :: Bool) :: Bool where ... infixl 3

Disjunction of type-level Booleans.

Equations

b1 .||. b2 = If b1 True b2

type family (a :: k) .~. (b :: k) :: Bool where ... infixl 5

Equality of types.

Equations

a .~. a = True

a .~. b = False

type family MaxN (n1 :: Nat) (n2 :: Nat) :: Nat where ...

Returns the maximum of two natural numbers.

Equations

MaxN 0 n2 = n2

MaxN n1 0 = n1

MaxN n n = n

MaxN n1 n2 = If (n1 <=? n2) n2 n1

type family MinN (n1 :: Nat) (n2 :: Nat) :: Nat where ...

Returns the minimum of two natural numbers.

Equations

MinN 0 n2 = 0

MinN n1 0 = 0

MinN n n = n

MinN n1 n2 = If (n1 <=? n2) n1 n2

Constraints

type Valid = (() :: Constraint)

Valid base constraint.

type Invalid = True ~ False

Invalid base constraint.

type family AllSatisfy (c :: a -> Constraint) (xs :: OptVector a n) :: Constraint where ...

Create a new constraint which is valid only if every element in the given vector satisfies the given unary constraint. Analogue of map for constraints and vectors.

Equations

AllSatisfy c End = Valid

AllSatisfy c ((x :* _) :- xs) = (c x, AllSatisfy c xs)

type family AllPairsSatisfy (c :: a -> b -> Constraint) (xs :: OptVector a n) (ys :: OptVector b n) :: Constraint where ...

Create a new constraint which is valid only if every pair of elements in the given optimised vectors satisfy the given binary constraint. Analogue of zipWith for constraints and optimised vectors.

Equations

AllPairsSatisfy c End End = Valid

AllPairsSatisfy c ((x :* _) :- xs) ((y :* _) :- ys) = (c x y, AllPairsSatisfy c xs ys)

type family AllPairsSatisfy' (c :: a -> b -> Constraint) (xs :: Vector a n) (ys :: Vector b n) :: Constraint where ...

Create a new constraint which is valid only if every pair of elements in the given vectors satisfy the given binary constraint. Analogue of zipWith for constraints and vectors.

Equations

AllPairsSatisfy' c None None = Valid

AllPairsSatisfy' c (x :-- xs) (y :-- ys) = (c x y, AllPairsSatisfy' c xs ys)

type family SatisfiesAll (cs :: [a -> Constraint]) (xs :: a) :: Constraint where ...

Create a new constraint which is valid only if the given value satisfies every unary constraint in the given list.

Equations

SatisfiesAll '[] a = Valid

SatisfiesAll (c ': cs) a = (c a, SatisfiesAll cs a)

type family AllSatisfyAll (c1 :: [a -> Constraint]) (xs :: Vector a n) :: Constraint where ...

Create a new constraint which is valid only if every element in the given vector satisfies every unary constraint in the given list.

Equations

AllSatisfyAll _ None = Valid

AllSatisfyAll cs (v :-- vs) = (SatisfiesAll cs v, AllSatisfyAll cs vs)