{-# LANGUAGE Safe #-}
{-# LANGUAGE ScopedTypeVariables #-}
module Data.Type.Dec (
Neg,
Dec (..),
Decidable (..),
toNegNeg,
tripleNeg,
contradict,
contraposition,
decNeg,
decShow,
decToMaybe,
decToBool,
boringYes,
absurdNo,
) where
import Data.Void (Void)
import Data.Boring (Absurd (..), Boring (..))
type Neg a = a -> Void
data Dec a
= Yes a
| No (Neg a)
class Decidable a where
decide :: Dec a
instance Decidable () where
decide :: Dec ()
decide = () -> Dec ()
forall a. a -> Dec a
Yes ()
instance Decidable Void where
decide :: Dec Void
decide = Neg Void -> Dec Void
forall a. Neg a -> Dec a
No Neg Void
forall a. a -> a
id
instance (Decidable a, Decidable b) => Decidable (a, b) where
decide :: Dec (a, b)
decide = case Dec a
forall a. Decidable a => Dec a
decide :: Dec a of
No Neg a
nx -> Neg (a, b) -> Dec (a, b)
forall a. Neg a -> Dec a
No (\(a, b)
c -> Neg a
nx ((a, b) -> a
forall a b. (a, b) -> a
fst (a, b)
c))
Yes a
x -> case Dec b
forall a. Decidable a => Dec a
decide :: Dec b of
No Neg b
ny -> Neg (a, b) -> Dec (a, b)
forall a. Neg a -> Dec a
No (\(a, b)
c -> Neg b
ny ((a, b) -> b
forall a b. (a, b) -> b
snd (a, b)
c))
Yes b
y -> (a, b) -> Dec (a, b)
forall a. a -> Dec a
Yes (a
x, b
y)
toNegNeg :: a -> Neg (Neg a)
toNegNeg :: forall a. a -> Neg (Neg a)
toNegNeg a
x = ((a -> Void) -> a -> Void
forall a b. (a -> b) -> a -> b
$ a
x)
tripleNeg :: Neg (Neg (Neg a)) -> Neg a
tripleNeg :: forall a. Neg (Neg (Neg a)) -> Neg a
tripleNeg Neg (Neg (Neg a))
f a
a = Neg (Neg (Neg a))
f (a -> Neg (Neg a)
forall a. a -> Neg (Neg a)
toNegNeg a
a)
contradict :: (a -> Neg b) -> b -> Neg a
contradict :: forall a b. (a -> Neg b) -> b -> Neg a
contradict a -> Neg b
f b
b a
a = a -> Neg b
f a
a b
b
contraposition :: (a -> b) -> Neg b -> Neg a
contraposition :: forall a b. (a -> b) -> Neg b -> Neg a
contraposition a -> b
f Neg b
nb a
a = Neg b
nb (a -> b
f a
a)
instance Eq a => Eq (Dec a) where
Yes a
x == :: Dec a -> Dec a -> Bool
== Yes a
y = a
x a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== a
y
Yes a
_ == No Neg a
_ = Bool
False
No Neg a
_ == Yes a
_ = Bool
False
No Neg a
_ == No Neg a
_ = Bool
True
instance Ord a => Ord (Dec a) where
compare :: Dec a -> Dec a -> Ordering
compare (Yes a
a) (Yes a
b) = a -> a -> Ordering
forall a. Ord a => a -> a -> Ordering
compare a
a a
b
compare (No Neg a
_) (Yes a
_) = Bool -> Bool -> Ordering
forall a. Ord a => a -> a -> Ordering
compare Bool
False Bool
True
compare (Yes a
_) (No Neg a
_) = Bool -> Bool -> Ordering
forall a. Ord a => a -> a -> Ordering
compare Bool
True Bool
False
compare (No Neg a
_) (No Neg a
_) = Ordering
EQ
decNeg :: Dec a -> Dec (Neg a)
decNeg :: forall a. Dec a -> Dec (Neg a)
decNeg (Yes a
p) = Neg (Neg a) -> Dec (Neg a)
forall a. Neg a -> Dec a
No (a -> Neg (Neg a)
forall a. a -> Neg (Neg a)
toNegNeg a
p)
decNeg (No Neg a
np) = Neg a -> Dec (Neg a)
forall a. a -> Dec a
Yes Neg a
np
decShow :: Show a => Dec a -> String
decShow :: forall a. Show a => Dec a -> String
decShow (Yes a
x) = String
"Yes " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> a -> String -> String
forall a. Show a => Int -> a -> String -> String
showsPrec Int
11 a
x String
""
decShow (No Neg a
_) = String
"No <toVoid>"
decToMaybe :: Dec a -> Maybe a
decToMaybe :: forall a. Dec a -> Maybe a
decToMaybe (Yes a
p) = a -> Maybe a
forall a. a -> Maybe a
Just a
p
decToMaybe (No Neg a
_) = Maybe a
forall a. Maybe a
Nothing
decToBool :: Dec a -> Bool
decToBool :: forall a. Dec a -> Bool
decToBool (Yes a
_) = Bool
True
decToBool (No Neg a
_) = Bool
False
instance Decidable a => Boring (Dec a) where
boring :: Dec a
boring = Dec a
forall a. Decidable a => Dec a
decide
boringYes :: Boring a => Dec a
boringYes :: forall a. Boring a => Dec a
boringYes = a -> Dec a
forall a. a -> Dec a
Yes a
forall a. Boring a => a
boring
absurdNo :: Absurd a => Dec a
absurdNo :: forall a. Absurd a => Dec a
absurdNo = Neg a -> Dec a
forall a. Neg a -> Dec a
No Neg a
forall b. a -> b
forall a b. Absurd a => a -> b
absurd