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

#if MIN_VERSION_base(4,7,0)
import           Data.Type.Bool
import           Data.Type.Dec      (Dec (..))
import           Data.Type.Equality
import           Unsafe.Coerce      (unsafeCoerce)
#endif

import Data.Proxy (Proxy (..))

-- $setup
-- >>> :set -XDataKinds -XTypeOperators
-- >>> import Data.Type.Dec (decShow)

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

-------------------------------------------------------------------------------
-- 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)

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

#if MIN_VERSION_base(4,7,0)
-- | 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
#endif

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

#if MIN_VERSION_base(4,7,0)
-- | >>> 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
#endif