{-# OPTIONS -Wall #-}
{-# OPTIONS -Wno-compat #-}
{-# OPTIONS -Wincomplete-record-updates #-}
{-# OPTIONS -Wincomplete-uni-patterns #-}
{-# OPTIONS -Wredundant-constraints #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE NoOverloadedLists #-}
{-# LANGUAGE NoStarIsType #-}
module Predicate.Data.Either (
IsLeft
, IsRight
, MkLeft
, MkLeft'
, MkRight
, MkRight'
, Left'
, Right'
, LeftDef
, LeftFail
, RightDef
, RightFail
, EitherBool
, EitherIn
, PartitionEithers
, type (|||)
, type (+++)
) where
import Predicate.Core
import Predicate.Util
import GHC.TypeLits (ErrorMessage((:$$:),(:<>:)))
import qualified GHC.TypeLits as GL
import Data.Proxy
import Data.Kind (Type)
import Data.Either
data Left'
instance (Show a
) => P Left' (Either a x) where
type PP Left' (Either a x) = a
eval _ opts lr =
let msg0 = "Left'"
in pure $ case lr of
Right _ -> mkNode opts (FailT (msg0 <> " found Right")) "" []
Left a -> mkNode opts (PresentT a) (msg0 <> " " <> showL opts a) []
data Right'
instance (Show a
) => P Right' (Either x a) where
type PP Right' (Either x a) = a
eval _ opts lr =
let msg0 = "Right'"
in pure $ case lr of
Left _ -> mkNode opts (FailT (msg0 <> " found Left")) "" []
Right a -> mkNode opts (PresentT a) (msg0 <> " " <> showL opts a) []
data p ||| q
infixr 2 |||
type EitherIn p q = p ||| q
instance (Show (PP p a)
, P p a
, P q b
, PP p a ~ PP q b
, Show a
, Show b
) => P (p ||| q) (Either a b) where
type PP (p ||| q) (Either a b) = PP p a
eval _ opts lr = do
let msg0 = "(|||)"
case lr of
Left a -> do
pp <- eval (Proxy @p) opts a
pure $ case getValueLR opts msg0 pp [] of
Left e -> e
Right a1 -> let msg1 = msg0 ++ " Left"
in mkNode opts (_tBool pp) (show01 opts msg1 a1 a) [hh pp]
Right a -> do
qq <- eval (Proxy @q) opts a
pure $ case getValueLR opts msg0 qq [] of
Left e -> e
Right a1 ->
let msg1 = msg0 ++ " Right"
in mkNode opts (_tBool qq) (show01 opts msg1 a1 a) [hh qq]
data IsLeft p
instance ( P p x
, PP p x ~ Either a b
) => P (IsLeft p) x where
type PP (IsLeft p) x = Bool
eval _ opts x = do
let msg0 = "IsLeft"
pp <- eval (Proxy @p) opts x
let hhs = [hh pp]
pure $ case getValueLR opts msg0 pp [] of
Left e -> e
Right (Left _) -> mkNodeB opts True msg0 hhs
Right (Right _) -> mkNodeB opts False msg0 hhs
data IsRight p
instance ( P p x
, PP p x ~ Either a b
) => P (IsRight p) x where
type PP (IsRight p) x = Bool
eval _ opts x = do
let msg0 = "IsRight"
pp <- eval (Proxy @p) opts x
let hhs = [hh pp]
pure $ case getValueLR opts msg0 pp [] of
Left e -> e
Right (Left _) -> mkNodeB opts False msg0 hhs
Right (Right _) -> mkNodeB opts True msg0 hhs
data p +++ q
infixr 2 +++
instance (Show (PP p a)
, Show (PP q b)
, P p a
, P q b
, Show a
, Show b
) => P (p +++ q) (Either a b) where
type PP (p +++ q) (Either a b) = Either (PP p a) (PP q b)
eval _ opts lr = do
let msg0 = "(+++)"
case lr of
Left a -> do
pp <- eval (Proxy @p) opts a
pure $ case getValueLR opts msg0 pp [] of
Left e -> e
Right a1 ->
let msg1 = msg0 ++ " Left"
in mkNode opts (PresentT (Left a1)) (msg1 <> " " <> showL opts a1 <> showVerbose opts " | " a) [hh pp]
Right a -> do
qq <- eval (Proxy @q) opts a
pure $ case getValueLR opts msg0 qq [] of
Left e -> e
Right a1 ->
let msg1 = msg0 ++ " Right"
in mkNode opts (PresentT (Right a1)) (msg1 <> " " <> showL opts a1 <> showVerbose opts " | " a) [hh qq]
data PartitionEithers
instance ( Show a
, Show b
) => P PartitionEithers [Either a b] where
type PP PartitionEithers [Either a b] = ([a], [b])
eval _ opts as =
let msg0 = "PartitionEithers"
b = partitionEithers as
in pure $ mkNode opts (PresentT b) (show01 opts msg0 b as) []
data EitherBool b p q
instance (Show (PP p a)
, P p a
, Show (PP q a)
, P q a
, P b a
, PP b a ~ Bool
) => P (EitherBool b p q) a where
type PP (EitherBool b p q) a = Either (PP p a) (PP q a)
eval _ opts z = do
let msg0 = "EitherBool"
bb <- evalBool (Proxy @b) opts z
case getValueLR opts (msg0 <> " b failed") bb [] of
Left e -> pure e
Right False -> do
pp <- eval (Proxy @p) opts z
pure $ case getValueLR opts (msg0 <> " p failed") pp [hh bb] of
Left e -> e
Right p -> mkNode opts (PresentT (Left p)) (msg0 <> "(False) Left " <> showL opts p) [hh bb, hh pp]
Right True -> do
qq <- eval (Proxy @q) opts z
pure $ case getValueLR opts (msg0 <> " q failed") qq [hh bb] of
Left e -> e
Right q -> mkNode opts (PresentT (Right q)) (msg0 <> "(True) Right " <> showL opts q) [hh bb, hh qq]
data EitherX p q r
instance (P r x
, P p (x,a)
, P q (x,b)
, PP r x ~ Either a b
, PP p (x,a) ~ c
, PP q (x,b) ~ c
) => P (EitherX p q r) x where
type PP (EitherX p q r) x = EitherXT (PP r x) x p
eval _ opts x = do
let msg0 = "EitherX"
rr <- eval (Proxy @r) opts x
case getValueLR opts msg0 rr [] of
Left e -> pure e
Right (Left a) -> do
let msg1 = msg0 <> "(Left)"
pp <- eval (Proxy @p) opts (x,a)
pure $ case getValueLR opts msg1 pp [hh rr] of
Left e -> e
Right _ -> mkNode opts (_tBool pp) msg1 [hh rr, hh pp]
Right (Right b) -> do
let msg1 = msg0 <> "(Right)"
qq <- eval (Proxy @q) opts (x,b)
pure $ case getValueLR opts msg1 qq [hh rr] of
Left e -> e
Right _ -> mkNode opts (_tBool qq) msg1 [hh rr, hh qq]
type family EitherXT lr x p where
EitherXT (Either a b) x p = PP p (x,a)
EitherXT o _ _ = GL.TypeError (
'GL.Text "EitherXT: expected 'Either a b' "
':$$: 'GL.Text "o = "
':<>: 'GL.ShowType o)
data MkLeft' t p
instance ( Show (PP p x)
, P p x
) => P (MkLeft' t p) x where
type PP (MkLeft' t p) x = Either (PP p x) (PP t x)
eval _ opts x = do
let msg0 = "MkLeft"
pp <- eval (Proxy @p) opts x
pure $ case getValueLR opts msg0 pp [] of
Left e -> e
Right p ->
let d = Left p
in mkNode opts (PresentT d) (msg0 <> " Left " <> showL opts p) [hh pp]
data MkLeft (t :: Type) p
type MkLeftT (t :: Type) p = MkLeft' (Hole t) p
instance P (MkLeftT t p) x => P (MkLeft t p) x where
type PP (MkLeft t p) x = PP (MkLeftT t p) x
eval _ = eval (Proxy @(MkLeftT t p))
data MkRight' t p
instance ( Show (PP p x)
, P p x
) => P (MkRight' t p) x where
type PP (MkRight' t p) x = Either (PP t x) (PP p x)
eval _ opts x = do
let msg0 = "MkRight"
pp <- eval (Proxy @p) opts x
pure $ case getValueLR opts msg0 pp [] of
Left e -> e
Right p ->
let d = Right p
in mkNode opts (PresentT d) (msg0 <> " Right " <> showL opts p) [hh pp]
data MkRight (t :: Type) p
type MkRightT (t :: Type) p = MkRight' (Hole t) p
instance P (MkRightT t p) x => P (MkRight t p) x where
type PP (MkRight t p) x = PP (MkRightT t p) x
eval _ = eval (Proxy @(MkRightT t p))
data LeftDef p q
instance ( PP q x ~ Either a b
, PP p (b,x) ~ a
, P q x
, P p (b,x)
) => P (LeftDef p q) x where
type PP (LeftDef p q) x = LeftT (PP q x)
eval _ opts x = do
let msg0 = "LeftDef"
qq <- eval (Proxy @q) opts x
case getValueLR opts msg0 qq [] of
Left e -> pure e
Right q ->
case q of
Left a -> pure $ mkNode opts (PresentT a) (msg0 <> " Left") [hh qq]
Right b -> do
pp <- eval (Proxy @p) opts (b,x)
pure $ case getValueLR opts msg0 pp [hh qq] of
Left e -> e
Right p -> mkNode opts (PresentT p) (msg0 <> " Right") [hh qq, hh pp]
data RightDef p q
instance ( PP q x ~ Either a b
, PP p (a,x) ~ b
, P q x
, P p (a,x)
) => P (RightDef p q) x where
type PP (RightDef p q) x = RightT (PP q x)
eval _ opts x = do
let msg0 = "RightDef"
qq <- eval (Proxy @q) opts x
case getValueLR opts msg0 qq [] of
Left e -> pure e
Right q ->
case q of
Right b -> pure $ mkNode opts (PresentT b) (msg0 <> " Right") [hh qq]
Left a -> do
pp <- eval (Proxy @p) opts (a,x)
pure $ case getValueLR opts msg0 pp [hh qq] of
Left e -> e
Right p -> mkNode opts (PresentT p) (msg0 <> " Left") [hh qq, hh pp]
data LeftFail p q
instance ( PP p (b,x) ~ String
, PP q x ~ Either a b
, P p (b,x)
, P q x)
=> P (LeftFail p q) x where
type PP (LeftFail p q) x = LeftT (PP q x)
eval _ opts x = do
let msg0 = "LeftFail"
qq <- eval (Proxy @q) opts x
case getValueLR opts msg0 qq [] of
Left e -> pure e
Right q ->
case q of
Left a -> pure $ mkNode opts (PresentT a) "Left" [hh qq]
Right b -> do
pp <- eval (Proxy @p) opts (b,x)
pure $ case getValueLR opts msg0 pp [hh qq] of
Left e -> e
Right p -> mkNode opts (FailT p) (msg0 <> " Right") [hh qq, hh pp]
data RightFail p q
instance ( PP p (a,x) ~ String
, PP q x ~ Either a b
, P p (a,x)
, P q x)
=> P (RightFail p q) x where
type PP (RightFail p q) x = RightT (PP q x)
eval _ opts x = do
let msg0 = "RightFail"
qq <- eval (Proxy @q) opts x
case getValueLR opts msg0 qq [] of
Left e -> pure e
Right q ->
case q of
Right b -> pure $ mkNode opts (PresentT b) "Right" [hh qq]
Left a -> do
pp <- eval (Proxy @p) opts (a,x)
pure $ case getValueLR opts msg0 pp [hh qq] of
Left e -> e
Right p -> mkNode opts (FailT p) (msg0 <> " Left") [hh qq, hh pp]