--------------------------------------------------------------------------------
--------------------------------------------------------------------------------
--Module       : Type.Logic
--Author       : Daniel Schüssler
--License      : BSD3
--Copyright    : Daniel Schüssler
--
--Maintainer   : Daniel Schüssler
--Stability    : Experimental
--Portability  : Uses various GHC extensions
--
--------------------------------------------------------------------------------
--Description  : 
--------------------------------------------------------------------------------
--------------------------------------------------------------------------------

{-# LANGUAGE EmptyDataDecls #-}
{-# LANGUAGE DeriveDataTypeable #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE TypeSynonymInstances #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE IncoherentInstances #-}


-- |
--
-- Propositions as types (of kind @*@), proofs as values
--
module Type.Logic where
    
import Data.Type.Equality
import Control.Monad.Cont
import Data.Typeable
import Data.Monoid hiding(All)
import Control.Exception

newtype Falsity = Falsity { elimFalsity :: forall a. a }
    deriving Typeable

data Truth = TruthProof
           deriving (Show,Typeable)
                    
instance Show Falsity where show _ = error "show: Proof of Falsity used"

type Not a = a -> Falsity
    
instance Typeable a => (Show (a -> Falsity)) where 
    show _ = "<< proof of falsity from " ++ show (typeOf (undefined :: a)) ++ " >>"
    
        
       
-- | This class collects lemmas. It plays no foundational role.
class Fact a where
    auto :: a
           
-- -- | Priority 1 facts
-- class Fact1 a where
--     auto1 :: a
            
-- instance Fact1 a => Fact a where
--     auto = auto1


instance Fact Truth where
    auto = TruthProof

instance Fact (Falsity -> a) where
    auto = elimFalsity

instance Fact ((a,b) -> a) where
    auto = fst

instance Fact ((a,b) -> b) where
    auto = snd

instance (Fact a, Fact b) => Fact (a,b) where
    auto = (auto, auto)
           
instance Fact (a -> Either a b) where
    auto = Left

instance Fact (b -> Either a b) where
    auto = Right

instance (Fact (a -> c), Fact (b -> c)) => Fact (Either a b -> c) where
    auto = either auto auto

instance Fact (a -> Not (Not a)) where
    auto p q = q p
               
               
data Decidable a = Decidable { decide :: Either (Not a) a }
                 deriving (Show,Typeable)
             
instance Fact (Decidable Falsity) where
    auto = Decidable (Left id)
             
instance Fact (Decidable Truth) where
    auto = Decidable (Right TruthProof)

instance Fact (Decidable a -> Decidable b -> Decidable (a,b)) where
    auto p1 p2 = Decidable (case (decide p1,decide p2) of
                              (Right p, Right q) -> Right (p,q)
                              (Left p, _) -> Left (p . fst)
                              (_, Left q) -> Left (q . snd)
                           )

instance Fact (Decidable a -> Decidable b -> Decidable (Either a b)) where
    auto p1 p2 = Decidable (case (decide p1,decide p2) of
                              (Left p, Left q) -> Left (either p q)
                              (Right p, _) -> Right (Left p)
                              (_, Right q) -> Right (Right q)
                           )

instance Fact (Decidable a -> Decidable b -> Decidable (a -> b)) where
    auto p1 p2 = Decidable (case decide p2 of
                              Right q -> Right (const q)
                              Left q -> case decide p1 of
                                         Right p -> Left (\f -> q (f p))
                                         Left p -> Right (elimFalsity . p)
                           )

instance Fact (Decidable a -> Decidable (Not a)) where
    auto p1 = Decidable (case decide p1 of
                           Right p -> Left ($p)
                           Left p -> Right p
                        )

-- isLeft :: Either t t1 -> Bool
-- isLeft (Left _) = True
-- isLeft (Right _) = False

-- isRight = not . isLeft


           
    
-- instance Show (a :=: b) where show Refl = "Refl"

-- | Existential quantification                                                         
data Ex p where
    Ex :: forall b. p b -> Ex p
         
         


exElim :: forall p r. (forall b. p b -> r) -> Ex p -> r
exElim k (Ex prf) = k prf
                        
instance (Fact (p a)) => Fact (Ex p) where auto = Ex (auto :: (p a))

-- | Universal quantification
newtype All p = All { allElim :: forall b. p b }

instance Fact (All p -> p b) where auto = allElim
    

-- | Unique existence
data ExUniq p where
    ExUniq :: p b -> (forall b'. p b' -> b :=: b') -> ExUniq p
               
instance Fact (ExUniq p -> Ex p) where
    auto (ExUniq p _) = Ex p
                        
instance Fact (ExUniq p -> p b -> p b' -> b :=: b') where
    auto (ExUniq _ uniq) pb pb' = 
        case (uniq pb, uniq pb') of
          (Refl,Refl) -> Refl


type COr r a b = Cont r (Either a b)

lem :: COr r (a -> r) a
lem = Cont (\k -> k (Left (\a -> k (Right a))))

elimCor :: COr r a b -> (a -> r) -> (b -> r) -> r
elimCor (Cont x) k1 k2 = x (either k1 k2) 
                       


deriving instance Typeable2 (:=:)
instance Show (a :=: b) where show Refl = "Refl"