Copyright | (c) Dima Szamozvancev |
---|---|
License | MIT |
Maintainer | ds709@cam.ac.uk |
Stability | experimental |
Portability | portable |
Safe Haskell | Safe |
Language | Haskell2010 |
Primitive types that make up the base for the Mezzo type model.
- data Vector :: Type -> Nat -> Type where
- data Times n where
- data Elem :: Type -> Nat -> Type where
- type family (v :: t) ** (d :: Nat) :: Elem t d where ...
- data OptVector :: Type -> Nat -> Type where
- type family Head (v :: OptVector t n) :: t where ...
- type family Head' (v :: Vector t n) :: t where ...
- type family Last (v :: OptVector t n) :: t where ...
- type family Tail' (v :: Vector t n) :: Vector t (n - 1) where ...
- type family Init' (v :: Vector t n) :: Vector t (n - 1) where ...
- type family Length (v :: OptVector t n) :: Nat where ...
- type family Length' (v :: Vector t n) :: Nat where ...
- type Matrix t p q = Vector (OptVector t q) p
- type family (x :: OptVector t n) ++ (y :: OptVector t m) :: OptVector t (n + m) where ...
- type family (x :: Vector t n) ++. (y :: Vector t m) :: Vector t (n + m) where ...
- type family (v :: Vector t n) :-| (e :: t) :: Vector t (n + 1) where ...
- type family (a :: t) +*+ (n :: Nat) :: OptVector t n where ...
- type family (a :: Matrix t p q) +|+ (b :: Matrix t p r) :: Matrix t p (q + r) where ...
- type family (a :: Matrix t p r) +-+ (b :: Matrix t q r) :: Matrix t (p + q) r where ...
- type family Align (a :: Matrix t p r) (b :: Matrix t q r) :: (Matrix t p r, Matrix t q r) where ...
- type family VectorToColMatrix (v :: Vector t n) (l :: Nat) :: Matrix t n l where ...
- type family If (b :: Bool) (t :: k) (e :: k) :: k where ...
- type family Not (a :: Bool) :: Bool where ...
- type family (b1 :: Bool) .&&. (b2 :: Bool) :: Bool where ...
- type family (b1 :: Bool) .||. (b2 :: Bool) :: Bool where ...
- type family (a :: k) .~. (b :: k) :: Bool where ...
- type family MaxN (n1 :: Nat) (n2 :: Nat) :: Nat where ...
- type family MinN (n1 :: Nat) (n2 :: Nat) :: Nat where ...
- type Valid = (() :: Constraint)
- type Invalid = True ~ False
- type family AllSatisfy (c :: a -> Constraint) (xs :: OptVector a n) :: Constraint where ...
- type family AllPairsSatisfy (c :: a -> b -> Constraint) (xs :: OptVector a n) (ys :: OptVector b n) :: Constraint where ...
- type family AllPairsSatisfy' (c :: a -> b -> Constraint) (xs :: Vector a n) (ys :: Vector b n) :: Constraint where ...
- type family SatisfiesAll (cs :: [a -> Constraint]) (xs :: a) :: Constraint where ...
- type family AllSatisfyAll (c1 :: [a -> Constraint]) (xs :: Vector a n) :: Constraint where ...
Vectors and matrices
data Vector :: Type -> Nat -> Type where Source #
Simple length-indexed vector.
(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) Source # | |
ValidHomConcat 0 n2 l ((,) (Vector (OptVector PitchType l) 0) (Partiture n2 l) (None (OptVector PitchType l)) vs) Source # | |
(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) Source # | |
ValidHarmConcat 0 n2 l ((,) (Vector (OptVector PitchType l) 0) (Partiture n2 l) (None (OptVector PitchType l)) vs) Source # | |
data Elem :: Type -> Nat -> Type where Source #
An element of a "run-length encoded" vector, containing the value and the number of repetitions
type family (v :: t) ** (d :: Nat) :: Elem t d where ... infixr 7 Source #
Replicate a value the specified number of times to create a new Elem
.
data OptVector :: Type -> Nat -> Type where Source #
A length-indexed vector, optimised for repetitions.
type family Head (v :: OptVector t n) :: t where ... Source #
Get the first element of an optimised vector.
type family Head' (v :: Vector t n) :: t where ... Source #
Get the first element of a simple vector.
type family Tail' (v :: Vector t n) :: Vector t (n - 1) where ... Source #
Get the tail of the vector.
type family Init' (v :: Vector t n) :: Vector t (n - 1) where ... Source #
Get everything but the last element of the vector.
type family Length (v :: OptVector t n) :: Nat where ... Source #
Get the length of an optimised vector.
type family (x :: OptVector t n) ++ (y :: OptVector t m) :: OptVector t (n + m) where ... infixl 4 Source #
Append two optimised vectors.
type family (x :: Vector t n) ++. (y :: Vector t m) :: Vector t (n + m) where ... Source #
Append two simple vectors.
type family (v :: Vector t n) :-| (e :: t) :: Vector t (n + 1) where ... Source #
Add an element to the end of a simple vector.
type family (a :: t) +*+ (n :: Nat) :: OptVector t n where ... infixl 4 Source #
Repeat the value the specified number of times to create a new OptVector
.
type family (a :: Matrix t p q) +|+ (b :: Matrix t p r) :: Matrix t p (q + r) where ... infixl 4 Source #
Horizontal concatenation of type-level matrices. Places the first matrix to the left of the second.
type family (a :: Matrix t p r) +-+ (b :: Matrix t q r) :: Matrix t (p + q) r where ... infixl 4 Source #
Vertical concatenation of type-level matrices. Places the first matrix on top of the second.
type family Align (a :: Matrix t p r) (b :: Matrix t q r) :: (Matrix t p r, Matrix t q r) where ... Source #
Vertically aligns two matrices by separating elements so that the element boundaries line up.
type family VectorToColMatrix (v :: Vector t n) (l :: Nat) :: Matrix t n l where ... Source #
Convert a simple vector to a column matrix.
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 ... Source #
Conditional expression at the type level.
type family (b1 :: Bool) .&&. (b2 :: Bool) :: Bool where ... infixl 3 Source #
Conjunction of type-level Booleans.
type family (b1 :: Bool) .||. (b2 :: Bool) :: Bool where ... infixl 3 Source #
Disjunction of type-level Booleans.
type family MaxN (n1 :: Nat) (n2 :: Nat) :: Nat where ... Source #
Returns the maximum of two natural numbers.
type family MinN (n1 :: Nat) (n2 :: Nat) :: Nat where ... Source #
Returns the minimum of two natural numbers.
Constraints
type Valid = (() :: Constraint) Source #
Valid base constraint.
type family AllSatisfy (c :: a -> Constraint) (xs :: OptVector a n) :: Constraint where ... Source #
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.
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 ... Source #
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.
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 ... Source #
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.
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 ... Source #
Create a new constraint which is valid only if the given value satisfies every unary constraint in the given list.
SatisfiesAll '[] a = Valid | |
SatisfiesAll (c ': cs) a = (c a, SatisfiesAll cs a) |
type family AllSatisfyAll (c1 :: [a -> Constraint]) (xs :: Vector a n) :: Constraint where ... Source #
Create a new constraint which is valid only if every element in the given vector satisfies every unary constraint in the given list.
AllSatisfyAll _ None = Valid | |
AllSatisfyAll cs (v :-- vs) = (SatisfiesAll cs v, AllSatisfyAll cs vs) |