{-# LANGUAGE DataKinds, DeriveDataTypeable, EmptyCase, ExplicitForAll     #-}
{-# LANGUAGE ExplicitNamespaces, FlexibleInstances, GADTs, KindSignatures #-}
{-# LANGUAGE LambdaCase, PolyKinds, RankNTypes, StandaloneDeriving        #-}
{-# LANGUAGE TemplateHaskell, TypeOperators                               #-}
{-# OPTIONS_GHC -fno-warn-orphans #-}
-- | Provides type synonyms for logical connectives.
module Proof.Propositional
       ( type (/\), type (\/), Not, exfalso, orIntroL
       , orIntroR, orElim, andIntro, andElimL
       , andElimR, orAssocL, orAssocR
       , andAssocL, andAssocR, IsTrue(..), withWitness
       , Empty(..), withEmpty, withEmpty'
       , refute
       , Inhabited (..), withInhabited
       , prove
       ) where
import Proof.Propositional.Empty
import Proof.Propositional.Inhabited
import Proof.Propositional.TH

import Data.Data          (Data)
import Data.Type.Equality ((:~:))
import Data.Typeable      (Typeable)
import Data.Void
import Unsafe.Coerce

type a /\ b = (a, b)
type a \/ b = Either a b
type Not a  = a -> Void

infixr 2 \/
infixr 3 /\

exfalso :: a -> Not a -> b
exfalso :: a -> Not a -> b
exfalso a
a Not a
neg = Void -> b
forall a. Void -> a
absurd (Not a
neg a
a)

orIntroL :: a -> a \/ b
orIntroL :: a -> a \/ b
orIntroL = a -> a \/ b
forall a b. a -> Either a b
Left

orIntroR :: b -> a \/ b
orIntroR :: b -> a \/ b
orIntroR = b -> a \/ b
forall a b. b -> Either a b
Right

orElim :: a \/ b -> (a -> c) -> (b -> c) -> c
orElim :: (a \/ b) -> (a -> c) -> (b -> c) -> c
orElim a \/ b
aORb a -> c
aTOc b -> c
bTOc = (a -> c) -> (b -> c) -> (a \/ b) -> c
forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either a -> c
aTOc b -> c
bTOc a \/ b
aORb

andIntro :: a -> b -> a /\ b
andIntro :: a -> b -> a /\ b
andIntro = (,)

andElimL :: a /\ b -> a
andElimL :: (a /\ b) -> a
andElimL = (a /\ b) -> a
forall a b. (a, b) -> a
fst

andElimR :: a /\ b -> b
andElimR :: (a /\ b) -> b
andElimR = (a /\ b) -> b
forall a b. (a, b) -> b
snd

andAssocL :: a /\ (b /\ c) -> (a /\ b) /\ c
andAssocL :: (a /\ (b /\ c)) -> (a /\ b) /\ c
andAssocL (a
a,(b
b,c
c)) = ((a
a,b
b), c
c)

andAssocR :: (a /\ b) /\ c -> a /\ (b /\ c)
andAssocR :: ((a /\ b) /\ c) -> a /\ (b /\ c)
andAssocR ((a
a,b
b),c
c) = (a
a,(b
b,c
c))

orAssocL :: a \/ (b \/ c) -> (a \/ b) \/ c
orAssocL :: (a \/ (b \/ c)) -> (a \/ b) \/ c
orAssocL (Left a
a)          = (a \/ b) -> (a \/ b) \/ c
forall a b. a -> Either a b
Left (a -> a \/ b
forall a b. a -> Either a b
Left a
a)
orAssocL (Right (Left b
b))  = (a \/ b) -> (a \/ b) \/ c
forall a b. a -> Either a b
Left (b -> a \/ b
forall a b. b -> Either a b
Right b
b)
orAssocL (Right (Right c
c)) = c -> (a \/ b) \/ c
forall a b. b -> Either a b
Right c
c

orAssocR :: (a \/ b) \/ c -> a \/ (b \/ c)
orAssocR :: ((a \/ b) \/ c) -> a \/ (b \/ c)
orAssocR (Left (Left a
a))  = a -> a \/ (b \/ c)
forall a b. a -> Either a b
Left a
a
orAssocR (Left (Right b
b)) = (b \/ c) -> a \/ (b \/ c)
forall a b. b -> Either a b
Right (b -> b \/ c
forall a b. a -> Either a b
Left b
b)
orAssocR (Right c
c)        = (b \/ c) -> a \/ (b \/ c)
forall a b. b -> Either a b
Right (c -> b \/ c
forall a b. b -> Either a b
Right c
c)


-- | Utility type to convert type-level (@'Bool'@-valued) predicate function
--   into concrete witness data-type.
data IsTrue (b :: Bool) where
  Witness :: IsTrue 'True

withWitness :: IsTrue b -> (b ~ 'True => r) -> r
withWitness :: IsTrue b -> ((b ~ 'True) => r) -> r
withWitness IsTrue b
Witness (b ~ 'True) => r
r = r
(b ~ 'True) => r
r
{-# NOINLINE withWitness #-}
{-# RULES
"withWitness/coercion" [~1] forall x.
  withWitness x = unsafeCoerce
  #-}

deriving instance Show (IsTrue b)
deriving instance Eq   (IsTrue b)
deriving instance Ord  (IsTrue b)
deriving instance Read (IsTrue 'True)
deriving instance Typeable IsTrue
deriving instance Data (IsTrue 'True)

instance {-# OVERLAPPABLE #-} (Inhabited a, Empty b) => Empty (a -> b) where
  eliminate :: (a -> b) -> x
eliminate a -> b
f = b -> x
forall a x. Empty a => a -> x
eliminate (a -> b
f a
forall a. Inhabited a => a
trivial)

refute [t| 0 :~: 1 |]
refute [t| () :~: Int |]
refute [t| 'True :~: 'False |]
refute [t| 'False :~: 'True |]
refute [t| 'LT :~: 'GT |]
refute [t| 'LT :~: 'EQ |]
refute [t| 'EQ :~: 'LT |]
refute [t| 'EQ :~: 'GT |]
refute [t| 'GT :~: 'LT |]
refute [t| 'GT :~: 'EQ |]

prove [t| Bool |]
prove [t| Int |]
prove [t| Integer |]
prove [t| Word |]
prove [t| Double |]
prove [t| Float |]
prove [t| Char |]
prove [t| Ordering |]
prove [t| forall a. [a] |]
prove [t| Rational |]
prove [t| forall a. Maybe a |]
prove [t| forall n. n :~: n |]
prove [t| IsTrue 'True |]

instance Empty (IsTrue 'False) where
  eliminate :: IsTrue 'False -> x
eliminate = \ case {}