module Darcs.Patch.Witnesses.Eq
    ( EqCheck(..)
    , Eq2(..)
    , isIsEq
    ) where

import Darcs.Prelude

import Darcs.Patch.Witnesses.Unsafe ( unsafeCoerceP )

-- |'EqCheck' is used to pass around evidence (or lack thereof) of
-- two witness types being equal.
data EqCheck wA wB where
    IsEq :: EqCheck wA wA
    NotEq :: EqCheck wA wB

instance Eq (EqCheck wA wB) where
    EqCheck wA wB
IsEq == :: EqCheck wA wB -> EqCheck wA wB -> Bool
== EqCheck wA wB
IsEq = Bool
True
    EqCheck wA wB
NotEq == EqCheck wA wB
NotEq = Bool
True
    EqCheck wA wB
_ == EqCheck wA wB
_ = Bool
False

instance Show (EqCheck wA wB) where
    show :: EqCheck wA wB -> String
show EqCheck wA wB
IsEq = String
"IsEq"
    show EqCheck wA wB
NotEq = String
"NotEq"

-- |An witness aware equality class.
-- A minimal definition defines any one of 'unsafeCompare', '=\/=' and '=/\='.
class Eq2 p where
    -- |It is unsafe to define a class instance via this method, because
    -- if it returns True then the default implementations of '=\/=' and '=/\='
    -- will coerce the equality of two witnesses.
    --
    -- Calling this method is safe, although '=\/=' or '=/\=' would be better
    -- choices as it is not usually meaningul to compare two patches that
    -- don't share either a starting or an ending context
    unsafeCompare :: p wA wB -> p wC wD -> Bool
    unsafeCompare p wA wB
a p wC wD
b = EqCheck wA wA
forall wA. EqCheck wA wA
IsEq EqCheck wA wA -> EqCheck wA wA -> Bool
forall a. Eq a => a -> a -> Bool
== (p wA wB
a p wA wB -> p wA wB -> EqCheck wA wA
forall (p :: * -> * -> *) wA wC wB.
Eq2 p =>
p wA wC -> p wB wC -> EqCheck wA wB
=/\= p wC wD -> p wA wB
forall (a :: * -> * -> *) wX wY wB wC. a wX wY -> a wB wC
unsafeCoerceP p wC wD
b)

    -- |Compare two things with the same starting witness. If the things
    -- compare equal, evidence of the ending witnesses being equal will
    -- be returned.
    (=\/=) :: p wA wB -> p wA wC -> EqCheck wB wC
    p wA wB
a =\/= p wA wC
b | p wA wB -> p wA wC -> Bool
forall (p :: * -> * -> *) wA wB wC wD.
Eq2 p =>
p wA wB -> p wC wD -> Bool
unsafeCompare p wA wB
a p wA wC
b = EqCheck Any Any -> EqCheck wB wC
forall (a :: * -> * -> *) wX wY wB wC. a wX wY -> a wB wC
unsafeCoerceP EqCheck Any Any
forall wA. EqCheck wA wA
IsEq
             | Bool
otherwise = EqCheck wB wC
forall wA wB. EqCheck wA wB
NotEq

    -- |Compare two things with the same ending witness. If the things
    -- compare equal, evidence of the starting witnesses being equal will
    -- be returned.
    (=/\=) :: p wA wC -> p wB wC -> EqCheck wA wB
    p wA wC
a =/\= p wB wC
b | EqCheck wC wC
forall wA. EqCheck wA wA
IsEq EqCheck wC wC -> EqCheck wC wC -> Bool
forall a. Eq a => a -> a -> Bool
== (p wA wC
a p wA wC -> p wA wC -> EqCheck wC wC
forall (p :: * -> * -> *) wA wB wC.
Eq2 p =>
p wA wB -> p wA wC -> EqCheck wB wC
=\/= p wB wC -> p wA wC
forall (a :: * -> * -> *) wX wY wB wC. a wX wY -> a wB wC
unsafeCoerceP p wB wC
b) = EqCheck Any Any -> EqCheck wA wB
forall (a :: * -> * -> *) wX wY wB wC. a wX wY -> a wB wC
unsafeCoerceP EqCheck Any Any
forall wA. EqCheck wA wA
IsEq
             | Bool
otherwise = EqCheck wA wB
forall wA wB. EqCheck wA wB
NotEq

infix 4 =\/=, =/\=

isIsEq :: EqCheck wA wB -> Bool
isIsEq :: EqCheck wA wB -> Bool
isIsEq EqCheck wA wB
IsEq = Bool
True
isIsEq EqCheck wA wB
NotEq = Bool
False