{-# 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.Iterator (
Scanl
, ScanN
, ScanNA
, FoldN
, Foldl
, Unfoldr
, IterateUntil
, IterateWhile
, IterateNWhile
, IterateNUntil
, UnfoldN
, Para
, ParaN
, DoN
, Repeat
, UnfoldrT
) where
import Predicate.Core
import Predicate.Misc
import Predicate.Util
import Predicate.Data.Tuple (type (***))
import Predicate.Data.Ordering (type (>))
import Predicate.Data.Enum (type (...), Pred)
import Predicate.Data.List (Last)
import Predicate.Data.Maybe (MaybeBool)
import GHC.TypeLits (Nat, KnownNat, ErrorMessage((:$$:),(:<>:)))
import qualified GHC.TypeLits as GL
import Data.Kind (Type)
import Control.Lens
import Data.Proxy (Proxy(Proxy))
import Data.Maybe (catMaybes)
import Control.Arrow (Arrow((&&&)))
import Data.Void (Void)
data Scanl p q r deriving Int -> Scanl p q r -> ShowS
[Scanl p q r] -> ShowS
Scanl p q r -> String
(Int -> Scanl p q r -> ShowS)
-> (Scanl p q r -> String)
-> ([Scanl p q r] -> ShowS)
-> Show (Scanl 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 -> Scanl p q r -> ShowS
forall k (p :: k) k (q :: k) k (r :: k). [Scanl p q r] -> ShowS
forall k (p :: k) k (q :: k) k (r :: k). Scanl p q r -> String
showList :: [Scanl p q r] -> ShowS
$cshowList :: forall k (p :: k) k (q :: k) k (r :: k). [Scanl p q r] -> ShowS
show :: Scanl p q r -> String
$cshow :: forall k (p :: k) k (q :: k) k (r :: k). Scanl p q r -> String
showsPrec :: Int -> Scanl p q r -> ShowS
$cshowsPrec :: forall k (p :: k) k (q :: k) k (r :: k).
Int -> Scanl p q r -> ShowS
Show
instance ( PP p (b,a) ~ b
, PP q x ~ b
, PP r x ~ [a]
, P p (b,a)
, P q x
, P r x
, Show b
, Show a
)
=> P (Scanl p q r) x where
type PP (Scanl p q r) x = [PP q x]
eval :: proxy (Scanl p q r) -> POpts -> x -> m (TT (PP (Scanl p q r) x))
eval proxy (Scanl p q r)
_ POpts
opts x
z = do
let msg0 :: String
msg0 = String
"Scanl"
Either (TT [b]) (b, [a], TT b, TT [a])
lr <- Inline
-> String
-> Proxy q
-> Proxy r
-> POpts
-> x
-> [Tree PE]
-> m (Either (TT [b]) (PP q x, PP r x, TT (PP q x), TT (PP r x)))
forall k1 k2 (p :: k1) a (q :: k2) (m :: Type -> Type)
(proxy1 :: k1 -> Type) (proxy2 :: k2 -> Type) x.
(P p a, P q a, MonadEval m) =>
Inline
-> String
-> proxy1 p
-> proxy2 q
-> POpts
-> a
-> [Tree PE]
-> m (Either (TT x) (PP p a, PP q a, TT (PP p a), TT (PP q a)))
runPQ Inline
NoInline String
msg0 (Proxy q
forall k (t :: k). Proxy t
Proxy @q) (Proxy r
forall k (t :: k). Proxy t
Proxy @r) POpts
opts x
z []
case Either (TT [b]) (b, [a], TT b, TT [a])
lr of
Left TT [b]
e -> TT [b] -> m (TT [b])
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure TT [b]
e
Right (b
q,[a]
r,TT b
qq,TT [a]
rr) ->
case POpts -> String -> [a] -> [Tree PE] -> Either (TT [b]) (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 [a]
r [TT [a] -> Tree PE
forall a. TT a -> Tree PE
hh TT [a]
rr] of
Left TT [b]
e -> TT [b] -> m (TT [b])
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure TT [b]
e
Right (Int, [a])
_ -> do
let ff :: Int
-> b
-> [a]
-> [((Int, b), TT b)]
-> m ([((Int, b), TT b)], Either (TT [b]) ())
ff Int
i b
b [a]
as' [((Int, b), TT b)]
rs
| Int
i Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>= POpts -> Int
getMaxRecursionValue POpts
opts = ([((Int, b), TT b)], Either (TT [b]) ())
-> m ([((Int, b), TT b)], Either (TT [b]) ())
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure ([((Int, b), TT b)]
rs, TT [b] -> Either (TT [b]) ()
forall a b. a -> Either a b
Left (TT [b] -> Either (TT [b]) ()) -> TT [b] -> Either (TT [b]) ()
forall a b. (a -> b) -> a -> b
$ POpts -> Val [b] -> String -> [Tree PE] -> TT [b]
forall a. POpts -> Val a -> String -> [Tree PE] -> TT a
mkNode POpts
opts (String -> Val [b]
forall a. String -> Val a
Fail (String
msg0 String -> ShowS
forall a. Semigroup a => a -> a -> a
<> String
":recursion limit i=" String -> ShowS
forall a. Semigroup a => a -> a -> a
<> Int -> String
forall a. Show a => a -> String
show Int
i)) (String
"(b,as')=" String -> ShowS
forall a. Semigroup a => a -> a -> a
<> POpts -> (b, [a]) -> String
forall a. Show a => POpts -> a -> String
showL POpts
opts (b
b,[a]
as')) [])
| Bool
otherwise =
case [a]
as' of
[] -> ([((Int, b), TT b)], Either (TT [b]) ())
-> m ([((Int, b), TT b)], Either (TT [b]) ())
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure ([((Int, b), TT b)]
rs, () -> Either (TT [b]) ()
forall a b. b -> Either a b
Right ())
a
a:[a]
as -> do
TT b
pp :: TT b <- POpts -> (b, a) -> m (TT (PP p (b, a)))
forall k (p :: k) a (m :: Type -> Type).
(MonadEval m, P p a) =>
POpts -> a -> m (TT (PP p a))
evalHide @p POpts
opts (b
b,a
a)
case Inline -> POpts -> String -> TT b -> [Tree PE] -> Either (TT [b]) b
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
" i=" String -> ShowS
forall a. Semigroup a => a -> a -> a
<> Int -> String
forall a. Show a => a -> String
show Int
i String -> ShowS
forall a. Semigroup a => a -> a -> a
<> String
" a=" 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 b
pp [] of
Left TT [b]
e -> ([((Int, b), TT b)], Either (TT [b]) ())
-> m ([((Int, b), TT b)], Either (TT [b]) ())
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure ([((Int, b), TT b)]
rs,TT [b] -> Either (TT [b]) ()
forall a b. a -> Either a b
Left TT [b]
e)
Right b
b' -> Int
-> b
-> [a]
-> [((Int, b), TT b)]
-> m ([((Int, b), TT b)], Either (TT [b]) ())
ff (Int
iInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
1) b
b' [a]
as ([((Int, b), TT b)]
rs [((Int, b), TT b)] -> [((Int, b), TT b)] -> [((Int, b), TT b)]
forall a. [a] -> [a] -> [a]
++ [((Int
i,b
b), TT b
pp)])
([((Int, b), TT b)]
ts,Either (TT [b]) ()
lrx) :: ([((Int, b), TT b)], Either (TT [b]) ()) <- Int
-> b
-> [a]
-> [((Int, b), TT b)]
-> m ([((Int, b), TT b)], Either (TT [b]) ())
ff Int
1 b
q [a]
r []
TT [b] -> m (TT [b])
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (TT [b] -> m (TT [b])) -> TT [b] -> m (TT [b])
forall a b. (a -> b) -> a -> b
$ case POpts
-> String
-> [((Int, b), TT b)]
-> Either (TT Any) [(b, (Int, b), TT b)]
forall x a w.
Show x =>
POpts
-> String
-> [((Int, x), TT a)]
-> Either (TT w) [(a, (Int, x), TT a)]
splitAndAlign POpts
opts String
msg0 (((Int
0,b
q), POpts -> Val b -> String -> [Tree PE] -> TT b
forall a. POpts -> Val a -> String -> [Tree PE] -> TT a
mkNode POpts
opts (b -> Val b
forall a. a -> Val a
Val b
q) (String
msg0 String -> ShowS
forall a. Semigroup a => a -> a -> a
<> String
"(initial)") []) ((Int, b), TT b) -> [((Int, b), TT b)] -> [((Int, b), TT b)]
forall a. a -> [a] -> [a]
: [((Int, b), TT b)]
ts) of
Left TT Any
e -> String -> TT [b]
forall x. HasCallStack => String -> x
errorInProgram (String -> TT [b]) -> String -> TT [b]
forall a b. (a -> b) -> a -> b
$ String
"Scanl e=" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Tree PE -> String
forall a. Show a => a -> String
show (TT Any -> Tree PE
forall a. TT a -> Tree PE
hh TT Any
e)
Right [(b, (Int, b), TT b)]
abcs ->
let vals :: [b]
vals = ((b, (Int, b), TT b) -> b) -> [(b, (Int, b), TT b)] -> [b]
forall a b. (a -> b) -> [a] -> [b]
map (Getting b (b, (Int, b), TT b) b -> (b, (Int, b), TT b) -> b
forall s (m :: Type -> Type) a.
MonadReader s m =>
Getting a s a -> m a
view Getting b (b, (Int, b), TT b) b
forall s t a b. Field1 s t a b => Lens s t a b
_1) [(b, (Int, b), TT b)]
abcs
itts :: [((Int, b), TT b)]
itts = ((b, (Int, b), TT b) -> ((Int, b), TT b))
-> [(b, (Int, b), TT b)] -> [((Int, b), TT b)]
forall a b. (a -> b) -> [a] -> [b]
map (Getting (Int, b) (b, (Int, b), TT b) (Int, b)
-> (b, (Int, b), TT b) -> (Int, b)
forall s (m :: Type -> Type) a.
MonadReader s m =>
Getting a s a -> m a
view Getting (Int, b) (b, (Int, b), TT b) (Int, b)
forall s t a b. Field2 s t a b => Lens s t a b
_2 ((b, (Int, b), TT b) -> (Int, b))
-> ((b, (Int, b), TT b) -> TT b)
-> (b, (Int, b), TT b)
-> ((Int, b), TT b)
forall (a :: Type -> Type -> Type) b c c'.
Arrow a =>
a b c -> a b c' -> a b (c, c')
&&& Getting (TT b) (b, (Int, b), TT b) (TT b)
-> (b, (Int, b), TT b) -> TT b
forall s (m :: Type -> Type) a.
MonadReader s m =>
Getting a s a -> m a
view Getting (TT b) (b, (Int, b), TT b) (TT b)
forall s t a b. Field3 s t a b => Lens s t a b
_3) [(b, (Int, b), TT b)]
abcs
in case Either (TT [b]) ()
lrx of
Left TT [b]
e -> POpts -> TT [b] -> String -> [Tree PE] -> TT [b]
forall a. POpts -> TT a -> String -> [Tree PE] -> TT a
mkNodeCopy POpts
opts TT [b]
e String
msg0 (TT b -> Tree PE
forall a. TT a -> Tree PE
hh TT b
qq Tree PE -> [Tree PE] -> [Tree PE]
forall a. a -> [a] -> [a]
: TT [a] -> Tree PE
forall a. TT a -> Tree PE
hh TT [a]
rr Tree PE -> [Tree PE] -> [Tree PE]
forall a. a -> [a] -> [a]
: (((Int, b), TT b) -> Tree PE) -> [((Int, b), TT b)] -> [Tree PE]
forall a b. (a -> b) -> [a] -> [b]
map (TT b -> Tree PE
forall a. TT a -> Tree PE
hh (TT b -> Tree PE)
-> (((Int, b), TT b) -> TT b) -> ((Int, b), TT b) -> Tree PE
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((Int, b), TT b) -> TT b
forall x a. ((Int, x), TT a) -> TT a
prefixNumberToTT) [((Int, b), TT b)]
itts)
Right () -> POpts -> Val [b] -> String -> [Tree PE] -> TT [b]
forall a. POpts -> Val a -> String -> [Tree PE] -> TT a
mkNode POpts
opts ([b] -> Val [b]
forall a. a -> Val a
Val [b]
vals) (POpts -> String -> [b] -> String -> b -> String
forall a1 a2.
(Show a1, Show a2) =>
POpts -> String -> a1 -> String -> a2 -> String
show3' POpts
opts String
msg0 [b]
vals String
"b=" b
q String -> ShowS
forall a. Semigroup a => a -> a -> a
<> POpts -> String -> [a] -> String
forall a. Show a => POpts -> String -> a -> String
showVerbose POpts
opts String
" | as=" [a]
r) (TT b -> Tree PE
forall a. TT a -> Tree PE
hh TT b
qq Tree PE -> [Tree PE] -> [Tree PE]
forall a. a -> [a] -> [a]
: TT [a] -> Tree PE
forall a. TT a -> Tree PE
hh TT [a]
rr Tree PE -> [Tree PE] -> [Tree PE]
forall a. a -> [a] -> [a]
: (((Int, b), TT b) -> Tree PE) -> [((Int, b), TT b)] -> [Tree PE]
forall a b. (a -> b) -> [a] -> [b]
map (TT b -> Tree PE
forall a. TT a -> Tree PE
hh (TT b -> Tree PE)
-> (((Int, b), TT b) -> TT b) -> ((Int, b), TT b) -> Tree PE
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((Int, b), TT b) -> TT b
forall x a. ((Int, x), TT a) -> TT a
prefixNumberToTT) [((Int, b), TT b)]
itts)
data ScanN n p q deriving Int -> ScanN n p q -> ShowS
[ScanN n p q] -> ShowS
ScanN n p q -> String
(Int -> ScanN n p q -> ShowS)
-> (ScanN n p q -> String)
-> ([ScanN n p q] -> ShowS)
-> Show (ScanN n p q)
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
forall k (n :: k) k (p :: k) k (q :: k).
Int -> ScanN n p q -> ShowS
forall k (n :: k) k (p :: k) k (q :: k). [ScanN n p q] -> ShowS
forall k (n :: k) k (p :: k) k (q :: k). ScanN n p q -> String
showList :: [ScanN n p q] -> ShowS
$cshowList :: forall k (n :: k) k (p :: k) k (q :: k). [ScanN n p q] -> ShowS
show :: ScanN n p q -> String
$cshow :: forall k (n :: k) k (p :: k) k (q :: k). ScanN n p q -> String
showsPrec :: Int -> ScanN n p q -> ShowS
$cshowsPrec :: forall k (n :: k) k (p :: k) k (q :: k).
Int -> ScanN n p q -> ShowS
Show
type ScanNT n p q = Scanl (Fst >> p) q (1...n)
instance P (ScanNT n p q) x => P (ScanN n p q) x where
type PP (ScanN n p q) x = PP (ScanNT n p q) x
eval :: proxy (ScanN n p q) -> POpts -> x -> m (TT (PP (ScanN n p q) x))
eval proxy (ScanN n p q)
_ = Proxy (ScanNT n p q) -> POpts -> x -> m (TT (PP (ScanNT n p q) x))
forall k (p :: k) a (m :: Type -> Type) (proxy :: k -> Type).
(P p a, MonadEval m) =>
proxy p -> POpts -> a -> m (TT (PP p a))
eval (Proxy (ScanNT n p q)
forall k (t :: k). Proxy t
Proxy @(ScanNT n p q))
data ScanNA q deriving Int -> ScanNA q -> ShowS
[ScanNA q] -> ShowS
ScanNA q -> String
(Int -> ScanNA q -> ShowS)
-> (ScanNA q -> String) -> ([ScanNA q] -> ShowS) -> Show (ScanNA q)
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
forall k (q :: k). Int -> ScanNA q -> ShowS
forall k (q :: k). [ScanNA q] -> ShowS
forall k (q :: k). ScanNA q -> String
showList :: [ScanNA q] -> ShowS
$cshowList :: forall k (q :: k). [ScanNA q] -> ShowS
show :: ScanNA q -> String
$cshow :: forall k (q :: k). ScanNA q -> String
showsPrec :: Int -> ScanNA q -> ShowS
$cshowsPrec :: forall k (q :: k). Int -> ScanNA q -> ShowS
Show
type ScanNAT q = ScanN Fst q Snd
instance P (ScanNAT q) x => P (ScanNA q) x where
type PP (ScanNA q) x = PP (ScanNAT q) x
eval :: proxy (ScanNA q) -> POpts -> x -> m (TT (PP (ScanNA q) x))
eval proxy (ScanNA q)
_ = Proxy (ScanNAT q) -> POpts -> x -> m (TT (PP (ScanNAT q) x))
forall k (p :: k) a (m :: Type -> Type) (proxy :: k -> Type).
(P p a, MonadEval m) =>
proxy p -> POpts -> a -> m (TT (PP p a))
eval (Proxy (ScanNAT q)
forall k (t :: k). Proxy t
Proxy @(ScanNAT q))
data FoldN n p q deriving Int -> FoldN n p q -> ShowS
[FoldN n p q] -> ShowS
FoldN n p q -> String
(Int -> FoldN n p q -> ShowS)
-> (FoldN n p q -> String)
-> ([FoldN n p q] -> ShowS)
-> Show (FoldN n p q)
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
forall k (n :: k) k (p :: k) k (q :: k).
Int -> FoldN n p q -> ShowS
forall k (n :: k) k (p :: k) k (q :: k). [FoldN n p q] -> ShowS
forall k (n :: k) k (p :: k) k (q :: k). FoldN n p q -> String
showList :: [FoldN n p q] -> ShowS
$cshowList :: forall k (n :: k) k (p :: k) k (q :: k). [FoldN n p q] -> ShowS
show :: FoldN n p q -> String
$cshow :: forall k (n :: k) k (p :: k) k (q :: k). FoldN n p q -> String
showsPrec :: Int -> FoldN n p q -> ShowS
$cshowsPrec :: forall k (n :: k) k (p :: k) k (q :: k).
Int -> FoldN n p q -> ShowS
Show
type FoldNT n p q = ScanN n p q >> Last
instance P (FoldNT n p q) x => P (FoldN n p q) x where
type PP (FoldN n p q) x = PP (FoldNT n p q) x
eval :: proxy (FoldN n p q) -> POpts -> x -> m (TT (PP (FoldN n p q) x))
eval proxy (FoldN n p q)
_ = Proxy (FoldNT n p q) -> POpts -> x -> m (TT (PP (FoldNT n p q) x))
forall k (p :: k) a (m :: Type -> Type) (proxy :: k -> Type).
(P p a, MonadEval m) =>
proxy p -> POpts -> a -> m (TT (PP p a))
eval (Proxy (FoldNT n p q)
forall k (t :: k). Proxy t
Proxy @(FoldNT n p q))
data Foldl p q r deriving Int -> Foldl p q r -> ShowS
[Foldl p q r] -> ShowS
Foldl p q r -> String
(Int -> Foldl p q r -> ShowS)
-> (Foldl p q r -> String)
-> ([Foldl p q r] -> ShowS)
-> Show (Foldl 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 -> Foldl p q r -> ShowS
forall k (p :: k) k (q :: k) k (r :: k). [Foldl p q r] -> ShowS
forall k (p :: k) k (q :: k) k (r :: k). Foldl p q r -> String
showList :: [Foldl p q r] -> ShowS
$cshowList :: forall k (p :: k) k (q :: k) k (r :: k). [Foldl p q r] -> ShowS
show :: Foldl p q r -> String
$cshow :: forall k (p :: k) k (q :: k) k (r :: k). Foldl p q r -> String
showsPrec :: Int -> Foldl p q r -> ShowS
$cshowsPrec :: forall k (p :: k) k (q :: k) k (r :: k).
Int -> Foldl p q r -> ShowS
Show
type FoldLT p q r = Scanl p q r >> Last
instance P (FoldLT p q r) x => P (Foldl p q r) x where
type PP (Foldl p q r) x = PP (FoldLT p q r) x
eval :: proxy (Foldl p q r) -> POpts -> x -> m (TT (PP (Foldl p q r) x))
eval proxy (Foldl p q r)
_ = Proxy (FoldLT p q r) -> POpts -> x -> m (TT (PP (FoldLT p q 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 (FoldLT p q r)
forall k (t :: k). Proxy t
Proxy @(FoldLT p q r))
data Unfoldr p q deriving Int -> Unfoldr p q -> ShowS
[Unfoldr p q] -> ShowS
Unfoldr p q -> String
(Int -> Unfoldr p q -> ShowS)
-> (Unfoldr p q -> String)
-> ([Unfoldr p q] -> ShowS)
-> Show (Unfoldr p q)
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
forall k (p :: k) k (q :: k). Int -> Unfoldr p q -> ShowS
forall k (p :: k) k (q :: k). [Unfoldr p q] -> ShowS
forall k (p :: k) k (q :: k). Unfoldr p q -> String
showList :: [Unfoldr p q] -> ShowS
$cshowList :: forall k (p :: k) k (q :: k). [Unfoldr p q] -> ShowS
show :: Unfoldr p q -> String
$cshow :: forall k (p :: k) k (q :: k). Unfoldr p q -> String
showsPrec :: Int -> Unfoldr p q -> ShowS
$cshowsPrec :: forall k (p :: k) k (q :: k). Int -> Unfoldr p q -> ShowS
Show
instance ( PP q a ~ s
, PP p s ~ Maybe (b,s)
, P q a
, P p s
, Show s
, Show b
)
=> P (Unfoldr p q) a where
type PP (Unfoldr p q) a = [UnfoldrT (PP p (PP q a))]
eval :: proxy (Unfoldr p q) -> POpts -> a -> m (TT (PP (Unfoldr p q) a))
eval proxy (Unfoldr p q)
_ POpts
opts a
z = do
let msg0 :: String
msg0 = String
"Unfoldr"
TT s
qq <- Proxy q -> POpts -> a -> m (TT (PP q a))
forall k (p :: k) a (m :: Type -> Type) (proxy :: k -> Type).
(P p a, MonadEval m) =>
proxy p -> POpts -> a -> m (TT (PP p a))
eval (Proxy q
forall k (t :: k). Proxy t
Proxy @q) POpts
opts a
z
case Inline -> POpts -> String -> TT s -> [Tree PE] -> Either (TT [b]) s
forall a x.
Inline -> POpts -> String -> TT a -> [Tree PE] -> Either (TT x) a
getValueLR Inline
NoInline POpts
opts String
msg0 TT s
qq [] of
Left TT [b]
e -> TT [b] -> m (TT [b])
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure TT [b]
e
Right s
q -> do
let msg1 :: String
msg1 = String
msg0 String -> ShowS
forall a. Semigroup a => a -> a -> a
<> String
" " String -> ShowS
forall a. Semigroup a => a -> a -> a
<> POpts -> s -> String
forall a. Show a => POpts -> a -> String
showL POpts
opts s
q
ff :: Int
-> s
-> [((Int, Maybe (b, s)), TT (Maybe (b, s)))]
-> m ([((Int, Maybe (b, s)), TT (Maybe (b, s)))],
Either (TT [b]) ())
ff Int
i s
s [((Int, Maybe (b, s)), TT (Maybe (b, s)))]
rs | Int
i Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>= POpts -> Int
getMaxRecursionValue POpts
opts = ([((Int, Maybe (b, s)), TT (Maybe (b, s)))], Either (TT [b]) ())
-> m ([((Int, Maybe (b, s)), TT (Maybe (b, s)))],
Either (TT [b]) ())
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure ([((Int, Maybe (b, s)), TT (Maybe (b, s)))]
rs, TT [b] -> Either (TT [b]) ()
forall a b. a -> Either a b
Left (TT [b] -> Either (TT [b]) ()) -> TT [b] -> Either (TT [b]) ()
forall a b. (a -> b) -> a -> b
$ POpts -> Val [b] -> String -> [Tree PE] -> TT [b]
forall a. POpts -> Val a -> String -> [Tree PE] -> TT a
mkNode POpts
opts (String -> Val [b]
forall a. String -> Val a
Fail (String
msg1 String -> ShowS
forall a. Semigroup a => a -> a -> a
<> String
":recursion limit i=" String -> ShowS
forall a. Semigroup a => a -> a -> a
<> Int -> String
forall a. Show a => a -> String
show Int
i)) (String
"s=" String -> ShowS
forall a. Semigroup a => a -> a -> a
<> POpts -> s -> String
forall a. Show a => POpts -> a -> String
showL POpts
opts s
s) [])
| Bool
otherwise = do
pp :: TT (PP p s) <- POpts -> s -> m (TT (PP p s))
forall k (p :: k) a (m :: Type -> Type).
(MonadEval m, P p a) =>
POpts -> a -> m (TT (PP p a))
evalHide @p POpts
opts s
s
case Inline
-> POpts
-> String
-> TT (Maybe (b, s))
-> [Tree PE]
-> Either (TT [b]) (Maybe (b, s))
forall a x.
Inline -> POpts -> String -> TT a -> [Tree PE] -> Either (TT x) a
getValueLR Inline
NoInline POpts
opts (String
msg1 String -> ShowS
forall a. Semigroup a => a -> a -> a
<> String
" i=" String -> ShowS
forall a. Semigroup a => a -> a -> a
<> Int -> String
forall a. Show a => a -> String
show Int
i String -> ShowS
forall a. Semigroup a => a -> a -> a
<> String
" s=" String -> ShowS
forall a. Semigroup a => a -> a -> a
<> s -> String
forall a. Show a => a -> String
show s
s) TT (Maybe (b, s))
TT (PP p s)
pp [] of
Left TT [b]
e -> ([((Int, Maybe (b, s)), TT (Maybe (b, s)))], Either (TT [b]) ())
-> m ([((Int, Maybe (b, s)), TT (Maybe (b, s)))],
Either (TT [b]) ())
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure ([((Int, Maybe (b, s)), TT (Maybe (b, s)))]
rs, TT [b] -> Either (TT [b]) ()
forall a b. a -> Either a b
Left TT [b]
e)
Right Maybe (b, s)
Nothing -> ([((Int, Maybe (b, s)), TT (Maybe (b, s)))], Either (TT [b]) ())
-> m ([((Int, Maybe (b, s)), TT (Maybe (b, s)))],
Either (TT [b]) ())
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure ([((Int, Maybe (b, s)), TT (Maybe (b, s)))]
rs [((Int, Maybe (b, s)), TT (Maybe (b, s)))]
-> [((Int, Maybe (b, s)), TT (Maybe (b, s)))]
-> [((Int, Maybe (b, s)), TT (Maybe (b, s)))]
forall a. [a] -> [a] -> [a]
++ [((Int
i,Maybe (b, s)
forall a. Maybe a
Nothing), TT (Maybe (b, s))
TT (PP p s)
pp)], () -> Either (TT [b]) ()
forall a b. b -> Either a b
Right ())
Right w :: Maybe (b, s)
w@(Just (b
_b,s
s')) -> Int
-> s
-> [((Int, Maybe (b, s)), TT (Maybe (b, s)))]
-> m ([((Int, Maybe (b, s)), TT (Maybe (b, s)))],
Either (TT [b]) ())
ff (Int
iInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
1) s
s' ([((Int, Maybe (b, s)), TT (Maybe (b, s)))]
rs [((Int, Maybe (b, s)), TT (Maybe (b, s)))]
-> [((Int, Maybe (b, s)), TT (Maybe (b, s)))]
-> [((Int, Maybe (b, s)), TT (Maybe (b, s)))]
forall a. [a] -> [a] -> [a]
++ [((Int
i,Maybe (b, s)
w), TT (Maybe (b, s))
TT (PP p s)
pp)])
(ts,lr) :: ([((Int, PP p s), TT (PP p s))], Either (TT [b]) ()) <- Int
-> s
-> [((Int, Maybe (b, s)), TT (Maybe (b, s)))]
-> m ([((Int, Maybe (b, s)), TT (Maybe (b, s)))],
Either (TT [b]) ())
ff Int
1 s
q []
TT [b] -> m (TT [b])
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (TT [b] -> m (TT [b])) -> TT [b] -> m (TT [b])
forall a b. (a -> b) -> a -> b
$ case POpts
-> String
-> [((Int, Maybe (b, s)), TT (Maybe (b, s)))]
-> Either
(TT Any) [(Maybe (b, s), (Int, Maybe (b, s)), TT (Maybe (b, s)))]
forall x a w.
Show x =>
POpts
-> String
-> [((Int, x), TT a)]
-> Either (TT w) [(a, (Int, x), TT a)]
splitAndAlign POpts
opts String
msg1 [((Int, Maybe (b, s)), TT (Maybe (b, s)))]
[((Int, PP p s), TT (PP p s))]
ts of
Left TT Any
e -> String -> TT [b]
forall x. HasCallStack => String -> x
errorInProgram (String -> TT [b]) -> String -> TT [b]
forall a b. (a -> b) -> a -> b
$ String
"Unfoldr e=" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Tree PE -> String
forall a. Show a => a -> String
show (TT Any -> Tree PE
forall a. TT a -> Tree PE
hh TT Any
e)
Right [(Maybe (b, s), (Int, Maybe (b, s)), TT (Maybe (b, s)))]
abcs ->
let vals :: [Maybe (b, s)]
vals = ((Maybe (b, s), (Int, Maybe (b, s)), TT (Maybe (b, s)))
-> Maybe (b, s))
-> [(Maybe (b, s), (Int, Maybe (b, s)), TT (Maybe (b, s)))]
-> [Maybe (b, s)]
forall a b. (a -> b) -> [a] -> [b]
map (Getting
(Maybe (b, s))
(Maybe (b, s), (Int, Maybe (b, s)), TT (Maybe (b, s)))
(Maybe (b, s))
-> (Maybe (b, s), (Int, Maybe (b, s)), TT (Maybe (b, s)))
-> Maybe (b, s)
forall s (m :: Type -> Type) a.
MonadReader s m =>
Getting a s a -> m a
view Getting
(Maybe (b, s))
(Maybe (b, s), (Int, Maybe (b, s)), TT (Maybe (b, s)))
(Maybe (b, s))
forall s t a b. Field1 s t a b => Lens s t a b
_1) [(Maybe (b, s), (Int, Maybe (b, s)), TT (Maybe (b, s)))]
abcs
itts :: [((Int, Maybe (b, s)), TT (Maybe (b, s)))]
itts = ((Maybe (b, s), (Int, Maybe (b, s)), TT (Maybe (b, s)))
-> ((Int, Maybe (b, s)), TT (Maybe (b, s))))
-> [(Maybe (b, s), (Int, Maybe (b, s)), TT (Maybe (b, s)))]
-> [((Int, Maybe (b, s)), TT (Maybe (b, s)))]
forall a b. (a -> b) -> [a] -> [b]
map (Getting
(Int, Maybe (b, s))
(Maybe (b, s), (Int, Maybe (b, s)), TT (Maybe (b, s)))
(Int, Maybe (b, s))
-> (Maybe (b, s), (Int, Maybe (b, s)), TT (Maybe (b, s)))
-> (Int, Maybe (b, s))
forall s (m :: Type -> Type) a.
MonadReader s m =>
Getting a s a -> m a
view Getting
(Int, Maybe (b, s))
(Maybe (b, s), (Int, Maybe (b, s)), TT (Maybe (b, s)))
(Int, Maybe (b, s))
forall s t a b. Field2 s t a b => Lens s t a b
_2 ((Maybe (b, s), (Int, Maybe (b, s)), TT (Maybe (b, s)))
-> (Int, Maybe (b, s)))
-> ((Maybe (b, s), (Int, Maybe (b, s)), TT (Maybe (b, s)))
-> TT (Maybe (b, s)))
-> (Maybe (b, s), (Int, Maybe (b, s)), TT (Maybe (b, s)))
-> ((Int, Maybe (b, s)), TT (Maybe (b, s)))
forall (a :: Type -> Type -> Type) b c c'.
Arrow a =>
a b c -> a b c' -> a b (c, c')
&&& Getting
(TT (Maybe (b, s)))
(Maybe (b, s), (Int, Maybe (b, s)), TT (Maybe (b, s)))
(TT (Maybe (b, s)))
-> (Maybe (b, s), (Int, Maybe (b, s)), TT (Maybe (b, s)))
-> TT (Maybe (b, s))
forall s (m :: Type -> Type) a.
MonadReader s m =>
Getting a s a -> m a
view Getting
(TT (Maybe (b, s)))
(Maybe (b, s), (Int, Maybe (b, s)), TT (Maybe (b, s)))
(TT (Maybe (b, s)))
forall s t a b. Field3 s t a b => Lens s t a b
_3) [(Maybe (b, s), (Int, Maybe (b, s)), TT (Maybe (b, s)))]
abcs
in case Either (TT [b]) ()
lr of
Left TT [b]
e -> POpts -> TT [b] -> String -> [Tree PE] -> TT [b]
forall a. POpts -> TT a -> String -> [Tree PE] -> TT a
mkNodeCopy POpts
opts TT [b]
e String
msg1 (TT s -> Tree PE
forall a. TT a -> Tree PE
hh TT s
qq Tree PE -> [Tree PE] -> [Tree PE]
forall a. a -> [a] -> [a]
: (((Int, Maybe (b, s)), TT (Maybe (b, s))) -> Tree PE)
-> [((Int, Maybe (b, s)), TT (Maybe (b, s)))] -> [Tree PE]
forall a b. (a -> b) -> [a] -> [b]
map (TT (Maybe (b, s)) -> Tree PE
forall a. TT a -> Tree PE
hh (TT (Maybe (b, s)) -> Tree PE)
-> (((Int, Maybe (b, s)), TT (Maybe (b, s))) -> TT (Maybe (b, s)))
-> ((Int, Maybe (b, s)), TT (Maybe (b, s)))
-> Tree PE
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((Int, Maybe (b, s)), TT (Maybe (b, s))) -> TT (Maybe (b, s))
forall x a. ((Int, x), TT a) -> TT a
prefixNumberToTT) [((Int, Maybe (b, s)), TT (Maybe (b, s)))]
itts)
Right () ->
let ret :: [b]
ret = (b, s) -> b
forall a b. (a, b) -> a
fst ((b, s) -> b) -> [(b, s)] -> [b]
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> [Maybe (b, s)] -> [(b, s)]
forall a. [Maybe a] -> [a]
catMaybes [Maybe (b, s)]
vals
in POpts -> Val [b] -> String -> [Tree PE] -> TT [b]
forall a. POpts -> Val a -> String -> [Tree PE] -> TT a
mkNode POpts
opts ([b] -> Val [b]
forall a. a -> Val a
Val [b]
ret) (POpts -> String -> [b] -> String -> s -> String
forall a1 a2.
(Show a1, Show a2) =>
POpts -> String -> a1 -> String -> a2 -> String
show3' POpts
opts String
msg1 [b]
ret String
"s=" s
q) (TT s -> Tree PE
forall a. TT a -> Tree PE
hh TT s
qq Tree PE -> [Tree PE] -> [Tree PE]
forall a. a -> [a] -> [a]
: (((Int, Maybe (b, s)), TT (Maybe (b, s))) -> Tree PE)
-> [((Int, Maybe (b, s)), TT (Maybe (b, s)))] -> [Tree PE]
forall a b. (a -> b) -> [a] -> [b]
map (TT (Maybe (b, s)) -> Tree PE
forall a. TT a -> Tree PE
hh (TT (Maybe (b, s)) -> Tree PE)
-> (((Int, Maybe (b, s)), TT (Maybe (b, s))) -> TT (Maybe (b, s)))
-> ((Int, Maybe (b, s)), TT (Maybe (b, s)))
-> Tree PE
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((Int, Maybe (b, s)), TT (Maybe (b, s))) -> TT (Maybe (b, s))
forall x a. ((Int, x), TT a) -> TT a
prefixNumberToTT) [((Int, Maybe (b, s)), TT (Maybe (b, s)))]
itts)
type family UnfoldrT (mbs :: Type) where
UnfoldrT (Maybe (b, _)) = b
UnfoldrT o = GL.TypeError (
'GL.Text "UnfoldrT: expected 'Maybe (b, _)' "
':$$: 'GL.Text "o = "
':<>: 'GL.ShowType o)
data UnfoldN n p s deriving Int -> UnfoldN n p s -> ShowS
[UnfoldN n p s] -> ShowS
UnfoldN n p s -> String
(Int -> UnfoldN n p s -> ShowS)
-> (UnfoldN n p s -> String)
-> ([UnfoldN n p s] -> ShowS)
-> Show (UnfoldN n p s)
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
forall k (n :: k) k (p :: k) k (s :: k).
Int -> UnfoldN n p s -> ShowS
forall k (n :: k) k (p :: k) k (s :: k). [UnfoldN n p s] -> ShowS
forall k (n :: k) k (p :: k) k (s :: k). UnfoldN n p s -> String
showList :: [UnfoldN n p s] -> ShowS
$cshowList :: forall k (n :: k) k (p :: k) k (s :: k). [UnfoldN n p s] -> ShowS
show :: UnfoldN n p s -> String
$cshow :: forall k (n :: k) k (p :: k) k (s :: k). UnfoldN n p s -> String
showsPrec :: Int -> UnfoldN n p s -> ShowS
$cshowsPrec :: forall k (n :: k) k (p :: k) k (s :: k).
Int -> UnfoldN n p s -> ShowS
Show
type IterateNT n p s = Unfoldr (MaybeBool (Snd > 0) ((p *** Pred) >> '(L11,'(L12,Snd)))) '(s,n)
instance P (IterateNT n p s) x => P (UnfoldN n p s) x where
type PP (UnfoldN n p s) x = PP (IterateNT n p s) x
eval :: proxy (UnfoldN n p s)
-> POpts -> x -> m (TT (PP (UnfoldN n p s) x))
eval proxy (UnfoldN n p s)
_ = Proxy (IterateNT n p s)
-> POpts -> x -> m (TT (PP (IterateNT n p s) 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 (IterateNT n p s)
forall k (t :: k). Proxy t
Proxy @(IterateNT n p s))
data IterateUntil p f deriving Int -> IterateUntil p f -> ShowS
[IterateUntil p f] -> ShowS
IterateUntil p f -> String
(Int -> IterateUntil p f -> ShowS)
-> (IterateUntil p f -> String)
-> ([IterateUntil p f] -> ShowS)
-> Show (IterateUntil p f)
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
forall k (p :: k) k (f :: k). Int -> IterateUntil p f -> ShowS
forall k (p :: k) k (f :: k). [IterateUntil p f] -> ShowS
forall k (p :: k) k (f :: k). IterateUntil p f -> String
showList :: [IterateUntil p f] -> ShowS
$cshowList :: forall k (p :: k) k (f :: k). [IterateUntil p f] -> ShowS
show :: IterateUntil p f -> String
$cshow :: forall k (p :: k) k (f :: k). IterateUntil p f -> String
showsPrec :: Int -> IterateUntil p f -> ShowS
$cshowsPrec :: forall k (p :: k) k (f :: k). Int -> IterateUntil p f -> ShowS
Show
type IterateUntilT p f = IterateWhile (Not p) f
instance P (IterateUntilT p f) x => P (IterateUntil p f) x where
type PP (IterateUntil p f) x = PP (IterateUntilT p f) x
eval :: proxy (IterateUntil p f)
-> POpts -> x -> m (TT (PP (IterateUntil p f) x))
eval proxy (IterateUntil p f)
_ = Proxy (IterateUntilT p f)
-> POpts -> x -> m (TT (PP (IterateUntilT p f) 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 (IterateUntilT p f)
forall k (t :: k). Proxy t
Proxy @(IterateUntilT p f))
data IterateWhile p f deriving Int -> IterateWhile p f -> ShowS
[IterateWhile p f] -> ShowS
IterateWhile p f -> String
(Int -> IterateWhile p f -> ShowS)
-> (IterateWhile p f -> String)
-> ([IterateWhile p f] -> ShowS)
-> Show (IterateWhile p f)
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
forall k (p :: k) k (f :: k). Int -> IterateWhile p f -> ShowS
forall k (p :: k) k (f :: k). [IterateWhile p f] -> ShowS
forall k (p :: k) k (f :: k). IterateWhile p f -> String
showList :: [IterateWhile p f] -> ShowS
$cshowList :: forall k (p :: k) k (f :: k). [IterateWhile p f] -> ShowS
show :: IterateWhile p f -> String
$cshow :: forall k (p :: k) k (f :: k). IterateWhile p f -> String
showsPrec :: Int -> IterateWhile p f -> ShowS
$cshowsPrec :: forall k (p :: k) k (f :: k). Int -> IterateWhile p f -> ShowS
Show
type IterateWhileT p f = Unfoldr (MaybeBool p '(Id, f)) Id
instance P (IterateWhileT p f) x => P (IterateWhile p f) x where
type PP (IterateWhile p f) x = PP (IterateWhileT p f) x
eval :: proxy (IterateWhile p f)
-> POpts -> x -> m (TT (PP (IterateWhile p f) x))
eval proxy (IterateWhile p f)
_ = Proxy (IterateWhileT p f)
-> POpts -> x -> m (TT (PP (IterateWhileT p f) 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 (IterateWhileT p f)
forall k (t :: k). Proxy t
Proxy @(IterateWhileT p f))
data IterateNWhile n p f deriving Int -> IterateNWhile n p f -> ShowS
[IterateNWhile n p f] -> ShowS
IterateNWhile n p f -> String
(Int -> IterateNWhile n p f -> ShowS)
-> (IterateNWhile n p f -> String)
-> ([IterateNWhile n p f] -> ShowS)
-> Show (IterateNWhile n p f)
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
forall k (n :: k) k (p :: k) k (f :: k).
Int -> IterateNWhile n p f -> ShowS
forall k (n :: k) k (p :: k) k (f :: k).
[IterateNWhile n p f] -> ShowS
forall k (n :: k) k (p :: k) k (f :: k).
IterateNWhile n p f -> String
showList :: [IterateNWhile n p f] -> ShowS
$cshowList :: forall k (n :: k) k (p :: k) k (f :: k).
[IterateNWhile n p f] -> ShowS
show :: IterateNWhile n p f -> String
$cshow :: forall k (n :: k) k (p :: k) k (f :: k).
IterateNWhile n p f -> String
showsPrec :: Int -> IterateNWhile n p f -> ShowS
$cshowsPrec :: forall k (n :: k) k (p :: k) k (f :: k).
Int -> IterateNWhile n p f -> ShowS
Show
type IterateNWhileT n p f = '(n, Id) >> IterateWhile (Fst > 0 && (Snd >> p)) (Pred *** f) >> Map Snd
instance P (IterateNWhileT n p f) x => P (IterateNWhile n p f) x where
type PP (IterateNWhile n p f) x = PP (IterateNWhileT n p f) x
eval :: proxy (IterateNWhile n p f)
-> POpts -> x -> m (TT (PP (IterateNWhile n p f) x))
eval proxy (IterateNWhile n p f)
_ = Proxy (IterateNWhileT n p f)
-> POpts -> x -> m (TT (PP (IterateNWhileT n p f) 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 (IterateNWhileT n p f)
forall k (t :: k). Proxy t
Proxy @(IterateNWhileT n p f))
data IterateNUntil n p f deriving Int -> IterateNUntil n p f -> ShowS
[IterateNUntil n p f] -> ShowS
IterateNUntil n p f -> String
(Int -> IterateNUntil n p f -> ShowS)
-> (IterateNUntil n p f -> String)
-> ([IterateNUntil n p f] -> ShowS)
-> Show (IterateNUntil n p f)
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
forall k (n :: k) k (p :: k) k (f :: k).
Int -> IterateNUntil n p f -> ShowS
forall k (n :: k) k (p :: k) k (f :: k).
[IterateNUntil n p f] -> ShowS
forall k (n :: k) k (p :: k) k (f :: k).
IterateNUntil n p f -> String
showList :: [IterateNUntil n p f] -> ShowS
$cshowList :: forall k (n :: k) k (p :: k) k (f :: k).
[IterateNUntil n p f] -> ShowS
show :: IterateNUntil n p f -> String
$cshow :: forall k (n :: k) k (p :: k) k (f :: k).
IterateNUntil n p f -> String
showsPrec :: Int -> IterateNUntil n p f -> ShowS
$cshowsPrec :: forall k (n :: k) k (p :: k) k (f :: k).
Int -> IterateNUntil n p f -> ShowS
Show
type IterateNUntilT n p f = IterateNWhile n (Not p) f
instance P (IterateNUntilT n p f) x => P (IterateNUntil n p f) x where
type PP (IterateNUntil n p f) x = PP (IterateNUntilT n p f) x
eval :: proxy (IterateNUntil n p f)
-> POpts -> x -> m (TT (PP (IterateNUntil n p f) x))
eval proxy (IterateNUntil n p f)
_ = Proxy (IterateNUntilT n p f)
-> POpts -> x -> m (TT (PP (IterateNUntilT n p f) 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 (IterateNUntilT n p f)
forall k (t :: k). Proxy t
Proxy @(IterateNUntilT n p f))
data ParaImpl (n :: Nat) (os :: [k]) deriving Int -> ParaImpl n os -> ShowS
[ParaImpl n os] -> ShowS
ParaImpl n os -> String
(Int -> ParaImpl n os -> ShowS)
-> (ParaImpl n os -> String)
-> ([ParaImpl n os] -> ShowS)
-> Show (ParaImpl n os)
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
forall (n :: Nat) k (os :: [k]). Int -> ParaImpl n os -> ShowS
forall (n :: Nat) k (os :: [k]). [ParaImpl n os] -> ShowS
forall (n :: Nat) k (os :: [k]). ParaImpl n os -> String
showList :: [ParaImpl n os] -> ShowS
$cshowList :: forall (n :: Nat) k (os :: [k]). [ParaImpl n os] -> ShowS
show :: ParaImpl n os -> String
$cshow :: forall (n :: Nat) k (os :: [k]). ParaImpl n os -> String
showsPrec :: Int -> ParaImpl n os -> ShowS
$cshowsPrec :: forall (n :: Nat) k (os :: [k]). Int -> ParaImpl n os -> ShowS
Show
data Para (ps :: [k]) deriving Int -> Para ps -> ShowS
[Para ps] -> ShowS
Para ps -> String
(Int -> Para ps -> ShowS)
-> (Para ps -> String) -> ([Para ps] -> ShowS) -> Show (Para ps)
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
forall k (ps :: [k]). Int -> Para ps -> ShowS
forall k (ps :: [k]). [Para ps] -> ShowS
forall k (ps :: [k]). Para ps -> String
showList :: [Para ps] -> ShowS
$cshowList :: forall k (ps :: [k]). [Para ps] -> ShowS
show :: Para ps -> String
$cshow :: forall k (ps :: [k]). Para ps -> String
showsPrec :: Int -> Para ps -> ShowS
$cshowsPrec :: forall k (ps :: [k]). Int -> Para ps -> ShowS
Show
instance ( [a] ~ x
, GetLen ps
, P (ParaImpl (LenT ps) ps) x
) => P (Para ps) x where
type PP (Para ps) x = PP (ParaImpl (LenT ps) ps) x
eval :: proxy (Para ps) -> POpts -> x -> m (TT (PP (Para ps) x))
eval proxy (Para ps)
_ POpts
opts x
as' = do
let msg0 :: String
msg0 = String
"Para"
n :: Int
n = GetLen ps => Int
forall k (xs :: k). GetLen xs => Int
getLen @ps
case POpts
-> String
-> [a]
-> [Tree PE]
-> Either (TT (PP (ParaImpl (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 (ParaImpl (LenT ps) ps) [a])
e -> TT (PP (ParaImpl (LenT ps) ps) [a])
-> m (TT (PP (ParaImpl (LenT ps) ps) [a]))
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure TT (PP (ParaImpl (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 (ParaImpl (LenT ps) ps)
-> POpts -> [a] -> m (TT (PP (ParaImpl (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 (ParaImpl (LenT ps) ps)
forall k (t :: k). Proxy t
Proxy @(ParaImpl (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 (ParaImpl (LenT ps) ps) [a])
-> m (TT (PP (ParaImpl (LenT ps) ps) [a]))
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (TT (PP (ParaImpl (LenT ps) ps) [a])
-> m (TT (PP (ParaImpl (LenT ps) ps) [a])))
-> TT (PP (ParaImpl (LenT ps) ps) [a])
-> m (TT (PP (ParaImpl (LenT ps) ps) [a]))
forall a b. (a -> b) -> a -> b
$ POpts
-> Val (PP (ParaImpl (LenT ps) ps) [a])
-> String
-> [Tree PE]
-> TT (PP (ParaImpl (LenT ps) ps) [a])
forall a. POpts -> Val a -> String -> [Tree PE] -> TT a
mkNode POpts
opts (String -> Val (PP (ParaImpl (LenT ps) ps) [a])
forall a. String -> Val a
Fail String
msg1) String
"" []
instance GL.TypeError ('GL.Text "ParaImpl '[] invalid: requires at least one value in the list")
=> P (ParaImpl n ('[] :: [k])) x where
type PP (ParaImpl n ('[] :: [k])) x = Void
eval :: proxy (ParaImpl n '[])
-> POpts -> x -> m (TT (PP (ParaImpl n '[]) x))
eval proxy (ParaImpl n '[])
_ POpts
_ x
_ = String -> m (TT Void)
forall x. HasCallStack => String -> x
errorInProgram String
"ParaImpl empty list"
instance ( KnownNat n
, Show a
, Show (PP p a)
, P p a
, x ~ [a]
) => P (ParaImpl n '[p]) x where
type PP (ParaImpl n '[p]) x = [PP p (ExtractAFromTA x)]
eval :: proxy (ParaImpl n '[p])
-> POpts -> x -> m (TT (PP (ParaImpl n '[p]) x))
eval proxy (ParaImpl n '[p])
_ POpts
opts x
as' = do
let msgbase0 :: String
msgbase0 = String
"Para"
msgbase1 :: String
msgbase1 = String
msgbase0 String -> ShowS
forall a. Semigroup a => a -> a -> a
<> String
"(" 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
case x
as' of
[a] -> do
TT (PP p a)
pp <- Proxy p -> POpts -> a -> m (TT (PP p a))
forall k (p :: k) a (m :: Type -> Type) (proxy :: k -> Type).
(P p a, MonadEval m) =>
proxy p -> POpts -> a -> m (TT (PP p a))
eval (Proxy p
forall k (t :: k). Proxy t
Proxy @p) POpts
opts a
a
TT [PP p a] -> m (TT [PP p a])
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (TT [PP p a] -> m (TT [PP p a])) -> TT [PP p a] -> m (TT [PP p a])
forall a b. (a -> b) -> a -> b
$ case Inline
-> POpts
-> String
-> TT (PP p a)
-> [Tree PE]
-> Either (TT [PP p a]) (PP p a)
forall a x.
Inline -> POpts -> String -> TT a -> [Tree PE] -> Either (TT x) a
getValueLR Inline
NoInline POpts
opts String
msgbase1 TT (PP p a)
pp [] of
Left TT [PP p a]
e -> TT [PP p a]
e
Right PP p a
b ->
let ret :: [PP p a]
ret = [PP p a
b]
in POpts -> Val [PP p a] -> String -> [Tree PE] -> TT [PP p a]
forall a. POpts -> Val a -> String -> [Tree PE] -> TT a
mkNode POpts
opts ([PP p a] -> Val [PP p a]
forall a. a -> Val a
Val [PP p a]
ret) (String
msgbase1 String -> ShowS
forall a. Semigroup a => a -> a -> a
<> String
" " String -> ShowS
forall a. Semigroup a => a -> a -> a
<> POpts -> [PP p a] -> String
forall a. Show a => POpts -> a -> String
showL POpts
opts [PP p a]
ret String -> ShowS
forall a. Semigroup a => a -> a -> a
<> POpts -> String -> a -> String
forall a. Show a => POpts -> String -> a -> String
showVerbose POpts
opts String
" | " a
a) [TT (PP p a) -> Tree PE
forall a. TT a -> Tree PE
hh TT (PP p a)
pp]
x
_ -> String -> m (TT [PP p a])
forall x. HasCallStack => String -> x
errorInProgram (String -> m (TT [PP p a])) -> String -> m (TT [PP p a])
forall a b. (a -> b) -> a -> b
$ String
"ParaImpl base case should have exactly one element but found " String -> ShowS
forall a. [a] -> [a] -> [a]
++ x -> String
forall a. Show a => a -> String
show x
as'
instance ( KnownNat n
, GetLen ps
, P p a
, P (ParaImpl n (p1 ': ps)) x
, PP (ParaImpl n (p1 ': ps)) x ~ [PP p a]
, Show a
, Show (PP p a)
, x ~ [a]
)
=> P (ParaImpl n (p ': p1 ': ps)) x where
type PP (ParaImpl n (p ': p1 ': ps)) x = [PP p (ExtractAFromTA x)]
eval :: proxy (ParaImpl n (p : p1 : ps))
-> POpts -> x -> m (TT (PP (ParaImpl n (p : p1 : ps)) x))
eval proxy (ParaImpl n (p : p1 : ps))
_ POpts
_ [] = String -> m (TT [PP p a])
forall x. HasCallStack => String -> x
errorInProgram String
"ParaImpl n+1 case has no data left"
eval proxy (ParaImpl n (p : p1 : 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
msgbase0 :: String
msgbase0 = String
"Para(" 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
"Para(" 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 p a)
pp <- Proxy p -> POpts -> a -> m (TT (PP p a))
forall k (p :: k) a (m :: Type -> Type) (proxy :: k -> Type).
(P p a, MonadEval m) =>
proxy p -> POpts -> a -> m (TT (PP p a))
eval (Proxy p
forall k (t :: k). Proxy t
Proxy @p) POpts
opts a
a
case Inline
-> POpts
-> String
-> TT (PP p a)
-> [Tree PE]
-> Either (TT [PP p a]) (PP p a)
forall a x.
Inline -> POpts -> String -> TT a -> [Tree PE] -> Either (TT x) a
getValueLR Inline
NoInline POpts
opts String
msgbase0 TT (PP p a)
pp [] of
Left TT [PP p a]
e -> TT [PP p a] -> m (TT [PP p a])
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure TT [PP p a]
e
Right PP p a
b -> do
TT [PP p a]
qq <- Proxy (ParaImpl n (p1 : ps))
-> POpts -> [a] -> m (TT (PP (ParaImpl n (p1 : 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 (ParaImpl n (p1 : ps))
forall k (t :: k). Proxy t
Proxy @(ParaImpl n (p1 ': ps))) POpts
opts [a]
as
TT [PP p a] -> m (TT [PP p a])
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (TT [PP p a] -> m (TT [PP p a])) -> TT [PP p a] -> m (TT [PP p a])
forall a b. (a -> b) -> a -> b
$ case Inline
-> POpts
-> String
-> TT [PP p a]
-> [Tree PE]
-> Either (TT [PP p a]) [PP p a]
forall a x.
Inline -> POpts -> String -> TT a -> [Tree PE] -> Either (TT x) a
getValueLR Inline
Inline POpts
opts String
"" TT [PP p a]
qq [TT (PP p a) -> Tree PE
forall a. TT a -> Tree PE
hh TT (PP p a)
pp] of
Left TT [PP p a]
e -> TT [PP p a]
e
Right [PP p a]
bs -> POpts -> Val [PP p a] -> String -> [Tree PE] -> TT [PP p a]
forall a. POpts -> Val a -> String -> [Tree PE] -> TT a
mkNode POpts
opts ([PP p a] -> Val [PP p a]
forall a. a -> Val a
Val (PP p a
bPP p a -> [PP p a] -> [PP p a]
forall a. a -> [a] -> [a]
:[PP p a]
bs)) (String
msgbase1 String -> ShowS
forall a. Semigroup a => a -> a -> a
<> String
" " String -> ShowS
forall a. Semigroup a => a -> a -> a
<> POpts -> [PP p a] -> String
forall a. Show a => POpts -> a -> String
showL POpts
opts (PP p a
bPP p a -> [PP p a] -> [PP p a]
forall a. a -> [a] -> [a]
:[PP p a]
bs) String -> ShowS
forall a. Semigroup a => a -> a -> a
<> POpts -> String -> [a] -> String
forall a. Show a => POpts -> String -> a -> String
showVerbose POpts
opts String
" | " (a
aa -> [a] -> [a]
forall a. a -> [a] -> [a]
:[a]
as)) [TT (PP p a) -> Tree PE
forall a. TT a -> Tree PE
hh TT (PP p a)
pp, TT [PP p a] -> Tree PE
forall a. TT a -> Tree PE
hh TT [PP p a]
qq]
data ParaN (n :: Nat) p deriving Int -> ParaN n p -> ShowS
[ParaN n p] -> ShowS
ParaN n p -> String
(Int -> ParaN n p -> ShowS)
-> (ParaN n p -> String)
-> ([ParaN n p] -> ShowS)
-> Show (ParaN n p)
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
forall (n :: Nat) k (p :: k). Int -> ParaN n p -> ShowS
forall (n :: Nat) k (p :: k). [ParaN n p] -> ShowS
forall (n :: Nat) k (p :: k). ParaN n p -> String
showList :: [ParaN n p] -> ShowS
$cshowList :: forall (n :: Nat) k (p :: k). [ParaN n p] -> ShowS
show :: ParaN n p -> String
$cshow :: forall (n :: Nat) k (p :: k). ParaN n p -> String
showsPrec :: Int -> ParaN n p -> ShowS
$cshowsPrec :: forall (n :: Nat) k (p :: k). Int -> ParaN n p -> ShowS
Show
instance ( x ~ [a]
, P (ParaImpl (LenT (RepeatT n p)) (RepeatT n p)) x
, GetLen (RepeatT n p)
) => P (ParaN n p) x where
type PP (ParaN n p) x = PP (Para (RepeatT n p)) x
eval :: proxy (ParaN n p) -> POpts -> x -> m (TT (PP (ParaN n p) x))
eval proxy (ParaN n p)
_ = Proxy (Para (RepeatT n p))
-> POpts -> x -> m (TT (PP (Para (RepeatT 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 (Para (RepeatT n p))
forall k (t :: k). Proxy t
Proxy @(Para (RepeatT n p)))
data Repeat (n :: Nat) p deriving Int -> Repeat n p -> ShowS
[Repeat n p] -> ShowS
Repeat n p -> String
(Int -> Repeat n p -> ShowS)
-> (Repeat n p -> String)
-> ([Repeat n p] -> ShowS)
-> Show (Repeat n p)
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
forall (n :: Nat) k (p :: k). Int -> Repeat n p -> ShowS
forall (n :: Nat) k (p :: k). [Repeat n p] -> ShowS
forall (n :: Nat) k (p :: k). Repeat n p -> String
showList :: [Repeat n p] -> ShowS
$cshowList :: forall (n :: Nat) k (p :: k). [Repeat n p] -> ShowS
show :: Repeat n p -> String
$cshow :: forall (n :: Nat) k (p :: k). Repeat n p -> String
showsPrec :: Int -> Repeat n p -> ShowS
$cshowsPrec :: forall (n :: Nat) k (p :: k). Int -> Repeat n p -> ShowS
Show
instance P (RepeatT n p) a => P (Repeat n p) a where
type PP (Repeat n p) a = PP (RepeatT n p) a
eval :: proxy (Repeat n p) -> POpts -> a -> m (TT (PP (Repeat n p) a))
eval proxy (Repeat n p)
_ = Proxy (RepeatT n p) -> POpts -> a -> m (TT (PP (RepeatT n p) a))
forall k (p :: k) a (m :: Type -> Type) (proxy :: k -> Type).
(P p a, MonadEval m) =>
proxy p -> POpts -> a -> m (TT (PP p a))
eval (Proxy (RepeatT n p)
forall k (t :: k). Proxy t
Proxy @(RepeatT n p))
data DoN (n :: Nat) p deriving Int -> DoN n p -> ShowS
[DoN n p] -> ShowS
DoN n p -> String
(Int -> DoN n p -> ShowS)
-> (DoN n p -> String) -> ([DoN n p] -> ShowS) -> Show (DoN n p)
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
forall (n :: Nat) k (p :: k). Int -> DoN n p -> ShowS
forall (n :: Nat) k (p :: k). [DoN n p] -> ShowS
forall (n :: Nat) k (p :: k). DoN n p -> String
showList :: [DoN n p] -> ShowS
$cshowList :: forall (n :: Nat) k (p :: k). [DoN n p] -> ShowS
show :: DoN n p -> String
$cshow :: forall (n :: Nat) k (p :: k). DoN n p -> String
showsPrec :: Int -> DoN n p -> ShowS
$cshowsPrec :: forall (n :: Nat) k (p :: k). Int -> DoN n p -> ShowS
Show
type DoNT (n :: Nat) p = Do (RepeatT n p)
instance P (DoNT n p) a => P (DoN n p) a where
type PP (DoN n p) a = PP (DoNT n p) a
eval :: proxy (DoN n p) -> POpts -> a -> m (TT (PP (DoN n p) a))
eval proxy (DoN n p)
_ = Proxy (DoNT n p) -> POpts -> a -> m (TT (PP (DoNT n p) a))
forall k (p :: k) a (m :: Type -> Type) (proxy :: k -> Type).
(P p a, MonadEval m) =>
proxy p -> POpts -> a -> m (TT (PP p a))
eval (Proxy (DoNT n p)
forall k (t :: k). Proxy t
Proxy @(DoNT n p))