{-# LANGUAGE Safe #-}
-- For `axiom`
{-# OPTIONS_GHC -Wno-deprecations #-}
{-# OPTIONS_GHC -Wno-orphans #-}
{-# OPTIONS_GHC -Wno-unused-top-binds #-}

module Logic.Theory.Bool (
  true,
  implies,
  unImplies,
  type True,
  type False,
  type (&&),
  andL,
  andR,
  unAnd,
  type (||),
  type UnOr,
  runOr,
  leftOr,
  rightOr,
  unOr,
  unOrL,
  unOrR,
  type Not (),
  type NotAsNonExistent,
  modusTollens,
  absurd,
  and,
  not,
  type NonContradiction,
  contradicts,
  type ExcludedMiddle,
)
where

import Control.Applicative (Applicative (..), liftA3)
import Control.Monad (Monad (..))
import Data.Either (Either (..), either)
import Data.Function (id, (.))
import Data.Functor ((<$>))
import Data.Tuple (fst, snd)
import Data.Void (Void)
import Data.Void qualified as Void

import Logic.Kernel

true :: Proof True
true = pure ()
{-# INLINE true #-}

type False = Void

-- | From a falsity, prove anything.
-- (aka. ex falso quodlibet).
absurd :: False -> p
absurd = Void.absurd
{-# INLINE absurd #-}

type True = ()

-- The conjunction in the logic side,
-- is the product type in the programming side.
type (&&) = (,)
infixl 3 &&

and :: Proof p -> Proof q -> Proof (p && q)
and = liftA2 (,)
{-# INLINE and #-}

andL :: Proof (p && q) -> Proof p
andL = (<$>) fst

andR :: Proof (p && q) -> Proof q
andR = (<$>) snd

unAnd :: Proof (p && q) -> (Proof p, Proof q)
unAnd c = (andL c, andR c)

-- The disjunction in the logic side,
-- is the sum type in the programming side.
type (||) = Either
infixl 2 ||

leftOr :: Proof p -> Proof (p || q)
leftOr = (<$>) Left

rightOr :: Proof q -> Proof (p || q)
rightOr = (<$>) Right

type UnOr p q r = (p -> r) -> (q -> r) -> (p || q) -> r
instance Lemma (UnOr p q r) where
  lemma = pure runOr

runOr :: UnOr p q r
runOr = either

unOr :: (Proof p -> Proof r) -> (Proof q -> Proof r) -> Proof (p || q) -> Proof r
unOr p2r q2r = (>>= either (p2r . pure) (q2r . pure))

unOrL :: (Proof p -> Proof r) -> Proof (p || q) -> (Proof q -> Proof r) -> Proof r
unOrL p2r poq q2r = unOr p2r q2r poq

unOrR :: (Proof q -> Proof r) -> Proof (p || q) -> (Proof p -> Proof r) -> Proof r
unOrR q2r poq p2r = unOr p2r q2r poq

-- | CorrectnessNote: the existence of a construction of @(`Not` p)@ is much stronger
-- than the non-existence of a construction of @(p)@.
newtype Not p = Not ()

-- | A construction of @(`Not` p)@, treated like @(p `->` `False`)@,
-- is an algorithm that, from a (hypothetical) construction of @(p)@
-- produces a non-existent object.
type NotAsNonExistent p = Not p <-> (p -> False)

instance Axiom (NotAsNonExistent p)

-- | contraprositive
not :: (Proof p -> Proof False) -> Proof (Not p)
not f = liftA2 (<--) (axiom @(NotAsNonExistent _)) (implies f)
{-# INLINE not #-}

modusTollens :: Proof (p -> q) -> Proof (Not q) -> Proof (Not p)
modusTollens p2qP nqP = not (contradicts nqP . unImplies p2qP)
{-# INLINE modusTollens #-}

-- | Non contradiction
type NonContradiction p = Not (p && Not p)

instance Axiom (NonContradiction p)

contradicts :: Proof (Not p) -> Proof p -> Proof False
contradicts = liftA3 (-->) (axiom @(NotAsNonExistent _))
{-# INLINE contradicts #-}

-- `RefHoTTBook`:
-- > It has been known for a long time, however, that principles such as AC and LEM are fundamentally
-- > antithetical to computability, since they assert baldly that certain things exist without giving any
-- > way to compute them. Thus, avoiding them is necessary to maintain the character of type theory
-- > as a theory of computation.

-- Intuitionistic logic rejects excluded middle (and the many equivalent rules)
type ExcludedMiddle p = p || Not p

type Contradiction p = (Not p -> False) -> p
instance Axiom (ExcludedMiddle p) => Lemma (Contradiction p) where
  lemma = (\em np2f -> runOr id (absurd . np2f) em) <$> axiom @(ExcludedMiddle p)