{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE CPP #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE EmptyCase #-}
{-# LANGUAGE ExplicitNamespaces #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE PatternGuards #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE RoleAnnotations #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE UndecidableInstances #-}

module Data.Parameterized.BoolRepr
  ( module Data.Type.Bool
  , BoolRepr(..)
  , ifRepr, notRepr, (%&&), (%||)
  , KnownBool

  , someBool

  -- * Re-exports
  , TestEquality(..)
  , (:~:)(..)
  , Data.Parameterized.Some.Some
  )
where

import           Data.Parameterized.Classes
import           Data.Parameterized.DecidableEq
import           Data.Parameterized.Some

import           Data.Type.Bool

-- | A Boolean flag
data BoolRepr (b :: Bool) where
  FalseRepr :: BoolRepr 'False
  TrueRepr  :: BoolRepr 'True

-- | conditional
ifRepr :: BoolRepr a -> BoolRepr b -> BoolRepr c -> BoolRepr (If a b c)
ifRepr :: forall (a :: Bool) (b :: Bool) (c :: Bool).
BoolRepr a -> BoolRepr b -> BoolRepr c -> BoolRepr (If a b c)
ifRepr BoolRepr a
TrueRepr BoolRepr b
b BoolRepr c
_ = BoolRepr b
b
ifRepr BoolRepr a
FalseRepr BoolRepr b
_ BoolRepr c
c = BoolRepr c
c

-- | negation
notRepr :: BoolRepr b -> BoolRepr (Not b)
notRepr :: forall (b :: Bool). BoolRepr b -> BoolRepr (Not b)
notRepr BoolRepr b
TrueRepr = BoolRepr 'False
FalseRepr
notRepr BoolRepr b
FalseRepr = BoolRepr 'True
TrueRepr

-- | Conjunction
(%&&) :: BoolRepr a -> BoolRepr b -> BoolRepr (a && b)
BoolRepr a
FalseRepr %&& :: forall (a :: Bool) (b :: Bool).
BoolRepr a -> BoolRepr b -> BoolRepr (a && b)
%&& BoolRepr b
_ = BoolRepr 'False
FalseRepr
BoolRepr a
TrueRepr  %&& BoolRepr b
a = BoolRepr b
a
infixr 3 %&&

-- | Disjunction
(%||) :: BoolRepr a -> BoolRepr b -> BoolRepr (a || b)
BoolRepr a
FalseRepr %|| :: forall (a :: Bool) (b :: Bool).
BoolRepr a -> BoolRepr b -> BoolRepr (a || b)
%|| BoolRepr b
a = BoolRepr b
a
BoolRepr a
TrueRepr  %|| BoolRepr b
_ = BoolRepr 'True
TrueRepr
infixr 2 %||

instance Hashable (BoolRepr n) where
  hashWithSalt :: Int -> BoolRepr n -> Int
hashWithSalt Int
i BoolRepr n
TrueRepr  = forall a. Hashable a => Int -> a -> Int
hashWithSalt Int
i Bool
True
  hashWithSalt Int
i BoolRepr n
FalseRepr = forall a. Hashable a => Int -> a -> Int
hashWithSalt Int
i Bool
False


instance Eq (BoolRepr m) where
  BoolRepr m
_ == :: BoolRepr m -> BoolRepr m -> Bool
== BoolRepr m
_ = Bool
True

instance TestEquality BoolRepr where
  testEquality :: forall (a :: Bool) (b :: Bool).
BoolRepr a -> BoolRepr b -> Maybe (a :~: b)
testEquality BoolRepr a
TrueRepr BoolRepr b
TrueRepr   = forall a. a -> Maybe a
Just forall {k} (a :: k). a :~: a
Refl
  testEquality BoolRepr a
FalseRepr BoolRepr b
FalseRepr = forall a. a -> Maybe a
Just forall {k} (a :: k). a :~: a
Refl
  testEquality BoolRepr a
_ BoolRepr b
_ = forall a. Maybe a
Nothing

instance DecidableEq BoolRepr where
  decEq :: forall (a :: Bool) (b :: Bool).
BoolRepr a -> BoolRepr b -> Either (a :~: b) ((a :~: b) -> Void)
decEq BoolRepr a
TrueRepr  BoolRepr b
TrueRepr  = forall a b. a -> Either a b
Left forall {k} (a :: k). a :~: a
Refl
  decEq BoolRepr a
FalseRepr BoolRepr b
FalseRepr = forall a b. a -> Either a b
Left forall {k} (a :: k). a :~: a
Refl
  decEq BoolRepr a
TrueRepr  BoolRepr b
FalseRepr = forall a b. b -> Either a b
Right forall a b. (a -> b) -> a -> b
$ \case {}
  decEq BoolRepr a
FalseRepr BoolRepr b
TrueRepr  = forall a b. b -> Either a b
Right forall a b. (a -> b) -> a -> b
$ \case {}

instance OrdF BoolRepr where
  compareF :: forall (x :: Bool) (y :: Bool).
BoolRepr x -> BoolRepr y -> OrderingF x y
compareF BoolRepr x
TrueRepr  BoolRepr y
TrueRepr  = forall {k} (x :: k). OrderingF x x
EQF
  compareF BoolRepr x
FalseRepr BoolRepr y
FalseRepr = forall {k} (x :: k). OrderingF x x
EQF
  compareF BoolRepr x
TrueRepr  BoolRepr y
FalseRepr = forall {k} (x :: k) (y :: k). OrderingF x y
GTF
  compareF BoolRepr x
FalseRepr BoolRepr y
TrueRepr  = forall {k} (x :: k) (y :: k). OrderingF x y
LTF

instance PolyEq (BoolRepr m) (BoolRepr n) where
  polyEqF :: BoolRepr m -> BoolRepr n -> Maybe (BoolRepr m :~: BoolRepr n)
polyEqF BoolRepr m
x BoolRepr n
y = (\m :~: n
Refl -> forall {k} (a :: k). a :~: a
Refl) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall {k} (f :: k -> *) (a :: k) (b :: k).
TestEquality f =>
f a -> f b -> Maybe (a :~: b)
testEquality BoolRepr m
x BoolRepr n
y

instance Show (BoolRepr m) where
  show :: BoolRepr m -> String
show BoolRepr m
FalseRepr = String
"FalseRepr"
  show BoolRepr m
TrueRepr  = String
"TrueRepr"

instance ShowF BoolRepr

instance HashableF BoolRepr where
  hashWithSaltF :: forall (n :: Bool). Int -> BoolRepr n -> Int
hashWithSaltF = forall a. Hashable a => Int -> a -> Int
hashWithSalt

----------------------------------------------------------
-- * Implicit runtime booleans

type KnownBool = KnownRepr BoolRepr

instance KnownRepr BoolRepr 'True where
  knownRepr :: BoolRepr 'True
knownRepr = BoolRepr 'True
TrueRepr
instance KnownRepr BoolRepr 'False where
  knownRepr :: BoolRepr 'False
knownRepr = BoolRepr 'False
FalseRepr

someBool :: Bool -> Some BoolRepr
someBool :: Bool -> Some BoolRepr
someBool Bool
True  = forall k (f :: k -> *) (x :: k). f x -> Some f
Some BoolRepr 'True
TrueRepr
someBool Bool
False = forall k (f :: k -> *) (x :: k). f x -> Some f
Some BoolRepr 'False
FalseRepr