-- For `(<)`
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE Safe #-}
-- For `axiom`
{-# OPTIONS_GHC -Wno-deprecations #-}

module Logic.Theory.Ord (
  -- * Lower than
  type (<),
  (<),

  -- * Lower or equal
  type (<=),
  (<=),

  -- * Greater than
  type (>),
  (>),

  -- * Greater or equal
  type (>=),
  (>=),

  -- * Compare
  type Compare (),
  compare,
  type CompareProof (..),
) where

import Control.Applicative ((<*>))
import Data.Bool (Bool)
import Data.Bool qualified as Bool
import Data.Either (Either (..))
import Data.Functor ((<$>))
import Data.Ord qualified as Ord

import Logic.Kernel
import Logic.Theory.Bool
import Logic.Theory.Eq

data (<) x y = LowerThanAxiom
data (<=) x y = LowerOrEqualAxiom
data (>) x y = GreaterThanAxiom
data (>=) x y = GreaterOrEqualAxiom
data Compare x y = Compare

type role (<) nominal nominal
type role (<=) nominal nominal
type role (>) nominal nominal
type role (>=) nominal nominal
type role Compare nominal nominal

infix 4 <
infix 4 <=
infix 4 >
infix 4 >=
infix 4 `Compare`

instance Axiom (x <= y <-> (x < y || x == y))
instance Axiom (x >= y <-> (x > y || x == y))
instance Axiom (x <= y && x >= y <-> x == y)

instance Axiom (x <= y <-> Not (x > y))
instance Axiom (x < y <-> Not (x >= y))
instance Axiom (x >= y <-> Not (x < y))
instance Axiom (x > y <-> Not (x <= y))

instance Axiom (x < y -> Not (x == y))
instance Axiom (x > y -> Not (x == y))

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 GreaterThanAxiom)
    Bool.True -> Right (proven LowerOrEqualAxiom)

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 GreaterOrEqualAxiom)
    Bool.True -> Right (proven LowerThanAxiom)

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 LowerThanAxiom)
    Bool.True -> Right (proven GreaterOrEqualAxiom)

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 LowerOrEqualAxiom)
    Bool.True -> Right (proven GreaterThanAxiom)

(<=) :: Ord.Ord a => x ::: a -> y ::: a -> (x <= y) ::: Bool
(<=) (Named x) (Named y) = LowerOrEqualAxiom ... x Ord.<= y

(<) :: Ord.Ord a => x ::: a -> y ::: a -> (x < y) ::: Bool
(<) (Named x) (Named y) = LowerThanAxiom ... x Ord.< y

(>=) :: Ord.Ord a => x ::: a -> y ::: a -> (x >= y) ::: Bool
(>=) (Named x) (Named y) = GreaterOrEqualAxiom ... x Ord.>= y

(>) :: Ord.Ord a => x ::: a -> y ::: a -> (x > y) ::: Bool
(>) (Named x) (Named y) = GreaterThanAxiom ... x Ord.> y

data CompareProof x y
  = CompareProofLT (Proof (x < y))
  | CompareProofEQ (Proof (x == y))
  | CompareProofGT (Proof (x > y))
data OrdEq x y = OrdEqAxiom
instance Axiom (OrdEq x y <-> (==) x y)

compare :: Ord.Ord a => x ::: a -> y ::: a -> Compare x y ::: Ord.Ordering
compare (Named x) (Named y) = Compare ... Ord.compare x y

instance Provable (Compare x y ::: Ord.Ordering) where
  type ProofOf (Compare x y ::: Ord.Ordering) = CompareProof x y
  prove (Named o) = case o of
    Ord.LT -> CompareProofLT (proven LowerThanAxiom)
    Ord.EQ -> CompareProofEQ ((-->) <$> axiom @(OrdEq x y <-> (==) x y) <*> proven OrdEqAxiom)
    Ord.GT -> CompareProofGT (proven GreaterThanAxiom)

-- instance Axiom (x ::: Int == y ::: Int <-> Forall (z:::Int) (z <= x <-> z <= y))