{-# LANGUAGE CPP                 #-}
{-# LANGUAGE DataKinds           #-}
{-# LANGUAGE EmptyCase           #-}
{-# LANGUAGE FlexibleContexts    #-}
{-# LANGUAGE GADTs               #-}
{-# LANGUAGE PolyKinds           #-}
{-# LANGUAGE RankNTypes          #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeOperators       #-}
#if __GLASGOW_HASKELL__ >= 800
{-# OPTIONS_GHC -Wno-redundant-constraints #-}
#endif
-- | Additions to "Data.Type.Bool".
module Data.Singletons.Bool (
    SBool(..),
    SBoolI(..),
    fromSBool,
    withSomeSBool,
    reflectBool,
    reifyBool,
    -- * Data.Type.Dec
    -- | 'discreteBool' is available with @base >= 4.7@ (GHC-7.8)
    discreteBool,
    -- * Data.Type.Bool and .Equality
    -- | These are only defined with @base >= 4.7@
    sboolAnd, sboolOr, sboolNot,
    eqToRefl, eqCast, sboolEqRefl,
    trivialRefl,
    ) where

import Control.DeepSeq    (NFData (..))
import Data.Boring        (Boring (..))
import Data.GADT.Compare  (GCompare (..), GEq (..), GOrdering (..))
import Data.GADT.DeepSeq  (GNFData (..))
import Data.GADT.Show     (GRead (..), GShow (..))
import Data.Proxy         (Proxy (..))
import Data.Type.Bool
import Data.Type.Dec      (Dec (..))
import Data.Type.Equality
import Unsafe.Coerce      (unsafeCoerce)

import qualified Data.Some.Church as Church

-- $setup
-- >>> :set -XDataKinds -XTypeOperators
-- >>> import Data.Proxy (Proxy (..))
-- >>> import Data.Type.Dec
-- >>> import Data.Some
-- >>> import Data.GADT.Compare
-- >>> import Data.GADT.Show
-- >>> import Data.Type.Equality

data SBool (b :: Bool) where
    STrue  :: SBool 'True
    SFalse :: SBool 'False

class    SBoolI (b :: Bool) where sbool :: SBool b
instance SBoolI 'True       where sbool :: SBool 'True
sbool = SBool 'True
STrue
instance SBoolI 'False      where sbool :: SBool 'False
sbool = SBool 'False
SFalse

-- | @since 0.1.5
instance Show (SBool b) where
    showsPrec :: Int -> SBool b -> ShowS
showsPrec Int
_ SBool b
STrue  = String -> ShowS
showString String
"STrue"
    showsPrec Int
_ SBool b
SFalse = String -> ShowS
showString String
"SFalse"

-- | @since 0.1.5
instance Eq (SBool b) where
    SBool b
_ == :: SBool b -> SBool b -> Bool
== SBool b
_ = Bool
True

-- | @since 0.1.5
instance Ord (SBool b) where
    compare :: SBool b -> SBool b -> Ordering
compare SBool b
_ SBool b
_ = Ordering
EQ

-- | @since 0.1.6
instance NFData (SBool b) where
    rnf :: SBool b -> ()
rnf SBool b
STrue  = ()
    rnf SBool b
SFalse = ()

-------------------------------------------------------------------------------
-- conversion to and from explicit SBool values
-------------------------------------------------------------------------------

-- | Convert an 'SBool' to the corresponding 'Bool'.
--
-- @since 0.1.4
fromSBool :: SBool b -> Bool
fromSBool :: SBool b -> Bool
fromSBool SBool b
STrue  = Bool
True
fromSBool SBool b
SFalse = Bool
False

-- | Convert a normal 'Bool' to an 'SBool', passing it into a continuation.
--
-- >>> withSomeSBool True fromSBool
-- True
--
-- @since 0.1.4
withSomeSBool :: Bool -> (forall b. SBool b -> r) -> r
withSomeSBool :: Bool -> (forall (b :: Bool). SBool b -> r) -> r
withSomeSBool Bool
True  forall (b :: Bool). SBool b -> r
f = SBool 'True -> r
forall (b :: Bool). SBool b -> r
f SBool 'True
STrue
withSomeSBool Bool
False forall (b :: Bool). SBool b -> r
f = SBool 'False -> r
forall (b :: Bool). SBool b -> r
f SBool 'False
SFalse

-------------------------------------------------------------------------------
-- reify & reflect
-------------------------------------------------------------------------------

-- | Reify 'Bool' to type-level.
--
-- >>> reifyBool True reflectBool
-- True
--
reifyBool :: forall r. Bool -> (forall b. SBoolI b => Proxy b -> r) -> r
reifyBool :: Bool -> (forall (b :: Bool). SBoolI b => Proxy b -> r) -> r
reifyBool Bool
True  forall (b :: Bool). SBoolI b => Proxy b -> r
f = Proxy 'True -> r
forall (b :: Bool). SBoolI b => Proxy b -> r
f (Proxy 'True
forall k (t :: k). Proxy t
Proxy :: Proxy 'True)
reifyBool Bool
False forall (b :: Bool). SBoolI b => Proxy b -> r
f = Proxy 'False -> r
forall (b :: Bool). SBoolI b => Proxy b -> r
f (Proxy 'False
forall k (t :: k). Proxy t
Proxy :: Proxy 'False)

-- | Reflect to term-level.
--
-- >>> reflectBool (Proxy :: Proxy 'True)
-- True
reflectBool :: forall b proxy. SBoolI b => proxy b -> Bool
reflectBool :: proxy b -> Bool
reflectBool proxy b
_ = SBool b -> Bool
forall (b :: Bool). SBool b -> Bool
fromSBool (SBool b
forall (b :: Bool). SBoolI b => SBool b
sbool :: SBool b)

-------------------------------------------------------------------------------
-- Boring
-------------------------------------------------------------------------------

-- | @since 0.1.6
instance SBoolI b => Boring (SBool b) where
    boring :: SBool b
boring = SBool b
forall (b :: Bool). SBoolI b => SBool b
sbool

-------------------------------------------------------------------------------
-- Data.GADT (some)
-------------------------------------------------------------------------------

-- |
--
-- >>> geq STrue STrue
-- Just Refl
--
-- >>> geq STrue SFalse
-- Nothing
--
-- @since 0.1.6
instance GEq SBool where
    geq :: SBool a -> SBool b -> Maybe (a :~: b)
geq SBool a
STrue  SBool b
STrue  = (a :~: a) -> Maybe (a :~: a)
forall a. a -> Maybe a
Just a :~: a
forall k (a :: k). a :~: a
Refl
    geq SBool a
SFalse SBool b
SFalse = (a :~: a) -> Maybe (a :~: a)
forall a. a -> Maybe a
Just a :~: a
forall k (a :: k). a :~: a
Refl
    geq SBool a
_      SBool b
_      = Maybe (a :~: b)
forall a. Maybe a
Nothing

-- |
--
-- @since 0.1.6
instance GCompare SBool where
    gcompare :: SBool a -> SBool b -> GOrdering a b
gcompare SBool a
SFalse SBool b
SFalse = GOrdering a b
forall k (a :: k). GOrdering a a
GEQ
    gcompare SBool a
SFalse SBool b
STrue  = GOrdering a b
forall k (a :: k) (b :: k). GOrdering a b
GLT
    gcompare SBool a
STrue  SBool b
SFalse = GOrdering a b
forall k (a :: k) (b :: k). GOrdering a b
GGT
    gcompare SBool a
STrue  SBool b
STrue  = GOrdering a b
forall k (a :: k). GOrdering a a
GEQ

-- | @since 0.1.6
instance GNFData SBool where
    grnf :: SBool a -> ()
grnf SBool a
STrue  = ()
    grnf SBool a
SFalse = ()

-- |
--
-- >>> showsPrec 0 STrue ""
-- "STrue"
--
-- @since 0.1.6
instance GShow SBool where
    gshowsPrec :: Int -> SBool a -> ShowS
gshowsPrec = Int -> SBool a -> ShowS
forall a. Show a => Int -> a -> ShowS
showsPrec

-- |
--
-- >>> readsPrec 0 "Some STrue" :: [(Some SBool, String)]
-- [(Some STrue,"")]
--
-- >>> readsPrec 0 "Some SFalse" :: [(Some SBool, String)]
-- [(Some SFalse,"")]
--
-- >>> readsPrec 0 "Some Else" :: [(Some SBool, String)]
-- []
--
-- @since 0.1.6
instance GRead SBool where
    greadsPrec :: Int -> GReadS SBool
greadsPrec Int
_ String
s =
        [ (SBool 'True -> Some SBool
forall k (tag :: k -> *) (a :: k). tag a -> Some tag
Church.mkSome SBool 'True
STrue, String
t)
        | (String
"STrue", String
t) <- ReadS String
lex String
s
        ]
        [(Some SBool, String)]
-> [(Some SBool, String)] -> [(Some SBool, String)]
forall a. [a] -> [a] -> [a]
++
        [ (SBool 'False -> Some SBool
forall k (tag :: k -> *) (a :: k). tag a -> Some tag
Church.mkSome SBool 'False
SFalse, String
t)
        | (String
"SFalse", String
t) <- ReadS String
lex String
s
        ]

-------------------------------------------------------------------------------
-- Discrete
-------------------------------------------------------------------------------

-- | Decidable equality.
--
-- >>> decShow (discreteBool :: Dec ('True :~: 'True))
-- "Yes Refl"
--
-- @since 0.1.5
discreteBool :: forall a b. (SBoolI a, SBoolI b) => Dec (a :~: b)
discreteBool :: Dec (a :~: b)
discreteBool = case (SBool a
forall (b :: Bool). SBoolI b => SBool b
sbool :: SBool a, SBool b
forall (b :: Bool). SBoolI b => SBool b
sbool :: SBool b) of
    (SBool a
STrue,  SBool b
STrue)  -> (a :~: a) -> Dec (a :~: a)
forall a. a -> Dec a
Yes a :~: a
forall k (a :: k). a :~: a
Refl
    (SBool a
STrue,  SBool b
SFalse) -> Neg (a :~: b) -> Dec (a :~: b)
forall a. Neg a -> Dec a
No (Neg (a :~: b) -> Dec (a :~: b)) -> Neg (a :~: b) -> Dec (a :~: b)
forall a b. (a -> b) -> a -> b
$ \a :~: b
p  -> case a :~: b
p of {}
    (SBool a
SFalse, SBool b
STrue)  -> Neg (a :~: b) -> Dec (a :~: b)
forall a. Neg a -> Dec a
No (Neg (a :~: b) -> Dec (a :~: b)) -> Neg (a :~: b) -> Dec (a :~: b)
forall a b. (a -> b) -> a -> b
$ \a :~: b
p  -> case a :~: b
p of {}
    (SBool a
SFalse, SBool b
SFalse) -> (a :~: a) -> Dec (a :~: a)
forall a. a -> Dec a
Yes a :~: a
forall k (a :: k). a :~: a
Refl

-------------------------------------------------------------------------------
-- Witnesses
-------------------------------------------------------------------------------

-- | >>> sboolAnd STrue SFalse
-- SFalse
sboolAnd :: SBool a -> SBool b -> SBool (a && b)
sboolAnd :: SBool a -> SBool b -> SBool (a && b)
sboolAnd SBool a
SFalse SBool b
_ = SBool 'False
SBool (a && b)
SFalse
sboolAnd SBool a
STrue  SBool b
b = SBool b
SBool (a && b)
b

sboolOr :: SBool a -> SBool b -> SBool (a || b)
sboolOr :: SBool a -> SBool b -> SBool (a || b)
sboolOr SBool a
STrue  SBool b
_ = SBool 'True
SBool (a || b)
STrue
sboolOr SBool a
SFalse SBool b
b = SBool b
SBool (a || b)
b

sboolNot :: SBool a -> SBool (Not a)
sboolNot :: SBool a -> SBool (Not a)
sboolNot SBool a
STrue  = SBool 'False
SBool (Not a)
SFalse
sboolNot SBool a
SFalse = SBool 'True
SBool (Not a)
STrue

-- | @since 0.1.1.0
eqToRefl :: (a == b) ~ 'True => a :~: b
eqToRefl :: a :~: b
eqToRefl = (() :~: ()) -> a :~: b
forall a b. a -> b
unsafeCoerce () :~: ()
trivialRefl

-- | @since 0.1.1.0
eqCast :: (a == b) ~ 'True => a -> b
eqCast :: a -> b
eqCast = a -> b
forall a b. a -> b
unsafeCoerce

-- | @since 0.1.1.0
trivialRefl :: () :~: ()
trivialRefl :: () :~: ()
trivialRefl = () :~: ()
forall k (a :: k). a :~: a
Refl

-- GHC 8.10+ requires that all kind variables be explicitly quantified after
-- a `forall`. Technically, GHC has had the ability to do this since GHC 8.0,
-- but GHC 8.0-8.4 require enabling TypeInType to do. To avoid having to faff
-- around with CPP to enable TypeInType on certain GHC versions, we only
-- explicitly quantify kind variables on GHC 8.6 or later, since those versions
-- do not require TypeInType, only PolyKinds.
# if __GLASGOW_HASKELL__ >= 806
#  define KVS(kvs) kvs
# else
#  define KVS(kvs)
# endif

-- | Useful combination of 'sbool' and 'eqToRefl'
--
-- @since 0.1.2.0
sboolEqRefl :: forall KVS(k) (a :: k) (b :: k). SBoolI (a == b) => Maybe (a :~: b)
sboolEqRefl :: Maybe (a :~: b)
sboolEqRefl = case SBool (a == b)
forall (b :: Bool). SBoolI b => SBool b
sbool :: SBool (a == b) of
    SBool (a == b)
STrue  -> (a :~: b) -> Maybe (a :~: b)
forall a. a -> Maybe a
Just a :~: b
forall k (a :: k) (b :: k). ((a == b) ~ 'True) => a :~: b
eqToRefl
    SBool (a == b)
SFalse -> Maybe (a :~: b)
forall a. Maybe a
Nothing