Repository : ssh://darcs.haskell.org//srv/darcs/testsuite On branch : type-nats
http://hackage.haskell.org/trac/ghc/changeset/f3ed78eb199cc27b62e44b97afe48172fe431048 >--------------------------------------------------------------- commit f3ed78eb199cc27b62e44b97afe48172fe431048 Author: Iavor S. Diatchki <iavor.diatc...@gmail.com> Date: Fri Dec 28 16:18:31 2012 -0800 Add some tests for the type-nat solver. >--------------------------------------------------------------- tests/typecheck/should_compile/TypeNatAC.hs | 44 ++++++++++++++ tests/typecheck/should_compile/TypeNatBasics.hs | 70 +++++++++++++++++++++++ tests/typecheck/should_compile/TypeNatNat1.hs | 46 +++++++++++++++ tests/typecheck/should_compile/TypeNatVec.hs | 44 ++++++++++++++ tests/typecheck/should_compile/all.T | 7 ++ 5 files changed, 211 insertions(+), 0 deletions(-) diff --git a/tests/typecheck/should_compile/TypeNatAC.hs b/tests/typecheck/should_compile/TypeNatAC.hs new file mode 100644 index 0000000..05c87de --- /dev/null +++ b/tests/typecheck/should_compile/TypeNatAC.hs @@ -0,0 +1,44 @@ +{-# LANGUAGE TypeOperators, DataKinds, PolyKinds #-} + +module TypeNatAC where +import GHC.TypeLits + +data S n = S + +-- Commutativity --------------------------------------------------------------- + +c1 :: S (a + b) -> S (b + a) +c1 = id + +c2 :: S (a * b) -> S (b * a) +c2 = id + + +-- Associativity --------------------------------------------------------------- + +a1 :: S (a + (b + c)) -> S ((a + b) + c) +a1 = id + +a2 :: S ((a + b) + c) -> S (a + (b + c)) +a2 = id + +-- Combinations ---------------------------------------------------------------- + +ac1 :: S ((a + b) + c) -> S (a + (c + b)) +ac1 = id + +ac2 :: S ((b + a) + c) -> S (a + (b + c)) +ac2 = id + +ac3 :: S (c + (a + b)) -> S (a + (b + c)) +ac3 = id + +ac4 :: S ((a + b) + c) -> S ((b + c) + a) +ac4 = id + +ac5 :: S ((c + b) + a) -> S (a + (b + c)) +ac5 = id + +ac6 :: S ((a + b) + c) -> S (c + (b + a)) +ac6 = id + diff --git a/tests/typecheck/should_compile/TypeNatBasics.hs b/tests/typecheck/should_compile/TypeNatBasics.hs new file mode 100644 index 0000000..4ce0c29 --- /dev/null +++ b/tests/typecheck/should_compile/TypeNatBasics.hs @@ -0,0 +1,70 @@ +{-# LANGUAGE TypeOperators, DataKinds, PolyKinds #-} +{-# LANGUAGE FlexibleContexts #-} +module TypeNatBasics where + +import GHC.TypeLits + +data S n = S + +-- Forward evaluation ---------------------------------------------------------- + +e1 :: S (2 + 8) -> S 10 +e1 = id + +e2 :: S (2 * 8) -> S 16 +e2 = id + +e3 :: S (2 ^ 8) -> S 256 +e3 = id + +e4 :: S (2 <=? 8) -> S True +e4 = id + +e5 :: S (8 <=? 2) -> S False +e5 = id + +e6 :: S (8 - 2) -> S 6 +e6 = id + + +-- Identities ------------------------------------------------------------------ + +i1 :: S (x + 0) -> S x +i1 = id + +i2 :: S (x * 0) -> S 0 +i2 = id + +i3 :: S (x * 1) -> S x +i3 = id + +i4 :: S (x ^ 0) -> S 1 +i4 = id + +i5 :: S (x ^ 1) -> S x +i5 = id + +i6 :: (1 <= x) => S (0 ^ x) -> S 0 +i6 = id + +i7 :: S (1 ^ x) -> S 1 +i7 = id + +i8 :: S (x - 0) -> S x +i8 = id + +-------------------------------------------------------------------------------- + +c1 :: S (a + b) -> S (b + a) +c1 = id + +c2 :: S (a * b) -> S (b * a) +c2 = id + + + + + + + + diff --git a/tests/typecheck/should_compile/TypeNatNat1.hs b/tests/typecheck/should_compile/TypeNatNat1.hs new file mode 100644 index 0000000..6dab8ab --- /dev/null +++ b/tests/typecheck/should_compile/TypeNatNat1.hs @@ -0,0 +1,46 @@ +{-# LANGUAGE DataKinds, TypeOperators, PolyKinds, TypeFamilies #-} +{-# LANGUAGE UndecidableInstances #-} +module TypeNatNat1 where + +import GHC.TypeLits + + +data P a = P + + +f1 :: (FromNat1 x ~ 0) => P x +f1 = P :: P Zero + +f2 :: (FromNat1 x ~ FromNat1 y) => P x -> P y +f2 = id + +f3 :: P (FromNat1 x) -> P x +f3 = undefined + +type family Get (n :: Nat1) (xs :: [*]) :: * + +type instance Get Zero (x ': xs) = x +type instance Get (Succ n) (x ': xs) = Get n xs + +f4 :: P (FromNat1 n) -> P xs -> P (Get n xs) +f4 _ _ = P + +f5 :: P Int +f5 = f4 (P :: P 0) (P :: P [Int,Char,Float]) + +f6 :: P Float +f6 = f4 (P :: P 2) (P :: P [Int,Char,Float]) + +class C n where + g :: Sing (FromNat1 n) + +instance C Zero where + g = sing + +instance C n => C (Succ n) where + g = incSucc g + +incSucc :: Sing a -> Sing (1 + a) +incSucc x = unsafeSingNat (fromSing x + 1) + + diff --git a/tests/typecheck/should_compile/TypeNatVec.hs b/tests/typecheck/should_compile/TypeNatVec.hs new file mode 100644 index 0000000..f7ecc18 --- /dev/null +++ b/tests/typecheck/should_compile/TypeNatVec.hs @@ -0,0 +1,44 @@ +{-# LANGUAGE DataKinds, KindSignatures, TypeOperators, GADTs #-} +module TypeNatVec where + +import GHC.TypeLits + +data Vec :: Nat -> * -> * + where + Nil :: Vec 0 a + Cons :: a -> Vec n a -> Vec (n + 1) a + +instance Functor (Vec n) where + fmap f Nil = Nil + fmap f (Cons x xs) = Cons (f x) (fmap f xs) + +data Ix :: Nat -> * + where + Z :: Ix (n + 1) + S :: Ix n -> Ix (n + 1) + +lkp :: Vec n a -> Ix n -> a +lkp (Cons x _) Z = x +lkp (Cons _ xs) (S x) = lkp xs x + +revAppend :: Vec m a -> Vec n a -> Vec (m + n) a +revAppend Nil ys = ys +revAppend (Cons x xs) ys = revAppend xs (Cons x ys) + +rev :: Vec n a -> Vec n a +rev xs = revAppend xs Nil + +append :: Vec m a -> Vec n a -> Vec (m + n) a +append Nil ys = ys +append (Cons x xs) ys = Cons x (append xs ys) + +instance Show a => Show (Vec n a) where + show Nil = "Nil" + show (Cons x xs) = show x ++ "," ++ show xs + +ex1 = Cons 1 $ Cons 2 Nil +ex2 = Cons 3 Nil +ex3 = append ex1 ex2 +ex4 = revAppend ex1 ex2 +ex5 = revAppend (Cons 1 (Cons 2 Nil)) (Cons 3 Nil) + diff --git a/tests/typecheck/should_compile/all.T b/tests/typecheck/should_compile/all.T index 5905bb7..6e18be4 100644 --- a/tests/typecheck/should_compile/all.T +++ b/tests/typecheck/should_compile/all.T @@ -395,3 +395,10 @@ test('holes2', normal, compile, ['-fdefer-type-errors']) test('holes3', normal, compile_fail, ['']) test('T7408', normal, compile, ['']) test('UnboxStrictPrimitiveFields', normal, compile, ['']) +test('TypeNatBasics', normal, compile, ['']) +test('TypeNatAC', normal, compile, ['']) +test('TypeNatVec', normal, compile, ['']) +test('TypeNatNat1', normal, compile, ['']) + + + _______________________________________________ Cvs-ghc mailing list Cvs-ghc@haskell.org http://www.haskell.org/mailman/listinfo/cvs-ghc
