1
1
mirror of https://github.com/idris-lang/Idris2.git synced 2024-12-21 10:41:59 +03:00
Idris2/libs/base/Decidable/Equality.idr

182 lines
6.9 KiB
Idris
Raw Normal View History

2020-05-18 15:59:07 +03:00
module Decidable.Equality
import Data.Maybe
import Data.Either
2020-05-18 15:59:07 +03:00
import Data.Nat
2020-06-30 04:18:40 +03:00
import Data.List
import Data.List1
2020-05-18 15:59:07 +03:00
import public Decidable.Equality.Core as Decidable.Equality
2020-05-18 15:59:07 +03:00
%default total
2020-05-18 15:59:07 +03:00
--------------------------------------------------------------------------------
--- Unit
--------------------------------------------------------------------------------
public export
2020-06-30 04:18:40 +03:00
DecEq () where
2020-05-18 15:59:07 +03:00
decEq () () = Yes Refl
--------------------------------------------------------------------------------
-- Booleans
--------------------------------------------------------------------------------
public export
2020-06-30 04:18:40 +03:00
DecEq Bool where
2020-05-18 15:59:07 +03:00
decEq True True = Yes Refl
decEq False False = Yes Refl
2020-06-30 04:18:40 +03:00
decEq False True = No absurd
decEq True False = No absurd
2020-05-18 15:59:07 +03:00
--------------------------------------------------------------------------------
-- Nat
--------------------------------------------------------------------------------
public export
2020-06-30 04:18:40 +03:00
DecEq Nat where
2020-05-18 15:59:07 +03:00
decEq Z Z = Yes Refl
2020-06-30 04:18:40 +03:00
decEq Z (S _) = No absurd
decEq (S _) Z = No absurd
2020-05-18 15:59:07 +03:00
decEq (S n) (S m) with (decEq n m)
decEq (S n) (S m) | Yes p = Yes $ cong S p
decEq (S n) (S m) | No p = No $ \h : (S n = S m) => p $ succInjective n m h
--------------------------------------------------------------------------------
-- Maybe
--------------------------------------------------------------------------------
public export
2020-06-30 04:18:40 +03:00
DecEq t => DecEq (Maybe t) where
2020-05-18 15:59:07 +03:00
decEq Nothing Nothing = Yes Refl
2020-06-30 04:18:40 +03:00
decEq Nothing (Just _) = No absurd
decEq (Just _) Nothing = No absurd
2020-05-18 15:59:07 +03:00
decEq (Just x') (Just y') with (decEq x' y')
decEq (Just x') (Just y') | Yes p = Yes $ cong Just p
decEq (Just x') (Just y') | No p
= No $ \h : Just x' = Just y' => p $ justInjective h
--------------------------------------------------------------------------------
-- Either
--------------------------------------------------------------------------------
public export
(DecEq t, DecEq s) => DecEq (Either t s) where
decEq (Left x) (Left y) with (decEq x y)
decEq (Left x) (Left x) | Yes Refl = Yes Refl
decEq (Left x) (Left y) | No contra = No (contra . leftInjective)
decEq (Left x) (Right y) = No absurd
decEq (Right x) (Left y) = No absurd
decEq (Right x) (Right y) with (decEq x y)
decEq (Right x) (Right x) | Yes Refl = Yes Refl
decEq (Right x) (Right y) | No contra = No (contra . rightInjective)
2020-05-18 15:59:07 +03:00
--------------------------------------------------------------------------------
-- Tuple
--------------------------------------------------------------------------------
2020-06-30 04:18:40 +03:00
pairInjective : (a, b) = (c, d) -> (a = c, b = d)
pairInjective Refl = (Refl, Refl)
2020-05-18 15:59:07 +03:00
public export
2020-06-30 04:18:40 +03:00
(DecEq a, DecEq b) => DecEq (a, b) where
decEq (a, b) (a', b') with (decEq a a')
decEq (a, b) (a', b') | (No contra) =
No $ contra . fst . pairInjective
decEq (a, b) (a, b') | (Yes Refl) with (decEq b b')
decEq (a, b) (a, b) | (Yes Refl) | (Yes Refl) = Yes Refl
decEq (a, b) (a, b') | (Yes Refl) | (No contra) =
No $ contra . snd . pairInjective
2020-05-18 15:59:07 +03:00
--------------------------------------------------------------------------------
-- List
--------------------------------------------------------------------------------
public export
2020-06-30 04:18:40 +03:00
DecEq a => DecEq (List a) where
2020-05-18 15:59:07 +03:00
decEq [] [] = Yes Refl
2020-06-30 04:18:40 +03:00
decEq (x :: xs) [] = No absurd
decEq [] (x :: xs) = No absurd
2020-05-18 15:59:07 +03:00
decEq (x :: xs) (y :: ys) with (decEq x y)
2020-06-30 04:18:40 +03:00
decEq (x :: xs) (y :: ys) | No contra =
No $ contra . fst . consInjective
2020-05-18 15:59:07 +03:00
decEq (x :: xs) (x :: ys) | Yes Refl with (decEq xs ys)
decEq (x :: xs) (x :: xs) | (Yes Refl) | (Yes Refl) = Yes Refl
2020-06-30 04:18:40 +03:00
decEq (x :: xs) (x :: ys) | (Yes Refl) | (No contra) =
No $ contra . snd . consInjective
--------------------------------------------------------------------------------
-- List1
--------------------------------------------------------------------------------
public export
DecEq a => DecEq (List1 a) where
decEq (x ::: xs) (y ::: ys) with (decEq x y)
decEq (x ::: xs) (y ::: ys) | No contra = No (contra . fst . consInjective)
decEq (x ::: xs) (y ::: ys) | Yes eqxy with (decEq xs ys)
decEq (x ::: xs) (y ::: ys) | Yes eqxy | No contra = No (contra . snd . consInjective)
decEq (x ::: xs) (y ::: ys) | Yes eqxy | Yes eqxsys = Yes (cong2 (:::) eqxy eqxsys)
2020-06-30 04:18:40 +03:00
-- TODO: Other prelude data types
-- For the primitives, we have to cheat because we don't have access to their
-- internal implementations. We use believe_me for the inequality proofs
-- because we don't them to reduce (and they should never be needed anyway...)
-- A postulate would be better, but erasure analysis may think they're needed
-- for computation in a higher order setting.
2020-05-18 15:59:07 +03:00
--------------------------------------------------------------------------------
-- Int
--------------------------------------------------------------------------------
public export
2020-05-18 15:59:07 +03:00
implementation DecEq Int where
decEq x y = case x == y of -- Blocks if x or y not concrete
True => Yes primitiveEq
False => No primitiveNotEq
where primitiveEq : forall x, y . x = y
primitiveEq = believe_me (Refl {x})
primitiveNotEq : forall x, y . x = y -> Void
primitiveNotEq prf = believe_me {b = Void} ()
--------------------------------------------------------------------------------
-- Char
--------------------------------------------------------------------------------
public export
2020-05-18 15:59:07 +03:00
implementation DecEq Char where
decEq x y = case x == y of -- Blocks if x or y not concrete
True => Yes primitiveEq
False => No primitiveNotEq
where primitiveEq : forall x, y . x = y
primitiveEq = believe_me (Refl {x})
primitiveNotEq : forall x, y . x = y -> Void
primitiveNotEq prf = believe_me {b = Void} ()
--------------------------------------------------------------------------------
-- Integer
--------------------------------------------------------------------------------
public export
2020-05-18 15:59:07 +03:00
implementation DecEq Integer where
decEq x y = case x == y of -- Blocks if x or y not concrete
True => Yes primitiveEq
False => No primitiveNotEq
where primitiveEq : forall x, y . x = y
primitiveEq = believe_me (Refl {x})
primitiveNotEq : forall x, y . x = y -> Void
primitiveNotEq prf = believe_me {b = Void} ()
--------------------------------------------------------------------------------
-- String
--------------------------------------------------------------------------------
public export
2020-05-18 15:59:07 +03:00
implementation DecEq String where
decEq x y = case x == y of -- Blocks if x or y not concrete
True => Yes primitiveEq
False => No primitiveNotEq
where primitiveEq : forall x, y . x = y
primitiveEq = believe_me (Refl {x})
primitiveNotEq : forall x, y . x = y -> Void
primitiveNotEq prf = believe_me {b = Void} ()