[commit: testsuite] type-nats-simple: Add some tests (d2b7f82)

[git at git.haskell.org]

Repository : ssh://git@git.haskell.org/testsuite

On branch  : type-nats-simple
Link       : http://ghc.haskell.org/trac/ghc/changeset/d2b7f8216537af0e337e31aed75f55e9e2478772/testsuite

>---------------------------------------------------------------

commit d2b7f8216537af0e337e31aed75f55e9e2478772
Author: Iavor S. Diatchki <iavor.diatchki at gmail.com>
Date:   Sun Sep 8 22:45:41 2013 -0700

    Add some tests


>---------------------------------------------------------------

d2b7f8216537af0e337e31aed75f55e9e2478772
 tests/typecheck/should_compile/TcTypeNatSimple.hs  |   81 ++++++++++++++++++++
 tests/typecheck/should_compile/all.T               |    1 +
 tests/typecheck/should_run/TcTypeNatSimpleRun.hs   |   32 ++++++++
 .../should_run/TcTypeNatSimpleRun.stdout}          |    0
 tests/typecheck/should_run/all.T                   |    1 +
 5 files changed, 115 insertions(+)

diff --git a/tests/typecheck/should_compile/TcTypeNatSimple.hs b/tests/typecheck/should_compile/TcTypeNatSimple.hs
new file mode 100644
index 0000000..e30656a
--- /dev/null
+++ b/tests/typecheck/should_compile/TcTypeNatSimple.hs
@@ -0,0 +1,81 @@
+{-# LANGUAGE DataKinds, TypeOperators, TypeFamilies #-}
+module TcTypeNatSimple where
+import GHC.TypeLits
+
+--------------------------------------------------------------------------------
+-- Test evaluation
+e1 :: Sing (2 + 3) -> Sing 5
+e1 = id
+
+e2 :: Sing (2 * 3) -> Sing 6
+e2 = id
+
+e3 :: Sing (2 ^ 3) -> Sing 8
+e3 = id
+
+e4 :: Sing (0 + x) -> Sing x
+e4 = id
+
+e5 :: Sing (x + 0) -> Sing x
+e5 = id
+
+e6 :: Sing (x * 0) -> Sing 0
+e6 = id
+
+e7 :: Sing (0 * x) -> Sing 0
+e7 = id
+
+e8 :: Sing (x * 1) -> Sing x
+e8 = id
+
+e9 :: Sing (1 * x) -> Sing x
+e9 = id
+
+e10 :: Sing (x ^ 1) -> Sing x
+e10 = id
+
+e11 :: Sing (1 ^ x) -> Sing 1
+e11 = id
+
+e12 :: Sing (x ^ 0) -> Sing 1
+e12 = id
+
+e13 :: Sing (1 <=? 2) -> Sing True
+e13 = id
+
+e14 :: Sing (2 <=? 1) -> Sing False
+e14 = id
+
+e15 :: Sing (x <=? x) -> Sing True
+e15 = id
+
+e16 :: Sing (0 <=? x) -> Sing True
+e16 = id
+
+--------------------------------------------------------------------------------
+-- Test interactions with inerts
+
+ti1 :: Sing (x + y) -> Sing x -> ()
+ti1 _ _ = ()
+
+ti2 :: Sing (y + x) -> Sing x -> ()
+ti2 _ _ = ()
+
+ti3 :: Sing (2 * y) -> ()
+ti3 _ = ()
+
+ti4 :: Sing (y * 2) -> ()
+ti4 _ = ()
+
+ti5 :: Sing (2 ^ y) -> ()
+ti5 _ = ()
+
+ti6 :: Sing (y ^ 2) -> ()
+ti6 _ = ()
+
+type family SomeFun (n :: Nat)
+
+ti7 :: (x <= y, y <= x) => Sing (SomeFun x) -> Sing y -> ()
+ti7 _ _ = ()
+
+
diff --git a/tests/typecheck/should_compile/all.T b/tests/typecheck/should_compile/all.T
index e28e597..f288071 100644
--- a/tests/typecheck/should_compile/all.T
+++ b/tests/typecheck/should_compile/all.T
@@ -408,3 +408,4 @@ test('T7268', normal, compile, [''])
 test('T7888', normal, compile, [''])
 test('T7891', normal, compile, [''])
 test('T7903', normal, compile, [''])
+test('TcTypeNatSimple', normal, compile, [''])
diff --git a/tests/typecheck/should_run/TcTypeNatSimpleRun.hs b/tests/typecheck/should_run/TcTypeNatSimpleRun.hs
new file mode 100644
index 0000000..22ad315
--- /dev/null
+++ b/tests/typecheck/should_run/TcTypeNatSimpleRun.hs
@@ -0,0 +1,32 @@
+{-# LANGUAGE DataKinds, TypeOperators, TypeFamilies #-}
+module Main(main) where
+import GHC.TypeLits
+
+--------------------------------------------------------------------------------
+-- Test top-reactions
+
+tsub :: SingI x => Sing (x + y) -> Sing y -> Sing x
+tsub _ _ = sing
+
+tdiv :: SingI x => Sing (x * y) -> Sing y -> Sing x
+tdiv _ _ = sing
+
+troot :: SingI x => Sing (x ^ y) -> Sing y -> Sing x
+troot _ _ = sing
+
+tlog :: SingI y => Sing (x ^ y) -> Sing x -> Sing y
+tlog _ _ = sing
+
+tleq :: (SingI x, (x <=? y) ~ True) => Sing y -> Sing x
+tleq _ = sing
+
+main :: IO ()
+main = print [ show (tsub  (sing :: Sing 5) (sing :: Sing 3)) == "2"
+             , show (tdiv  (sing :: Sing 8) (sing :: Sing 2)) == "4"
+             , show (troot (sing :: Sing 9) (sing :: Sing 2)) == "3"
+             , show (tlog  (sing :: Sing 8) (sing :: Sing 2)) == "3"
+             , show (tleq  (sing :: Sing 0))                  == "0"
+             ]
+
+
+
diff --git a/tests/deSugar/should_run/DsLambdaCase.stdout b/tests/typecheck/should_run/TcTypeNatSimpleRun.stdout
similarity index 100%
copy from tests/deSugar/should_run/DsLambdaCase.stdout
copy to tests/typecheck/should_run/TcTypeNatSimpleRun.stdout
diff --git a/tests/typecheck/should_run/all.T b/tests/typecheck/should_run/all.T
index 1d714a2..b566c33 100755
--- a/tests/typecheck/should_run/all.T
+++ b/tests/typecheck/should_run/all.T
@@ -110,3 +110,4 @@ test('T5913', normal, compile_and_run, [''])
 test('T7748', normal, compile_and_run, [''])
 test('TcNullaryTC', when(compiler_lt('ghc', '7.7'), skip), compile_and_run, [''])
 test('T7861', exit_code(1), compile_and_run, [''])
+test('TcTypeNatSimpleRun', normal, compile_and_run, [''])