0 | module Decidable.HDecEq
  1 |
  2 | import public Data.List.Quantifiers
  3 | import public Data.Maybe0
  4 |
  5 | %default total
  6 |
  7 | ||| Hemi-decidable equality.
  8 | public export
  9 | interface HDecEq a where
 10 |   constructor MkHDecEq
 11 |   hdecEq : (x,y : a) -> Maybe0 (x === y)
 12 |
 13 | export
 14 | HDecEq Bits8 where
 15 |   hdecEq x y = case prim__eq_Bits8 x y of
 16 |     0 => Nothing0
 17 |     _ => Just0 (believe_me $ Refl {x})
 18 |
 19 | export
 20 | HDecEq Bits16 where
 21 |   hdecEq x y = case prim__eq_Bits16 x y of
 22 |     0 => Nothing0
 23 |     _ => Just0 (believe_me $ Refl {x})
 24 |
 25 | export
 26 | HDecEq Bits32 where
 27 |   hdecEq x y = case prim__eq_Bits32 x y of
 28 |     0 => Nothing0
 29 |     _ => Just0 (believe_me $ Refl {x})
 30 |
 31 | export
 32 | HDecEq Bits64 where
 33 |   hdecEq x y = case prim__eq_Bits64 x y of
 34 |     0 => Nothing0
 35 |     _ => Just0 (believe_me $ Refl {x})
 36 |
 37 | export
 38 | HDecEq Int8 where
 39 |   hdecEq x y = case prim__eq_Int8 x y of
 40 |     0 => Nothing0
 41 |     _ => Just0 (believe_me $ Refl {x})
 42 |
 43 | export
 44 | HDecEq Int16 where
 45 |   hdecEq x y = case prim__eq_Int16 x y of
 46 |     0 => Nothing0
 47 |     _ => Just0 (believe_me $ Refl {x})
 48 |
 49 | export
 50 | HDecEq Int32 where
 51 |   hdecEq x y = case prim__eq_Int32 x y of
 52 |     0 => Nothing0
 53 |     _ => Just0 (believe_me $ Refl {x})
 54 |
 55 | export
 56 | HDecEq Int64 where
 57 |   hdecEq x y = case prim__eq_Int64 x y of
 58 |     0 => Nothing0
 59 |     _ => Just0 (believe_me $ Refl {x})
 60 |
 61 | export
 62 | HDecEq Integer where
 63 |   hdecEq x y = case prim__eq_Integer x y of
 64 |     0 => Nothing0
 65 |     _ => Just0 (believe_me $ Refl {x})
 66 |
 67 | export
 68 | HDecEq Int where
 69 |   hdecEq x y = case prim__eq_Int x y of
 70 |     0 => Nothing0
 71 |     _ => Just0 (believe_me $ Refl {x})
 72 |
 73 | export
 74 | HDecEq Char where
 75 |   hdecEq x y = case prim__eq_Char x y of
 76 |     0 => Nothing0
 77 |     _ => Just0 (believe_me $ Refl {x})
 78 |
 79 | export
 80 | HDecEq String where
 81 |   hdecEq x y = case prim__eq_String x y of
 82 |     0 => Nothing0
 83 |     _ => Just0 (believe_me $ Refl {x})
 84 |
 85 | export
 86 | HDecEq a => HDecEq (Maybe a) where
 87 |   hdecEq Nothing Nothing   = Just0 Refl
 88 |   hdecEq (Just x) (Just y) = map (\x => cong Just x) (hdecEq x y)
 89 |   hdecEq _        _        = Nothing0
 90 |
 91 | export
 92 | HDecEq a => HDecEq b => HDecEq (Either a b) where
 93 |   hdecEq (Left x)  (Left y)  = map (\x => cong Left x) (hdecEq x y)
 94 |   hdecEq (Right x) (Right y) = map (\x => cong Right x) (hdecEq x y)
 95 |   hdecEq _        _          = Nothing0
 96 |
 97 | export
 98 | HDecEq a => HDecEq b => HDecEq (Pair a b) where
 99 |   hdecEq (x1,y1) (x2,y2) = case hdecEq x1 x2 of
100 |     Just0 r1 => case hdecEq y1 y2 of
101 |       Just0 r2 => Just0 (cong2 MkPair r1 r2)
102 |       Nothing0   => Nothing0
103 |     Nothing0 => Nothing0
104 |
105 | 0 eqNatToEqual : (x,y : Nat) -> (x == y) === True -> x === y
106 | eqNatToEqual 0 0         p = Refl
107 | eqNatToEqual (S k) (S m) p = cong S $ eqNatToEqual k m p
108 | eqNatToEqual Z     (S k) p impossible
109 | eqNatToEqual (S k) Z     p impossible
110 |
111 | hdecEqNat : (x,y : Nat) -> Maybe0 (x === y)
112 | hdecEqNat x y with (x == y) proof eq
113 |   _ | True  = Just0 (eqNatToEqual x y eq)
114 |   _ | False = Nothing0
115 |
116 | export %inline
117 | HDecEq Nat where
118 |   hdecEq = hdecEqNat
119 |
120 | export
121 | HDecEq a => HDecEq (List a) where
122 |   hdecEq [] [] = Just0 Refl
123 |   hdecEq (h1 :: t1) (h2 :: t2) = case hdecEq h1 h2 of
124 |     Just0 r1 => case hdecEq t1 t2 of
125 |       Just0 r2 => Just0 (cong2 (::) r1 r2)
126 |       Nothing0   => Nothing0
127 |     Nothing0 => Nothing0
128 |   hdecEq _ _ = Nothing0
129 |
130 | export
131 | (prf : All (HDecEq . f) ks) => HDecEq (All f ks) where
132 |   hdecEq [] [] = Just0 Refl
133 |   hdecEq {prf = _ :: _} (h1 :: t1) (h2 :: t2) = case hdecEq h1 h2 of
134 |     Just0 r1 => case hdecEq t1 t2 of
135 |       Just0 r2 => Just0 (cong2 (::) r1 r2)
136 |       Nothing0   => Nothing0
137 |     Nothing0 => Nothing0
138 |   hdecEq _ _ = Nothing0
139 |
140 | export
141 | (p : All (HDecEq . f) ks) => HDecEq (Any f ks) where
142 |   hdecEq {p = _ :: _} (Here x)  (Here y)  = map (\x => cong Here x) $ hdecEq x y
143 |   hdecEq {p = _ :: _} (There x) (There y) = map (\x => cong There x) $ hdecEq x y
144 |   hdecEq _ _ = Nothing0
145 |