{-# LANGUAGE DataKinds           #-}
{-# LANGUAGE EmptyCase           #-}
{-# LANGUAGE FlexibleContexts    #-}
{-# LANGUAGE GADTs               #-}
{-# LANGUAGE PolyKinds           #-}
{-# LANGUAGE RankNTypes          #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeOperators       #-}
{-# OPTIONS_GHC -Wno-redundant-constraints #-}
-- | 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 Data.EqP  (EqP (..))
import Data.OrdP (OrdP (..))

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 = 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 :: forall r.
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 :: forall (b :: Bool) (proxy :: Bool -> *).
SBoolI b =>
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 :: forall (a :: Bool) (b :: Bool).
SBool a -> SBool b -> Maybe (a :~: b)
geq SBool a
STrue  SBool b
STrue  = (a :~: b) -> Maybe (a :~: b)
forall a. a -> Maybe a
Just a :~: a
a :~: b
forall {k} (a :: k). a :~: a
Refl
    geq SBool a
SFalse SBool b
SFalse = (a :~: b) -> Maybe (a :~: b)
forall a. a -> Maybe a
Just a :~: a
a :~: b
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 :: forall (a :: Bool) (b :: Bool). SBool a -> SBool b -> GOrdering a b
gcompare SBool a
SFalse SBool b
SFalse = GOrdering a a
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 a
GOrdering a b
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 = 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
        ]

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

-------------------------------------------------------------------------------
-- 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 (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 :~: b) -> Dec (a :~: b)
forall a. a -> Dec a
Yes a :~: a
a :~: b
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 :~: b) -> Dec (a :~: b)
forall a. a -> Dec a
Yes a :~: a
a :~: b
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
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 :: forall (a :: Bool) (b :: Bool).
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 :: forall (a :: Bool). 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 :: forall {k} (a :: k) (b :: k). ((a == b) ~ 'True) => a :~: b
eqToRefl = (() :~: ()) -> a :~: b
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 = a -> b
forall a b. a -> b
unsafeCoerce

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

-- | Useful combination of 'sbool' and 'eqToRefl'
--
-- @since 0.1.2.0
sboolEqRefl :: forall 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 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