-- For `(==)`
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE Safe #-}

module Logic.Theory.Eq (
  type (==) (),
  type (/=) (),
  (==),
  (/=),
) where

import Data.Bool (Bool)
import Data.Bool qualified as Bool
import Data.Either (Either (..))
import Data.Eq qualified as Eq
import Logic.Kernel

data (==) x y = EqualAxiom
data (/=) x y = NotEqualAxiom

type role (==) nominal nominal
type role (/=) nominal nominal

instance Axiom (Associative (==) x y z)
instance Axiom (Associative (/=) x y z)
instance Axiom (Commutative (==) x y)
instance Axiom (Commutative (/=) x y)

(==) :: Eq.Eq a => x ::: a -> y ::: a -> (x == y) ::: Bool
(==) (Named x) (Named y) = EqualAxiom ... x Eq.== y
{-# INLINE (==) #-}

(/=) :: Eq.Eq a => x ::: a -> y ::: a -> (x /= y) ::: Bool
(/=) (Named x) (Named y) = NotEqualAxiom ... x Eq./= y
{-# INLINE (/=) #-}

infix 4 ==
infix 4 /=

instance Provable ((x == y) ::: Bool) where
  type ProofOf ((x == y) ::: Bool) = Either (Proof (x /= y)) (Proof (x == y))
  prove (Named b) = case b of
    Bool.False -> Left (proven NotEqualAxiom)
    Bool.True -> Right (proven EqualAxiom)

instance Provable ((x /= y) ::: Bool) where
  type ProofOf ((x /= y) ::: Bool) = Either (Proof (x == y)) (Proof (x /= y))
  prove (Named b) = case b of
    Bool.False -> Left (proven EqualAxiom)
    Bool.True -> Right (proven NotEqualAxiom)