{-# LANGUAGE UndecidableInstances #-}

-- |
-- Module        : Data.Bool.Kill
-- Copyright     : Gautier DI FOLCO
-- License       : ISC
--
-- Maintainer    : Gautier DI FOLCO <gautier.difolco@gmail.com>
-- Stability     : Unstable
-- Portability   : not portable
--
-- Strongly-typed booleans
--
-- Example:
--
-- > type TT = TBool "missing" "present"
-- >
-- > isPresent :: TT
-- > isPresent = mkIs $ Proxy @"present"
-- >
-- > is (Proxy @"missing") isPresent == False
module Data.Bool.Kill
  ( TBool (..),
    is,
    isNot,
    mkIs,
    mkTBool,
    ShouldBe,
    ShouldBeVal,

    -- * Reexport
    Proxy (..),
  )
where

import Data.Kind
import Data.Proxy
import GHC.TypeLits

-- | Strongly-typed 'Bool'
data TBool (false :: Symbol) (true :: Symbol)
  = IsFalse
  | IsTrue

instance (KnownSymbol f, KnownSymbol t) => Show (TBool f t) where
  show :: TBool f t -> String
show =
    \case
      TBool f t
IsTrue -> String
"True (" forall a. Semigroup a => a -> a -> a
<> forall (n :: Symbol) (proxy :: Symbol -> *).
KnownSymbol n =>
proxy n -> String
symbolVal (forall {k} (t :: k). Proxy t
Proxy @t) forall a. Semigroup a => a -> a -> a
<> String
")"
      TBool f t
IsFalse -> String
"False (" forall a. Semigroup a => a -> a -> a
<> forall (n :: Symbol) (proxy :: Symbol -> *).
KnownSymbol n =>
proxy n -> String
symbolVal (forall {k} (t :: k). Proxy t
Proxy @f) forall a. Semigroup a => a -> a -> a
<> String
")"

-- | Check "if 'True'"
is :: forall b f t. ShouldBeVal (ShouldBe (TBool f t) b) => Proxy b -> TBool f t -> Bool
is :: forall (b :: Symbol) (f :: Symbol) (t :: Symbol).
ShouldBeVal (ShouldBe (TBool f t) b) =>
Proxy b -> TBool f t -> Bool
is Proxy b
_ = forall a (t :: Symbol) (f :: Symbol).
ShouldBeVal a =>
Proxy a -> TBool t f -> Bool
is' (forall {k} (t :: k). Proxy t
Proxy @(ShouldBe (TBool f t) b))

-- | Check "if 'False'"
isNot :: forall b f t. ShouldBeVal (ShouldBe (TBool f t) b) => Proxy b -> TBool f t -> Bool
isNot :: forall (b :: Symbol) (f :: Symbol) (t :: Symbol).
ShouldBeVal (ShouldBe (TBool f t) b) =>
Proxy b -> TBool f t -> Bool
isNot Proxy b
_ = Bool -> Bool
not forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a (t :: Symbol) (f :: Symbol).
ShouldBeVal a =>
Proxy a -> TBool t f -> Bool
is' (forall {k} (t :: k). Proxy t
Proxy @(ShouldBe (TBool f t) b))

-- | Create 'True'/'False' from its name
mkIs :: forall b f t. ShouldBeVal (ShouldBe (TBool f t) b) => Proxy b -> TBool f t
mkIs :: forall (b :: Symbol) (f :: Symbol) (t :: Symbol).
ShouldBeVal (ShouldBe (TBool f t) b) =>
Proxy b -> TBool f t
mkIs Proxy b
_ = forall a (t :: Symbol) (f :: Symbol).
ShouldBeVal a =>
Proxy a -> TBool t f
mkIs' forall a b. (a -> b) -> a -> b
$ forall {k} (t :: k). Proxy t
Proxy @(ShouldBe (TBool f t) b)

-- | Create 'TBool' from 'Bool'
mkTBool :: forall f t. Bool -> TBool f t
mkTBool :: forall (f :: Symbol) (t :: Symbol). Bool -> TBool f t
mkTBool Bool
p = if Bool
p then forall (false :: Symbol) (true :: Symbol). TBool false true
IsTrue else forall (false :: Symbol) (true :: Symbol). TBool false true
IsFalse

data TTrue = TTrue deriving (Int -> TTrue -> ShowS
[TTrue] -> ShowS
TTrue -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [TTrue] -> ShowS
$cshowList :: [TTrue] -> ShowS
show :: TTrue -> String
$cshow :: TTrue -> String
showsPrec :: Int -> TTrue -> ShowS
$cshowsPrec :: Int -> TTrue -> ShowS
Show)

data TFalse = TFalse deriving (Int -> TFalse -> ShowS
[TFalse] -> ShowS
TFalse -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [TFalse] -> ShowS
$cshowList :: [TFalse] -> ShowS
show :: TFalse -> String
$cshow :: TFalse -> String
showsPrec :: Int -> TFalse -> ShowS
$cshowsPrec :: Int -> TFalse -> ShowS
Show)

type family ShouldBe (tbool :: Type) (a :: Symbol) :: Type where
  ShouldBe (TBool f t) t = TTrue
  ShouldBe (TBool f t) f = TFalse
  ShouldBe (TBool f t) o = TypeError ('Text "Cannot find " ':$$: 'ShowType o ':$$: 'Text " valid choices are " ':$$: 'ShowType f ':$$: 'Text " and " ':$$: 'ShowType t)

class ShouldBeVal a where
  is' :: Proxy a -> TBool t f -> Bool
  mkIs' :: Proxy a -> TBool t f

instance ShouldBeVal TTrue where
  is' :: forall (t :: Symbol) (f :: Symbol).
Proxy TTrue -> TBool t f -> Bool
is' Proxy TTrue
_ =
    \case
      TBool t f
IsTrue -> Bool
True
      TBool t f
IsFalse -> Bool
False
  mkIs' :: forall (t :: Symbol) (f :: Symbol). Proxy TTrue -> TBool t f
mkIs' Proxy TTrue
_ = forall (false :: Symbol) (true :: Symbol). TBool false true
IsTrue

instance ShouldBeVal TFalse where
  is' :: forall (t :: Symbol) (f :: Symbol).
Proxy TFalse -> TBool t f -> Bool
is' Proxy TFalse
_ =
    \case
      TBool t f
IsTrue -> Bool
False
      TBool t f
IsFalse -> Bool
True
  mkIs' :: forall (t :: Symbol) (f :: Symbol). Proxy TFalse -> TBool t f
mkIs' Proxy TFalse
_ = forall (false :: Symbol) (true :: Symbol). TBool false true
IsFalse