git.iko.soy/Idris-dev
on master help sign in
Add decEq unit test
commitf4449c7afd3a635dc3ea5bf016cc8e681bb3b3a6 authorSimon Fowler <simon@simonjf.com> dateThu 23 Jan 2014, 19:06 (13 years ago) parentdd1665b
3 files changed+95
compare with master
unifiedsplit
test/test038/expected+29 test/test038/run+4 test/test038/test038.idr+62
test/test038/expectednew file+29
@@ -0,0 +1,29 @@
1+True
2+False
3+True
4+False
5+True
6+False
7+True
8+False
9+True
10+False
11+False
12+True
13+False
14+True
15+True
16+False
17+True
18+False
19+True
20+False
21+False
22+True
23+False
24+False
25+False
26+True
27+False
28+True
29+False
test/test038/runnew file+4
@@ -0,0 +1,4 @@
1+#!/usr/bin/env bash
2+idris $@ -o test038 test038.idr --nocolour
3+./test038
4+rm -f test038 *.ibc
test/test038/test038.idrnew file+62
@@ -0,0 +1,62 @@
1+module Main
2+
3+test : DecEq a => a -> a -> Bool
4+test i1 i2 with (decEq i1 i2)
5+ test i1 i1 | Yes refl = True
6+ test i1 i2 | No p = False
7+
8+main : IO ()
9+main = do
10+-- Primitives
11+ putStrLn . show $ test (the Int 3) (the Int 3)
12+ putStrLn . show $ test (the Integer 3) (the Integer 4)
13+ putStrLn . show $ test "hello" "hello"
14+ putStrLn . show $ test "hello" "world"
15+ putStrLn . show $ test (the Char '\0') (the Char '\0')
16+ putStrLn . show $ test (the Char '\1') (the Char '\2')
17+-- Non-primitives
18+ -- Vect
19+ putStrLn . show $
20+ test (the (Vect _ Int) [1,2,3]) (the (Vect _ Int) [1,2,3])
21+ putStrLn . show $
22+ test (the (Vect _ Int) [1,2,3]) (the (Vect _ Int) [1,2,4])
23+ -- List
24+ putStrLn . show $
25+ test (the (List Int) [1,2,3]) (the (List Int) [1,2,3])
26+ putStrLn . show $
27+ test (the (List Int) [1,2,3]) (the (List Int) [1,2])
28+ putStrLn . show $
29+ test (the (List Int) [1,2,3]) (the (List Int) [1,2,4])
30+ -- Tuple
31+ putStrLn . show $
32+ test (the (Int, Int) (1, 1)) (the (Int, Int) (1, 1))
33+ putStrLn . show $
34+ test (the (Int, Int) (1, 2)) (the (Int, Int) (1, 1))
35+ -- Unit
36+ putStrLn . show $ test () ()
37+ -- Booleans
38+ putStrLn . show $ test True True
39+ putStrLn . show $ test True False
40+ -- Float
41+ putStrLn . show $ test 1.0 1.0
42+ putStrLn . show $ test 1.0 2.0
43+ -- Maybe
44+ putStrLn . show $ test (Just "hello") (Just "hello")
45+ putStrLn . show $ test (Just "hello") (Just "world")
46+ putStrLn . show $ test (Just "hello") Nothing
47+ -- Either
48+ putStrLn . show $ test (the (Either String Bool) (Left "hello"))
49+ (the (Either String Bool) (Left "hello"))
50+ putStrLn . show $ test (the (Either String Bool) (Left "hello"))
51+ (the (Either String Bool) (Left "world"))
52+ putStrLn . show $ test (Left "hello") (Right "world")
53+ putStrLn . show $ test (Left "hello") (Right False)
54+ -- Fin
55+ putStrLn . show $ test (the (Fin (S (S (S (Z))))) (fS (fS (fZ))))
56+ (the (Fin (S (S (S (Z))))) (fS (fS (fZ))))
57+ putStrLn . show $ test (the (Fin (S (S (S (Z))))) (fS (fS (fZ))))
58+ (the (Fin (S (S (S (Z))))) (fS (fZ)))
59+ -- Nat
60+ putStrLn . show $ test (S (S (S Z))) (S (S (S Z)))
61+ putStrLn . show $ test (S (S (S Z))) (S (S Z))
62+