mezzo-0.1.0.0: test/PrimSpec.hs

{-# OPTIONS_GHC -fdefer-type-errors #-}
-- {-# OPTIONS_GHC -w #-}
{-# LANGUAGE TypeInType, TypeOperators, GADTs, MultiParamTypeClasses, FlexibleInstances #-}

module PrimSpec where

import Test.Hspec
import GHC.TypeLits
import Control.Exception (evaluate)
import Test.ShouldNotTypecheck (shouldNotTypecheck)

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

        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

        describe "Arithmetic operations" $ do
            it "should calculate maximum of two numbers" $ do
                maxNat `shouldBe` True
            it "should calculate minimum of two numbers" $ do
                minNat `shouldBe` True

        describe "Constraint operations" $ do
            it "should apply a constraint to an optimised vector" $ do
                allSatisfy `shouldBe` True
                -- shouldNotTypecheck allSatisfyInv
            it "should apply a binary constraint to two optimised vectors" $ do
                allPairsSatisfy `shouldBe` True
                shouldNotTypecheck allPairsSatisfyInv
            it "should apply a binary constraint to two vectors" $ do
                allPairsSatisfy' `shouldBe` True
                shouldNotTypecheck allPairsSatisfyInv'
            it "should apply all constraints to a value" $ do
                satisfiesAll `shouldBe` True
                -- shouldNotTypecheck satisfiesAllInv
            it "should apply all constraints to all values" $ do
                allSatisfyAll `shouldBe` True
                -- shouldNotTypecheck allSatisfyAllInv


timesReplicate :: (True ** 23) ~ (True :* (T :: Times 23)) => Bool
timesReplicate = True

optVectorHead :: (Head (True ** 4 :- End)) ~ True => Bool
optVectorHead = True

vectorHead :: (Head' (True :-- None)) ~ True => Bool
vectorHead = True

optVectorLast :: (Last (True ** 4 :- False ** 9 :- End)) ~ False => Bool
optVectorLast = True

vectorTail :: (Tail' (True :-- False :-- None)) ~ (False :-- None) => Bool
vectorTail = True

vectorInit :: (Init' (True :-- False :-- None)) ~ (True :-- None) => Bool
vectorInit = True

optVectorLength :: (Length (True ** 4 :- False ** 9 :- End)) ~ 13 => Bool
optVectorLength = True

vectorLength :: (Length' (True :-- False :-- None)) ~ 2 => Bool
vectorLength = True

optVectorAppend :: ((True ** 5 :- False ** 2 :- End) ++ End ++ (False ** 9 :- End))
                  ~ (True ** 5 :- False ** 2 :- False ** 9 :- End) => Bool
optVectorAppend = True

vectorAppend :: ((2 :-- 43 :-- None) ++. None ++. (6 :-- None))
                  ~ (2 :-- 43 :-- 6 :-- None) => Bool
vectorAppend = True

snoc :: ((2 :-- 5 :-- None) :-| 6) ~ (2 :-- 5 :-- 6 :-- None) => Bool
snoc = True

repeatVec :: (True +*+ 3) ~ (True ** 3 :- End) => Bool
repeatVec = True

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

align ::
          -- Right fragment
        ( Align (True ** 2 :- False ** 2 :- End :-- None) (True ** 4 :- End :-- None)
          ~ '(True ** 2 :- False ** 2 :- End :-- None, True ** 2 :- True ** 2 :- End :-- None)
          -- Left fragment
        , Align (False ** 18 :- End :-- None) (True ** 8 :- False ** 10 :- End :-- None)
          ~ '(False ** 8 :- False ** 10 :- End :-- None, True ** 8 :- False ** 10 :- End :-- None)
          -- No fragment
        , Align (True ** 4 :- End :-- None) (False ** 4 :- End :-- None)
          ~ '(True ** 4 :- End :-- None, False ** 4 :- End :-- None)
          -- Both fragment
        , Align (False ** 18 :- True ** 3 :- End :-- None) (True ** 8 :- False ** 13 :- End :-- None)
          ~ '(False ** 8 :- False ** 10 :- True ** 3 :- End :-- None, True ** 8 :- False ** 10 :- False ** 3 :- End :-- None)
        ) => Bool
align = True

matVConcat ::
          -- No fragmentation
        (    ((True ** 3 :- False ** 6 :- End :-- None)
          +-+ (False ** 3 :- True ** 6 :- End :-- None))
          ~ (True ** 3 :- False ** 6 :- End :-- False ** 3 :- True ** 6 :- End :-- None)
          -- Top fragment
        ,    ((True ** 9 :- End :-- None)
          +-+ (False ** 3 :- True ** 6 :- End :-- None))
          ~ (True ** 3 :- True ** 6 :- End :-- False ** 3 :- True ** 6 :- End :-- None)
          -- Bottom fragment
        ,    ((True ** 3 :- False ** 6 :- End :-- None)
          +-+ (False ** 9 :- End :-- None))
          ~ (True ** 3 :- False ** 6 :- End :-- False ** 3 :- False ** 6 :- End :-- None)
          -- Both fragment
        ,    ((True ** 3 :- False ** 6 :- End :-- None)
          +-+ (False ** 6 :- True ** 3 :- End :-- None))
          ~ (True ** 3 :- False ** 3 :- False ** 3 :- End :-- False ** 3 :- False ** 3 :- True ** 3 :- End :-- None)
          -- More voices
        ,    ((True ** 2 :- False ** 8 :- End :-- False ** 2 :- True ** 8 :- End :-- None)
          +-+ (False ** 4 :- True ** 6 :- End :-- None)
          +-+ (True ** 1 :- False ** 8 :- True ** 1 :- End :-- False ** 1 :- True ** 8 :- False ** 1 :- End :-- None))
          ~    ((True ** 1 :- True ** 1 :- False ** 2 :- False ** 5 :- False ** 1 :- End)
            :-- (False ** 1 :- False ** 1 :- True ** 2 :- True ** 5 :- True ** 1 :- End)
            :-- (False ** 1 :- False ** 1 :- False ** 2 :- True ** 5 :- True ** 1 :- End)
            :-- (True ** 1 :- False ** 1 :- False ** 2 :- False ** 5 :- True ** 1 :- End)
            :-- (False ** 1 :- True ** 1 :- True ** 2 :- True ** 5 :- False ** 1 :- End) :-- None
            )
        ) => Bool
matVConcat = True

vecToColMatrix ::
        ( (VectorToColMatrix (True :-- False :-- None) 24)
          ~ (False ** 24 :- End :-- True ** 24 :- End :-- None)
        , (VectorToColMatrix None 11) ~ None
        ) => Bool
vecToColMatrix = True


-- Let's assume that the Boolean functions work...

maxNat :: ((MaxN 5 9) ~ 9, (MaxN 7 4) ~ 7, (MaxN 0 8) ~ 8, (MaxN 1 0) ~ 1, (MaxN 3 3) ~ 3
          , (MaxN (MaxN 133 43) 235) ~ 235) => Bool
maxNat = True

minNat :: ((MinN 5 9) ~ 5, (MinN 7 4) ~ 4, (MinN 0 8) ~ 0, (MinN 1 0) ~ 0, (MinN 3 3) ~ 3
          , (MinN (MinN 133 43) 235) ~ 43) => Bool
minNat = True

allSatisfy :: (AllSatisfy Num (Int ** 1 :- Integer ** 1 :- Double ** 1 :- End)) => Bool
allSatisfy = True

-- allSatisfyInv :: (AllSatisfy Integral (Double ** 1 :- String ** 1 :- Bool ** 1 :- End)) => Bool
-- allSatisfyInv = True

class TestConstraint (a :: Nat) (b :: Nat)
instance (MaxN a b ~ b) => TestConstraint a b

allPairsSatisfy :: (AllPairsSatisfy TestConstraint
                    (1 ** 1 :- 3 ** 1 :- 5 ** 1 :- End) (2 ** 1 :- 4 ** 1 :- 6 ** 1 :- End)) => Bool
allPairsSatisfy = True

allPairsSatisfyInv :: (AllPairsSatisfy TestConstraint (4 ** 1 :- End) (1 ** 1 :- End)) => Bool
allPairsSatisfyInv = True

allPairsSatisfy' :: (AllPairsSatisfy' TestConstraint
                    (1 :-- 3 :-- 5 :-- None) (2 :-- 4 :-- 6 :-- None)) => Bool
allPairsSatisfy' = True

allPairsSatisfyInv' :: (AllPairsSatisfy' TestConstraint (2 :-- None) (1 :-- None)) => Bool
allPairsSatisfyInv' = True

satisfiesAll :: (SatisfiesAll '[Num, Integral, Show] Int) => Bool
satisfiesAll = True

-- Doesn't work unfortunately
-- satisfiesAllInv :: (SatisfiesAll '[Num, Integral, Show] Bool) => Bool
-- satisfiesAllInv = True

allSatisfyAll :: (AllSatisfyAll '[Num, Show] (Double :-- Int :-- Integer :-- None)) => Bool
allSatisfyAll = True

-- allSatisfyAllInv :: (AllSatisfyAll '[Num, Show] (Bool :-- String :-- Integer :-- None)) => Bool
-- allSatisfyAllInv = True



{- MALFORMED TYPE SIGNATURES: should never typecheck
-- (Comment out line above to expose)

timesReplicateW :: (True ** 23) ~ (True :* (T :: Times 1)) => Bool
optVectorHeadW :: (Head (True ** 4 :- End)) ~ False => Bool
vectorHeadW :: (Head' (True :-- None)) ~ False => Bool
optVectorLastW :: (Last (True ** 4 :- False ** 9 :- End)) ~ True => Bool
vectorTailW :: (Tail' (True :-- False :-- None)) ~ (True :-- None) => Bool
vectorInitW :: (Init' (True :-- False :-- None)) ~ (False :-- None) => Bool
optVectorLengthW :: (Length (True ** 4 :- False ** 9 :- End)) ~ 12 => Bool
vectorLengthW :: (Length' (True :-- False :-- None)) ~ 3 => Bool
optVectorAppendW :: ((True ** 5 :- False ** 2 :- End) ++ (False ** 9 :- End))
                  ~ (True ** 5 :- False ** 11 :- End) => Bool
vectorAppendW :: ((2 :-- 43 :-- None) ++. None ++. (6 :-- None))
                ~ (2 :-- 3 :-- 6 :-- None) => Bool
snocW :: ((2 :-- 5 :-- None) :-| 6) ~ (2 :-- 5 :-- 4 :-- None) => Bool
repeatVecW :: (True +*+ 3) ~ (True ** 4 :- End) => Bool
matHConcatW ::
        (  ((True ** 2 :- End :-- False ** 2 :- End :-- None)
           +|+ (False ** 5 :- End :-- True ** 5 :- End :-- None))
           ~ ((True ** 2 :- False ** 5 :- End :-- True ** 2 :- True ** 5 :- End :-- None))

        ,  ((True ** 2 :- End :-- False ** 2 :- End :-- None)
           +|+ (End :-- None))
           ~ (True ** 2 :- End :-- False ** 2 :- End :-- None)

        , (None +|+ None) ~ (None :-- None)
        )
          => Bool
alignW ::
          -- Right fragment
        ( Align (True ** 2 :- False ** 2 :- End :-- None) (True ** 4 :- End :-- None)
          ~ '(True ** 2 :- False ** 2 :- End :-- None, True ** 1 :- True ** 3 :- End :-- None)
          -- Left fragment
        , Align (False ** 18 :- End :-- None) (True ** 8 :- False ** 10 :- End :-- None)
          ~ '(False ** 7 :- False ** 11 :- End :-- None, True ** 8 :- False ** 10 :- End :-- None)
          -- No fragment
        , Align (True ** 4 :- End :-- None) (False ** 4 :- End :-- None)
          ~ '(True ** 4 :- End :-- None, True ** 4 :- End :-- None)
          -- Both fragment
        , Align (False ** 18 :- True ** 3 :- End :-- None) (True ** 8 :- False ** 13 :- End :-- None)
          ~ '(False ** 8 :- False ** 9 :- True ** 4 :- End :-- None, True ** 8 :- False ** 10 :- False ** 3 :- End :-- None)
        ) => Bool
vecToColMatrixW ::
        ( (VectorToColMatrix (True :-- False :-- None) 24)
          ~ (False ** 24 :- End :-- False ** 24 :- End :-- None)
        , (VectorToColMatrix None 11) ~ (True ** 11 :- End :-- None)
        ) => Bool

allSatisfyW :: (AllSatisfy Num (Int ** 1 :- Bool ** 1 :- Double ** 1 :- End)) => Bool


timesReplicateW = True
optVectorHeadW = True
vectorHeadW = True
optVectorLastW = True
vectorTailW = True
vectorInitW = True
optVectorLengthW = True
vectorLengthW = True
optVectorAppendW = True
vectorAppendW = True
snocW = True
repeatVecW = True
matHConcatW = True
alignW = True
vecToColMatrixW = True
allSatisfyW = True

-- -}