{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE NoStarIsType #-}
{-# LANGUAGE EmptyDataDeriving #-}
module Predicate.Data.Condition (
If
, Case
, Case'
, Case''
, Guards
, GuardsQuick
, Guard
, ExitWhen
, GuardSimple
, GuardsN
, GuardsDetail
, GuardBool
, Bools
, BoolsQuick
, BoolsN
) 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
import Data.Bool (bool)
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
<> String -> String -> Bool -> String
forall a. a -> a -> Bool -> a
bool String
"'False" String
"'True" 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, TT (PP r a) -> Tree PE
forall a. TT a -> Tree PE
hh TT (PP r a)
qqrr]
type family GuardsT (ps :: [k]) where
GuardsT '[] = '[]
GuardsT (p ': ps) = Guard "fromGuardsT" p ': GuardsT ps
type family ToGuardsT (prt :: k) (os :: [k1]) :: [(k,k1)] where
ToGuardsT _prt '[] = GL.TypeError ('GL.Text "ToGuardsT cannot be empty")
ToGuardsT prt '[p] = '(prt,p) : '[]
ToGuardsT prt (p ': ps) = '(prt,p) ': ToGuardsT prt ps
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
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
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
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
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
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))
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)
b -> POpts
-> Val (PP q (PP r x)) -> String -> [Tree PE] -> TT (PP q (PP r x))
forall a. POpts -> Val a -> String -> [Tree PE] -> TT a
mkNode POpts
opts (PP q (PP r x) -> Val (PP q (PP r x))
forall a. a -> Val a
Val PP q (PP r x)
b) (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)
b PP r x
a) (TT (PP r x) -> Tree PE
forall a. TT a -> Tree PE
hh TT (PP r x)
rr Tree PE -> [Tree PE] -> [Tree PE]
forall a. a -> [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 (PP q (PP r x)) -> [Tree PE]
forall a. POpts -> TT a -> [Tree PE]
verboseList POpts
opts TT (PP q (PP r x))
qq)
Right Bool
False -> do
TT (PP q (PP r x))
ee <- 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))
ee 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))
ee [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)
b -> POpts
-> Val (PP q (PP r x)) -> String -> [Tree PE] -> TT (PP q (PP r x))
forall a. POpts -> Val a -> String -> [Tree PE] -> TT a
mkNode POpts
opts (PP q (PP r x) -> Val (PP q (PP r x))
forall a. a -> Val a
Val PP q (PP r x)
b) (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)
b 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, TT (PP q (PP r x)) -> Tree PE
forall a. TT a -> Tree PE
hh TT (PP q (PP r x))
ee]
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)
b -> POpts
-> Val (PP q (PP r x)) -> String -> [Tree PE] -> TT (PP q (PP r x))
forall a. POpts -> Val a -> String -> [Tree PE] -> TT a
mkNode POpts
opts (PP q (PP r x) -> Val (PP q (PP r x))
forall a. a -> Val a
Val PP q (PP r x)
b) (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)
b PP r x
a) (TT (PP r x) -> Tree PE
forall a. TT a -> Tree PE
hh TT (PP r x)
rr Tree PE -> [Tree PE] -> [Tree PE]
forall a. a -> [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 (PP q (PP r x)) -> [Tree PE]
forall a. POpts -> TT a -> [Tree PE]
verboseList POpts
opts TT (PP q (PP r x))
qq)
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)
b -> POpts
-> Val (PP q (PP r x)) -> String -> [Tree PE] -> TT (PP q (PP r x))
forall a. POpts -> Val a -> String -> [Tree PE] -> TT a
mkNode POpts
opts (PP q (PP r x) -> Val (PP q (PP r x))
forall a. a -> Val a
Val PP q (PP r x)
b) (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)
b 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, TT (PP q (PP r x)) -> Tree PE
forall a. TT a -> Tree PE
hh TT (PP q (PP r x))
ww]
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
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
if Int
n Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
/= [a] -> Int
forall (t :: Type -> Type) a. Foldable t => t a -> Int
length x
[a]
as then
let msg1 :: String
msg1 = String
msg0 String -> ShowS
forall a. Semigroup a => a -> a -> a
<> [a] -> Int -> String
forall (t :: Type -> Type) a. Foldable t => t a -> Int -> String
badLength x
[a]
as 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
"" []
else Proxy (GuardsImpl (LenT ps) ps)
-> POpts -> x -> m (TT (PP (GuardsImpl (LenT ps) 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 (GuardsImpl (LenT ps) ps)
forall k (t :: k). Proxy t
Proxy @(GuardsImpl (LenT ps) ps)) POpts
opts x
as
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)
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
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)
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))
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) [a]
forall (t :: Type -> Type) a x.
Foldable t =>
POpts -> String -> t a -> [Tree PE] -> Either (TT x) [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 [a]
ws ->
if Int
n Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
/= [a] -> Int
forall (t :: Type -> Type) a. Foldable t => t a -> Int
length [a]
ws then
let msg2 :: String
msg2 = String
msg0 String -> ShowS
forall a. Semigroup a => a -> a -> a
<> [a] -> Int -> String
forall (t :: Type -> Type) a. Foldable t => t a -> Int -> String
badLength [a]
ws 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
"" []
else 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]
ws
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)
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 -> 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 (TT Bool -> String
forall a. TT a -> String
topMessage TT Bool
pp))) 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
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
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]
:)
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)
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))
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
if Int
n Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
/= [a] -> Int
forall (t :: Type -> Type) a. Foldable t => t a -> Int
length x
[a]
as then
let msg1 :: String
msg1 = String
msg0 String -> ShowS
forall a. Semigroup a => a -> a -> a
<> [a] -> Int -> String
forall (t :: Type -> Type) a. Foldable t => t a -> Int -> String
badLength x
[a]
as 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
"" []
else Proxy (GuardsImpl (LenT ps) ps)
-> POpts -> x -> m (TT (PP (GuardsImpl (LenT ps) 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 (GuardsImpl (LenT ps) ps)
forall k (t :: k). Proxy t
Proxy @(GuardsImpl (LenT ps) ps)) POpts
opts x
as
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))
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")
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))
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
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) (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
msg0 String -> ShowS
forall a. Semigroup a => a -> a -> a
<> String
"(ok) | " 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]
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 -> 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 (TT Bool -> String
forall a. TT a -> String
topMessage TT Bool
pp)) [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]
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))
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
subopts 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 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 msgx :: String
msgx = TT Bool -> String
forall a. TT a -> String
topMessage TT Bool
pp
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
msgx) (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) [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
msg0 String -> ShowS
forall a. Semigroup a => a -> a -> a
<> String
"(ok) | " 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]