{-# 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 #-}
-- | promoted 'Maybe' functions

module Predicate.Data.Maybe (

 -- ** predicates

    IsNothing
  , IsJust

 -- ** constructors

  , MkNothing
  , MkNothing'
  , MkJust

 -- ** get rid of Maybe

  , Just'
  , JustDef
  , JustFail
  , MapMaybe
  , CatMaybes
  , MaybeBool
  , MaybeIn
  , MaybeId

 -- ** type families

  , 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

-- $setup

-- >>> :set -XDataKinds

-- >>> :set -XTypeApplications

-- >>> :set -XTypeOperators

-- >>> :set -XOverloadedStrings

-- >>> import qualified Data.Map.Strict as M

-- >>> import Predicate

-- >>> import qualified Data.Semigroup as SG


-- | similar to 'Data.Maybe.fromJust'

--

-- >>> pz @(Just' >> Succ) (Just 20)

-- Val 21

--

-- >>> pz @(Just' >> Succ) Nothing

-- Fail "Just' found Nothing"

--

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) []

-- | constructs a Nothing for a given type

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
-- works always! MaybeBool is a good alternative and then dont need the extra 't'


-- for this to be useful has to have 't' else we end up with tons of problems

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 []

-- | constructs a Nothing for a given type

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))

-- | 'GHC.Maybe.Just' constructor

--

-- >>> pz @(MkJust Id) 44

-- Val (Just 44)

--

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]

-- | similar to 'Data.Maybe.isJust'

--

-- >>> pz @IsJust Nothing

-- Val False

--

-- >>> pz @IsJust (Just 'a')

-- Val True

--

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" []

-- | similar to 'Data.Maybe.isNothing'

--

-- >>> pz @IsNothing (Just 123)

-- Val False

--

-- >>> pz @IsNothing Nothing

-- Val True

--

-- >>> pl @(Not IsNothing &&& ('Just Id >> Id + 12)) (Just 1)

-- Present (True,13) ('(True,13))

-- Val (True,13)

--

-- >>> pl @(Not IsNothing &&& ('Just Id >> Id + 12)) Nothing

-- Error 'Just(empty) ('(,))

-- Fail "'Just(empty)"

--

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" []

-- | like 'Data.Maybe.mapMaybe'

--

-- >>> pl @(MapMaybe (MaybeBool (Le 3) Id) Id) [1..5]

-- Present [1,2,3] ((>>) [1,2,3] | {Concat [1,2,3] | [[1],[2],[3],[],[]]})

-- Val [1,2,3]

--

-- >>> pl @(MapMaybe (MaybeBool (Gt 3) Id) Id) [1..5]

-- Present [4,5] ((>>) [4,5] | {Concat [4,5] | [[],[],[],[4],[5]]})

-- Val [4,5]

--

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))

-- | similar to 'Data.Maybe.catMaybes'

--

-- >>> pl @CatMaybes [Just 'a',Nothing,Just 'c',Just 'd',Nothing]

-- Present "acd" ((>>) "acd" | {Concat "acd" | ["a","","c","d",""]})

-- Val "acd"

--

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)

-- | Convenient method to convert a value @p@ to a 'Maybe' based on a predicate @b@

-- if @b@ then Just @p@ else Nothing

--

-- >>> pz @(MaybeBool (Id > 4) Id) 24

-- Val (Just 24)

--

-- >>> pz @(MaybeBool (Id > 4) Id) (-5)

-- Val Nothing

--

-- >>> pz @(MaybeBool 'True 10) ()

-- Val (Just 10)

--

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))

-- | extract the value from a 'Maybe' otherwise use the default value: similar to 'Data.Maybe.fromMaybe'

--

-- >>> pl @(JustDef 'True Id) Nothing -- preserves TrueP/FalseP in the default case

-- True (JustDef Nothing)

-- Val True

--

-- >>> pl @(JustDef (Fst > 12) Snd) (3,Just False) -- ValP for normal case

-- Present False (JustDef Just)

-- Val False

--

-- >>> pl @(JustDef Fst Snd) (True,Nothing)

-- Present True (JustDef Nothing)

-- Val True

--

-- >>> pz @(JustDef (1 % 4) Id) (Just 20.4)

-- Val (102 % 5)

--

-- >>> pz @(JustDef (1 % 4) Id) Nothing

-- Val (1 % 4)

--

-- >>> pz @(JustDef (MEmptyT _) Id) (Just "xy")

-- Val "xy"

--

-- >>> pz @(JustDef (MEmptyT _) Id) Nothing

-- Val ()

--

-- >>> pz @(JustDef (MEmptyT (SG.Sum _)) Id) Nothing

-- Val (Sum {getSum = 0})

--

-- >>> pl @(JustDef 0 Id) (Just 123)

-- Present 123 (JustDef Just)

-- Val 123

--

-- >>> pl @(JustDef 0 Id) Nothing

-- Present 0 (JustDef Nothing)

-- Val 0

--

-- >>> pl @(JustDef 99 Id) (Just 12)

-- Present 12 (JustDef Just)

-- Val 12

--

-- >>> pl @(JustDef 99 Id) Nothing

-- Present 99 (JustDef Nothing)

-- Val 99

--

-- >>> pl @(JustDef (99 -% 1) Id) Nothing

-- Present (-99) % 1 (JustDef Nothing)

-- Val ((-99) % 1)

--

-- >>> pl @(JustDef (MEmptyT _) Id) (Just (SG.Sum 123))

-- Present Sum {getSum = 123} (JustDef Just)

-- Val (Sum {getSum = 123})

--

-- >>> pl @(JustDef (MEmptyT _) Id) (Nothing @(SG.Sum _))

-- Present Sum {getSum = 0} (JustDef Nothing)

-- Val (Sum {getSum = 0})

--

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]


