{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE NoStarIsType #-}
{-# LANGUAGE EmptyDataDeriving #-}
module Predicate.Data.Maybe (
IsNothing
, IsJust
, MkNothing
, MkNothing'
, MkJust
, Just'
, JustDef
, JustFail
, MapMaybe
, CatMaybes
, MaybeBool
, MaybeIn
, MaybeId
, MaybeInT
) where
import Predicate.Core
import Predicate.Misc
import Predicate.Util
import Predicate.Data.Foldable (ConcatMap)
import Predicate.Data.Monoid (MEmptyP)
import Predicate.Data.Lifted (EmptyBool)
import Data.Proxy (Proxy(..))
import Data.Kind (Type)
import Data.Maybe (isJust, isNothing)
import GHC.TypeLits (ErrorMessage((:$$:),(:<>:)))
import qualified GHC.TypeLits as GL
data Just' deriving Int -> Just' -> ShowS
[Just'] -> ShowS
Just' -> String
(Int -> Just' -> ShowS)
-> (Just' -> String) -> ([Just'] -> ShowS) -> Show Just'
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Just'] -> ShowS
$cshowList :: [Just'] -> ShowS
show :: Just' -> String
$cshow :: Just' -> String
showsPrec :: Int -> Just' -> ShowS
$cshowsPrec :: Int -> Just' -> ShowS
Show
instance Show a => P Just' (Maybe a) where
type PP Just' (Maybe a) = a
eval :: proxy Just' -> POpts -> Maybe a -> m (TT (PP Just' (Maybe a)))
eval proxy Just'
_ POpts
opts Maybe a
lr =
let msg0 :: String
msg0 = String
"Just'"
in TT a -> m (TT a)
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (TT a -> m (TT a)) -> TT a -> m (TT a)
forall a b. (a -> b) -> a -> b
$ case Maybe a
lr of
Maybe a
Nothing -> POpts -> Val a -> String -> [Tree PE] -> TT a
forall a. POpts -> Val a -> String -> [Tree PE] -> TT a
mkNode POpts
opts (String -> Val a
forall a. String -> Val a
Fail (String
msg0 String -> ShowS
forall a. Semigroup a => a -> a -> a
<> String
" found Nothing")) String
"" []
Just a
a -> POpts -> Val a -> String -> [Tree PE] -> TT a
forall a. POpts -> Val a -> String -> [Tree PE] -> TT a
mkNode POpts
opts (a -> Val a
forall a. a -> Val a
Val a
a) (String
msg0 String -> ShowS
forall a. Semigroup a => a -> a -> a
<> String
" " String -> ShowS
forall a. Semigroup a => a -> a -> a
<> POpts -> a -> String
forall a. Show a => POpts -> a -> String
showL POpts
opts a
a) []
data MkNothing' t deriving Int -> MkNothing' t -> ShowS
[MkNothing' t] -> ShowS
MkNothing' t -> String
(Int -> MkNothing' t -> ShowS)
-> (MkNothing' t -> String)
-> ([MkNothing' t] -> ShowS)
-> Show (MkNothing' t)
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
forall k (t :: k). Int -> MkNothing' t -> ShowS
forall k (t :: k). [MkNothing' t] -> ShowS
forall k (t :: k). MkNothing' t -> String
showList :: [MkNothing' t] -> ShowS
$cshowList :: forall k (t :: k). [MkNothing' t] -> ShowS
show :: MkNothing' t -> String
$cshow :: forall k (t :: k). MkNothing' t -> String
showsPrec :: Int -> MkNothing' t -> ShowS
$cshowsPrec :: forall k (t :: k). Int -> MkNothing' t -> ShowS
Show
instance P (MkNothing' t) a where
type PP (MkNothing' t) a = Maybe (PP t a)
eval :: proxy (MkNothing' t) -> POpts -> a -> m (TT (PP (MkNothing' t) a))
eval proxy (MkNothing' t)
_ POpts
opts a
_ =
let msg0 :: String
msg0 = String
"MkNothing"
in TT (Maybe (PP t a)) -> m (TT (Maybe (PP t a)))
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (TT (Maybe (PP t a)) -> m (TT (Maybe (PP t a))))
-> TT (Maybe (PP t a)) -> m (TT (Maybe (PP t a)))
forall a b. (a -> b) -> a -> b
$ POpts
-> Val (Maybe (PP t a))
-> String
-> [Tree PE]
-> TT (Maybe (PP t a))
forall a. POpts -> Val a -> String -> [Tree PE] -> TT a
mkNode POpts
opts (Maybe (PP t a) -> Val (Maybe (PP t a))
forall a. a -> Val a
Val Maybe (PP t a)
forall a. Maybe a
Nothing) String
msg0 []
data MkNothing (t :: Type) deriving Int -> MkNothing t -> ShowS
[MkNothing t] -> ShowS
MkNothing t -> String
(Int -> MkNothing t -> ShowS)
-> (MkNothing t -> String)
-> ([MkNothing t] -> ShowS)
-> Show (MkNothing t)
forall t. Int -> MkNothing t -> ShowS
forall t. [MkNothing t] -> ShowS
forall t. MkNothing t -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [MkNothing t] -> ShowS
$cshowList :: forall t. [MkNothing t] -> ShowS
show :: MkNothing t -> String
$cshow :: forall t. MkNothing t -> String
showsPrec :: Int -> MkNothing t -> ShowS
$cshowsPrec :: forall t. Int -> MkNothing t -> ShowS
Show
type MkNothingT (t :: Type) = MkNothing' (Hole t)
instance P (MkNothing t) x where
type PP (MkNothing t) x = PP (MkNothingT t) x
eval :: proxy (MkNothing t) -> POpts -> x -> m (TT (PP (MkNothing t) x))
eval proxy (MkNothing t)
_ = Proxy (MkNothingT t) -> POpts -> x -> m (TT (PP (MkNothingT t) x))
forall k (p :: k) a (m :: Type -> Type) (proxy :: k -> Type).
(P p a, MonadEval m) =>
proxy p -> POpts -> a -> m (TT (PP p a))
eval (Proxy (MkNothingT t)
forall k (t :: k). Proxy t
Proxy @(MkNothingT t))
data MkJust p deriving Int -> MkJust p -> ShowS
[MkJust p] -> ShowS
MkJust p -> String
(Int -> MkJust p -> ShowS)
-> (MkJust p -> String) -> ([MkJust p] -> ShowS) -> Show (MkJust p)
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
forall k (p :: k). Int -> MkJust p -> ShowS
forall k (p :: k). [MkJust p] -> ShowS
forall k (p :: k). MkJust p -> String
showList :: [MkJust p] -> ShowS
$cshowList :: forall k (p :: k). [MkJust p] -> ShowS
show :: MkJust p -> String
$cshow :: forall k (p :: k). MkJust p -> String
showsPrec :: Int -> MkJust p -> ShowS
$cshowsPrec :: forall k (p :: k). Int -> MkJust p -> ShowS
Show
instance ( PP p x ~ a
, P p x
, Show a
) => P (MkJust p) x where
type PP (MkJust p) x = Maybe (PP p x)
eval :: proxy (MkJust p) -> POpts -> x -> m (TT (PP (MkJust p) x))
eval proxy (MkJust p)
_ POpts
opts x
x = do
let msg0 :: String
msg0 = String
"MkJust"
TT a
pp <- Proxy p -> POpts -> x -> m (TT (PP p x))
forall k (p :: k) a (m :: Type -> Type) (proxy :: k -> Type).
(P p a, MonadEval m) =>
proxy p -> POpts -> a -> m (TT (PP p a))
eval (Proxy p
forall k (t :: k). Proxy t
Proxy @p) POpts
opts x
x
TT (Maybe a) -> m (TT (Maybe a))
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (TT (Maybe a) -> m (TT (Maybe a)))
-> TT (Maybe a) -> m (TT (Maybe a))
forall a b. (a -> b) -> a -> b
$ case Inline
-> POpts -> String -> TT a -> [Tree PE] -> Either (TT (Maybe a)) a
forall a x.
Inline -> POpts -> String -> TT a -> [Tree PE] -> Either (TT x) a
getValueLR Inline
NoInline POpts
opts String
msg0 TT a
pp [] of
Left TT (Maybe a)
e -> TT (Maybe a)
e
Right a
p ->
let d :: Maybe a
d = a -> Maybe a
forall a. a -> Maybe a
Just a
p
in POpts -> Val (Maybe a) -> String -> [Tree PE] -> TT (Maybe a)
forall a. POpts -> Val a -> String -> [Tree PE] -> TT a
mkNode POpts
opts (Maybe a -> Val (Maybe a)
forall a. a -> Val a
Val Maybe a
d) (String
msg0 String -> ShowS
forall a. Semigroup a => a -> a -> a
<> String
" Just " String -> ShowS
forall a. Semigroup a => a -> a -> a
<> POpts -> a -> String
forall a. Show a => POpts -> a -> String
showL POpts
opts a
p) [TT a -> Tree PE
forall a. TT a -> Tree PE
hh TT a
pp]
data IsJust deriving Int -> IsJust -> ShowS
[IsJust] -> ShowS
IsJust -> String
(Int -> IsJust -> ShowS)
-> (IsJust -> String) -> ([IsJust] -> ShowS) -> Show IsJust
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [IsJust] -> ShowS
$cshowList :: [IsJust] -> ShowS
show :: IsJust -> String
$cshow :: IsJust -> String
showsPrec :: Int -> IsJust -> ShowS
$cshowsPrec :: Int -> IsJust -> ShowS
Show
instance x ~ Maybe a
=> P IsJust x where
type PP IsJust x = Bool
eval :: proxy IsJust -> POpts -> x -> m (TT (PP IsJust x))
eval proxy IsJust
_ POpts
opts x
x = TT Bool -> m (TT Bool)
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (TT Bool -> m (TT Bool)) -> TT Bool -> m (TT Bool)
forall a b. (a -> b) -> a -> b
$ POpts -> Bool -> String -> [Tree PE] -> TT Bool
mkNodeB POpts
opts (Maybe a -> Bool
forall a. Maybe a -> Bool
isJust x
Maybe a
x) String
"IsJust" []
data IsNothing deriving Int -> IsNothing -> ShowS
[IsNothing] -> ShowS
IsNothing -> String
(Int -> IsNothing -> ShowS)
-> (IsNothing -> String)
-> ([IsNothing] -> ShowS)
-> Show IsNothing
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [IsNothing] -> ShowS
$cshowList :: [IsNothing] -> ShowS
show :: IsNothing -> String
$cshow :: IsNothing -> String
showsPrec :: Int -> IsNothing -> ShowS
$cshowsPrec :: Int -> IsNothing -> ShowS
Show
instance x ~ Maybe a
=> P IsNothing x where
type PP IsNothing x = Bool
eval :: proxy IsNothing -> POpts -> x -> m (TT (PP IsNothing x))
eval proxy IsNothing
_ POpts
opts x
x = TT Bool -> m (TT Bool)
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (TT Bool -> m (TT Bool)) -> TT Bool -> m (TT Bool)
forall a b. (a -> b) -> a -> b
$ POpts -> Bool -> String -> [Tree PE] -> TT Bool
mkNodeB POpts
opts (Maybe a -> Bool
forall a. Maybe a -> Bool
isNothing x
Maybe a
x) String
"IsNothing" []
data MapMaybe p q deriving Int -> MapMaybe p q -> ShowS
[MapMaybe p q] -> ShowS
MapMaybe p q -> String
(Int -> MapMaybe p q -> ShowS)
-> (MapMaybe p q -> String)
-> ([MapMaybe p q] -> ShowS)
-> Show (MapMaybe p q)
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
forall k (p :: k) k (q :: k). Int -> MapMaybe p q -> ShowS
forall k (p :: k) k (q :: k). [MapMaybe p q] -> ShowS
forall k (p :: k) k (q :: k). MapMaybe p q -> String
showList :: [MapMaybe p q] -> ShowS
$cshowList :: forall k (p :: k) k (q :: k). [MapMaybe p q] -> ShowS
show :: MapMaybe p q -> String
$cshow :: forall k (p :: k) k (q :: k). MapMaybe p q -> String
showsPrec :: Int -> MapMaybe p q -> ShowS
$cshowsPrec :: forall k (p :: k) k (q :: k). Int -> MapMaybe p q -> ShowS
Show
type MapMaybeT p q = ConcatMap (p >> MaybeId MEmptyP '[Id]) q
instance P (MapMaybeT p q) x => P (MapMaybe p q) x where
type PP (MapMaybe p q) x = PP (MapMaybeT p q) x
eval :: proxy (MapMaybe p q) -> POpts -> x -> m (TT (PP (MapMaybe p q) x))
eval proxy (MapMaybe p q)
_ = Proxy (MapMaybeT p q)
-> POpts -> x -> m (TT (PP (MapMaybeT p q) x))
forall k (p :: k) a (m :: Type -> Type) (proxy :: k -> Type).
(P p a, MonadEval m) =>
proxy p -> POpts -> a -> m (TT (PP p a))
eval (Proxy (MapMaybeT p q)
forall k (t :: k). Proxy t
Proxy @(MapMaybeT p q))
data CatMaybes deriving Int -> CatMaybes -> ShowS
[CatMaybes] -> ShowS
CatMaybes -> String
(Int -> CatMaybes -> ShowS)
-> (CatMaybes -> String)
-> ([CatMaybes] -> ShowS)
-> Show CatMaybes
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [CatMaybes] -> ShowS
$cshowList :: [CatMaybes] -> ShowS
show :: CatMaybes -> String
$cshow :: CatMaybes -> String
showsPrec :: Int -> CatMaybes -> ShowS
$cshowsPrec :: Int -> CatMaybes -> ShowS
Show
type CatMaybesT = MapMaybe Id Id
instance P CatMaybesT x => P CatMaybes x where
type PP CatMaybes x = PP CatMaybesT x
eval :: proxy CatMaybes -> POpts -> x -> m (TT (PP CatMaybes x))
eval proxy CatMaybes
_ = Proxy CatMaybesT -> POpts -> x -> m (TT (PP CatMaybesT x))
forall k (p :: k) a (m :: Type -> Type) (proxy :: k -> Type).
(P p a, MonadEval m) =>
proxy p -> POpts -> a -> m (TT (PP p a))
eval (Proxy CatMaybesT
forall k (t :: k). Proxy t
Proxy @CatMaybesT)
data MaybeBool b p deriving Int -> MaybeBool b p -> ShowS
[MaybeBool b p] -> ShowS
MaybeBool b p -> String
(Int -> MaybeBool b p -> ShowS)
-> (MaybeBool b p -> String)
-> ([MaybeBool b p] -> ShowS)
-> Show (MaybeBool b p)
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
forall k (b :: k) k (p :: k). Int -> MaybeBool b p -> ShowS
forall k (b :: k) k (p :: k). [MaybeBool b p] -> ShowS
forall k (b :: k) k (p :: k). MaybeBool b p -> String
showList :: [MaybeBool b p] -> ShowS
$cshowList :: forall k (b :: k) k (p :: k). [MaybeBool b p] -> ShowS
show :: MaybeBool b p -> String
$cshow :: forall k (b :: k) k (p :: k). MaybeBool b p -> String
showsPrec :: Int -> MaybeBool b p -> ShowS
$cshowsPrec :: forall k (b :: k) k (p :: k). Int -> MaybeBool b p -> ShowS
Show
type MaybeBoolT b p = EmptyBool Maybe b p
instance P (MaybeBoolT b p) x => P (MaybeBool b p) x where
type PP (MaybeBool b p) x = PP (MaybeBoolT b p) x
eval :: proxy (MaybeBool b p)
-> POpts -> x -> m (TT (PP (MaybeBool b p) x))
eval proxy (MaybeBool b p)
_ = Proxy (MaybeBoolT b p)
-> POpts -> x -> m (TT (PP (MaybeBoolT b p) x))
forall k (p :: k) a (m :: Type -> Type) (proxy :: k -> Type).
(P p a, MonadEval m) =>
proxy p -> POpts -> a -> m (TT (PP p a))
eval (Proxy (MaybeBoolT b p)
forall k (t :: k). Proxy t
Proxy @(MaybeBoolT b p))
data JustDef p q deriving Int -> JustDef p q -> ShowS
[JustDef p q] -> ShowS
JustDef p q -> String
(Int -> JustDef p q -> ShowS)
-> (JustDef p q -> String)
-> ([JustDef p q] -> ShowS)
-> Show (JustDef p q)
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
forall k (p :: k) k (q :: k). Int -> JustDef p q -> ShowS
forall k (p :: k) k (q :: k). [JustDef p q] -> ShowS
forall k (p :: k) k (q :: k). JustDef p q -> String
showList :: [JustDef p q] -> ShowS
$cshowList :: forall k (p :: k) k (q :: k). [JustDef p q] -> ShowS
show :: JustDef p q -> String
$cshow :: forall k (p :: k) k (q :: k). JustDef p q -> String
showsPrec :: Int -> JustDef p q -> ShowS
$cshowsPrec :: forall k (p :: k) k (q :: k). Int -> JustDef p q -> ShowS
Show
instance ( PP p x ~ a
, PP q x ~ Maybe a
, P p x
, P q x
)
=> P (JustDef p q) x where
type PP (JustDef p q) x = MaybeT (PP q x)
eval :: proxy (JustDef p q) -> POpts -> x -> m (TT (PP (JustDef p q) x))
eval proxy (JustDef p q)
_ POpts
opts x
x = do
let msg0 :: String
msg0 = String
"JustDef"
TT (Maybe a)
qq <- Proxy q -> POpts -> x -> m (TT (PP q x))
forall k (p :: k) a (m :: Type -> Type) (proxy :: k -> Type).
(P p a, MonadEval m) =>
proxy p -> POpts -> a -> m (TT (PP p a))
eval (Proxy q
forall k (t :: k). Proxy t
Proxy @q) POpts
opts x
x
case Inline
-> POpts
-> String
-> TT (Maybe a)
-> [Tree PE]
-> Either (TT a) (Maybe a)
forall a x.
Inline -> POpts -> String -> TT a -> [Tree PE] -> Either (TT x) a
getValueLR Inline
NoInline POpts
opts String
msg0 TT (Maybe a)
qq [] of
Left TT a
e -> TT a -> m (TT a)
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure TT a
e
Right Maybe a
q ->
case Maybe a
q of
Just a
b -> TT a -> m (TT a)
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (TT a -> m (TT a)) -> TT a -> m (TT a)
forall a b. (a -> b) -> a -> b
$ POpts -> Val a -> String -> [Tree PE] -> TT a
forall a. POpts -> Val a -> String -> [Tree PE] -> TT a
mkNode POpts
opts (a -> Val a
forall a. a -> Val a
Val a
b) (String
msg0 String -> ShowS
forall a. Semigroup a => a -> a -> a
<> String
" Just") [TT (Maybe a) -> Tree PE
forall a. TT a -> Tree PE
hh TT (Maybe a)
qq]
Maybe a
Nothing -> do
TT a
pp <- Proxy p -> POpts -> x -> m (TT (PP p x))
forall k (p :: k) a (m :: Type -> Type) (proxy :: k -> Type).
(P p a, MonadEval m) =>
proxy p -> POpts -> a -> m (TT (PP p a))
eval (Proxy p
forall k (t :: k). Proxy t
Proxy @p) POpts
opts x
x
TT a -> m (TT a)
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (TT a -> m (TT a)) -> TT a -> m (TT a)
forall a b. (a -> b) -> a -> b
$ case Inline -> POpts -> String -> TT a -> [Tree PE] -> Either (TT a) a
forall a x.
Inline -> POpts -> String -> TT a -> [Tree PE] -> Either (TT x) a
getValueLR Inline
NoInline POpts
opts String
msg0 TT a
pp [TT (Maybe a) -> Tree PE
forall a. TT a -> Tree PE
hh TT (Maybe a)
qq] of
Left TT a
e -> TT a
e
Right a
_ -> POpts -> TT a -> String -> [Tree PE] -> TT a
forall a. POpts -> TT a -> String -> [Tree PE] -> TT a
mkNodeCopy POpts
opts TT a
pp (String
msg0 String -> ShowS
forall a. Semigroup a => a -> a -> a
<> String
" Nothing") [TT (Maybe a) -> Tree PE
forall a. TT a -> Tree PE
hh TT (Maybe a)
qq]
data JustFail p q deriving Int -> JustFail p q -> ShowS
[JustFail p q] -> ShowS
JustFail p q -> String
(Int -> JustFail p q -> ShowS)
-> (JustFail p q -> String)
-> ([JustFail p q] -> ShowS)
-> Show (JustFail p q)
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
forall k (p :: k) k (q :: k). Int -> JustFail p q -> ShowS
forall k (p :: k) k (q :: k). [JustFail p q] -> ShowS
forall k (p :: k) k (q :: k). JustFail p q -> String
showList :: [JustFail p q] -> ShowS
$cshowList :: forall k (p :: k) k (q :: k). [JustFail p q] -> ShowS
show :: JustFail p q -> String
$cshow :: forall k (p :: k) k (q :: k). JustFail p q -> String
showsPrec :: Int -> JustFail p q -> ShowS
$cshowsPrec :: forall k (p :: k) k (q :: k). Int -> JustFail p q -> ShowS
Show
instance ( PP p x ~ String
, PP q x ~ Maybe a
, P p x
, P q x
)
=> P (JustFail p q) x where
type PP (JustFail p q) x = MaybeT (PP q x)
eval :: proxy (JustFail p q) -> POpts -> x -> m (TT (PP (JustFail p q) x))
eval proxy (JustFail p q)
_ POpts
opts x
x = do
let msg0 :: String
msg0 = String
"JustFail"
TT (Maybe a)
qq <- Proxy q -> POpts -> x -> m (TT (PP q x))
forall k (p :: k) a (m :: Type -> Type) (proxy :: k -> Type).
(P p a, MonadEval m) =>
proxy p -> POpts -> a -> m (TT (PP p a))
eval (Proxy q
forall k (t :: k). Proxy t
Proxy @q) POpts
opts x
x
case Inline
-> POpts
-> String
-> TT (Maybe a)
-> [Tree PE]
-> Either (TT a) (Maybe a)
forall a x.
Inline -> POpts -> String -> TT a -> [Tree PE] -> Either (TT x) a
getValueLR Inline
NoInline POpts
opts String
msg0 TT (Maybe a)
qq [] of
Left TT a
e -> TT a -> m (TT a)
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure TT a
e
Right Maybe a
q ->
case Maybe a
q of
Just a
b -> TT a -> m (TT a)
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (TT a -> m (TT a)) -> TT a -> m (TT a)
forall a b. (a -> b) -> a -> b
$ POpts -> Val a -> String -> [Tree PE] -> TT a
forall a. POpts -> Val a -> String -> [Tree PE] -> TT a
mkNode POpts
opts (a -> Val a
forall a. a -> Val a
Val a
b) (String
msg0 String -> ShowS
forall a. Semigroup a => a -> a -> a
<> String
" Just") [TT (Maybe a) -> Tree PE
forall a. TT a -> Tree PE
hh TT (Maybe a)
qq]
Maybe a
Nothing -> do
TT String
pp <- Proxy p -> POpts -> x -> m (TT (PP p x))
forall k (p :: k) a (m :: Type -> Type) (proxy :: k -> Type).
(P p a, MonadEval m) =>
proxy p -> POpts -> a -> m (TT (PP p a))
eval (Proxy p
forall k (t :: k). Proxy t
Proxy @p) POpts
opts x
x
TT a -> m (TT a)
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (TT a -> m (TT a)) -> TT a -> m (TT a)
forall a b. (a -> b) -> a -> b
$ case Inline
-> POpts
-> String
-> TT String
-> [Tree PE]
-> Either (TT a) String
forall a x.
Inline -> POpts -> String -> TT a -> [Tree PE] -> Either (TT x) a
getValueLR Inline
NoInline POpts
opts String
msg0 TT String
pp [TT (Maybe a) -> Tree PE
forall a. TT a -> Tree PE
hh TT (Maybe a)
qq] of
Left TT a
e -> TT a
e
Right String
p -> POpts -> Val a -> String -> [Tree PE] -> TT a
forall a. POpts -> Val a -> String -> [Tree PE] -> TT a
mkNode POpts
opts (String -> Val a
forall a. String -> Val a
Fail String
p) (String
msg0 String -> ShowS
forall a. Semigroup a => a -> a -> a
<> String
" Nothing") [TT (Maybe a) -> Tree PE
forall a. TT a -> Tree PE
hh TT (Maybe a)
qq, TT String -> Tree PE
forall a. TT a -> Tree PE
hh TT String
pp]
data MaybeIn n p s t deriving Int -> MaybeIn n p s t -> ShowS
[MaybeIn n p s t] -> ShowS
MaybeIn n p s t -> String
(Int -> MaybeIn n p s t -> ShowS)
-> (MaybeIn n p s t -> String)
-> ([MaybeIn n p s t] -> ShowS)
-> Show (MaybeIn n p s t)
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
forall k (n :: k) k (p :: k) k (s :: k) k (t :: k).
Int -> MaybeIn n p s t -> ShowS
forall k (n :: k) k (p :: k) k (s :: k) k (t :: k).
[MaybeIn n p s t] -> ShowS
forall k (n :: k) k (p :: k) k (s :: k) k (t :: k).
MaybeIn n p s t -> String
showList :: [MaybeIn n p s t] -> ShowS
$cshowList :: forall k (n :: k) k (p :: k) k (s :: k) k (t :: k).
[MaybeIn n p s t] -> ShowS
show :: MaybeIn n p s t -> String
$cshow :: forall k (n :: k) k (p :: k) k (s :: k) k (t :: k).
MaybeIn n p s t -> String
showsPrec :: Int -> MaybeIn n p s t -> ShowS
$cshowsPrec :: forall k (n :: k) k (p :: k) k (s :: k) k (t :: k).
Int -> MaybeIn n p s t -> ShowS
Show
instance ( Show a
, Show (PP p (y,a))
, P n (y,Proxy z)
, P p (y,a)
, PP n (y,Proxy z) ~ PP p (y,a)
, z ~ PP p (y,a)
, P s x
, P t x
, PP t x ~ Maybe a
, PP s x ~ y
) => P (MaybeIn n p s t) x where
type PP (MaybeIn n p s t) x = MaybeInT p (PP s x) (PP t x)
eval :: proxy (MaybeIn n p s t)
-> POpts -> x -> m (TT (PP (MaybeIn n p s t) x))
eval proxy (MaybeIn n p s t)
_ POpts
opts x
x = do
let msg0 :: String
msg0 = String
"MaybeIn"
Either (TT z) (y, Maybe a, TT y, TT (Maybe a))
lr <- Inline
-> String
-> Proxy s
-> Proxy t
-> POpts
-> x
-> [Tree PE]
-> m (Either (TT z) (PP s x, PP t x, TT (PP s x), TT (PP t x)))
forall k1 k2 (p :: k1) a (q :: k2) (m :: Type -> Type)
(proxy1 :: k1 -> Type) (proxy2 :: k2 -> Type) x.
(P p a, P q a, MonadEval m) =>
Inline
-> String
-> proxy1 p
-> proxy2 q
-> POpts
-> a
-> [Tree PE]
-> m (Either (TT x) (PP p a, PP q a, TT (PP p a), TT (PP q a)))
runPQ Inline
NoInline String
msg0 (Proxy s
forall k (t :: k). Proxy t
Proxy @s) (Proxy t
forall k (t :: k). Proxy t
Proxy @t) POpts
opts x
x []
case Either (TT z) (y, Maybe a, TT y, TT (Maybe a))
lr of
Left TT z
e -> TT z -> m (TT z)
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure TT z
e
Right (y
s,Maybe a
t,TT y
ss,TT (Maybe a)
tt) -> do
let hhs :: [Tree PE]
hhs = [TT y -> Tree PE
forall a. TT a -> Tree PE
hh TT y
ss, TT (Maybe a) -> Tree PE
forall a. TT a -> Tree PE
hh TT (Maybe a)
tt]
case Maybe a
t of
Maybe a
Nothing -> do
let msg1 :: String
msg1 = String
msg0 String -> ShowS
forall a. Semigroup a => a -> a -> a
<> String
"(Nothing)"
TT z
nn <- Proxy n -> POpts -> (y, Proxy z) -> m (TT (PP n (y, Proxy z)))
forall k (p :: k) a (m :: Type -> Type) (proxy :: k -> Type).
(P p a, MonadEval m) =>
proxy p -> POpts -> a -> m (TT (PP p a))
eval (Proxy n
forall k (t :: k). Proxy t
Proxy @n) POpts
opts (y
s,Proxy z
forall k (t :: k). Proxy t
Proxy @z)
TT z -> m (TT z)
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (TT z -> m (TT z)) -> TT z -> m (TT z)
forall a b. (a -> b) -> a -> b
$ case Inline -> POpts -> String -> TT z -> [Tree PE] -> Either (TT z) z
forall a x.
Inline -> POpts -> String -> TT a -> [Tree PE] -> Either (TT x) a
getValueLR Inline
NoInline POpts
opts (String
msg1 String -> ShowS
forall a. Semigroup a => a -> a -> a
<> String
" n failed") TT z
nn [Tree PE]
hhs of
Left TT z
e -> TT z
e
Right z
c -> POpts -> TT z -> String -> [Tree PE] -> TT z
forall a. POpts -> TT a -> String -> [Tree PE] -> TT a
mkNodeCopy POpts
opts TT z
nn (POpts -> String -> z -> () -> String
forall a1 a2.
(Show a1, Show a2) =>
POpts -> String -> a1 -> a2 -> String
show3 POpts
opts String
msg1 z
c ()) [Tree PE]
hhs
Just a
a -> do
let msg1 :: String
msg1 = String
msg0 String -> ShowS
forall a. Semigroup a => a -> a -> a
<> String
"(Just)"
TT z
pp <- Proxy p -> POpts -> (y, a) -> m (TT (PP p (y, a)))
forall k (p :: k) a (m :: Type -> Type) (proxy :: k -> Type).
(P p a, MonadEval m) =>
proxy p -> POpts -> a -> m (TT (PP p a))
eval (Proxy p
forall k (t :: k). Proxy t
Proxy @p) POpts
opts (y
s,a
a)
TT z -> m (TT z)
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (TT z -> m (TT z)) -> TT z -> m (TT z)
forall a b. (a -> b) -> a -> b
$ case Inline -> POpts -> String -> TT z -> [Tree PE] -> Either (TT z) z
forall a x.
Inline -> POpts -> String -> TT a -> [Tree PE] -> Either (TT x) a
getValueLR Inline
NoInline POpts
opts (String
msg1 String -> ShowS
forall a. Semigroup a => a -> a -> a
<> String
" p failed") TT z
pp [Tree PE]
hhs of
Left TT z
e -> TT z
e
Right z
c -> POpts -> TT z -> String -> [Tree PE] -> TT z
forall a. POpts -> TT a -> String -> [Tree PE] -> TT a
mkNodeCopy POpts
opts TT z
pp (POpts -> String -> z -> a -> String
forall a1 a2.
(Show a1, Show a2) =>
POpts -> String -> a1 -> a2 -> String
show3 POpts
opts String
msg1 z
c a
a) [Tree PE]
hhs
type family MaybeInT (p :: k) (y :: Type) (ma :: Type) where
MaybeInT p y (Maybe a) = PP p (y,a)
MaybeInT _ _ o = GL.TypeError (
'GL.Text "MaybeInT: expected 'Maybe a' "
':$$: 'GL.Text "o = "
':<>: 'GL.ShowType o)
data MaybeId n p deriving Int -> MaybeId n p -> ShowS
[MaybeId n p] -> ShowS
MaybeId n p -> String
(Int -> MaybeId n p -> ShowS)
-> (MaybeId n p -> String)
-> ([MaybeId n p] -> ShowS)
-> Show (MaybeId n p)
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
forall k (n :: k) k (p :: k). Int -> MaybeId n p -> ShowS
forall k (n :: k) k (p :: k). [MaybeId n p] -> ShowS
forall k (n :: k) k (p :: k). MaybeId n p -> String
showList :: [MaybeId n p] -> ShowS
$cshowList :: forall k (n :: k) k (p :: k). [MaybeId n p] -> ShowS
show :: MaybeId n p -> String
$cshow :: forall k (n :: k) k (p :: k). MaybeId n p -> String
showsPrec :: Int -> MaybeId n p -> ShowS
$cshowsPrec :: forall k (n :: k) k (p :: k). Int -> MaybeId n p -> ShowS
Show
type MaybeIdT n p = MaybeIn (Snd >> n) (Snd >> p) () Id
instance P (MaybeIdT n p) x => P (MaybeId n p) x where
type PP (MaybeId n p) x = PP (MaybeIdT n p) x
eval :: proxy (MaybeId n p) -> POpts -> x -> m (TT (PP (MaybeId n p) x))
eval proxy (MaybeId n p)
_ = Proxy (MaybeIdT n p) -> POpts -> x -> m (TT (PP (MaybeIdT n p) x))
forall k (p :: k) a (m :: Type -> Type) (proxy :: k -> Type).
(P p a, MonadEval m) =>
proxy p -> POpts -> a -> m (TT (PP p a))
eval (Proxy (MaybeIdT n p)
forall k (t :: k). Proxy t
Proxy @(MaybeIdT n p))