{-# 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 conditional functions

module Predicate.Data.Condition (
  -- ** functions

    If
  , Case
  , Case'
  , Case''
  , Guards
  , GuardsQuick
  , Guard
  , ExitWhen
  , GuardSimple
  , GuardsN
  , GuardsDetail
  , GuardBool
  , Bools
  , BoolsQuick
  , BoolsN

  -- ** type families

  , ToGuardsT
  , ToGuardsDetailT
 ) where
import Predicate.Core
import Predicate.Misc
import Predicate.Util
import Predicate.Data.ReadShow (PrintT)
import GHC.TypeLits (Nat,KnownNat,ErrorMessage((:<>:)))
import qualified GHC.TypeLits as GL
import Control.Lens
import Data.Proxy (Proxy(..))
import Data.Kind (Type)
import Data.Void (Void)
import qualified Data.Type.Equality as DE
-- $setup

-- >>> import Predicate

-- >>> :set -XDataKinds

-- >>> :set -XTypeApplications

-- >>> :set -XTypeOperators

-- >>> :set -XAllowAmbiguousTypes

-- >>> :set -XOverloadedStrings

-- >>> :set -XFlexibleContexts

-- >>> import qualified Data.Text as T



-- | similar to an if statement: if @p@ then run @q@ else run @r@

--

-- >>> pz @(If (Gt 4) "greater than 4" "less than or equal to 4") 10

-- Val "greater than 4"

--

-- >>> pz @(If (Gt 4) "greater than 4" "less than or equal to 4") 0

-- Val "less than or equal to 4"

--

-- >>> pz @(If (Snd == "a") '("xxx",Fst + 13) (If (Snd == "b") '("yyy",Fst + 7) (FailT _ "oops"))) (99,"b")

-- Val ("yyy",106)

--

-- >>> pl @(If (Len > 2) (Map Succ) (FailS "someval")) [12,15,16]