-- | extract the value from a 'Maybe' or fail with the given message

--

-- >>> pz @(JustFail "nope" Id) (Just 99)

-- Val 99

--

-- >>> pz @(JustFail "nope" Id) Nothing

-- Fail "nope"

--

-- >>> pz @(JustFail (PrintF "oops=%d" Snd) Fst) (Nothing, 123)

-- Fail "oops=123"

--

-- >>> pz @(JustFail (PrintF "oops=%d" Snd) Fst) (Just 'x', 123)

-- Val 'x'

--

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]

-- | destructs an Maybe value

--   @n@ @Nothing@ receives @(PP s x,Proxy result)@ (you can use the proxy with MEmptyP)

--   @p@ @Just a@ receives @(PP s x,a)@

--   @s@ points to the environment you want to pass in

--   @t@ points to the Maybe value

--

-- >>> pz @(MaybeIn Fst Snd Fst Snd) ('a', Just 'x')

-- Val 'x'

--

-- >>> pz @(MaybeIn Fst Snd Fst Snd) ('a', Nothing)

-- Val 'a'

--

-- >>> pl @(MaybeIn "none" "just"() Id) (Just (SG.Sum 12))

-- Present "just" (MaybeIn(Just) "just" | Sum {getSum = 12})

-- Val "just"

--

-- >>> pl @(MaybeIn (Snd >> FailP "oops") Snd Fst Snd) ("abc", Nothing)

-- Error oops (Proxy | MaybeIn(Nothing) n failed)

-- Fail "oops"

--

-- >>> pl @(MaybeIn (Snd >> MEmptyP) Snd Fst Snd) ("abc", Nothing)

-- Present () (MaybeIn(Nothing) () | ())

-- Val ()

--

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

-- | calculate the return type for 'MaybeIn'

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)

-- | simple version of 'MaybeIn' with Id as the Maybe value and the environment set to ()

--

-- >>> pz @(MaybeId '("x","oops") '(Id,"fromjust")) (Just "ok")

-- Val ("ok","fromjust")

--

-- >>> pz @(MaybeId '("x","oops") '(Id,"fromjust")) Nothing

-- Val ("x","oops")

--

-- >>> pz @(MaybeId "found nothing" (ShowP Pred)) (Just 20)

-- Val "19"

--

-- >>> pz @(MaybeId "found nothing" (ShowP Pred)) Nothing

-- Val "found nothing"

--

-- >>> pl @(MaybeId 'True Id) Nothing

-- True (MaybeIn(Nothing) True | ())

-- Val True

--

-- >>> pl @(MaybeId 'True IdBool) (Just False)

-- False (MaybeIn(Just) False | False)

-- Val False

--

-- >>> pl @(MaybeId (FailT _ "failed4") Id) (Just 10)

-- Present 10 (MaybeIn(Just) 10 | 10)

-- Val 10

--

-- >>> pl @(MaybeId 'False Id) Nothing

-- False (MaybeIn(Nothing) False | ())

-- Val False

--

-- >>> pl @(MaybeId (FailT _ "err") Id) Nothing

-- Error err (Proxy | MaybeIn(Nothing) n failed)

-- Fail "err"

--

-- >>> pz @(MaybeId 99 Id) (Just 12)

-- Val 12

--

-- >>> pz @(MaybeId 99 Id) Nothing

-- Val 99

--

-- >>> pl @(MaybeId MEmptyP Ones) (Just "ab")

-- Present ["a","b"] (MaybeIn(Just) ["a","b"] | "ab")

-- Val ["a","b"]

--

-- >>> pl @(MaybeId MEmptyP Ones) Nothing

-- Present [] (MaybeIn(Nothing) [] | ())

-- Val []

--

-- >>> pl @(MaybeId MEmptyP (Fst ==! Snd)) (Just ('x','z'))

-- Present LT (MaybeIn(Just) LT | ('x','z'))

-- Val LT

--

-- >>> pl @(MaybeId MEmptyP (Fst ==! Snd)) (Nothing @(Char,Char))

-- Present EQ (MaybeIn(Nothing) EQ | ())

-- Val EQ

--

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))