{-# 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
, MaybeIn
, MaybeBool
, EmptyBool
) where
import Predicate.Core
import Predicate.Misc
import Predicate.Util
import Predicate.Data.Foldable (ConcatMap)
import Predicate.Data.Monoid (MEmptyP)
import Data.Proxy (Proxy(..))
import Data.Kind (Type)
import Data.Maybe (isJust, isNothing)
import Control.Applicative (Alternative(empty))
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 MaybeIn p q deriving Int -> MaybeIn p q -> ShowS
[MaybeIn p q] -> ShowS
MaybeIn p q -> String
(Int -> MaybeIn p q -> ShowS)
-> (MaybeIn p q -> String)
-> ([MaybeIn p q] -> ShowS)
-> Show (MaybeIn p q)
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
forall k (p :: k) k (q :: k). Int -> MaybeIn p q -> ShowS
forall k (p :: k) k (q :: k). [MaybeIn p q] -> ShowS
forall k (p :: k) k (q :: k). MaybeIn p q -> String
showList :: [MaybeIn p q] -> ShowS
$cshowList :: forall k (p :: k) k (q :: k). [MaybeIn p q] -> ShowS
show :: MaybeIn p q -> String
$cshow :: forall k (p :: k) k (q :: k). MaybeIn p q -> String
showsPrec :: Int -> MaybeIn p q -> ShowS
$cshowsPrec :: forall k (p :: k) k (q :: k). Int -> MaybeIn p q -> ShowS
Show
instance ( P q a
, Show a
, Show (PP q a)
, PP p (Proxy (PP q a)) ~ PP q a
, P p (Proxy (PP q a))
) => P (MaybeIn p q) (Maybe a) where
type PP (MaybeIn p q) (Maybe a) = PP q a
eval :: proxy (MaybeIn p q)
-> POpts -> Maybe a -> m (TT (PP (MaybeIn p q) (Maybe a)))
eval proxy (MaybeIn p q)
_ POpts
opts Maybe a
ma = do
let msg0 :: String
msg0 = String
"MaybeIn"
case Maybe a
ma of
Maybe a
Nothing -> do
let msg1 :: String
msg1 = String
msg0 String -> ShowS
forall a. Semigroup a => a -> a -> a
<> String
"(Nothing)"
TT (PP q a)
pp <- Proxy p
-> POpts -> Proxy (PP q a) -> m (TT (PP p (Proxy (PP q 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 (Proxy (PP q a)
forall k (t :: k). Proxy t
Proxy @(PP q a))
TT (PP q a) -> m (TT (PP q a))
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (TT (PP q a) -> m (TT (PP q a))) -> TT (PP q a) -> m (TT (PP q a))
forall a b. (a -> b) -> a -> b
$ case Inline
-> POpts
-> String
-> TT (PP q a)
-> [Tree PE]
-> Either (TT (PP q a)) (PP q a)
forall a x.
Inline -> POpts -> String -> TT a -> [Tree PE] -> Either (TT x) a
getValueLR Inline
NoInline POpts
opts String
msg1 TT (PP q a)
pp [] of
Left TT (PP q a)
e -> TT (PP q a)
e
Right PP q a
b -> POpts -> TT (PP q a) -> String -> [Tree PE] -> TT (PP q a)
forall a. POpts -> TT a -> String -> [Tree PE] -> TT a
mkNodeCopy POpts
opts TT (PP q a)
pp (String
msg1 String -> ShowS
forall a. Semigroup a => a -> a -> a
<> String
" " String -> ShowS
forall a. Semigroup a => a -> a -> a
<> POpts -> PP q a -> String
forall a. Show a => POpts -> a -> String
showL POpts
opts PP q a
b String -> ShowS
forall a. Semigroup a => a -> a -> a
<> String
" | Proxy") [TT (PP q a) -> Tree PE
forall a. TT a -> Tree PE
hh TT (PP q a)
pp]
Just a
a -> do
let msg1 :: String
msg1 = String
msg0 String -> ShowS
forall a. Semigroup a => a -> a -> a
<> String
"(Just)"
TT (PP q a)
qq <- Proxy q -> POpts -> a -> m (TT (PP q 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 q
forall k (t :: k). Proxy t
Proxy @q) POpts
opts a
a
TT (PP q a) -> m (TT (PP q a))
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (TT (PP q a) -> m (TT (PP q a))) -> TT (PP q a) -> m (TT (PP q a))
forall a b. (a -> b) -> a -> b
$ case Inline
-> POpts
-> String
-> TT (PP q a)
-> [Tree PE]
-> Either (TT (PP q a)) (PP q a)
forall a x.
Inline -> POpts -> String -> TT a -> [Tree PE] -> Either (TT x) a
getValueLR Inline
NoInline POpts
opts String
msg1 TT (PP q a)
qq [] of
Left TT (PP q a)
e -> TT (PP q a)
e
Right PP q a
b -> POpts -> TT (PP q a) -> String -> [Tree PE] -> TT (PP q a)
forall a. POpts -> TT a -> String -> [Tree PE] -> TT a
mkNodeCopy POpts
opts TT (PP q a)
qq (POpts -> String -> PP q a -> a -> String
forall a1 a2.
(Show a1, Show a2) =>
POpts -> String -> a1 -> a2 -> String
show3 POpts
opts String
msg1 PP q a
b a
a) [TT (PP q a) -> Tree PE
forall a. TT a -> Tree PE
hh TT (PP q a)
qq]
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 >> MaybeIn 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 EmptyBool t b p deriving Int -> EmptyBool t b p -> ShowS
[EmptyBool t b p] -> ShowS
EmptyBool t b p -> String
(Int -> EmptyBool t b p -> ShowS)
-> (EmptyBool t b p -> String)
-> ([EmptyBool t b p] -> ShowS)
-> Show (EmptyBool t b p)
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
forall k (t :: k) k (b :: k) k (p :: k).
Int -> EmptyBool t b p -> ShowS
forall k (t :: k) k (b :: k) k (p :: k). [EmptyBool t b p] -> ShowS
forall k (t :: k) k (b :: k) k (p :: k). EmptyBool t b p -> String
showList :: [EmptyBool t b p] -> ShowS
$cshowList :: forall k (t :: k) k (b :: k) k (p :: k). [EmptyBool t b p] -> ShowS
show :: EmptyBool t b p -> String
$cshow :: forall k (t :: k) k (b :: k) k (p :: k). EmptyBool t b p -> String
showsPrec :: Int -> EmptyBool t b p -> ShowS
$cshowsPrec :: forall k (t :: k) k (b :: k) k (p :: k).
Int -> EmptyBool t b p -> ShowS
Show
instance ( Show (PP p a)
, P b a
, P p a
, PP b a ~ Bool
, Alternative t
) => P (EmptyBool t b p) a where
type PP (EmptyBool t b p) a = t (PP p a)
eval :: proxy (EmptyBool t b p)
-> POpts -> a -> m (TT (PP (EmptyBool t b p) a))
eval proxy (EmptyBool t b p)
_ POpts
opts a
z = do
let msg0 :: String
msg0 = String
"EmptyBool"
TT Bool
bb <- Proxy b -> POpts -> a -> m (TT (PP b a))
forall k (m :: Type -> Type) (p :: k) a (proxy :: k -> Type).
(MonadEval m, P p a, PP p a ~ Bool) =>
proxy p -> POpts -> a -> m (TT (PP p a))
evalBool (Proxy b
forall k (t :: k). Proxy t
Proxy @b) POpts
opts a
z
case Inline
-> POpts
-> String
-> TT Bool
-> [Tree PE]
-> Either (TT (t (PP p a))) Bool
forall a x.
Inline -> POpts -> String -> TT a -> [Tree PE] -> Either (TT x) a
getValueLR Inline
NoInline POpts
opts (String
msg0 String -> ShowS
forall a. Semigroup a => a -> a -> a
<> String
" b failed") TT Bool
bb [] of
Left TT (t (PP p a))
e -> TT (t (PP p a)) -> m (TT (t (PP p a)))
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure TT (t (PP p a))
e
Right Bool
True -> do
TT (PP p a)
pp <- Proxy p -> POpts -> a -> m (TT (PP p 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 a
z
TT (t (PP p a)) -> m (TT (t (PP p a)))
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (TT (t (PP p a)) -> m (TT (t (PP p a))))
-> TT (t (PP p a)) -> m (TT (t (PP p a)))
forall a b. (a -> b) -> a -> b
$ case Inline
-> POpts
-> String
-> TT (PP p a)
-> [Tree PE]
-> Either (TT (t (PP p a))) (PP p a)
forall a x.
Inline -> POpts -> String -> TT a -> [Tree PE] -> Either (TT x) a
getValueLR Inline
NoInline POpts
opts (String
msg0 String -> ShowS
forall a. Semigroup a => a -> a -> a
<> String
" p failed") TT (PP p a)
pp [TT Bool -> Tree PE
forall a. TT a -> Tree PE
hh TT Bool
bb] of
Left TT (t (PP p a))
e -> TT (t (PP p a))
e
Right PP p a
p -> POpts -> Val (t (PP p a)) -> String -> [Tree PE] -> TT (t (PP p a))
forall a. POpts -> Val a -> String -> [Tree PE] -> TT a
mkNode POpts
opts (t (PP p a) -> Val (t (PP p a))
forall a. a -> Val a
Val (PP p a -> t (PP p a)
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure PP p a
p)) (String
msg0 String -> ShowS
forall a. Semigroup a => a -> a -> a
<> String
"(False) Just " String -> ShowS
forall a. Semigroup a => a -> a -> a
<> POpts -> PP p a -> String
forall a. Show a => POpts -> a -> String
showL POpts
opts PP p a
p) [TT Bool -> Tree PE
forall a. TT a -> Tree PE
hh TT Bool
bb, TT (PP p a) -> Tree PE
forall a. TT a -> Tree PE
hh TT (PP p a)
pp]
Right Bool
False -> TT (t (PP p a)) -> m (TT (t (PP p a)))
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (TT (t (PP p a)) -> m (TT (t (PP p a))))
-> TT (t (PP p a)) -> m (TT (t (PP p a)))
forall a b. (a -> b) -> a -> b
$ POpts -> Val (t (PP p a)) -> String -> [Tree PE] -> TT (t (PP p a))
forall a. POpts -> Val a -> String -> [Tree PE] -> TT a
mkNode POpts
opts (t (PP p a) -> Val (t (PP p a))
forall a. a -> Val a
Val t (PP p a)
forall (f :: Type -> Type) a. Alternative f => f a
empty) (String
msg0 String -> ShowS
forall a. Semigroup a => a -> a -> a
<> String
"(True)") [TT Bool -> Tree PE
forall a. TT a -> Tree PE
hh TT Bool
bb]
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
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
" Nothing") [TT (Maybe a) -> Tree PE
forall a. TT a -> Tree PE
hh TT (Maybe a)
qq, TT a -> Tree PE
forall a. TT a -> Tree PE
hh TT a
pp]
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]