-- Present [13,16,17] (If 'True [13,16,17])

-- Val [13,16,17]

--

-- >>> pl @(Map (If (Lt 3) 'True (FailT _ "err"))) [1..10]

-- Error err(8) (Map(i=2, a=3) excnt=8)

-- Fail "err(8)"

--

-- >>> pl @(Map (If (Lt 3) 'True (FailT _ "someval"))) [1..10]

-- Error someval(8) (Map(i=2, a=3) excnt=8)

-- Fail "someval(8)"

--

-- >>> pl @(Map (If (Lt 3) 'True 'False)) [1..5]

-- Present [True,True,False,False,False] (Map [True,True,False,False,False] | [1,2,3,4,5])

-- Val [True,True,False,False,False]

--

-- >>> pl @(If (Gt 4) (Fail (Hole _) (PrintF "failing with %d" Id)) ()) 45

-- Error failing with 45 (If 'True)

-- Fail "failing with 45"

--

-- >>> pl @(If (Gt 4) (Fail (Hole _) (PrintF "failing with %d" Id)) (Id * 7)) 3

-- Present 21 (If 'False 21)

-- Val 21

--

-- >>> pl @(If (Gt 4) (FailT _ (PrintF "failing with %d" Id)) (Id * 7 >> ShowP Id >> Ones)) 3

-- Present ["2","1"] (If 'False ["2","1"])

-- Val ["2","1"]

--

-- >>> pl @(If (Gt 4) (FailT _ (PrintF "failing with %d" Id)) (ShowP (Id * 7) >> Ones)) 19

-- Error failing with 19 (If 'True)

-- Fail "failing with 19"

--

data If p q r deriving Int -> If p q r -> ShowS
[If p q r] -> ShowS
If p q r -> String
(Int -> If p q r -> ShowS)
-> (If p q r -> String) -> ([If p q r] -> ShowS) -> Show (If p q r)
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
forall k (p :: k) k (q :: k) k (r :: k). Int -> If p q r -> ShowS
forall k (p :: k) k (q :: k) k (r :: k). [If p q r] -> ShowS
forall k (p :: k) k (q :: k) k (r :: k). If p q r -> String
showList :: [If p q r] -> ShowS
$cshowList :: forall k (p :: k) k (q :: k) k (r :: k). [If p q r] -> ShowS
show :: If p q r -> String
$cshow :: forall k (p :: k) k (q :: k) k (r :: k). If p q r -> String
showsPrec :: Int -> If p q r -> ShowS
$cshowsPrec :: forall k (p :: k) k (q :: k) k (r :: k). Int -> If p q r -> ShowS
Show

instance ( Show (PP r a)
         , P p a
         , PP p a ~ Bool
         , P q a
         , P r a
         , PP q a ~ PP r a
         ) => P (If p q r) a where
  type PP (If p q r) a = PP q a
  eval :: proxy (If p q r) -> POpts -> a -> m (TT (PP (If p q r) a))
eval proxy (If p q r)
_ POpts
opts a
a = do
    let msg0 :: String
msg0 = String
"If"
    TT Bool
pp <- Proxy p -> POpts -> a -> m (TT (PP p 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 p
forall k (t :: k). Proxy t
Proxy @p) POpts
opts a
a
    case Inline
-> POpts
-> String
-> TT Bool
-> [Tree PE]
-> Either (TT (PP r 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
" condition failed") TT Bool
pp [] of
      Left TT (PP r a)
e -> TT (PP r a) -> m (TT (PP r a))
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure TT (PP r a)
e
      Right Bool
b -> do
        TT (PP r a)
qqrr <- if Bool
b
                then 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
                else Proxy r -> POpts -> a -> m (TT (PP r 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 r
forall k (t :: k). Proxy t
Proxy @r) POpts
opts a
a
        TT (PP r a) -> m (TT (PP r a))
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (TT (PP r a) -> m (TT (PP r a))) -> TT (PP r a) -> m (TT (PP r a))
forall a b. (a -> b) -> a -> b
$ case Inline
-> POpts
-> String
-> TT (PP r a)
-> [Tree PE]
-> Either (TT (PP r a)) (PP r a)
forall a x.
Inline -> POpts -> String -> TT a -> [Tree PE] -> Either (TT x) a
getValueLR Inline
Inline POpts
opts (String
msg0 String -> ShowS
forall a. Semigroup a => a -> a -> a
<> String
" '" String -> ShowS
forall a. Semigroup a => a -> a -> a
<> Bool -> String
forall a. Show a => a -> String
show Bool
b) TT (PP r a)
qqrr [TT Bool -> Tree PE
forall a. TT a -> Tree PE
hh TT Bool
pp, TT (PP r a) -> Tree PE
forall a. TT a -> Tree PE
hh TT (PP r a)
qqrr] of
          Left TT (PP r a)
e -> TT (PP r a)
e
          Right PP r a
ret -> POpts -> TT (PP r a) -> String -> [Tree PE] -> TT (PP r a)
forall a. POpts -> TT a -> String -> [Tree PE] -> TT a
mkNodeCopy POpts
opts TT (PP r a)
qqrr (String
msg0 String -> ShowS
forall a. Semigroup a => a -> a -> a
<> String
" '" String -> ShowS
forall a. Semigroup a => a -> a -> a
<> Bool -> String
forall a. Show a => a -> String
show Bool
b String -> ShowS
forall a. Semigroup a => a -> a -> a
<> String
" " String -> ShowS
forall a. Semigroup a => a -> a -> a
<> POpts -> PP r a -> String
forall a. Show a => POpts -> a -> String
showL POpts
opts PP r a
ret) [TT Bool -> Tree PE
forall a. TT a -> Tree PE
hh TT Bool
pp]

-- | expands out the condition parameter used by 'Guards' and 'Bools'

type family ToGuardsT (prt :: k) (os :: [k1]) :: [(k,k1)] where
  ToGuardsT prt '[] = GL.TypeError
                       ('GL.Text "ToGuardsT cannot be empty: prt="
                       ':<>:
                       'GL.ShowType prt)
  ToGuardsT prt '[p] = '(prt,p) : '[]
  ToGuardsT prt (p ': ps) = '(prt,p) ': ToGuardsT prt ps

-- | tries to match the value @r@ with a condition in @ps@ and if there is a match calls the associated @qs@ entry else run @e@

--   ps = conditions

--   qs = what to do [one to one with ps]

--   r = the value

--   e = otherwise  -- leave til later

--

-- >>> pl @(Case (Snd >> FailP "xx") '[Gt 3, Lt 2, Same 3] '["gt3","lt2","eq3"] Id) 15

-- Present "gt3" (Case(0 of 2) "gt3" | 15)

-- Val "gt3"

--

-- >>> pl @(Case (Snd >> FailP "xx") '[Gt 3, Lt 2, Same 3] '["gt3","lt2","eq3"] Id) 1

-- Present "lt2" (Case(0) "lt2" | 1)

-- Val "lt2"

--

-- >>> pl @(Case (Snd >> FailP "xx") '[Gt 3, Lt 2, Same 3] '["gt3","lt2","eq3"] Id) 3

-- Present "eq3" (Case(0) "eq3" | 3)

-- Val "eq3"

--

-- >>> pl @(Case (Snd >> FailP "no match") '[Same 1, Same 2, Same 3] '["eq1","eq2","eq3"] Id) 15

-- Error no match (Case:otherwise failed:Proxy)

-- Fail "no match"

--

-- >>> pl @(Case (Fail (Snd >> UnproxyT) (PrintF "no match for %03d" Fst)) '[Same 1, Same 2, Same 3] '["eq1","eq2","eq3"] Id) 15

-- Error no match for 015 (Case:otherwise failed)

-- Fail "no match for 015"

--

-- >>> pl @(Case "other" '[Same 1, Same 2, Same 3] '["eq1","eq2","eq3"] Id) 15

-- Present "other" (Case(0) "other" | 15)

-- Val "other"

--

-- >>> pl @(Case (ShowP Fst >> Id <> Id <> Id) '[Same 1, Same 2, Same 3] '["eq1","eq2","eq3"] Id) 15

-- Present "151515" (Case(0) "151515" | 15)

-- Val "151515"

--

-- >>> pz @(Case (FailT _ "asdf") '[Lt 4,Lt 10,Same 50] '[PrintF "%d is lt4" Id, PrintF "%d is lt10" Id, PrintF "%d is same50" Id] Id) 50

-- Val "50 is same50"

--

-- >>> pz @(Case (FailT _ "asdf") '[Lt 4,Lt 10,Same 50] '[PrintF "%d is lt4" Id, PrintF "%d is lt10" Id, PrintF "%d is same50" Id] Id) 9

-- Val "9 is lt10"

--

-- >>> pz @(Case (FailT _ "asdf") '[Lt 4,Lt 10,Same 50] '[PrintF "%d is lt4" Id, PrintF "%d is lt10" Id, PrintF "%d is same50" Id] Id) 3

-- Val "3 is lt4"

--

-- >>> pz @(Case (FailT _ "asdf") '[Lt 4,Lt 10,Same 50] '[PrintF "%d is lt4" Id, PrintF "%d is lt10" Id, PrintF "%d is same50" Id] Id) 99

-- Fail "asdf"

--

-- >>> pz @(Case (FailS "asdf" >> Snd >> UnproxyT) '[Lt 4,Lt 10,Same 50] '[PrintF "%d is lt4" Id, PrintF "%d is lt10" Id, PrintF "%d is same50" Id] Id) 99

-- Fail "asdf"

--

-- >>> pz @(Case (FailT _ "x") '[Same "a",Same "b"] '["hey","there"] Id) "b"

-- Val "there"

--

-- >>> pz @(Case (FailT _ "x") '[Id == "a",Id == "b"] '["hey","there"] Id) "a"

-- Val "hey"

--

-- >>> pz @(Case (FailT _ "x") '[Same "a",Same "b"] '["hey","there"] Id) "c"

-- Fail "x"

--

data Case (e :: k0) (ps :: [k]) (qs :: [k1]) (r :: k2) deriving Int -> Case e ps qs r -> ShowS
[Case e ps qs r] -> ShowS
Case e ps qs r -> String
(Int -> Case e ps qs r -> ShowS)
-> (Case e ps qs r -> String)
-> ([Case e ps qs r] -> ShowS)
-> Show (Case e ps qs r)
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
forall k0 (e :: k0) k (ps :: [k]) k1 (qs :: [k1]) k2 (r :: k2).
Int -> Case e ps qs r -> ShowS
forall k0 (e :: k0) k (ps :: [k]) k1 (qs :: [k1]) k2 (r :: k2).
[Case e ps qs r] -> ShowS
forall k0 (e :: k0) k (ps :: [k]) k1 (qs :: [k1]) k2 (r :: k2).
Case e ps qs r -> String
showList :: [Case e ps qs r] -> ShowS
$cshowList :: forall k0 (e :: k0) k (ps :: [k]) k1 (qs :: [k1]) k2 (r :: k2).
[Case e ps qs r] -> ShowS
show :: Case e ps qs r -> String
$cshow :: forall k0 (e :: k0) k (ps :: [k]) k1 (qs :: [k1]) k2 (r :: k2).
Case e ps qs r -> String
showsPrec :: Int -> Case e ps qs r -> ShowS
$cshowsPrec :: forall k0 (e :: k0) k (ps :: [k]) k1 (qs :: [k1]) k2 (r :: k2).
Int -> Case e ps qs r -> ShowS
Show

-- | like 'Case' but uses a generic error message (skips the @e@ parameter)

--

-- >>> pl @(Case' '[Same 1, Same 2, Same 3] '["eq1","eq2","eq3"] Id) 15

-- Error Case:no match (Case:otherwise failed:Proxy)

-- Fail "Case:no match"

--

data Case' (ps :: [k]) (qs :: [k1]) (r :: k2) deriving Int -> Case' ps qs r -> ShowS
[Case' ps qs r] -> ShowS
Case' ps qs r -> String
(Int -> Case' ps qs r -> ShowS)
-> (Case' ps qs r -> String)
-> ([Case' ps qs r] -> ShowS)
-> Show (Case' ps qs r)
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
forall k (ps :: [k]) k1 (qs :: [k1]) k2 (r :: k2).
Int -> Case' ps qs r -> ShowS
forall k (ps :: [k]) k1 (qs :: [k1]) k2 (r :: k2).
[Case' ps qs r] -> ShowS
forall k (ps :: [k]) k1 (qs :: [k1]) k2 (r :: k2).
Case' ps qs r -> String
showList :: [Case' ps qs r] -> ShowS
$cshowList :: forall k (ps :: [k]) k1 (qs :: [k1]) k2 (r :: k2).
[Case' ps qs r] -> ShowS
show :: Case' ps qs r -> String
$cshow :: forall k (ps :: [k]) k1 (qs :: [k1]) k2 (r :: k2).
Case' ps qs r -> String
showsPrec :: Int -> Case' ps qs r -> ShowS
$cshowsPrec :: forall k (ps :: [k]) k1 (qs :: [k1]) k2 (r :: k2).
Int -> Case' ps qs r -> ShowS
Show

-- | like 'Case' but allows you to use the value in the error message

--

-- >>> pl @(Case'' (PrintF "no match for %03d" Id) '[Same 1, Same 2, Same 3] '["eq1","eq2","eq3"] Id) 15

-- Error no match for 015 (Case:otherwise failed)

-- Fail "no match for 015"

--

-- >>> pl @(Case'' (PrintF "no match for %03d" Id) '[Same 1, Same 2, Same 3] '["eq1","eq2","eq3"] Id) 2

-- Present "eq2" (Case(0) "eq2" | 2)

-- Val "eq2"

--

-- >>> pl @(Case'' (PrintF "no match for %04d" Id) '[Between 0 5 Id, Same 6, Between 7 10 Id] '[ 'LT, 'EQ, 'GT] Id) (-12)

-- Error no match for -012 (Case:otherwise failed)

-- Fail "no match for -012"

--

data Case'' s (ps :: [k]) (qs :: [k1]) (r :: k2) deriving Int -> Case'' s ps qs r -> ShowS
[Case'' s ps qs r] -> ShowS
Case'' s ps qs r -> String
(Int -> Case'' s ps qs r -> ShowS)
-> (Case'' s ps qs r -> String)
-> ([Case'' s ps qs r] -> ShowS)
-> Show (Case'' s ps qs r)
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
forall k (s :: k) k (ps :: [k]) k1 (qs :: [k1]) k2 (r :: k2).
Int -> Case'' s ps qs r -> ShowS
forall k (s :: k) k (ps :: [k]) k1 (qs :: [k1]) k2 (r :: k2).
[Case'' s ps qs r] -> ShowS
forall k (s :: k) k (ps :: [k]) k1 (qs :: [k1]) k2 (r :: k2).
Case'' s ps qs r -> String
showList :: [Case'' s ps qs r] -> ShowS
$cshowList :: forall k (s :: k) k (ps :: [k]) k1 (qs :: [k1]) k2 (r :: k2).
[Case'' s ps qs r] -> ShowS
show :: Case'' s ps qs r -> String
$cshow :: forall k (s :: k) k (ps :: [k]) k1 (qs :: [k1]) k2 (r :: k2).
Case'' s ps qs r -> String
showsPrec :: Int -> Case'' s ps qs r -> ShowS
$cshowsPrec :: forall k (s :: k) k (ps :: [k]) k1 (qs :: [k1]) k2 (r :: k2).
Int -> Case'' s ps qs r -> ShowS
Show

type CaseT' (ps :: [k]) (qs :: [k1]) (r :: k2) = Case (Snd >> FailP "Case:no match") ps qs r
type CaseT'' s (ps :: [k]) (qs :: [k1]) (r :: k2) = Case (FailCaseT s) ps qs r -- eg s= PrintF "%s" (ShowP Id)


instance P (CaseT'' s ps qs r) x => P (Case'' s ps qs r) x where
  type PP (Case'' s ps qs r) x = PP (CaseT'' s ps qs r) x
  eval :: proxy (Case'' s ps qs r)
-> POpts -> x -> m (TT (PP (Case'' s ps qs r) x))
eval proxy (Case'' s ps qs r)
_ = Proxy (CaseT'' s ps qs r)
-> POpts -> x -> m (TT (PP (CaseT'' s ps qs r) 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 (CaseT'' s ps qs r)
forall k (t :: k). Proxy t
Proxy @(CaseT'' s ps qs r))

instance P (CaseT' ps qs r) x => P (Case' ps qs r) x where
  type PP (Case' ps qs r) x = PP (CaseT' ps qs r) x
  eval :: proxy (Case' ps qs r)
-> POpts -> x -> m (TT (PP (Case' ps qs r) x))
eval proxy (Case' ps qs r)
_ = Proxy (CaseT' ps qs r)
-> POpts -> x -> m (TT (PP (CaseT' ps qs r) 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 (CaseT' ps qs r)
forall k (t :: k). Proxy t
Proxy @(CaseT' ps qs r))

type FailCaseT p = Fail (Snd >> UnproxyT) (Fst >> p)

type CaseImplT e ps qs r = CaseImpl (LenT ps) e ps qs r

-- passthru but adds the length of ps (replaces LenT in the type synonym to avoid type synonyms being expanded out

instance (FailUnlessT (LenT ps DE.== LenT qs)
                  ('GL.Text "lengths are not the same "
                   ':<>: 'GL.ShowType (LenT ps)
                   ':<>: 'GL.Text " vs "
                   ':<>: 'GL.ShowType (LenT qs))
        , P (CaseImplT e ps qs r) x
        ) => P (Case e ps qs r) x where
  type PP (Case e ps qs r) x = PP (CaseImplT e ps qs r) x
  eval :: proxy (Case e ps qs r)
-> POpts -> x -> m (TT (PP (Case e ps qs r) x))
eval proxy (Case e ps qs r)
_ = Proxy (CaseImplT e ps qs r)
-> POpts -> x -> m (TT (PP (CaseImplT e ps qs r) 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 (CaseImplT e ps qs r)
forall k (t :: k). Proxy t
Proxy @(CaseImplT e ps qs r))

data CaseImpl (n :: Nat) (e :: k0) (ps :: [k]) (qs :: [k1]) (r :: k2) deriving Int -> CaseImpl n e ps qs r -> ShowS
[CaseImpl n e ps qs r] -> ShowS
CaseImpl n e ps qs r -> String
(Int -> CaseImpl n e ps qs r -> ShowS)
-> (CaseImpl n e ps qs r -> String)
-> ([CaseImpl n e ps qs r] -> ShowS)
-> Show (CaseImpl n e ps qs r)
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
forall (n :: Nat) k0 (e :: k0) k (ps :: [k]) k1 (qs :: [k1]) k2
       (r :: k2).
Int -> CaseImpl n e ps qs r -> ShowS
forall (n :: Nat) k0 (e :: k0) k (ps :: [k]) k1 (qs :: [k1]) k2
       (r :: k2).
[CaseImpl n e ps qs r] -> ShowS
forall (n :: Nat) k0 (e :: k0) k (ps :: [k]) k1 (qs :: [k1]) k2
       (r :: k2).
CaseImpl n e ps qs r -> String
showList :: [CaseImpl n e ps qs r] -> ShowS
$cshowList :: forall (n :: Nat) k0 (e :: k0) k (ps :: [k]) k1 (qs :: [k1]) k2
       (r :: k2).
[CaseImpl n e ps qs r] -> ShowS
show :: CaseImpl n e ps qs r -> String
$cshow :: forall (n :: Nat) k0 (e :: k0) k (ps :: [k]) k1 (qs :: [k1]) k2
       (r :: k2).
CaseImpl n e ps qs r -> String
showsPrec :: Int -> CaseImpl n e ps qs r -> ShowS
$cshowsPrec :: forall (n :: Nat) k0 (e :: k0) k (ps :: [k]) k1 (qs :: [k1]) k2
       (r :: k2).
Int -> CaseImpl n e ps qs r -> ShowS
Show

-- only allow non empty lists!

instance (GL.TypeError ('GL.Text "CaseImpl '[] invalid: lhs requires at least one value in the list"))
   => P (CaseImpl n e ('[] :: [k]) (q ': qs) r) x where
  type PP (CaseImpl n e ('[] :: [k]) (q ': qs) r) x = Void
  eval :: proxy (CaseImpl n e '[] (q : qs) r)
-> POpts -> x -> m (TT (PP (CaseImpl n e '[] (q : qs) r) x))
eval proxy (CaseImpl n e '[] (q : qs) r)
_ POpts
_ x
_ = String -> m (TT Void)
forall x. HasCallStack => String -> x
errorInProgram String
"CaseImpl lhs empty"

instance (GL.TypeError ('GL.Text "CaseImpl '[] invalid: rhs requires at least one value in the list"))
   => P (CaseImpl n e (p ': ps) ('[] :: [k1]) r) x where
  type PP (CaseImpl n e (p ': ps) ('[] :: [k1]) r) x = Void
  eval :: proxy (CaseImpl n e (p : ps) '[] r)
-> POpts -> x -> m (TT (PP (CaseImpl n e (p : ps) '[] r) x))
eval proxy (CaseImpl n e (p : ps) '[] r)
_ POpts
_ x
_ = String -> m (TT Void)
forall x. HasCallStack => String -> x
errorInProgram String
"CaseImpl rhs empty"

instance (GL.TypeError ('GL.Text "CaseImpl '[] invalid: lists are both empty"))
   => P (CaseImpl n e ('[] :: [k]) ('[] :: [k1]) r) x where
  type PP (CaseImpl n e ('[] :: [k]) ('[] :: [k1]) r) x = Void
  eval :: proxy (CaseImpl n e '[] '[] r)
-> POpts -> x -> m (TT (PP (CaseImpl n e '[] '[] r) x))
eval proxy (CaseImpl n e '[] '[] r)
_ POpts
_ x
_ = String -> m (TT Void)
forall x. HasCallStack => String -> x
errorInProgram String
"CaseImpl both lists empty"

instance ( P r x
         , P q (PP r x)
         , Show (PP q (PP r x))
         , P p (PP r x)
         , PP p (PP r x) ~ Bool
         , KnownNat n
         , Show (PP r x)
         , P e (PP r x, Proxy (PP q (PP r x)))
         , PP e (PP r x, Proxy (PP q (PP r x))) ~ PP q (PP r x)
         ) => P (CaseImpl n e '[p] '[q] r) x where
  type PP (CaseImpl n e '[p] '[q] r) x = PP q (PP r x)
  eval :: proxy (CaseImpl n e '[p] '[q] r)
-> POpts -> x -> m (TT (PP (CaseImpl n e '[p] '[q] r) x))
eval proxy (CaseImpl n e '[p] '[q] r)
_ POpts
opts x
z = do
    let msgbase0 :: String
msgbase0 = String
"Case(" String -> ShowS
forall a. Semigroup a => a -> a -> a
<> Int -> String
forall a. Show a => a -> String
show (Int
nInt -> Int -> Int
forall a. Num a => a -> a -> a
-Int
1) String -> ShowS
forall a. Semigroup a => a -> a -> a
<> String
")"
        n :: Int
n = (KnownNat n, Num Int) => Int
forall (n :: Nat) a. (KnownNat n, Num a) => a
nat @n @Int
    TT (PP r x)
rr <- Proxy r -> POpts -> x -> m (TT (PP r 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 r
forall k (t :: k). Proxy t
Proxy @r) POpts
opts x
z
    case Inline
-> POpts
-> String
-> TT (PP r x)
-> [Tree PE]
-> Either (TT (PP q (PP r x))) (PP r x)
forall a x.
Inline -> POpts -> String -> TT a -> [Tree PE] -> Either (TT x) a
getValueLR Inline
NoInline POpts
opts String
msgbase0 TT (PP r x)
rr [] of
      Left TT (PP q (PP r x))
e -> TT (PP q (PP r x)) -> m (TT (PP q (PP r x)))
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure TT (PP q (PP r x))
e
      Right PP r x
a -> do
        TT Bool
pp <- Proxy p -> POpts -> PP r x -> m (TT (PP p (PP r x)))
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 p
forall k (t :: k). Proxy t
Proxy @p) POpts
opts PP r x
a
        case Inline
-> POpts
-> String
-> TT Bool
-> [Tree PE]
-> Either (TT (PP q (PP r x))) Bool
forall a x.
Inline -> POpts -> String -> TT a -> [Tree PE] -> Either (TT x) a
getValueLR Inline
NoInline POpts
opts String
msgbase0 TT Bool
pp [TT (PP r x) -> Tree PE
forall a. TT a -> Tree PE
hh TT (PP r x)
rr] of
          Left TT (PP q (PP r x))
e -> TT (PP q (PP r x)) -> m (TT (PP q (PP r x)))
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure TT (PP q (PP r x))
e
          Right Bool
True -> do
            TT (PP q (PP r x))
qq <- Proxy q -> POpts -> PP r x -> m (TT (PP q (PP r 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 PP r x
a
            TT (PP q (PP r x)) -> m (TT (PP q (PP r x)))
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (TT (PP q (PP r x)) -> m (TT (PP q (PP r x))))
-> TT (PP q (PP r x)) -> m (TT (PP q (PP r x)))
forall a b. (a -> b) -> a -> b
$ case Inline
-> POpts
-> String
-> TT (PP q (PP r x))
-> [Tree PE]
-> Either (TT (PP q (PP r x))) (PP q (PP r x))
forall a x.
Inline -> POpts -> String -> TT a -> [Tree PE] -> Either (TT x) a
getValueLR Inline
NoInline POpts
opts String
msgbase0 TT (PP q (PP r x))
qq [TT (PP r x) -> Tree PE
forall a. TT a -> Tree PE
hh TT (PP r x)
rr, TT Bool -> Tree PE
forall a. TT a -> Tree PE
hh TT Bool
pp] of
              Left TT (PP q (PP r x))
e -> TT (PP q (PP r x))
e
              Right PP q (PP r x)
q -> POpts
-> TT (PP q (PP r x)) -> String -> [Tree PE] -> TT (PP q (PP r x))
forall a. POpts -> TT a -> String -> [Tree PE] -> TT a
mkNodeCopy POpts
opts TT (PP q (PP r x))
qq (POpts -> String -> PP q (PP r x) -> PP r x -> String
forall a1 a2.
(Show a1, Show a2) =>
POpts -> String -> a1 -> a2 -> String
show3 POpts
opts String
msgbase0 PP q (PP r x)
q PP r x
a) [TT (PP r x) -> Tree PE
forall a. TT a -> Tree PE
hh TT (PP r x)
rr, TT Bool -> Tree PE
forall a. TT a -> Tree PE
hh TT Bool
pp]
          Right Bool
False -> do
            TT (PP q (PP r x))
ww <- Proxy e
-> POpts
-> (PP r x, Proxy (PP q (PP r x)))
-> m (TT (PP e (PP r x, Proxy (PP q (PP r 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 e
forall k (t :: k). Proxy t
Proxy @e) POpts
opts (PP r x
a, Proxy (PP q (PP r x))
forall k (t :: k). Proxy t
Proxy @(PP q (PP r x)))
            TT (PP q (PP r x)) -> m (TT (PP q (PP r x)))
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (TT (PP q (PP r x)) -> m (TT (PP q (PP r x))))
-> TT (PP q (PP r x)) -> m (TT (PP q (PP r x)))
forall a b. (a -> b) -> a -> b
$ case Inline
-> POpts
-> String
-> TT (PP q (PP r x))
-> [Tree PE]
-> Either (TT (PP q (PP r x))) (PP q (PP r x))
forall a x.
Inline -> POpts -> String -> TT a -> [Tree PE] -> Either (TT x) a
getValueLR Inline
NoInline POpts
opts (String
"Case:otherwise failed" String -> ShowS
forall a. Semigroup a => a -> a -> a
<> String -> ShowS
nullIf String
":" (TT (PP q (PP r x))
ww TT (PP q (PP r x))
-> Getting String (TT (PP q (PP r x))) String -> String
forall s a. s -> Getting a s a -> a
^. Getting String (TT (PP q (PP r x))) String
forall a. Lens' (TT a) String
ttString)) TT (PP q (PP r x))
ww [TT (PP r x) -> Tree PE
forall a. TT a -> Tree PE
hh TT (PP r x)
rr, TT Bool -> Tree PE
forall a. TT a -> Tree PE
hh TT Bool
pp] of
              Left TT (PP q (PP r x))
e -> TT (PP q (PP r x))
e
              Right PP q (PP r x)
w -> POpts
-> TT (PP q (PP r x)) -> String -> [Tree PE] -> TT (PP q (PP r x))
forall a. POpts -> TT a -> String -> [Tree PE] -> TT a
mkNodeCopy POpts
opts TT (PP q (PP r x))
ww (POpts -> String -> PP q (PP r x) -> PP r x -> String
forall a1 a2.
(Show a1, Show a2) =>
POpts -> String -> a1 -> a2 -> String
show3 POpts
opts String
msgbase0 PP q (PP r x)
w PP r x
a) [TT (PP r x) -> Tree PE
forall a. TT a -> Tree PE
hh TT (PP r x)
rr, TT Bool -> Tree PE
forall a. TT a -> Tree PE
hh TT Bool
pp]

instance ( KnownNat n
         , GetLen ps
         , P r x
         , P p (PP r x)
         , P q (PP r x)
         , PP p (PP r x) ~ Bool
         , Show (PP q (PP r x))
         , Show (PP r x)
         , P (CaseImpl n e (p1 ': ps) (q1 ': qs) r) x
         , PP (CaseImpl n e (p1 ': ps) (q1 ': qs) r) x ~ PP q (PP r x)
         )
     => P (CaseImpl n e (p ': p1 ': ps) (q ': q1 ': qs) r) x where
  type PP (CaseImpl n e (p ': p1 ': ps) (q ': q1 ': qs) r) x = PP q (PP r x)
  eval :: proxy (CaseImpl n e (p : p1 : ps) (q : q1 : qs) r)
-> POpts
-> x
-> m (TT (PP (CaseImpl n e (p : p1 : ps) (q : q1 : qs) r) x))
eval proxy (CaseImpl n e (p : p1 : ps) (q : q1 : qs) r)
_ POpts
opts x
z = do
    let cpos :: Int
cpos = Int
nInt -> Int -> Int
forall a. Num a => a -> a -> a
-Int
posInt -> Int -> Int
forall a. Num a => a -> a -> a
-Int
1
        msgbase0 :: String
msgbase0 = String
"Case(" String -> ShowS
forall a. Semigroup a => a -> a -> a
<> Int -> String
forall a. Show a => a -> String
show Int
cpos String -> ShowS
forall a. Semigroup a => a -> a -> a
<> String
" of " String -> ShowS
forall a. Semigroup a => a -> a -> a
<> Int -> String
forall a. Show a => a -> String
show (Int
nInt -> Int -> Int
forall a. Num a => a -> a -> a
-Int
1) String -> ShowS
forall a. Semigroup a => a -> a -> a
<> String
")"
        msgbase1 :: String
msgbase1 = String
"Case(" String -> ShowS
forall a. Semigroup a => a -> a -> a
<> Int -> String
forall a. Show a => a -> String
show Int
cpos String -> ShowS
forall a. Semigroup a => a -> a -> a
<> String
")"
        n :: Int
n = forall a. (KnownNat n, Num a) => a
forall (n :: Nat) a. (KnownNat n, Num a) => a
nat @n
        pos :: Int
pos = Int
1 Int -> Int -> Int
forall a. Num a => a -> a -> a
+ GetLen ps => Int
forall k (xs :: k). GetLen xs => Int
getLen @ps
    TT (PP r x)
rr <- Proxy r -> POpts -> x -> m (TT (PP r 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 r
forall k (t :: k). Proxy t
Proxy @r) POpts
opts x
z
    case Inline
-> POpts
-> String
-> TT (PP r x)
-> [Tree PE]
-> Either (TT (PP q (PP r x))) (PP r x)
forall a x.
Inline -> POpts -> String -> TT a -> [Tree PE] -> Either (TT x) a
getValueLR Inline
NoInline POpts
opts String
msgbase0 TT (PP r x)
rr [] of
      Left TT (PP q (PP r x))
e -> TT (PP q (PP r x)) -> m (TT (PP q (PP r x)))
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure TT (PP q (PP r x))
e
      Right PP r x
a -> do
        TT Bool
pp <- Proxy p -> POpts -> PP r x -> m (TT (PP p (PP r x)))
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 p
forall k (t :: k). Proxy t
Proxy @p) POpts
opts PP r x
a
        case Inline
-> POpts
-> String
-> TT Bool
-> [Tree PE]
-> Either (TT (PP q (PP r x))) Bool
forall a x.
Inline -> POpts -> String -> TT a -> [Tree PE] -> Either (TT x) a
getValueLR Inline
NoInline POpts
opts String
msgbase0 TT Bool
pp [TT (PP r x) -> Tree PE
forall a. TT a -> Tree PE
hh TT (PP r x)
rr] of
          Left TT (PP q (PP r x))
e -> TT (PP q (PP r x)) -> m (TT (PP q (PP r x)))
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure TT (PP q (PP r x))
e
          Right Bool
True -> do
            TT (PP q (PP r x))
qq <- Proxy q -> POpts -> PP r x -> m (TT (PP q (PP r 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 PP r x
a
            TT (PP q (PP r x)) -> m (TT (PP q (PP r x)))
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (TT (PP q (PP r x)) -> m (TT (PP q (PP r x))))
-> TT (PP q (PP r x)) -> m (TT (PP q (PP r x)))
forall a b. (a -> b) -> a -> b
$ case Inline
-> POpts
-> String
-> TT (PP q (PP r x))
-> [Tree PE]
-> Either (TT (PP q (PP r x))) (PP q (PP r x))
forall a x.
Inline -> POpts -> String -> TT a -> [Tree PE] -> Either (TT x) a
getValueLR Inline
NoInline POpts
opts String
msgbase0 TT (PP q (PP r x))
qq [TT Bool -> Tree PE
forall a. TT a -> Tree PE
hh TT Bool
pp, TT (PP r x) -> Tree PE
forall a. TT a -> Tree PE
hh TT (PP r x)
rr] of
              Left TT (PP q (PP r x))
e -> TT (PP q (PP r x))
e
              Right PP q (PP r x)
q -> POpts
-> TT (PP q (PP r x)) -> String -> [Tree PE] -> TT (PP q (PP r x))
forall a. POpts -> TT a -> String -> [Tree PE] -> TT a
mkNodeCopy POpts
opts TT (PP q (PP r x))
qq (POpts -> String -> PP q (PP r x) -> PP r x -> String
forall a1 a2.
(Show a1, Show a2) =>
POpts -> String -> a1 -> a2 -> String
show3 POpts
opts String
msgbase0 PP q (PP r x)
q PP r x
a) [TT (PP r x) -> Tree PE
forall a. TT a -> Tree PE
hh TT (PP r x)
rr, TT Bool -> Tree PE
forall a. TT a -> Tree PE
hh TT Bool
pp]
          Right Bool
False -> do
            TT (PP q (PP r x))
ww <- Proxy (CaseImpl n e (p1 : ps) (q1 : qs) r)
-> POpts -> x -> m (TT (PP (CaseImpl n e (p1 : ps) (q1 : qs) r) 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 (CaseImpl n e (p1 : ps) (q1 : qs) r)
forall k (t :: k). Proxy t
Proxy @(CaseImpl n e (p1 ': ps) (q1 ': qs) r)) POpts
opts x
z
            TT (PP q (PP r x)) -> m (TT (PP q (PP r x)))
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (TT (PP q (PP r x)) -> m (TT (PP q (PP r x))))
-> TT (PP q (PP r x)) -> m (TT (PP q (PP r x)))
forall a b. (a -> b) -> a -> b
$ case Inline
-> POpts
-> String
-> TT (PP q (PP r x))
-> [Tree PE]
-> Either (TT (PP q (PP r x))) (PP q (PP r x))
forall a x.
Inline -> POpts -> String -> TT a -> [Tree PE] -> Either (TT x) a
getValueLR Inline
Inline POpts
opts String
"" TT (PP q (PP r x))
ww [TT (PP r x) -> Tree PE
forall a. TT a -> Tree PE
hh TT (PP r x)
rr, TT Bool -> Tree PE
forall a. TT a -> Tree PE
hh TT Bool
pp] of
              Left TT (PP q (PP r x))
e -> TT (PP q (PP r x))
e
              Right PP q (PP r x)
w -> POpts
-> TT (PP q (PP r x)) -> String -> [Tree PE] -> TT (PP q (PP r x))
forall a. POpts -> TT a -> String -> [Tree PE] -> TT a
mkNodeCopy POpts
opts TT (PP q (PP r x))
ww (POpts -> String -> PP q (PP r x) -> PP r x -> String
forall a1 a2.
(Show a1, Show a2) =>
POpts -> String -> a1 -> a2 -> String
show3 POpts
opts String
msgbase1 PP q (PP r x)
w PP r x
a) [TT (PP r x) -> Tree PE
forall a. TT a -> Tree PE
hh TT (PP r x)
rr, TT Bool -> Tree PE
forall a. TT a -> Tree PE
hh TT Bool
pp]


data GuardsImpl (n :: Nat) (os :: [(k,k1)]) deriving Int -> GuardsImpl n os -> ShowS
[GuardsImpl n os] -> ShowS
GuardsImpl n os -> String
(Int -> GuardsImpl n os -> ShowS)
-> (GuardsImpl n os -> String)
-> ([GuardsImpl n os] -> ShowS)
-> Show (GuardsImpl n os)
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
forall (n :: Nat) k k1 (os :: [(k, k1)]).
Int -> GuardsImpl n os -> ShowS
forall (n :: Nat) k k1 (os :: [(k, k1)]).
[GuardsImpl n os] -> ShowS
forall (n :: Nat) k k1 (os :: [(k, k1)]). GuardsImpl n os -> String
showList :: [GuardsImpl n os] -> ShowS
$cshowList :: forall (n :: Nat) k k1 (os :: [(k, k1)]).
[GuardsImpl n os] -> ShowS
show :: GuardsImpl n os -> String
$cshow :: forall (n :: Nat) k k1 (os :: [(k, k1)]). GuardsImpl n os -> String
showsPrec :: Int -> GuardsImpl n os -> ShowS
$cshowsPrec :: forall (n :: Nat) k k1 (os :: [(k, k1)]).
Int -> GuardsImpl n os -> ShowS
Show

-- | Guards contain a type level list of tuples the action to run on failure of the predicate and the predicate itself

--   Each tuple validating against the corresponding value in a value list

--

-- @prt@ receives (Int,a) as input which is the position and value if there is a failure

--

-- >>> pz @(Guards '[ '("arg1 failed",Gt 4), '("arg2 failed", Same 4)]) [17,4]

-- Val [17,4]

--

-- >>> pz @(Guards '[ '("arg1 failed",Gt 4), '("arg2 failed", Same 5)]) [17,4]

-- Fail "arg2 failed"

--

-- >>> pz @(Guards '[ '("arg1 failed",Gt 99), '("arg2 failed", Same 4)]) [17,4]

-- Fail "arg1 failed"

--

-- >>> pz @(Guards '[ '(PrintT "arg %d failed with value %d" Id,Gt 4), '(PrintT "%d %d" Id, Same 4)]) [17,3]

-- Fail "1 3"

--

-- >>> pz @(Msg "isbn10" (Resplit "-") >> Concat >> 'Just Unsnoc >> Map (ReadP Int (Singleton Id)) *** If (Singleton Id ==~ "X") 10 (ReadP Int (Singleton Id)) >> ZipWith (Fst * Snd) (1...10 >> Reverse) (Fst +: Snd) >> Sum >> Guard ("mod 0 oops") (Id `Mod` 11 == 0)) "0-306-40614-X"

-- Fail "mod 0 oops"

--

-- >>> pz @(Resplit "-" >> Concat >> 'Just Unsnoc >> Map (ReadP Int (Singleton Id)) *** If (Singleton Id ==~ "X") 10 (ReadP Int (Singleton Id)) >> ZipWith (Fst * Snd) (1...10 >> Reverse) (Fst +: Snd) >> Sum >> Guard ("mod 0 oops") (Id `Mod` 11 == 0)) "0-306-40611-X"

-- Val 132

--

-- >>> pz @(Msg "isbn13" (Resplit "-") >> Concat >> Map (ReadP Int (Singleton Id)) >> ZipWith (Fst * Snd) (Cycle 13 [1,3] >> Reverse) Id >> Sum >> '(Id,Id `Mod` 10) >> Guard (PrintT "sum=%d mod 10=%d" Id) (Snd == 0)) "978-0-306-40615-7"

-- Val (100,0)

--

-- >>> pz @(Resplit "-" >> Concat >> Map (ReadP Int (Singleton Id)) >> ZipWith (Fst * Snd) (Cycle 13 [1,3] >> Reverse) Id >> Sum >> '(Id,Id `Mod` 10) >> Guard (PrintT "sum=%d mod 10=%d" Id) (Snd == 0)) "978-0-306-40615-8"

-- Fail "sum=101 mod 10=1"

--

-- >>> pz @(Do '[Resplit "-", Concat, ZipWith (Fst * Snd) (Cycle 13 [1,3]) (Map (ReadP Int (Singleton Id))), Sum, Guard (PrintF "%d is not evenly divisible by 10" Id) (Id `Mod` 10 == 0)]) "978-0-7167-0344-9"

-- Fail "109 is not evenly divisible by 10"

--

-- >>> pz @(Do '[Resplit "-", Concat, ZipWith (Fst * Snd) (Cycle 13 [1,3]) (Map (ReadP Int (Singleton Id))), Sum, Guard (PrintF "%d is not evenly divisible by 10" Id) (Id `Mod` 10 == 0)]) "978-0-7167-0344-0"

-- Val 100

--

data Guards (ps :: [(k,k1)]) deriving Int -> Guards ps -> ShowS
[Guards ps] -> ShowS
Guards ps -> String
(Int -> Guards ps -> ShowS)
-> (Guards ps -> String)
-> ([Guards ps] -> ShowS)
-> Show (Guards ps)
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
forall k k1 (ps :: [(k, k1)]). Int -> Guards ps -> ShowS
forall k k1 (ps :: [(k, k1)]). [Guards ps] -> ShowS
forall k k1 (ps :: [(k, k1)]). Guards ps -> String
showList :: [Guards ps] -> ShowS
$cshowList :: forall k k1 (ps :: [(k, k1)]). [Guards ps] -> ShowS
show :: Guards ps -> String
$cshow :: forall k k1 (ps :: [(k, k1)]). Guards ps -> String
showsPrec :: Int -> Guards ps -> ShowS
$cshowsPrec :: forall k k1 (ps :: [(k, k1)]). Int -> Guards ps -> ShowS
Show

instance ( [a] ~ x
         , GetLen ps
         , P (GuardsImpl (LenT ps) ps) x
         ) => P (Guards ps) x where
  type PP (Guards ps) x = PP (GuardsImpl (LenT ps) ps) x
  eval :: proxy (Guards ps) -> POpts -> x -> m (TT (PP (Guards ps) x))
eval proxy (Guards ps)
_ POpts
opts x
as' = do
    let msg0 :: String
msg0 = String
"Guards"
        n :: Int
n = GetLen ps => Int
forall k (xs :: k). GetLen xs => Int
getLen @ps
    case POpts
-> String
-> [a]
-> [Tree PE]
-> Either (TT (PP (GuardsImpl (LenT ps) ps) [a])) (Int, [a])
forall (t :: Type -> Type) a x.
Foldable t =>
POpts -> String -> t a -> [Tree PE] -> Either (TT x) (Int, [a])
chkSize POpts
opts String
msg0 x
[a]
as' [] of
      Left TT (PP (GuardsImpl (LenT ps) ps) [a])
e -> TT (PP (GuardsImpl (LenT ps) ps) [a])
-> m (TT (PP (GuardsImpl (LenT ps) ps) [a]))
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure TT (PP (GuardsImpl (LenT ps) ps) [a])
e
      Right (Int
asLen,[a]
as)
           | Int
n Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
asLen -> Proxy (GuardsImpl (LenT ps) ps)
-> POpts -> [a] -> m (TT (PP (GuardsImpl (LenT ps) ps) [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 (GuardsImpl (LenT ps) ps)
forall k (t :: k). Proxy t
Proxy @(GuardsImpl (LenT ps) ps)) POpts
opts [a]
as
           | Bool
otherwise ->
               let msg2 :: String
msg2 = String
msg0 String -> ShowS
forall a. Semigroup a => a -> a -> a
<> Int -> Int -> String
badLength Int
asLen Int
n
               in TT (PP (GuardsImpl (LenT ps) ps) [a])
-> m (TT (PP (GuardsImpl (LenT ps) ps) [a]))
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (TT (PP (GuardsImpl (LenT ps) ps) [a])
 -> m (TT (PP (GuardsImpl (LenT ps) ps) [a])))
-> TT (PP (GuardsImpl (LenT ps) ps) [a])
-> m (TT (PP (GuardsImpl (LenT ps) ps) [a]))
forall a b. (a -> b) -> a -> b
$ POpts
-> Val (PP (GuardsImpl (LenT ps) ps) [a])
-> String
-> [Tree PE]
-> TT (PP (GuardsImpl (LenT ps) ps) [a])
forall a. POpts -> Val a -> String -> [Tree PE] -> TT a
mkNode POpts
opts (String -> Val (PP (GuardsImpl (LenT ps) ps) [a])
forall a. String -> Val a
Fail String
msg2) String
"" []

instance ( [a] ~ x
         , Show a
         , KnownNat n
         ) => P (GuardsImpl n ('[] :: [(k,k1)])) x where
  type PP (GuardsImpl n ('[] :: [(k,k1)])) x = x

  eval :: proxy (GuardsImpl n '[])
-> POpts -> x -> m (TT (PP (GuardsImpl n '[]) x))
eval proxy (GuardsImpl n '[])
_ POpts
_ as :: x
as@(_:_) = String -> m (TT [a])
forall x. HasCallStack => String -> x
errorInProgram (String -> m (TT [a])) -> String -> m (TT [a])
forall a b. (a -> b) -> a -> b
$ String
"GuardsImpl base case has extra data " String -> ShowS
forall a. [a] -> [a] -> [a]
++ x -> String
forall a. Show a => a -> String
show x
as

  eval proxy (GuardsImpl n '[])
_ POpts
opts [] =
    let n :: Int
n = (KnownNat n, Num Int) => Int
forall (n :: Nat) a. (KnownNat n, Num a) => a
nat @n @Int
    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
$ 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 []) (String
"Guards(" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
n String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
")") []

instance ( PP prt (Int, a) ~ String
         , P prt (Int, a)
         , KnownNat n
         , GetLen ps
         , P p a
         , PP p a ~ Bool
         , P (GuardsImpl n ps) x
         , PP (GuardsImpl n ps) x ~ x
         , Show a
         , [a] ~ x
         ) => P (GuardsImpl n ('(prt,p) ': ps)) x where
  type PP (GuardsImpl n ('(prt,p) ': ps)) x = x

  eval :: proxy (GuardsImpl n ('(prt, p) : ps))
-> POpts -> x -> m (TT (PP (GuardsImpl n ('(prt, p) : ps)) x))
eval proxy (GuardsImpl n ('(prt, p) : ps))
_ POpts
_ [] = String -> m (TT [a])
forall x. HasCallStack => String -> x
errorInProgram String
"GuardsImpl n+1 case has no data"

  eval proxy (GuardsImpl n ('(prt, p) : ps))
_ POpts
opts (a:as) = do
     let cpos :: Int
cpos = Int
nInt -> Int -> Int
forall a. Num a => a -> a -> a
-Int
posInt -> Int -> Int
forall a. Num a => a -> a -> a
-Int
1
         msgbase1 :: String
msgbase1 = String
"Guard(" String -> ShowS
forall a. Semigroup a => a -> a -> a
<> Int -> String
forall a. Show a => a -> String
show Int
cpos String -> ShowS
forall a. Semigroup a => a -> a -> a
<> String
")"
         msgbase2 :: String
msgbase2 = String
"Guards"
         n :: Int
n = (KnownNat n, Num Int) => Int
forall (n :: Nat) a. (KnownNat n, Num a) => a
nat @n @Int
         pos :: Int
pos = GetLen ps => Int
forall k (xs :: k). GetLen xs => Int
getLen @ps
     TT Bool
pp <- POpts -> a -> m (TT (PP p a))
forall k (p :: k) a (m :: Type -> Type).
(MonadEval m, P p a, PP p a ~ Bool) =>
POpts -> a -> m (TT (PP p a))
evalBoolHide @p POpts
opts a
a
     case Inline
-> POpts -> String -> TT Bool -> [Tree PE] -> Either (TT [a]) Bool
forall a x.
Inline -> POpts -> String -> TT a -> [Tree PE] -> Either (TT x) a
getValueLR Inline
NoInline POpts
opts (String
msgbase1 String -> ShowS
forall a. Semigroup a => a -> a -> a
<> String
" p failed") TT Bool
pp [] 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 Bool
False -> do
         TT String
qq <- Proxy prt -> POpts -> (Int, a) -> m (TT (PP prt (Int, 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 prt
forall k (t :: k). Proxy t
Proxy @prt) POpts
opts (Int
cpos,a
a) -- only run prt when predicate is False

         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
msgbase2 String -> ShowS
forall a. Semigroup a => a -> a -> a
<> String
" False predicate and prt failed") TT String
qq [TT Bool -> Tree PE
forall a. TT a -> Tree PE
hh TT Bool
pp] of
            Left TT [a]
e -> TT [a]
e
            Right String
msgx -> 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
msgx) (String
msgbase1 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) (TT Bool -> Tree PE
forall a. TT a -> Tree PE
hh TT Bool
pp Tree PE -> [Tree PE] -> [Tree PE]
forall a. a -> [a] -> [a]
: POpts -> TT String -> [Tree PE]
forall a. POpts -> TT a -> [Tree PE]
verboseList POpts
opts TT String
qq)
       Right Bool
True -> do
         TT [a]
ss <- Proxy (GuardsImpl n ps)
-> POpts -> [a] -> m (TT (PP (GuardsImpl n ps) [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 (GuardsImpl n ps)
forall k (t :: k). Proxy t
Proxy @(GuardsImpl n ps)) POpts
opts [a]
as
         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
Inline POpts
opts String
"" TT [a]
ss [TT Bool -> Tree PE
forall a. TT a -> Tree PE
hh TT Bool
pp] of
           Left TT [a]
e -> TT [a]
e -- shortcut else we get too compounding errors with the pp tree being added each time!

           Right [a]
zs -> TT [a]
ss TT [a] -> (TT [a] -> TT [a]) -> TT [a]
forall a b. a -> (a -> b) -> b
& ([Tree PE] -> Identity [Tree PE]) -> TT [a] -> Identity (TT [a])
forall a. Lens' (TT a) [Tree PE]
ttForest (([Tree PE] -> Identity [Tree PE]) -> TT [a] -> Identity (TT [a]))
-> ([Tree PE] -> [Tree PE]) -> TT [a] -> TT [a]
forall s t a b. ASetter s t a b -> (a -> b) -> s -> t
%~ (TT Bool -> Tree PE
forall a. TT a -> Tree PE
hh TT Bool
ppTree PE -> [Tree PE] -> [Tree PE]
forall a. a -> [a] -> [a]
:)
                          TT [a] -> (TT [a] -> TT [a]) -> TT [a]
forall a b. a -> (a -> b) -> b
& (Val [a] -> Identity (Val [a])) -> TT [a] -> Identity (TT [a])
forall a b. Lens (TT a) (TT b) (Val a) (Val b)
ttVal ((Val [a] -> Identity (Val [a])) -> TT [a] -> Identity (TT [a]))
-> Val [a] -> TT [a] -> TT [a]
forall s t a b. ASetter s t a b -> b -> s -> t
.~ [a] -> Val [a]
forall a. a -> Val a
Val (a
aa -> [a] -> [a]
forall a. a -> [a] -> [a]
:[a]
zs)

-- | GuardsQuick contain a type level list of conditions and one of matching values: on no match will fail using the first parameter

--

-- >>> pz @(GuardsQuick (PrintT "arg %d failed with value %d" Id) '[Gt 4, Ge 3, Same 4]) [17,3,5]

-- Fail "arg 2 failed with value 5"

--

-- >>> pz @(GuardsQuick (PrintT "arg %d failed with value %d" Id) '[Gt 4, Ge 3, Same 4]) [17,3,5,99]

-- Fail "Guards:invalid length(4) expected 3"

--

-- >>> pl @(GuardsQuick (PrintT "guard(%d) %d is out of range" Id) '[Between 0 11 Id, Between 1 4 Id,Between 3 5 Id]) [10,2,5]

-- Present [10,2,5] (Guards(3))

-- Val [10,2,5]

--

-- >>> pl @(GuardsQuick (PrintT "guard(%d) %d is out of range" Id) '[Between 1 31 Id, Between 1 12 Id, Between 1990 2050 Id]) [31,11,1999]

-- Present [31,11,1999] (Guards(3))

-- Val [31,11,1999]

--

-- >>> pl @(GuardsQuick (PrintT "guard(%d) %d is out of range" Id) '[Between 1 31 Id, Between 1 12 Id, Between 1990 2050 Id]) [31,11]

-- Error Guards:invalid length(2) expected 3

-- Fail "Guards:invalid length(2) expected 3"

--

-- >>> pl @(GuardsQuick (PrintT "guard(%d) %d is out of range" Id) '[Between 1 31 Id, Between 1 12 Id, Between 1990 2050 Id]) [31,13,1999]

-- Error guard(1) 13 is out of range (Guard(1) 13)

-- Fail "guard(1) 13 is out of range"

--

-- >>> pl @(GuardsQuick (PrintT "guard(%d) %d is out of range" Id) '[Between 1 31 Id, Between 1 12 Id, Between 1990 2050 Id]) [0,44,1999]

-- Error guard(0) 0 is out of range (Guard(0) 0)

-- Fail "guard(0) 0 is out of range"

--

-- >>> pl @(GuardsQuick (PrintT "guard(%d) %d is out of range" Id) '[Between 1 31 Id, Between 1 12 Id, Between 1990 2050 Id]) [31,11,2000,1,2]

-- Error Guards:invalid length(5) expected 3

-- Fail "Guards:invalid length(5) expected 3"

--

-- >>> pl @(GuardsQuick (PrintT "guard(%d) err %03d" Id) '[W 'True, Ge 12, W 'False, Lt 2]) [1,2,-99,-999]

-- Error guard(1) err 002 (Guard(1) 2)

-- Fail "guard(1) err 002"

--

-- >>> pl @(GuardsQuick (PrintT "guard(%d) err %03d" Id) '[W 'True, Ge 12, W 'False, Lt 2]) [1,2,-99]

-- Error Guards:invalid length(3) expected 4

-- Fail "Guards:invalid length(3) expected 4"

--

-- >>> pl @(GuardsQuick (PrintT "guard(%d) err %03d" Id) '[W 'True, Ge 12, W 'True, Lt 2]) [1,22,-99,-999,1,1,2]

-- Error Guards:invalid length(7) expected 4

-- Fail "Guards:invalid length(7) expected 4"

--

data GuardsQuick (prt :: k) (ps :: [k1]) deriving Int -> GuardsQuick prt ps -> ShowS
[GuardsQuick prt ps] -> ShowS
GuardsQuick prt ps -> String
(Int -> GuardsQuick prt ps -> ShowS)
-> (GuardsQuick prt ps -> String)
-> ([GuardsQuick prt ps] -> ShowS)
-> Show (GuardsQuick prt ps)
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
forall k (prt :: k) k1 (ps :: [k1]).
Int -> GuardsQuick prt ps -> ShowS
forall k (prt :: k) k1 (ps :: [k1]). [GuardsQuick prt ps] -> ShowS
forall k (prt :: k) k1 (ps :: [k1]). GuardsQuick prt ps -> String
showList :: [GuardsQuick prt ps] -> ShowS
$cshowList :: forall k (prt :: k) k1 (ps :: [k1]). [GuardsQuick prt ps] -> ShowS
show :: GuardsQuick prt ps -> String
$cshow :: forall k (prt :: k) k1 (ps :: [k1]). GuardsQuick prt ps -> String
showsPrec :: Int -> GuardsQuick prt ps -> ShowS
$cshowsPrec :: forall k (prt :: k) k1 (ps :: [k1]).
Int -> GuardsQuick prt ps -> ShowS
Show
type GuardsQuickT (prt :: k) (ps :: [k1]) = Guards (ToGuardsT prt ps)

instance P (GuardsQuickT prt ps) x => P (GuardsQuick prt ps) x where
  type PP (GuardsQuick prt ps) x = PP (GuardsQuickT prt ps) x
  eval :: proxy (GuardsQuick prt ps)
-> POpts -> x -> m (TT (PP (GuardsQuick prt ps) x))
eval proxy (GuardsQuick prt ps)
_ = Proxy (GuardsQuickT prt ps)
-> POpts -> x -> m (TT (PP (GuardsQuickT prt ps) 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 (GuardsQuickT prt ps)
forall k (t :: k). Proxy t
Proxy @(GuardsQuickT prt ps))

-- prefer 'Bools' as 'BoolsQuick' doesnt give much added value: passes in the index and the value to prt but you already have the index in the message

-- pulls the top message from the tree if a predicate is false


-- | boolean guard which checks a given a list of predicates against the list of values

--

-- >>> pl @(Bools '[ '(W "hh",Between 0 23 Id), '(W "mm",Between 0 59 Id), '(PrintT "<<<%d %d>>>" Id,Between 0 59 Id) ]) [12,93,14]

-- Error Bool(1) [mm] (93 <= 59)

-- Fail "Bool(1) [mm] (93 <= 59)"

--

-- >>> pl @(Bools '[ '(W "hh",Between 0 23 Id), '(W "mm",Between 0 59 Id), '(PrintT "<<<%d %d>>>" Id,Between 0 59 Id) ]) [12,13,94]

-- Error Bool(2) [<<<2 94>>>] (94 <= 59)

-- Fail "Bool(2) [<<<2 94>>>] (94 <= 59)"

--

-- >>> pl @(Bools '[ '(W "hh",Between 0 23 Id), '(W "mm",Between 0 59 Id), '(PrintT "<<<%d %d>>>" Id,Between 0 59 Id) ]) [12,13,14]

-- True (Bools)

-- Val True

--

-- >>> pl @(Bools '[ '("hours",Between 0 23 Id), '("minutes",Between 0 59 Id), '("seconds",Between 0 59 Id)]) [12,13,14]

-- True (Bools)

-- Val True

--

-- >>> pl @(Bools '[ '("hours",Between 0 23 Id), '("minutes",Between 0 59 Id), '("seconds",Between 0 59 Id)]) [12,60,14]

-- Error Bool(1) [minutes] (60 <= 59)

-- Fail "Bool(1) [minutes] (60 <= 59)"

--

-- >>> pl @(Bools '[ '("hours",Between 0 23 Id), '("minutes",Between 0 59 Id), '("seconds",Between 0 59 Id)]) [12,60,14,20]

-- Error Bools:invalid length(4) expected 3

-- Fail "Bools:invalid length(4) expected 3"

--

data Bools (ps :: [(k,k1)]) deriving Int -> Bools ps -> ShowS
[Bools ps] -> ShowS
Bools ps -> String
(Int -> Bools ps -> ShowS)
-> (Bools ps -> String) -> ([Bools ps] -> ShowS) -> Show (Bools ps)
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
forall k k1 (ps :: [(k, k1)]). Int -> Bools ps -> ShowS
forall k k1 (ps :: [(k, k1)]). [Bools ps] -> ShowS
forall k k1 (ps :: [(k, k1)]). Bools ps -> String
showList :: [Bools ps] -> ShowS
$cshowList :: forall k k1 (ps :: [(k, k1)]). [Bools ps] -> ShowS
show :: Bools ps -> String
$cshow :: forall k k1 (ps :: [(k, k1)]). Bools ps -> String
showsPrec :: Int -> Bools ps -> ShowS
$cshowsPrec :: forall k k1 (ps :: [(k, k1)]). Int -> Bools ps -> ShowS
Show

instance ( [a] ~ x
         , GetLen ps
         , P (BoolsImpl (LenT ps) ps) x
         , PP (BoolsImpl (LenT ps) ps) x ~ Bool
         ) => P (Bools ps) x where
  type PP (Bools ps) x = Bool
  eval :: proxy (Bools ps) -> POpts -> x -> m (TT (PP (Bools ps) x))
eval proxy (Bools ps)
_ POpts
opts x
as' = do
    let msg0 :: String
msg0 = String
"Bools"
        msg1 :: String
msg1 = String
"Bool(" String -> ShowS
forall a. Semigroup a => a -> a -> a
<> Int -> String
forall a. Show a => a -> String
show (Int
nInt -> Int -> Int
forall a. Num a => a -> a -> a
-Int
1) String -> ShowS
forall a. Semigroup a => a -> a -> a
<> String
")"
        n :: Int
n = GetLen ps => Int
forall k (xs :: k). GetLen xs => Int
getLen @ps
    case POpts -> String -> [a] -> [Tree PE] -> Either (TT Bool) (Int, [a])
forall (t :: Type -> Type) a x.
Foldable t =>
POpts -> String -> t a -> [Tree PE] -> Either (TT x) (Int, [a])
chkSize POpts
opts String
msg1 x
[a]
as' [] of
      Left TT Bool
e -> TT Bool -> m (TT Bool)
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure TT Bool
e
      Right (Int
asLen,[a]
as)
           | Int
n Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
asLen -> Proxy (BoolsImpl (LenT ps) ps)
-> POpts -> [a] -> m (TT (PP (BoolsImpl (LenT ps) ps) [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 (BoolsImpl (LenT ps) ps)
forall k (t :: k). Proxy t
Proxy @(BoolsImpl (LenT ps) ps)) POpts
opts [a]
as
           | Bool
otherwise ->
               let msg2 :: String
msg2 = String
msg0 String -> ShowS
forall a. Semigroup a => a -> a -> a
<> Int -> Int -> String
badLength Int
asLen Int
n
               in 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 -> Val Bool -> String -> [Tree PE] -> TT Bool
forall a. POpts -> Val a -> String -> [Tree PE] -> TT a
mkNode POpts
opts (String -> Val Bool
forall a. String -> Val a
Fail String
msg2) String
"" []

data BoolsImpl (n :: Nat) (os :: [(k,k1)]) deriving Int -> BoolsImpl n os -> ShowS
[BoolsImpl n os] -> ShowS
BoolsImpl n os -> String
(Int -> BoolsImpl n os -> ShowS)
-> (BoolsImpl n os -> String)
-> ([BoolsImpl n os] -> ShowS)
-> Show (BoolsImpl n os)
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
forall (n :: Nat) k k1 (os :: [(k, k1)]).
Int -> BoolsImpl n os -> ShowS
forall (n :: Nat) k k1 (os :: [(k, k1)]). [BoolsImpl n os] -> ShowS
forall (n :: Nat) k k1 (os :: [(k, k1)]). BoolsImpl n os -> String
showList :: [BoolsImpl n os] -> ShowS
$cshowList :: forall (n :: Nat) k k1 (os :: [(k, k1)]). [BoolsImpl n os] -> ShowS
show :: BoolsImpl n os -> String
$cshow :: forall (n :: Nat) k k1 (os :: [(k, k1)]). BoolsImpl n os -> String
showsPrec :: Int -> BoolsImpl n os -> ShowS
$cshowsPrec :: forall (n :: Nat) k k1 (os :: [(k, k1)]).
Int -> BoolsImpl n os -> ShowS
Show

instance ( KnownNat n
         , Show a
         , [a] ~ x
         ) => P (BoolsImpl n ('[] :: [(k,k1)])) x where
  type PP (BoolsImpl n ('[] :: [(k,k1)])) x = Bool

  eval :: proxy (BoolsImpl n '[])
-> POpts -> x -> m (TT (PP (BoolsImpl n '[]) x))
eval proxy (BoolsImpl n '[])
_ POpts
_ as :: x
as@(_:_) = String -> m (TT Bool)
forall x. HasCallStack => String -> x
errorInProgram (String -> m (TT Bool)) -> String -> m (TT Bool)
forall a b. (a -> b) -> a -> b
$ String
"BoolsImpl base case has extra data " String -> ShowS
forall a. [a] -> [a] -> [a]
++ x -> String
forall a. Show a => a -> String
show x
as

  eval proxy (BoolsImpl n '[])
_ POpts
opts [] =
    let msg0 :: String
msg0 = String
"Bool(" String -> ShowS
forall a. Semigroup a => a -> a -> a
<> Int -> String
forall a. Show a => a -> String
show (Int
nInt -> Int -> Int
forall a. Num a => a -> a -> a
-Int
1) String -> ShowS
forall a. Semigroup a => a -> a -> a
<> String
")"
        n :: Int
n = (KnownNat n, Num Int) => Int
forall (n :: Nat) a. (KnownNat n, Num a) => a
nat @n @Int
    in 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 Bool
True (String
msg0 String -> ShowS
forall a. Semigroup a => a -> a -> a
<> String
" empty") []

instance ( PP prt (Int, a) ~ String
         , P prt (Int, a)
         , KnownNat n
         , GetLen ps
         , P p a
         , PP p a ~ Bool
         , P (BoolsImpl n ps) x
         , PP (BoolsImpl n ps) x ~ Bool
         , [a] ~ x
         ) => P (BoolsImpl n ('(prt,p) ': ps)) x where
  type PP (BoolsImpl n ('(prt,p) ': ps)) x = Bool

  eval :: proxy (BoolsImpl n ('(prt, p) : ps))
-> POpts -> x -> m (TT (PP (BoolsImpl n ('(prt, p) : ps)) x))
eval proxy (BoolsImpl n ('(prt, p) : ps))
_ POpts
_ [] = String -> m (TT Bool)
forall x. HasCallStack => String -> x
errorInProgram String
"BoolsImpl n+1 case has no data"

  eval proxy (BoolsImpl n ('(prt, p) : ps))
_ POpts
opts (a:as) = do
     let cpos :: Int
cpos = Int
nInt -> Int -> Int
forall a. Num a => a -> a -> a
-Int
posInt -> Int -> Int
forall a. Num a => a -> a -> a
-Int
1
         msgbase1 :: String
msgbase1 = String
"Bool(" String -> ShowS
forall a. Semigroup a => a -> a -> a
<> Int -> String
forall a. Show a => a -> String
show Int
cpos String -> ShowS
forall a. Semigroup a => a -> a -> a
<> String
")"
         msgbase2 :: String
msgbase2 = String
"Bools"
         n :: Int
n = (KnownNat n, Num Int) => Int
forall (n :: Nat) a. (KnownNat n, Num a) => a
nat @n @Int
         pos :: Int
pos = GetLen ps => Int
forall k (xs :: k). GetLen xs => Int
getLen @ps
     TT Bool
pp <- POpts -> a -> m (TT (PP p a))
forall k (p :: k) a (m :: Type -> Type).
(MonadEval m, P p a, PP p a ~ Bool) =>
POpts -> a -> m (TT (PP p a))
evalBoolHide @p POpts
opts a
a
     case Inline
-> POpts -> String -> TT Bool -> [Tree PE] -> Either (TT Bool) Bool
forall a x.
Inline -> POpts -> String -> TT a -> [Tree PE] -> Either (TT x) a
getValueLR Inline
NoInline POpts
opts (String
msgbase1 String -> ShowS
forall a. Semigroup a => a -> a -> a
<> String
" p failed") TT Bool
pp [] of
       Left TT Bool
e -> TT Bool -> m (TT Bool)
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure TT Bool
e
       Right Bool
False -> do
         TT String
qq <- Proxy prt -> POpts -> (Int, a) -> m (TT (PP prt (Int, 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 prt
forall k (t :: k). Proxy t
Proxy @prt) POpts
opts (Int
cpos,a
a) -- only run prt when predicate is False

         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
$ case Inline
-> POpts
-> String
-> TT String
-> [Tree PE]
-> Either (TT Bool) String
forall a x.
Inline -> POpts -> String -> TT a -> [Tree PE] -> Either (TT x) a
getValueLR Inline
NoInline POpts
opts (String
msgbase2 String -> ShowS
forall a. Semigroup a => a -> a -> a
<> String
" False predicate and prt failed") TT String
qq [TT Bool -> Tree PE
forall a. TT a -> Tree PE
hh TT Bool
pp] of
            Left TT Bool
e -> TT Bool
e
            Right String
msgx ->
              let top :: String
top = TT Bool -> String
forall a. TT a -> String
topMessage TT Bool
pp
              in POpts -> Val Bool -> String -> [Tree PE] -> TT Bool
forall a. POpts -> Val a -> String -> [Tree PE] -> TT a
mkNode POpts
opts (String -> Val Bool
forall a. String -> Val a
Fail (String
msgbase1 String -> ShowS
forall a. Semigroup a => a -> a -> a
<> String
" [" String -> ShowS
forall a. Semigroup a => a -> a -> a
<> String
msgx String -> ShowS
forall a. Semigroup a => a -> a -> a
<> String
"]" String -> ShowS
forall a. Semigroup a => a -> a -> a
<> ShowS
nullSpace String
top)) String
"" (TT Bool -> Tree PE
forall a. TT a -> Tree PE
hh TT Bool
pp Tree PE -> [Tree PE] -> [Tree PE]
forall a. a -> [a] -> [a]
: POpts -> TT String -> [Tree PE]
forall a. POpts -> TT a -> [Tree PE]
verboseList POpts
opts TT String
qq)
       Right Bool
True ->
         if Int
pos Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
0 then -- we are at the bottom of the tree

            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 Bool
True String
msgbase2 [TT Bool -> Tree PE
forall a. TT a -> Tree PE
hh TT Bool
pp]
         else do
           TT Bool
ss <- Proxy (BoolsImpl n ps)
-> POpts -> [a] -> m (TT (PP (BoolsImpl n ps) [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 (BoolsImpl n ps)
forall k (t :: k). Proxy t
Proxy @(BoolsImpl n ps)) POpts
opts [a]
as
           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
$ case Inline
-> POpts -> String -> TT Bool -> [Tree PE] -> Either (TT Bool) Bool
forall a x.
Inline -> POpts -> String -> TT a -> [Tree PE] -> Either (TT x) a
getValueLR Inline
Inline POpts
opts String
"" TT Bool
ss [TT Bool -> Tree PE
forall a. TT a -> Tree PE
hh TT Bool
pp] of
             Left TT Bool
e -> TT Bool
e -- shortcut else we get too compounding errors with the pp tree being added each time!

             Right Bool
_ -> TT Bool
ss TT Bool -> (TT Bool -> TT Bool) -> TT Bool
forall a b. a -> (a -> b) -> b
& ([Tree PE] -> Identity [Tree PE]) -> TT Bool -> Identity (TT Bool)
forall a. Lens' (TT a) [Tree PE]
ttForest (([Tree PE] -> Identity [Tree PE])
 -> TT Bool -> Identity (TT Bool))
-> ([Tree PE] -> [Tree PE]) -> TT Bool -> TT Bool
forall s t a b. ASetter s t a b -> (a -> b) -> s -> t
%~ (TT Bool -> Tree PE
forall a. TT a -> Tree PE
hh TT Bool
ppTree PE -> [Tree PE] -> [Tree PE]
forall a. a -> [a] -> [a]
:)

-- | boolean guard which checks a given a list of predicates against the list of values

--

-- >>> pl @(BoolsQuick "abc" '[Between 0 23 Id, Between 0 59 Id, Between 0 59 Id]) [12,13,14]

-- True (Bools)

-- Val True

--

-- >>> pl @(BoolsQuick (PrintT "id=%d val=%d" Id) '[Between 0 23 Id, Between 0 59 Id, Between 0 59 Id]) [12,13,14]

-- True (Bools)

-- Val True

--

-- >>> pl @(BoolsQuick (PrintT "id=%d val=%d" Id) '[Between 0 23 Id, Between 0 59 Id, Between 0 59 Id]) [12,13,99]

-- Error Bool(2) [id=2 val=99] (99 <= 59)

-- Fail "Bool(2) [id=2 val=99] (99 <= 59)"

--

data BoolsQuick (prt :: k) (ps :: [k1]) deriving Int -> BoolsQuick prt ps -> ShowS
[BoolsQuick prt ps] -> ShowS
BoolsQuick prt ps -> String
(Int -> BoolsQuick prt ps -> ShowS)
-> (BoolsQuick prt ps -> String)
-> ([BoolsQuick prt ps] -> ShowS)
-> Show (BoolsQuick prt ps)
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
forall k (prt :: k) k1 (ps :: [k1]).
Int -> BoolsQuick prt ps -> ShowS
forall k (prt :: k) k1 (ps :: [k1]). [BoolsQuick prt ps] -> ShowS
forall k (prt :: k) k1 (ps :: [k1]). BoolsQuick prt ps -> String
showList :: [BoolsQuick prt ps] -> ShowS
$cshowList :: forall k (prt :: k) k1 (ps :: [k1]). [BoolsQuick prt ps] -> ShowS
show :: BoolsQuick prt ps -> String
$cshow :: forall k (prt :: k) k1 (ps :: [k1]). BoolsQuick prt ps -> String
showsPrec :: Int -> BoolsQuick prt ps -> ShowS
$cshowsPrec :: forall k (prt :: k) k1 (ps :: [k1]).
Int -> BoolsQuick prt ps -> ShowS
Show
type BoolsQuickT (prt :: k) (ps :: [k1]) = Bools (ToGuardsT prt ps)

-- why do we need this? when BoolsN works without [use the x ~ [a] trick in BoolsN]

instance ( PP (Bools (ToGuardsT prt ps)) x ~ Bool
         , P (BoolsQuickT prt ps) x
         ) => P (BoolsQuick prt ps) x where
  type PP (BoolsQuick prt ps) x = Bool
  eval :: proxy (BoolsQuick prt ps)
-> POpts -> x -> m (TT (PP (BoolsQuick prt ps) x))
eval proxy (BoolsQuick prt ps)
_ = Proxy (Bools (ToGuardsT prt ps))
-> POpts -> x -> m (TT (PP (Bools (ToGuardsT prt ps)) x))
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 (Bools (ToGuardsT prt ps))
forall k (t :: k). Proxy t
Proxy @(BoolsQuickT prt ps))

-- | leverages 'RepeatT' for repeating predicates (passthrough method)

--

-- >>> pl @(BoolsN (PrintT "id=%d must be between 0 and 255, found %d" Id) 4 (0 <..> 0xff)) [121,33,7,256]

-- Error Bool(3) [id=3 must be between 0 and 255, found 256] (256 <= 255)

-- Fail "Bool(3) [id=3 must be between 0 and 255, found 256] (256 <= 255)"

--

-- >>> pl @(BoolsN (PrintT "id=%d must be between 0 and 255, found %d" Id) 4 (0 <..> 0xff)) [121,33,7,44]

-- True (Bools)

-- Val True

--

data BoolsN prt (n :: Nat) (p :: k1) deriving Int -> BoolsN prt n p -> ShowS
[BoolsN prt n p] -> ShowS
BoolsN prt n p -> String
(Int -> BoolsN prt n p -> ShowS)
-> (BoolsN prt n p -> String)
-> ([BoolsN prt n p] -> ShowS)
-> Show (BoolsN prt n p)
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
forall k (prt :: k) (n :: Nat) k1 (p :: k1).
Int -> BoolsN prt n p -> ShowS
forall k (prt :: k) (n :: Nat) k1 (p :: k1).
[BoolsN prt n p] -> ShowS
forall k (prt :: k) (n :: Nat) k1 (p :: k1).
BoolsN prt n p -> String
showList :: [BoolsN prt n p] -> ShowS
$cshowList :: forall k (prt :: k) (n :: Nat) k1 (p :: k1).
[BoolsN prt n p] -> ShowS
show :: BoolsN prt n p -> String
$cshow :: forall k (prt :: k) (n :: Nat) k1 (p :: k1).
BoolsN prt n p -> String
showsPrec :: Int -> BoolsN prt n p -> ShowS
$cshowsPrec :: forall k (prt :: k) (n :: Nat) k1 (p :: k1).
Int -> BoolsN prt n p -> ShowS
Show
type BoolsNT prt (n :: Nat) (p :: k1) = Bools (ToGuardsT prt (RepeatT n p))

instance ( x ~ [a]
         , P (BoolsNT prt n p) x
         ) => P (BoolsN prt n p) x where
  type PP (BoolsN prt n p) x = Bool
  eval :: proxy (BoolsN prt n p)
-> POpts -> x -> m (TT (PP (BoolsN prt n p) x))
eval proxy (BoolsN prt n p)
_ = Proxy (BoolsNT prt n p)
-> POpts -> x -> m (TT (PP (BoolsNT prt n p) x))
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 (BoolsNT prt n p)
forall k (t :: k). Proxy t
Proxy @(BoolsNT prt n p))

data GuardsDetailImpl (ps :: [(k,k1)]) deriving Int -> GuardsDetailImpl ps -> ShowS
[GuardsDetailImpl ps] -> ShowS
GuardsDetailImpl ps -> String
(Int -> GuardsDetailImpl ps -> ShowS)
-> (GuardsDetailImpl ps -> String)
-> ([GuardsDetailImpl ps] -> ShowS)
-> Show (GuardsDetailImpl ps)
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
forall k k1 (ps :: [(k, k1)]). Int -> GuardsDetailImpl ps -> ShowS
forall k k1 (ps :: [(k, k1)]). [GuardsDetailImpl ps] -> ShowS
forall k k1 (ps :: [(k, k1)]). GuardsDetailImpl ps -> String
showList :: [GuardsDetailImpl ps] -> ShowS
$cshowList :: forall k k1 (ps :: [(k, k1)]). [GuardsDetailImpl ps] -> ShowS
show :: GuardsDetailImpl ps -> String
$cshow :: forall k k1 (ps :: [(k, k1)]). GuardsDetailImpl ps -> String
showsPrec :: Int -> GuardsDetailImpl ps -> ShowS
$cshowsPrec :: forall k k1 (ps :: [(k, k1)]). Int -> GuardsDetailImpl ps -> ShowS
Show

instance ( [a] ~ x
         , GetLen ps
         , P (GuardsImpl (LenT ps) ps) x
         ) => P (GuardsDetailImpl ps) x where
  type PP (GuardsDetailImpl ps) x = PP (GuardsImpl (LenT ps) ps) x
  eval :: proxy (GuardsDetailImpl ps)
-> POpts -> x -> m (TT (PP (GuardsDetailImpl ps) x))
eval proxy (GuardsDetailImpl ps)
_ POpts
opts x
as' = do
    let msg0 :: String
msg0 = String
"Guards"
        n :: Int
n = GetLen ps => Int
forall k (xs :: k). GetLen xs => Int
getLen @ps
    case POpts
-> String
-> [a]
-> [Tree PE]
-> Either (TT (PP (GuardsImpl (LenT ps) ps) [a])) (Int, [a])
forall (t :: Type -> Type) a x.
Foldable t =>
POpts -> String -> t a -> [Tree PE] -> Either (TT x) (Int, [a])
chkSize POpts
opts String
msg0 x
[a]
as' [] of
      Left TT (PP (GuardsImpl (LenT ps) ps) [a])
e -> TT (PP (GuardsImpl (LenT ps) ps) [a])
-> m (TT (PP (GuardsImpl (LenT ps) ps) [a]))
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure TT (PP (GuardsImpl (LenT ps) ps) [a])
e
      Right (Int
asLen,[a]
as)
           | Int
n Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
asLen -> Proxy (GuardsImpl (LenT ps) ps)
-> POpts -> [a] -> m (TT (PP (GuardsImpl (LenT ps) ps) [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 (GuardsImpl (LenT ps) ps)
forall k (t :: k). Proxy t
Proxy @(GuardsImpl (LenT ps) ps)) POpts
opts [a]
as
           | Bool
otherwise ->
               let msg1 :: String
msg1 = String
msg0 String -> ShowS
forall a. Semigroup a => a -> a -> a
<> Int -> Int -> String
badLength Int
asLen Int
n
               in TT (PP (GuardsImpl (LenT ps) ps) [a])
-> m (TT (PP (GuardsImpl (LenT ps) ps) [a]))
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (TT (PP (GuardsImpl (LenT ps) ps) [a])
 -> m (TT (PP (GuardsImpl (LenT ps) ps) [a])))
-> TT (PP (GuardsImpl (LenT ps) ps) [a])
-> m (TT (PP (GuardsImpl (LenT ps) ps) [a]))
forall a b. (a -> b) -> a -> b
$ POpts
-> Val (PP (GuardsImpl (LenT ps) ps) [a])
-> String
-> [Tree PE]
-> TT (PP (GuardsImpl (LenT ps) ps) [a])
forall a. POpts -> Val a -> String -> [Tree PE] -> TT a
mkNode POpts
opts (String -> Val (PP (GuardsImpl (LenT ps) ps) [a])
forall a. String -> Val a
Fail String
msg1) String
"" []

-- | if a predicate fails then then the corresponding symbol and value will be passed to the print function

--

-- >>> pz @(GuardsDetail "%s invalid: found %d" '[ '("hours", Between 0 23 Id),'("minutes",Between 0 59 Id),'("seconds",Between 0 59 Id)]) [13,59,61]

-- Fail "seconds invalid: found 61"

--

-- >>> pz @(GuardsDetail "%s invalid: found %d" '[ '("hours", Between 0 23 Id),'("minutes",Between 0 59 Id),'("seconds",Between 0 59 Id)]) [27,59,12]

-- Fail "hours invalid: found 27"

--

-- >>> pz @(GuardsDetail "%s invalid: found %d" '[ '("hours", Between 0 23 Id),'("minutes",Between 0 59 Id),'("seconds",Between 0 59 Id)]) [23,59,12]

-- Val [23,59,12]

--

data GuardsDetail prt (ps :: [(k0,k1)]) deriving Int -> GuardsDetail prt ps -> ShowS
[GuardsDetail prt ps] -> ShowS
GuardsDetail prt ps -> String
(Int -> GuardsDetail prt ps -> ShowS)
-> (GuardsDetail prt ps -> String)
-> ([GuardsDetail prt ps] -> ShowS)
-> Show (GuardsDetail prt ps)
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
forall k (prt :: k) k0 k1 (ps :: [(k0, k1)]).
Int -> GuardsDetail prt ps -> ShowS
forall k (prt :: k) k0 k1 (ps :: [(k0, k1)]).
[GuardsDetail prt ps] -> ShowS
forall k (prt :: k) k0 k1 (ps :: [(k0, k1)]).
GuardsDetail prt ps -> String
showList :: [GuardsDetail prt ps] -> ShowS
$cshowList :: forall k (prt :: k) k0 k1 (ps :: [(k0, k1)]).
[GuardsDetail prt ps] -> ShowS
show :: GuardsDetail prt ps -> String
$cshow :: forall k (prt :: k) k0 k1 (ps :: [(k0, k1)]).
GuardsDetail prt ps -> String
showsPrec :: Int -> GuardsDetail prt ps -> ShowS
$cshowsPrec :: forall k (prt :: k) k0 k1 (ps :: [(k0, k1)]).
Int -> GuardsDetail prt ps -> ShowS
Show
type GuardsDetailT prt (ps :: [(k0,k1)]) = GuardsDetailImpl (ToGuardsDetailT prt ps)

instance P (GuardsDetailT prt ps) x => P (GuardsDetail prt ps) x where
  type PP (GuardsDetail prt ps) x = PP (GuardsDetailT prt ps) x
  eval :: proxy (GuardsDetail prt ps)
-> POpts -> x -> m (TT (PP (GuardsDetail prt ps) x))
eval proxy (GuardsDetail prt ps)
_ = Proxy (GuardsDetailT prt ps)
-> POpts -> x -> m (TT (PP (GuardsDetailT prt ps) 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 (GuardsDetailT prt ps)
forall k (t :: k). Proxy t
Proxy @(GuardsDetailT prt ps))

-- | expands out the condition parameter used by 'GuardsDetail'

type family ToGuardsDetailT (prt :: k1) (os :: [(k2,k3)]) :: [(Type,k3)] where
  ToGuardsDetailT prt '[ '(s,p) ] = '(PrintT prt '(s,Snd), p) : '[]
  ToGuardsDetailT prt ( '(s,p) ': ps) = '(PrintT prt '(s,Snd), p) ': ToGuardsDetailT prt ps
  ToGuardsDetailT _prt '[] = GL.TypeError ('GL.Text "ToGuardsDetailT cannot be empty")

-- | leverages 'RepeatT' for repeating predicates (passthrough method)

--

-- >>> pz @(GuardsN 4 (PrintT "id=%d must be between 0 and 255, found %d" Id) (0 <..> 0xff)) [121,33,7,256]

-- Fail "id=3 must be between 0 and 255, found 256"

--

-- >>> pz @(GuardsN 4 (PrintT "id=%d must be between 0 and 255, found %d" Id) (0 <..> 0xff)) [121,33,7,44]

-- Val [121,33,7,44]

--

-- >>> pl @(GuardsN 4 (PrintT "guard(%d) %d is out of range" Id) (0 <..> 0xff)) [1,2,3,4]

-- Present [1,2,3,4] (Guards(4))

-- Val [1,2,3,4]

--

-- >>> pl @(GuardsN 4 (PrintT "guard(%d) %d is out of range" Id) (0 <..> 0xff)) [1,2,3,4,5]

-- Error Guards:invalid length(5) expected 4

-- Fail "Guards:invalid length(5) expected 4"

--

-- >>> pl @(GuardsN 4 (PrintT "guard(%d) %d is out of range" Id) (0 <..> 0xff)) [1,2,3]

-- Error Guards:invalid length(3) expected 4

-- Fail "Guards:invalid length(3) expected 4"

--

-- >>> pl @(Resplit "\\." >> Map (ReadP Int Id) >> GuardsN 4 (PrintT "invalid pos=%d val=%d" Id) (0 <..> 0xff)) "13.22.44.1231"

-- Error invalid pos=3 val=1231 (Guard(3) 1231 | [13,22,44,1231])

-- Fail "invalid pos=3 val=1231"

--

data GuardsN (n :: Nat) prt p deriving Int -> GuardsN n prt p -> ShowS
[GuardsN n prt p] -> ShowS
GuardsN n prt p -> String
(Int -> GuardsN n prt p -> ShowS)
-> (GuardsN n prt p -> String)
-> ([GuardsN n prt p] -> ShowS)
-> Show (GuardsN n prt p)
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
forall (n :: Nat) k (prt :: k) k (p :: k).
Int -> GuardsN n prt p -> ShowS
forall (n :: Nat) k (prt :: k) k (p :: k).
[GuardsN n prt p] -> ShowS
forall (n :: Nat) k (prt :: k) k (p :: k).
GuardsN n prt p -> String
showList :: [GuardsN n prt p] -> ShowS
$cshowList :: forall (n :: Nat) k (prt :: k) k (p :: k).
[GuardsN n prt p] -> ShowS
show :: GuardsN n prt p -> String
$cshow :: forall (n :: Nat) k (prt :: k) k (p :: k).
GuardsN n prt p -> String
showsPrec :: Int -> GuardsN n prt p -> ShowS
$cshowsPrec :: forall (n :: Nat) k (prt :: k) k (p :: k).
Int -> GuardsN n prt p -> ShowS
Show
type GuardsNT (n :: Nat) prt p = Guards (ToGuardsT prt (RepeatT n p))

instance ( x ~ [a]
         , P (GuardsNT prt n p) x
         ) => P (GuardsN prt n p) x where
  type PP (GuardsN prt n p) x = PP (GuardsNT prt n p) x
  eval :: proxy (GuardsN prt n p)
-> POpts -> x -> m (TT (PP (GuardsN prt n p) x))
eval proxy (GuardsN prt n p)
_ = Proxy (GuardsNT prt n p)
-> POpts -> x -> m (TT (PP (GuardsNT prt 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 (GuardsNT prt n p)
forall k (t :: k). Proxy t
Proxy @(GuardsNT prt n p))

-- | @p@ is the predicate and on failure of the predicate runs @prt@

--

-- >>> pz @(Guard "expected > 3" (Gt 3)) 17

-- Val 17

--

-- >>> pz @(Guard "expected > 3" (Gt 3)) 1

-- Fail "expected > 3"

--

-- >>> pz @(Guard (PrintF "%d not > 3" Id) (Gt 3)) (-99)

-- Fail "-99 not > 3"

--

-- >>> pl @(Map (Guard "someval" (Lt 3) >> 'True)) [1 ..10]

-- Error someval(8) (Map(i=2, a=3) excnt=8)

-- Fail "someval(8)"

--

-- >>> pl @(Guard "someval" (Len == 2) >> (ShowP Id &&& Id)) ([] :: [Int])

-- Error someval (Guard | [])

-- Fail "someval"

--

-- >>> pl @(Guard "someval" (Len == 2) >> (Id &&& ShowP Id)) [2,3]

-- Present ([2,3],"[2,3]") ((>>) ([2,3],"[2,3]") | {'([2,3],"[2,3]")})

-- Val ([2,3],"[2,3]")

--

-- >>> pl @(Guard "someval" (Len == 2) >> (ShowP Id &&& Id)) [2,3,4]

-- Error someval (Guard | [2,3,4])

-- Fail "someval"

--

-- >>> pl @(Map (Guard "someval" (Lt 3) >> 'True)) [1 ..10]

-- Error someval(8) (Map(i=2, a=3) excnt=8)

-- Fail "someval(8)"

--

-- >>> pl @(Guard "oops" (Len > 2) >> Map Succ) [12,15,16]

-- Present [13,16,17] ((>>) [13,16,17] | {Map [13,16,17] | [12,15,16]})

-- Val [13,16,17]

--

-- >>> pl @(Guard "err" (Len > 2) >> Map Succ) [12]

-- Error err (Guard | [12])

-- Fail "err"

--

-- >>> pl @(Guard (PrintF "err found len=%d" Len) (Len > 5) >> Map Succ) [12,15,16]

-- Error err found len=3 (Guard | [12,15,16])

-- Fail "err found len=3"

--

data Guard prt p deriving Int -> Guard prt p -> ShowS
[Guard prt p] -> ShowS
Guard prt p -> String
(Int -> Guard prt p -> ShowS)
-> (Guard prt p -> String)
-> ([Guard prt p] -> ShowS)
-> Show (Guard prt p)
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
forall k (prt :: k) k (p :: k). Int -> Guard prt p -> ShowS
forall k (prt :: k) k (p :: k). [Guard prt p] -> ShowS
forall k (prt :: k) k (p :: k). Guard prt p -> String
showList :: [Guard prt p] -> ShowS
$cshowList :: forall k (prt :: k) k (p :: k). [Guard prt p] -> ShowS
show :: Guard prt p -> String
$cshow :: forall k (prt :: k) k (p :: k). Guard prt p -> String
showsPrec :: Int -> Guard prt p -> ShowS
$cshowsPrec :: forall k (prt :: k) k (p :: k). Int -> Guard prt p -> ShowS
Show


instance ( Show a
         , P prt a
         , PP prt a ~ String
         , P p a
         , PP p a ~ Bool
         ) => P (Guard prt p) a where
  type PP (Guard prt p) a = a
  eval :: proxy (Guard prt p) -> POpts -> a -> m (TT (PP (Guard prt p) a))
eval proxy (Guard prt p)
_ POpts
opts a
a = do
    let msg0 :: String
msg0 = String
"Guard"
    TT Bool
pp <- Proxy p -> POpts -> a -> m (TT (PP p 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 p
forall k (t :: k). Proxy t
Proxy @p) POpts
opts a
a
    case Inline
-> POpts -> String -> TT Bool -> [Tree PE] -> Either (TT a) Bool
forall a x.
Inline -> POpts -> String -> TT a -> [Tree PE] -> Either (TT x) a
getValueLR Inline
NoInline POpts
opts String
msg0 TT Bool
pp [] 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 Bool
False -> do
        TT String
qq <- Proxy prt -> POpts -> a -> m (TT (PP prt 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 prt
forall k (t :: k). Proxy t
Proxy @prt) POpts
opts a
a
        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 String -> ShowS
forall a. Semigroup a => a -> a -> a
<> String
" Msg") TT String
qq [TT Bool -> Tree PE
forall a. TT a -> Tree PE
hh TT Bool
pp] of
          Left TT a
e -> TT a
e
          Right String
ee -> 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
ee) (String -> ShowS
joinStrings String
msg0 (POpts -> a -> String
forall a. Show a => POpts -> a -> String
showL POpts
opts a
a)) (TT Bool -> Tree PE
forall a. TT a -> Tree PE
hh TT Bool
pp Tree PE -> [Tree PE] -> [Tree PE]
forall a. a -> [a] -> [a]
: POpts -> TT String -> [Tree PE]
forall a. POpts -> TT a -> [Tree PE]
verboseList POpts
opts TT String
qq)
      Right Bool
True -> 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
a) (String -> ShowS
joinStrings (String
msg0 String -> ShowS
forall a. Semigroup a => a -> a -> a
<> String
"(ok)") (POpts -> a -> String
forall a. Show a => POpts -> a -> String
showL POpts
opts a
a)) [TT Bool -> Tree PE
forall a. TT a -> Tree PE
hh TT Bool
pp]  -- dont show the guard message if successful


-- | boolean guard

--

-- >>> pl @(GuardBool (PrintF "bad length = %d" Len) (Len > 9)) [3..8]

-- Error bad length = 6 (GuardBool (6 > 9))

-- Fail "bad length = 6"

--

data GuardBool prt p deriving Int -> GuardBool prt p -> ShowS
[GuardBool prt p] -> ShowS
GuardBool prt p -> String
(Int -> GuardBool prt p -> ShowS)
-> (GuardBool prt p -> String)
-> ([GuardBool prt p] -> ShowS)
-> Show (GuardBool prt p)
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
forall k (prt :: k) k (p :: k). Int -> GuardBool prt p -> ShowS
forall k (prt :: k) k (p :: k). [GuardBool prt p] -> ShowS
forall k (prt :: k) k (p :: k). GuardBool prt p -> String
showList :: [GuardBool prt p] -> ShowS
$cshowList :: forall k (prt :: k) k (p :: k). [GuardBool prt p] -> ShowS
show :: GuardBool prt p -> String
$cshow :: forall k (prt :: k) k (p :: k). GuardBool prt p -> String
showsPrec :: Int -> GuardBool prt p -> ShowS
$cshowsPrec :: forall k (prt :: k) k (p :: k). Int -> GuardBool prt p -> ShowS
Show

instance ( P prt a
         , PP prt a ~ String
         , P p a
         , PP p a ~ Bool
         ) => P (GuardBool prt p) a where
  type PP (GuardBool prt p) a = Bool
  eval :: proxy (GuardBool prt p)
-> POpts -> a -> m (TT (PP (GuardBool prt p) a))
eval proxy (GuardBool prt p)
_ POpts
opts a
a = do
    let msg0 :: String
msg0 = String
"GuardBool"
    TT Bool
pp <- Proxy p -> POpts -> a -> m (TT (PP p 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 p
forall k (t :: k). Proxy t
Proxy @p) POpts
opts a
a
    case Inline
-> POpts -> String -> TT Bool -> [Tree PE] -> Either (TT Bool) Bool
forall a x.
Inline -> POpts -> String -> TT a -> [Tree PE] -> Either (TT x) a
getValueLR Inline
NoInline POpts
opts String
msg0 TT Bool
pp [] of
      Left TT Bool
e -> TT Bool -> m (TT Bool)
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure TT Bool
e
      Right Bool
False -> do
        TT String
qq <- Proxy prt -> POpts -> a -> m (TT (PP prt 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 prt
forall k (t :: k). Proxy t
Proxy @prt) POpts
opts a
a
        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
$ case Inline
-> POpts
-> String
-> TT String
-> [Tree PE]
-> Either (TT Bool) String
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
" Msg") TT String
qq [TT Bool -> Tree PE
forall a. TT a -> Tree PE
hh TT Bool
pp] of
          Left TT Bool
e -> TT Bool
e
          Right String
ee ->
            let top :: String
top = TT Bool -> String
forall a. TT a -> String
topMessage TT Bool
pp
            in POpts -> Val Bool -> String -> [Tree PE] -> TT Bool
forall a. POpts -> Val a -> String -> [Tree PE] -> TT a
mkNode POpts
opts (String -> Val Bool
forall a. String -> Val a
Fail String
ee) (String
msg0 String -> ShowS
forall a. Semigroup a => a -> a -> a
<> ShowS
nullSpace String
top) [TT Bool -> Tree PE
forall a. TT a -> Tree PE
hh TT Bool
pp, TT String -> Tree PE
forall a. TT a -> Tree PE
hh TT String
qq]
      Right Bool
True -> 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 Bool
True String
"" [TT Bool -> Tree PE
forall a. TT a -> Tree PE
hh TT Bool
pp]  -- dont show the guard message if successful


-- | uses 'Guard' but negates @p@

--

-- >>> pl @(HeadFail "failedn" Id &&& (Len == 1 >> ExitWhen "ExitWhen" Id) >> Fst) [3]

-- Error ExitWhen (Guard | True | True | '(,))

-- Fail "ExitWhen"

--

-- >>> pl @(Head &&& (Len == 1 >> Not Id >> ExitWhen "ExitWhen" Id) >> Fst) [3]

-- Present 3 ((>>) 3 | {Fst 3 | (3,False)})

-- Val 3

--

-- >>> pl @(Head &&& (Len == 1 >> ExitWhen "ExitWhen" (Not Id)) >> Fst) [3]

-- Present 3 ((>>) 3 | {Fst 3 | (3,True)})

-- Val 3

--

-- >>> pl @(ExitWhen "ExitWhen" (Len /= 1) >> Head) [3,1]

-- Error ExitWhen (Guard | [3,1])

-- Fail "ExitWhen"

--

-- >>> pl @(ExitWhen "ExitWhen" (Len /= 1) >> Head) [3]

-- Present 3 ((>>) 3 | {Head 3 | [3]})

-- Val 3

--

-- >>> pl @(ExitWhen "ExitWhen" (Len /= 1) >> Head >> Gt (20 -% 1)) [3]

-- True ((>>) True | {3 % 1 > (-20) % 1})

-- Val True

--

-- >>> pl @(ExitWhen "ExitWhen" (Len /= 1) >> Head >> Gt (20 -% 1)) [-23]

-- False ((>>) False | {(-23) % 1 > (-20) % 1})

-- Val False

--

-- >>> pl @(Map (ExitWhen "ExitWhen" (Gt 10) >> Gt 2)) [1..5]

-- Present [False,False,True,True,True] (Map [False,False,True,True,True] | [1,2,3,4,5])

-- Val [False,False,True,True,True]

--

-- >>> pl @(ExitWhen "err" (Len > 2) >> Map Succ) [12,15,16]

-- Error err (Guard | [12,15,16])

-- Fail "err"

--

-- >>> pl @(ExitWhen "err" (Len > 2) >> Map Succ) [12]

-- Present [13] ((>>) [13] | {Map [13] | [12]})

-- Val [13]

--

data ExitWhen prt p deriving Int -> ExitWhen prt p -> ShowS
[ExitWhen prt p] -> ShowS
ExitWhen prt p -> String
(Int -> ExitWhen prt p -> ShowS)
-> (ExitWhen prt p -> String)
-> ([ExitWhen prt p] -> ShowS)
-> Show (ExitWhen prt p)
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
forall k (prt :: k) k (p :: k). Int -> ExitWhen prt p -> ShowS
forall k (prt :: k) k (p :: k). [ExitWhen prt p] -> ShowS
forall k (prt :: k) k (p :: k). ExitWhen prt p -> String
showList :: [ExitWhen prt p] -> ShowS
$cshowList :: forall k (prt :: k) k (p :: k). [ExitWhen prt p] -> ShowS
show :: ExitWhen prt p -> String
$cshow :: forall k (prt :: k) k (p :: k). ExitWhen prt p -> String
showsPrec :: Int -> ExitWhen prt p -> ShowS
$cshowsPrec :: forall k (prt :: k) k (p :: k). Int -> ExitWhen prt p -> ShowS
Show
type ExitWhenT prt p = Guard prt (Not p)

instance P (ExitWhenT prt p) x => P (ExitWhen prt p) x where
  type PP (ExitWhen prt p) x = PP (ExitWhenT prt p) x
  eval :: proxy (ExitWhen prt p)
-> POpts -> x -> m (TT (PP (ExitWhen prt p) x))
eval proxy (ExitWhen prt p)
_ = Proxy (ExitWhenT prt p)
-> POpts -> x -> m (TT (PP (ExitWhenT prt 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 (ExitWhenT prt p)
forall k (t :: k). Proxy t
Proxy @(ExitWhenT prt p))

-- | similar to 'Guard' but uses the root message of the False predicate case as the failure message

--

-- >>> pz @(GuardSimple IsLuhn) [1..4]

-- Fail "(IsLuhn map=[2,2,6,4] sum=14 ret=4 | [1,2,3,4])"

--

-- >>> pz @(GuardSimple IsLuhn) [1,2,3,0]

-- Val [1,2,3,0]

--

-- >>> pz @(GuardSimple (Len > 30)) [1,2,3,0]

-- Fail "(4 > 30)"

--

-- >>> pl @(Map (GuardSimple (Lt 3) >> 'True)) [1 .. 10]

-- Error (3 < 3) | (4 < 3) | (5 < 3) | (6 < 3) | (7 < 3) | (8 < 3) | (9 < 3) | (10 < 3) (Map(i=2, a=3) excnt=8)

-- Fail "(3 < 3) | (4 < 3) | (5 < 3) | (6 < 3) | (7 < 3) | (8 < 3) | (9 < 3) | (10 < 3)"

--

-- >>> pl @(Map (GuardSimple (Ge 1) >> 'True)) [1 .. 10]

-- Present [True,True,True,True,True,True,True,True,True,True] (Map [True,True,True,True,True,True,True,True,True,True] | [1,2,3,4,5,6,7,8,9,10])

-- Val [True,True,True,True,True,True,True,True,True,True]

--

-- >>> pl @(Map (GuardSimple (Lt 3) >> 'True)) [1 .. 10]

-- Error (3 < 3) | (4 < 3) | (5 < 3) | (6 < 3) | (7 < 3) | (8 < 3) | (9 < 3) | (10 < 3) (Map(i=2, a=3) excnt=8)

-- Fail "(3 < 3) | (4 < 3) | (5 < 3) | (6 < 3) | (7 < 3) | (8 < 3) | (9 < 3) | (10 < 3)"

--

data GuardSimple p deriving Int -> GuardSimple p -> ShowS
[GuardSimple p] -> ShowS
GuardSimple p -> String
(Int -> GuardSimple p -> ShowS)
-> (GuardSimple p -> String)
-> ([GuardSimple p] -> ShowS)
-> Show (GuardSimple p)
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
forall k (p :: k). Int -> GuardSimple p -> ShowS
forall k (p :: k). [GuardSimple p] -> ShowS
forall k (p :: k). GuardSimple p -> String
showList :: [GuardSimple p] -> ShowS
$cshowList :: forall k (p :: k). [GuardSimple p] -> ShowS
show :: GuardSimple p -> String
$cshow :: forall k (p :: k). GuardSimple p -> String
showsPrec :: Int -> GuardSimple p -> ShowS
$cshowsPrec :: forall k (p :: k). Int -> GuardSimple p -> ShowS
Show

instance ( Show a
         , P p a
         , PP p a ~ Bool
         ) => P (GuardSimple p) a where
  type PP (GuardSimple p) a = a
  eval :: proxy (GuardSimple p)
-> POpts -> a -> m (TT (PP (GuardSimple p) a))
eval proxy (GuardSimple p)
_ POpts
opts a
a = do
    let msg0 :: String
msg0 = String
"GuardSimple"
    TT Bool
pp <- Proxy p -> POpts -> a -> m (TT (PP p 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 p
forall k (t :: k). Proxy t
Proxy @p) (POpts -> POpts
zeroToLite POpts
opts) a
a -- temporarily lift DZero to DLite so as not to lose the failure message

    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 Bool -> [Tree PE] -> Either (TT a) Bool
forall a x.
Inline -> POpts -> String -> TT a -> [Tree PE] -> Either (TT x) a
getValueLR Inline
NoInline POpts
opts String
msg0 TT Bool
pp [] of
      Left TT a
e -> TT a
e
      Right Bool
False ->
        let top :: String
top = TT Bool -> String
forall a. TT a -> String
topMessage TT Bool
pp -- need DLite at least to get a reasonable message for the Fail case

        in 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
top) (String -> ShowS
joinStrings String
msg0 (POpts -> a -> String
forall a. Show a => POpts -> a -> String
showL POpts
opts a
a)) [TT Bool -> Tree PE
forall a. TT a -> Tree PE
hh TT Bool
pp]
      Right Bool
True ->
        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 -> ShowS
joinStrings (String
msg0 String -> ShowS
forall a. Semigroup a => a -> a -> a
<> String
"(ok)") (POpts -> a -> String
forall a. Show a => POpts -> a -> String
showL POpts
opts a
a)) [TT Bool -> Tree PE
forall a. TT a -> Tree PE
hh TT Bool
pp]