--------------------------------------------------------------------------------
--------------------------------------------------------------------------------
--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 Control.Exception
import Control.Monad.Trans.Cont
import Data.Functor.Identity
import Data.Monoid hiding(All)
import Data.Type.Equality
import Data.Typeable

    
-- class Prop p where
--     proofs :: [p]
-- instance (Prop a, Prop b) => Prop (Either a b) where
--     proofs = diagonal [ fmap Left proofs, fmap Right proofs ]
             
-- instance (Prop a, Prop b) => Prop (a, b) where
--     proofs = liftM2 (,) proofs proofs
             
-- instance (Prop a, Prop b) => Prop (a -> b) where
--     proofs = case

newtype Falsity = Falsity { elimFalsity :: forall a. a }
    deriving Typeable
             
-- instance Prop Falsity where proofs = []
                                     
-- instance Show Falsity where show _ = error "show: Proof of Falsity used"


data Truth = TruthProof
           deriving (Show,Typeable)
                    
-- instance Prop Truth where proofs = [TruthProof]
                    

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"

class Decidable a where decide :: Either (Not a) a
             
instance (Decidable Falsity) where
    decide = (Left id)
             
instance (Decidable Truth) where
    decide = (Right TruthProof)

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

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

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

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









-- | Existential quantification                                                         
data Ex p where
    Ex :: 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 = ContT (\k -> k (Left (\a -> (runIdentity . k . Right) a)))

elimCor :: COr r a b -> (a -> r) -> (b -> r) -> r
elimCor (ContT x) k1 k2 = (runIdentity . x) (Identity . either k1 k2) 
                       


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


class Decidable1 s where
    decide1 :: Either (Not (s a)) (s a)

class Finite s where
    enum :: [Ex s]

instance Finite s => Decidable (Ex s) where
    decide = case enum of
               [] -> Left (\_ -> Falsity (assert False undefined))
               [x] -> Right x

-- instance Finite s => Decidable (Ex s) where
--     decide = case enum of
--                [] -> Left (\_ -> Falsity (assert False undefined))
--                [x] -> Right x