0 | module Decidable.Equality

  2 | import Control.Function

  3 | import Data.Maybe

  4 | import Data.Either

  5 | import Data.Nat

  6 | import Data.List

  7 | import Data.List1

  8 | import Data.List1.Properties

  9 | import Data.SnocList

 10 | import Data.These

 12 | import public Decidable.Equality.Core as Decidable.Equality

 14 | %default total

 20 | public export

 21 | DecEq () where

 22 |   decEq () () = Yes Refl

 28 | public export

 29 | DecEq Bool where

 30 |   decEq True  True  = Yes Refl

 31 |   decEq False False = Yes Refl

 32 |   decEq False True  = No absurd

 33 |   decEq True  False = No absurd

 39 | public export

 40 | DecEq Nat where

 41 |   decEq Z     Z     = Yes Refl

 42 |   decEq (S n) (S m) = decEqCong $ decEq n m

 43 |   decEq Z     (S _) = No absurd

 44 |   decEq (S _) Z     = No absurd

 50 | public export

 51 | DecEq t => DecEq (Maybe t) where

 52 |   decEq Nothing Nothing = Yes Refl

 53 |   decEq (Just x) (Just y) = decEqCong $ decEq x y

 54 |   decEq Nothing (Just _) = No absurd

 55 |   decEq (Just _) Nothing = No absurd

 61 | public export

 62 | (DecEq t, DecEq s) => DecEq (Either t s) where

 63 |   decEq (Left x)  (Left y)  = decEqCong $ decEq x y

 64 |   decEq (Right x) (Right y) = decEqCong $ decEq x y

 65 |   decEq (Left x) (Right y) = No absurd

 66 |   decEq (Right x) (Left y) = No absurd

 72 | public export

 73 | DecEq t => DecEq s => DecEq (These t s) where

 74 |   decEq (This x) (This y) = decEqCong $ decEq x y

 75 |   decEq (That x) (That y) = decEqCong $ decEq x y

 76 |   decEq (Both x z) (Both y w) = decEqCong2 (decEq x y) (decEq z w)

 77 |   decEq (This x)   (That y)    = No $ \case Refl impossible

 78 |   decEq (This x)   (Both y z)  = No $ \case Refl impossible

 79 |   decEq (That x)   (This y)    = No $ \case Refl impossible

 80 |   decEq (That x)   (Both y z)  = No $ \case Refl impossible

 81 |   decEq (Both x z) (This y)    = No $ \case Refl impossible

 82 |   decEq (Both x z) (That y)    = No $ \case Refl impossible

 88 | pairInjective : (a, b) = (c, d) -> (a = c, b = d)

 89 | pairInjective Refl = (Refl, Refl)

 91 | public export

 92 | (DecEq a, DecEq b) => DecEq (a, b) where

 93 |   decEq (a, b) (a', b') = decEqCong2 (decEq a a') (decEq b b')

 99 | public export

100 | DecEq a => DecEq (List a) where

101 |   decEq [] [] = Yes Refl

102 |   decEq (x :: xs) [] = No absurd

103 |   decEq [] (x :: xs) = No absurd

104 |   decEq (x :: xs) (y :: ys) = decEqCong2 (decEq x y) (decEq xs ys)

110 | public export

111 | DecEq a => DecEq (List1 a) where

112 |   decEq (x ::: xs) (y ::: ys) = decEqCong2 (decEq x y) (decEq xs ys)

118 | public export

119 | DecEq a => DecEq (SnocList a) where

120 |   decEq Lin Lin = Yes Refl

121 |   decEq (xs :< x) Lin = No absurd

122 |   decEq Lin (xs :< x) = No absurd

123 |   decEq (xs :< x) (ys :< y) = decEqCong2 (decEq xs ys) (decEq x y)

136 | public export

137 | [FromEq] Eq a => DecEq a where

138 |     decEq x y = case x == y of -- Blocks if x or y not concrete

139 |                      True => Yes primitiveEq

140 |                      False => No primitiveNotEq

141 |        where primitiveEq : forall x, y . x = y

142 |              primitiveEq = believe_me (Refl {x})

143 |              primitiveNotEq : forall x, y . Not (x = y)

144 |              primitiveNotEq prf = believe_me {b = Void} ()

150 | public export

151 | DecEq Int where

152 |     decEq = decEq @{FromEq}

158 | public export

159 | DecEq Bits8 where

160 |     decEq = decEq @{FromEq}

166 | public export

167 | DecEq Bits16 where

168 |     decEq = decEq @{FromEq}

174 | public export

175 | DecEq Bits32 where

176 |     decEq = decEq @{FromEq}

182 | public export

183 | DecEq Bits64 where

184 |     decEq = decEq @{FromEq}

190 | public export

191 | DecEq Int8 where

192 |     decEq = decEq @{FromEq}

198 | public export

199 | DecEq Int16 where

200 |     decEq = decEq @{FromEq}

206 | public export

207 | DecEq Int32 where

208 |     decEq = decEq @{FromEq}

214 | public export

215 | DecEq Int64 where

216 |     decEq = decEq @{FromEq}

221 | public export

222 | DecEq Char where

223 |     decEq = decEq @{FromEq}

228 | public export

229 | DecEq Integer where

230 |     decEq = decEq @{FromEq}

235 | public export

236 | DecEq String where

237 |     decEq = decEq @{FromEq}