{-# 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
) 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)
import qualified GHC.TypeLits as GL
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]) [a]
forall (t :: Type -> Type) a x.
Foldable t =>
POpts -> String -> t a -> [Tree PE] -> Either (TT x) [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 [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 -> HKD Identity Int
forall (f :: Type -> Type). HOpts f -> HKD f Int
oRecursion 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 [Tree PE] -> [Tree PE] -> [Tree PE]
forall a. [a] -> [a] -> [a]
++ [TT [b] -> Tree PE
forall a. TT a -> Tree PE
hh TT [b]
e])
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 -> HKD Identity Int
forall (f :: Type -> Type). HOpts f -> HKD f Int
oRecursion 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 [Tree PE] -> [Tree PE] -> [Tree PE]
forall a. [a] -> [a] -> [a]
++ [TT [b] -> Tree PE
forall a. TT a -> Tree PE
hh TT [b]
e])
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 where
UnfoldrT (Maybe (b, _s)) = b
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
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 (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
"" []
else Proxy (ParaImpl (LenT ps) ps)
-> POpts -> x -> m (TT (PP (ParaImpl (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 (ParaImpl (LenT ps) ps)
forall k (t :: k). Proxy t
Proxy @(ParaImpl (LenT ps) ps)) POpts
opts x
as
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))