git.iko.soy/Idris-dev
on master help sign in
Merge pull request #795 from SimonJF/deceq-str

Add decidable equality instance for String, and a decEq unit test

commit3cc603cd81e39e9a4ca8ceb165b334faefca700e authorEdwin Brady <edwin.brady@gmail.com> dateTue 28 Jan 2014, 05:29 (13 years ago) parentfe3f03ff4449c7
4 files changed+105−1
compare with master
unifiedsplit
libs/prelude/Decidable/Equality.idr+10−1 test/test038/expected+29 test/test038/run+4 test/test038/test038.idr+62
libs/prelude/Decidable/Equality.idr+10−1
@@ -153,7 +153,7 @@ instance DecEq a => DecEq (List a) where
153153 decEq [] (x :: xs) = No (negEqSym lemma_val_not_nil)
154154 decEq (x :: xs) (y :: ys) with (decEq x y)
155155 decEq (x :: xs) (x :: ys) | Yes refl with (decEq xs ys)
156− decEq (x :: xs) (x :: xs) | (Yes refl) | (Yes refl) = Yes refl -- maybe another yes refl
156+ decEq (x :: xs) (x :: xs) | (Yes refl) | (Yes refl) = Yes refl
157157 decEq (x :: xs) (x :: ys) | (Yes refl) | (No p) = No (\eq => lemma_x_eq_xs_neq refl p eq)
158158 decEq (x :: xs) (y :: ys) | No p with (decEq xs ys)
159159 decEq (x :: xs) (y :: xs) | (No p) | (Yes refl) = No (\eq => lemma_x_neq_xs_eq p refl eq)
@@ -215,3 +215,12 @@ instance DecEq Float where
215215 decEq x y = if x == y then Yes (really_believe_me {a = x=x} {b = x=y} refl)
216216 else No (really_believe_me _|_)
217217
218+--------------------------------------------------------------------------------
219+-- String
220+--------------------------------------------------------------------------------
221+
222+instance DecEq String where
223+ decEq x y = if x == y then Yes (really_believe_me {a = x=x} {b = x=y} refl)
224+ else No (really_believe_me _|_)
225+
226+
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+