git.iko.soy/Idris-dev
on master help sign in
Merge branch 'master' of github.com:edwinb/Idris-dev
1898213Edwin Brady
lib/Builtins.idr+4−4
compare with master
unifiedsplit
@@ -75,6 +75,10 @@ f $ a = f a
75cong : {f : t -> u} -> (a = b) -> f a = f b
75cong : {f : t -> u} -> (a = b) -> f a = f b
76cong refl = refl
76cong refl = refl
77
77
78+data Dec : Type -> Type where
79+ Yes : {A : Type} -> A -> Dec A
80+ No : {A : Type} -> (A -> _|_) -> Dec A
81+
78data Bool = False | True
82data Bool = False | True
79
83
80boolElim : Bool -> |(t : a) -> |(f : a) -> a
84boolElim : Bool -> |(t : a) -> |(f : a) -> a
@@ -83,10 +87,6 @@ boolElim False t e = e
83
87
84data so : Bool -> Type where oh : so True
88data so : Bool -> Type where oh : so True
85
89
86−data Equality : {A : Type} -> (x : A) -> (y : A) -> Type where
87− Unequal : {A : Type} -> {x : A} -> {y : A} -> (x = y -> _|_) -> Equality x y
88− Equal : {A : Type} -> {x : A} -> {y : A} -> (x = y) -> Equality x y
89−
90syntax if [test] then [t] else [e] = boolElim test t e
90syntax if [test] then [t] else [e] = boolElim test t e
91syntax [test] "?" [t] ":" [e] = if test then t else e
91syntax [test] "?" [t] ":" [e] = if test then t else e
92
92
lib/Decidable/Equality.idrnew file+102
@@ -0,0 +1,102 @@
1+module Decidable.Equality
2+
3+import Builtins
4+
5+--------------------------------------------------------------------------------
6+-- Utility lemmas
7+--------------------------------------------------------------------------------
8+
9+total negEqSym : {a : t} -> {b : t} -> (a = b -> _|_) -> (b = a -> _|_)
10+negEqSym p h = p (sym h)
11+
12+
13+--------------------------------------------------------------------------------
14+-- Decidable equality
15+--------------------------------------------------------------------------------
16+
17+class DecEq t where
18+ total decEq : (x1 : t) -> (x2 : t) -> Dec (x1 = x2)
19+
20+--------------------------------------------------------------------------------
21+--- Unit
22+--------------------------------------------------------------------------------
23+
24+instance DecEq () where
25+ decEq () () = Yes refl
26+
27+--------------------------------------------------------------------------------
28+-- Booleans
29+--------------------------------------------------------------------------------
30+
31+total trueNotFalse : True = False -> _|_
32+trueNotFalse refl impossible
33+
34+instance DecEq Bool where
35+ decEq True True = Yes refl
36+ decEq False False = Yes refl
37+ decEq True False = No trueNotFalse
38+ decEq False True = No (negEqSym trueNotFalse)
39+
40+--------------------------------------------------------------------------------
41+-- Nat
42+--------------------------------------------------------------------------------
43+
44+total OnotS : O = S n -> _|_
45+OnotS refl impossible
46+
47+instance DecEq Nat where
48+ decEq O O = Yes refl
49+ decEq O (S _) = No OnotS
50+ decEq (S _) O = No (negEqSym OnotS)
51+ decEq (S n) (S m) with (decEq n m)
52+ | Yes p = Yes $ cong p
53+ | No p = No $ \h : (S n = S m) => p $ succInjective n m h
54+
55+--------------------------------------------------------------------------------
56+-- Maybe
57+--------------------------------------------------------------------------------
58+
59+total nothingNotJust : {x : t} -> (Nothing {a = t} = Just x) -> _|_
60+nothingNotJust refl impossible
61+
62+instance (DecEq t) => DecEq (Maybe t) where
63+ decEq Nothing Nothing = Yes refl
64+ decEq (Just x') (Just y') with (decEq x' y')
65+ | Yes p = Yes $ cong p
66+ | No p = No $ \h : Just x' = Just y' => p $ justInjective h
67+ decEq Nothing (Just _) = No nothingNotJust
68+ decEq (Just _) Nothing = No (negEqSym nothingNotJust)
69+
70+--------------------------------------------------------------------------------
71+-- Either
72+--------------------------------------------------------------------------------
73+
74+total leftNotRight : {x : a} -> {y : b} -> Left {b = b} x = Right {a = a} y -> _|_
75+leftNotRight refl impossible
76+
77+instance (DecEq a, DecEq b) => DecEq (Either a b) where
78+ decEq {b=b} (Left x') (Left y') with (decEq x' y')
79+ | Yes p = Yes $ cong p
80+ | No p = No $ \h : Left x' = Left y' => p $ leftInjective {b = b} h
81+ decEq (Right x') (Right y') with (decEq x' y')
82+ | Yes p = Yes $ cong p
83+ | No p = No $ \h : Right x' = Right y' => p $ rightInjective {a = a} h
84+ decEq (Left x') (Right y') = No leftNotRight
85+ decEq (Right x') (Left y') = No $ negEqSym leftNotRight
86+
87+--------------------------------------------------------------------------------
88+-- Fin
89+--------------------------------------------------------------------------------
90+
91+total fONotfS : {f : Fin n} -> fO {k = n} = fS f -> _|_
92+fONotfS refl impossible
93+
94+instance DecEq (Fin n) where
95+ decEq fO fO = Yes refl
96+ decEq fO (fS f) = No fONotfS
97+ decEq (fS f) fO = No $ negEqSym fONotfS
98+ decEq (fS f) (fS f') with (decEq f f')
99+ | Yes p = Yes $ cong p
100+ | No p = No $ \h => p $ fSinjective {f = f} {f' = f'} h
101+
102+
lib/Prelude/Either.idr+13
@@ -61,3 +61,16 @@ fromEither (Right r) = r
61maybeToEither : e -> Maybe a -> Either e a
61maybeToEither : e -> Maybe a -> Either e a
62maybeToEither def (Just j) = Right j
62maybeToEither def (Just j) = Right j
63maybeToEither def Nothing = Left def
63maybeToEither def Nothing = Left def
64+
65+
66+--------------------------------------------------------------------------------
67+-- Injectivity of constructors
68+--------------------------------------------------------------------------------
69+
70+total leftInjective : {b : Type} -> {x : a} -> {y : a}
71+ -> (Left {b = b} x = Left {b = b} y) -> (x = y)
72+leftInjective refl = refl
73+
74+total rightInjective : {a : Type} -> {x : b} -> {y : b}
75+ -> (Right {a = a} x = Right {a = a} y) -> (x = y)
76+rightInjective refl = refl
lib/Prelude/Fin.idr+3
@@ -40,3 +40,6 @@ strengthen f = Left f
40last : Fin (S n)
40last : Fin (S n)
41last {n=O} = fO
41last {n=O} = fO
42last {n=S _} = fS last
42last {n=S _} = fS last
43+
44+total fSinjective : {f : Fin n} -> {f' : Fin n} -> (fS f = fS f') -> f = f'
45+fSinjective refl = refl
lib/Prelude/Maybe.idr+4
@@ -39,6 +39,10 @@ toMaybe : Bool -> a -> Maybe a
39toMaybe True j = Just j
39toMaybe True j = Just j
40toMaybe False j = Nothing
40toMaybe False j = Nothing
41
41
42+justInjective : {x : t} -> {y : t} -> (Just x = Just y) -> x = y
43+justInjective refl = refl
44+
45+
42--------------------------------------------------------------------------------
46--------------------------------------------------------------------------------
43-- Class instances
47-- Class instances
44--------------------------------------------------------------------------------
48--------------------------------------------------------------------------------
lib/base.ipkg+2
@@ -13,6 +13,8 @@ modules = Builtins, Prelude, IO, System,
13
13
14 System.Concurrency.Raw, System.Concurrency.Process,
14 System.Concurrency.Raw, System.Concurrency.Process,
15
15
16+ Decidable.Equality,
17+
16 Language.Reflection,
18 Language.Reflection,
17
19
18 Data.Morphisms, Data.Bits, Data.Mod2,
20 Data.Morphisms, Data.Bits, Data.Mod2,