{-# 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 :: BoolRepr a -> BoolRepr b -> BoolRepr c -> BoolRepr (If a b c)
ifRepr BoolRepr a
TrueRepr BoolRepr b
b BoolRepr c
_ = BoolRepr b
BoolRepr (If a b c)
b
ifRepr BoolRepr a
FalseRepr BoolRepr b
_ BoolRepr c
c = BoolRepr c
BoolRepr (If a b c)
c

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

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

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

instance Hashable (BoolRepr n) where
  hashWithSalt :: Int -> BoolRepr n -> Int
hashWithSalt Int
i BoolRepr n
TrueRepr  = Int -> Bool -> Int
forall a. Hashable a => Int -> a -> Int
hashWithSalt Int
i Bool
True
  hashWithSalt Int
i BoolRepr n
FalseRepr = Int -> Bool -> Int
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 :: BoolRepr a -> BoolRepr b -> Maybe (a :~: b)
testEquality BoolRepr a
TrueRepr BoolRepr b
TrueRepr   = (a :~: a) -> Maybe (a :~: a)
forall a. a -> Maybe a
Just a :~: a
forall k (a :: k). a :~: a
Refl
  testEquality BoolRepr a
FalseRepr BoolRepr b
FalseRepr = (a :~: a) -> Maybe (a :~: a)
forall a. a -> Maybe a
Just a :~: a
forall k (a :: k). a :~: a
Refl
  testEquality BoolRepr a
_ BoolRepr b
_ = Maybe (a :~: b)
forall a. Maybe a
Nothing

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

instance OrdF BoolRepr where
  compareF :: BoolRepr x -> BoolRepr y -> OrderingF x y
compareF BoolRepr x
TrueRepr  BoolRepr y
TrueRepr  = OrderingF x y
forall k (x :: k). OrderingF x x
EQF
  compareF BoolRepr x
FalseRepr BoolRepr y
FalseRepr = OrderingF x y
forall k (x :: k). OrderingF x x
EQF
  compareF BoolRepr x
TrueRepr  BoolRepr y
FalseRepr = OrderingF x y
forall k (x :: k) (y :: k). OrderingF x y
GTF
  compareF BoolRepr x
FalseRepr BoolRepr y
TrueRepr  = OrderingF x y
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 -> BoolRepr m :~: BoolRepr n
forall k (a :: k). a :~: a
Refl) ((m :~: n) -> BoolRepr m :~: BoolRepr n)
-> Maybe (m :~: n) -> Maybe (BoolRepr m :~: BoolRepr n)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> BoolRepr m -> BoolRepr n -> Maybe (m :~: n)
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 :: Int -> BoolRepr tp -> Int
hashWithSaltF = Int -> BoolRepr tp -> Int
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  = BoolRepr 'True -> Some BoolRepr
forall k (f :: k -> *) (x :: k). f x -> Some f
Some BoolRepr 'True
TrueRepr
someBool Bool
False = BoolRepr 'False -> Some BoolRepr
forall k (f :: k -> *) (x :: k). f x -> Some f
Some BoolRepr 'False
FalseRepr