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

Reply via email to