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

#if MIN_VERSION_some(1,0,5)
import Data.EqP  (EqP (..))
import Data.OrdP (OrdP (..))
#endif

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 :: forall (b :: Bool). 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 :: forall r. Bool -> (forall (b :: Bool). SBool b -> r) -> r
withSomeSBool Bool
True  forall (b :: Bool). SBool b -> r
f = forall (b :: Bool). SBool b -> r
f SBool 'True
STrue
withSomeSBool Bool
False forall (b :: Bool). SBool b -> r
f = 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 :: forall r.
Bool -> (forall (b :: Bool). SBoolI b => Proxy b -> r) -> r
reifyBool Bool
True  forall (b :: Bool). SBoolI b => Proxy b -> r
f = forall (b :: Bool). SBoolI b => Proxy b -> r
f (forall {k} (t :: k). Proxy t
Proxy :: Proxy 'True)
reifyBool Bool
False forall (b :: Bool). SBoolI b => Proxy b -> r
f = forall (b :: Bool). SBoolI b => Proxy b -> r
f (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 :: forall (b :: Bool) (proxy :: Bool -> *).
SBoolI b =>
proxy b -> Bool
reflectBool proxy b
_ = forall (b :: Bool). SBool b -> Bool
fromSBool (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 = 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 :: forall (a :: Bool) (b :: Bool).
SBool a -> SBool b -> Maybe (a :~: b)
geq SBool a
STrue  SBool b
STrue  = forall a. a -> Maybe a
Just forall {k} (a :: k). a :~: a
Refl
    geq SBool a
SFalse SBool b
SFalse = forall a. a -> Maybe a
Just forall {k} (a :: k). a :~: a
Refl
    geq SBool a
_      SBool b
_      = forall a. Maybe a
Nothing

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

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

-- |
--
-- >>> showsPrec 0 STrue ""
-- "STrue"
--
-- @since 0.1.6
instance GShow SBool where
    gshowsPrec :: forall (b :: Bool). Int -> SBool b -> ShowS
gshowsPrec = 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 =
        [ (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
        ]
        forall a. [a] -> [a] -> [a]
++
        [ (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
        ]

#if MIN_VERSION_some(1,0,5)
-- | @since 0.1.7
instance EqP SBool where
    eqp :: forall (a :: Bool) (b :: Bool). SBool a -> SBool b -> Bool
eqp SBool a
STrue  SBool b
STrue  = Bool
True
    eqp SBool a
SFalse SBool b
SFalse = Bool
True
    eqp SBool a
_      SBool b
_      = Bool
False

-- | @since 0.1.7
instance OrdP SBool where
    comparep :: forall (a :: Bool) (b :: Bool). SBool a -> SBool b -> Ordering
comparep SBool a
STrue  SBool b
STrue  = Ordering
EQ
    comparep SBool a
SFalse SBool b
SFalse = Ordering
EQ
    comparep SBool a
STrue  SBool b
SFalse = Ordering
GT
    comparep SBool a
SFalse SBool b
STrue  = Ordering
LT
#endif

-------------------------------------------------------------------------------
-- 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 :: forall (a :: Bool) (b :: Bool).
(SBoolI a, SBoolI b) =>
Dec (a :~: b)
discreteBool = case (forall (b :: Bool). SBoolI b => SBool b
sbool :: SBool a, forall (b :: Bool). SBoolI b => SBool b
sbool :: SBool b) of
    (SBool a
STrue,  SBool b
STrue)  -> forall a. a -> Dec a
Yes forall {k} (a :: k). a :~: a
Refl
    (SBool a
STrue,  SBool b
SFalse) -> forall a. Neg a -> Dec a
No forall a b. (a -> b) -> a -> b
$ \a :~: b
p  -> case a :~: b
p of {}
    (SBool a
SFalse, SBool b
STrue)  -> forall a. Neg a -> Dec a
No forall a b. (a -> b) -> a -> b
$ \a :~: b
p  -> case a :~: b
p of {}
    (SBool a
SFalse, SBool b
SFalse) -> forall a. a -> Dec a
Yes forall {k} (a :: k). a :~: a
Refl

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

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

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

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

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

-- | @since 0.1.1.0
eqCast :: (a == b) ~ 'True => a -> b
eqCast :: forall a b. ((a == b) ~ 'True) => a -> b
eqCast = 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 :: forall k (a :: k) (b :: k). SBoolI (a == b) => Maybe (a :~: b)
sboolEqRefl = case forall (b :: Bool). SBoolI b => SBool b
sbool :: SBool (a == b) of
    SBool (a == b)
STrue  -> forall a. a -> Maybe a
Just forall {k} (a :: k) (b :: k). ((a == b) ~ 'True) => a :~: b
eqToRefl
    SBool (a == b)
SFalse -> forall a. Maybe a
Nothing