{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE DerivingStrategies #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE StandaloneKindSignatures #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilyDependencies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
module Cybus.NatHelper (
NatToPeanoT,
PeanoToNatT,
Peano (..),
DiffT,
DiffTC,
FacT,
type (<=!),
type (<!),
LTEQT,
D1,
D2,
D3,
D4,
D5,
D6,
D7,
D8,
D9,
D10,
ProductT,
NN,
NN',
ReverseT,
ListTupleT,
ValidateNestedListC (..),
ValidateNestedNonEmptyC (..),
validateNestedList,
validateNestedNonEmpty,
ValidateNestedListT,
ValidateNestedNonEmptyT,
nestedNonEmptyToList,
nestedListToNonEmpty,
NestedListC (..),
NonEmptyNST,
ListNST,
) where
import Data.Kind
import Data.List.NonEmpty (NonEmpty (..))
import qualified Data.List.NonEmpty as N
import Data.Pos
import Data.Proxy
import qualified GHC.TypeLits as GL
import GHC.TypeNats (Nat,KnownNat)
import qualified GHC.TypeNats as GN
import Primus.Error
import Primus.Fold
import Primus.List
import Primus.NonEmpty
import Primus.One
import Primus.TypeLevel (FailUnless)
type FacT :: Nat -> Nat
type family FacT x where
FacT 0 = 1
FacT 1 = 1
FacT n = n GN.* FacT (n GN.- 1)
type (<=!) :: Nat -> Nat -> Constraint
type i <=! n =
( FailUnless
(i GN.<=? n)
( 'GL.Text "i>n"
'GL.:<>: 'GL.Text ": i="
'GL.:<>: 'GL.ShowType i
'GL.:<>: 'GL.Text " n="
'GL.:<>: 'GL.ShowType n
)
, PosC i
)
type LTEQT :: GL.ErrorMessage -> Nat -> Nat -> Constraint
type LTEQT msg i n =
( FailUnless
(i GN.<=? n)
( 'GL.Text "i>n"
'GL.:<>: 'GL.Text ": i="
'GL.:<>: 'GL.ShowType i
'GL.:<>: 'GL.Text " n="
'GL.:<>: 'GL.ShowType n
'GL.:<>: msg
)
, PosC i
)
type (<!) :: Nat -> Nat -> Constraint
type i <! n =
( FailUnless
(i GN.+ 1 GN.<=? n)
( 'GL.Text "i>=n"
'GL.:<>: 'GL.Text ": i="
'GL.:<>: 'GL.ShowType i
'GL.:<>: 'GL.Text " n="
'GL.:<>: 'GL.ShowType n
)
, KnownNat i
)
type LTEQC :: Nat -> Nat -> Constraint
class (KnownNat i, KnownNat n) => LTEQC i n where
instance
( KnownNat i
, KnownNat n
, FailUnless
(i GL.<=? n)
( 'GL.Text "LTEQC n: requires n >= i but found i="
'GL.:<>: 'GL.ShowType i
'GL.:<>: 'GL.Text " n="
'GL.:<>: 'GL.ShowType n
)
) =>
LTEQC i n
type DiffTC :: Nat -> Nat -> Nat -> Constraint
type DiffTC i j n = (i <=! j, j <=! n)
type DiffT :: Nat -> Nat -> Nat -> Nat
type DiffT i j n = j GN.+ 1 GN.- i
type ReverseT :: forall k. [k] -> [k]
type family ReverseT ns where
ReverseT (n ': ns) = ReverseT' (n ': ns) '[]
type ReverseT' :: forall k. [k] -> [k] -> [k]
type family ReverseT' ns ret where
ReverseT' '[] (r ': rs) = r ': rs
ReverseT' (n ': ns) ret = ReverseT' ns (n ': ret)
type ProductT :: [Nat] -> Nat
type family ProductT ns where
ProductT '[] = GL.TypeError ( 'GL.Text "ProductT: empty indices")
ProductT '[n] = n
ProductT (n ': n1 ': ns) = n GN.* ProductT (n1 ': ns)
type ValidateNestedListT :: Type -> Peano
type family ValidateNestedListT x where
ValidateNestedListT [x] = 'S (ValidateNestedListT x)
ValidateNestedListT _ = 'S 'Z
type ValidateNestedNonEmptyT :: Type -> Peano
type family ValidateNestedNonEmptyT x where
ValidateNestedNonEmptyT (NonEmpty x) = 'S (ValidateNestedNonEmptyT x)
ValidateNestedNonEmptyT _ = 'S 'Z
validateNestedNonEmpty :: forall x. ValidateNestedNonEmptyC x (ValidateNestedNonEmptyT x) => x -> Either String (NonEmpty Pos)
validateNestedNonEmpty :: x -> Either String (NonEmpty Pos)
validateNestedNonEmpty x
x = [Pos] -> x -> [x] -> Either String (NonEmpty Pos)
forall x (y :: Peano).
ValidateNestedNonEmptyC x y =>
[Pos] -> x -> [x] -> Either String (NonEmpty Pos)
validateNestedNonEmptyC @x @(ValidateNestedNonEmptyT x) [] x
x []
validateNestedList :: forall x. ValidateNestedListC x (ValidateNestedListT x) => x -> Either String (NonEmpty Pos)
validateNestedList :: x -> Either String (NonEmpty Pos)
validateNestedList x
x = [Pos] -> x -> [x] -> Either String (NonEmpty Pos)
forall x (y :: Peano).
ValidateNestedListC x y =>
[Pos] -> x -> [x] -> Either String (NonEmpty Pos)
validateNestedListC @x @(ValidateNestedListT x) [] x
x []
type ValidateNestedNonEmptyC :: Type -> Peano -> Constraint
class ValidateNestedNonEmptyC x y where
validateNestedNonEmptyC :: [Pos] -> x -> [x] -> Either String (NonEmpty Pos)
instance GL.TypeError ( 'GL.Text "ValidateNestedNonEmptyC: not defined at 'Z") => ValidateNestedNonEmptyC x 'Z where
validateNestedNonEmptyC :: [Pos] -> x -> [x] -> Either String (NonEmpty Pos)
validateNestedNonEmptyC = String -> [Pos] -> x -> [x] -> Either String (NonEmpty Pos)
forall a. HasCallStack => String -> a
compileError String
"validateNestedNonEmptyC: ValidateNestedNonEmptyC x 'Z"
instance ValidateNestedNonEmptyC x ( 'S 'Z) where
validateNestedNonEmptyC :: [Pos] -> x -> [x] -> Either String (NonEmpty Pos)
validateNestedNonEmptyC [Pos]
ixes x
_ [x]
_ =
case [Pos]
ixes of
Pos
i : [Pos]
is -> NonEmpty Pos -> Either String (NonEmpty Pos)
forall a b. b -> Either a b
Right (Pos
i Pos -> [Pos] -> NonEmpty Pos
forall a. a -> [a] -> NonEmpty a
:| [Pos]
is)
[] -> String -> Either String (NonEmpty Pos)
forall a. HasCallStack => String -> a
programmError String
"ValidateNestedNonEmptyC: ('S 'Z): empty list of indices"
instance ValidateNestedNonEmptyC x ( 'S zs) => ValidateNestedNonEmptyC (NonEmpty x) ( 'S ( 'S zs)) where
validateNestedNonEmptyC :: [Pos] -> NonEmpty x -> [NonEmpty x] -> Either String (NonEmpty Pos)
validateNestedNonEmptyC [Pos]
ixes x :: NonEmpty x
x@(x
n :| [x]
ns) [NonEmpty x]
xs =
let cs :: [Maybe Ordering]
cs = (CLCount x -> Maybe Ordering) -> [CLCount x] -> [Maybe Ordering]
forall a b. (a -> b) -> [a] -> [b]
map CLCount x -> Maybe Ordering
forall b. CLCount b -> Maybe Ordering
clOrdering ([CLCount x] -> [Maybe Ordering])
-> [CLCount x] -> [Maybe Ordering]
forall a b. (a -> b) -> a -> b
$ NonEmpty x -> [NonEmpty x] -> [CLCount x]
forall a b (t :: * -> *) (u :: * -> *).
(Foldable t, Foldable u) =>
t a -> [u b] -> [CLCount b]
compareLengths NonEmpty x
x [NonEmpty x]
xs
in if (Maybe Ordering -> Bool) -> [Maybe Ordering] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (Ordering -> Maybe Ordering
forall a. a -> Maybe a
Just Ordering
EQ Maybe Ordering -> Maybe Ordering -> Bool
forall a. Eq a => a -> a -> Bool
==) [Maybe Ordering]
cs
then
let zs :: [x]
zs = [x]
ns [x] -> [x] -> [x]
forall a. Semigroup a => a -> a -> a
<> (NonEmpty x -> [x]) -> [NonEmpty x] -> [x]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap NonEmpty x -> [x]
forall a. NonEmpty a -> [a]
N.toList [NonEmpty x]
xs
in [Pos] -> x -> [x] -> Either String (NonEmpty Pos)
forall x (y :: Peano).
ValidateNestedNonEmptyC x y =>
[Pos] -> x -> [x] -> Either String (NonEmpty Pos)
validateNestedNonEmptyC @x @( 'S zs) ([Pos]
ixes [Pos] -> Pos -> [Pos]
forall a. [a] -> a -> [a]
`snocL` NonEmpty x -> Pos
forall (t :: * -> *) a. Foldable1 t => t a -> Pos
lengthP NonEmpty x
x) x
n [x]
zs
else String -> Either String (NonEmpty Pos)
forall a b. a -> Either a b
Left (String -> Either String (NonEmpty Pos))
-> String -> Either String (NonEmpty Pos)
forall a b. (a -> b) -> a -> b
$ String
"validateNestedNonEmptyC: lengths=" String -> String -> String
forall a. [a] -> [a] -> [a]
++ [Int] -> String
forall a. Show a => a -> String
show ((NonEmpty x -> Int) -> [NonEmpty x] -> [Int]
forall a b. (a -> b) -> [a] -> [b]
map NonEmpty x -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length (NonEmpty x
x NonEmpty x -> [NonEmpty x] -> [NonEmpty x]
forall a. a -> [a] -> [a]
: [NonEmpty x]
xs)) String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" ixes=" String -> String -> String
forall a. [a] -> [a] -> [a]
++ [Int] -> String
forall a. Show a => a -> String
show ((Pos -> Int) -> [Pos] -> [Int]
forall a b. (a -> b) -> [a] -> [b]
map Pos -> Int
unP [Pos]
ixes)
type ValidateNestedListC :: Type -> Peano -> Constraint
class ValidateNestedListC x y where
validateNestedListC :: [Pos] -> x -> [x] -> Either String (NonEmpty Pos)
instance GL.TypeError ( 'GL.Text "ValidateNestedListC: not defined at 0") => ValidateNestedListC x 'Z where
validateNestedListC :: [Pos] -> x -> [x] -> Either String (NonEmpty Pos)
validateNestedListC = String -> [Pos] -> x -> [x] -> Either String (NonEmpty Pos)
forall a. HasCallStack => String -> a
compileError String
"validateNestedListC: ValidateNestedListC x 'Z"
instance ValidateNestedListC x ( 'S 'Z) where
validateNestedListC :: [Pos] -> x -> [x] -> Either String (NonEmpty Pos)
validateNestedListC [Pos]
ixes x
_ [x]
_ =
case [Pos]
ixes of
Pos
i : [Pos]
is -> NonEmpty Pos -> Either String (NonEmpty Pos)
forall a b. b -> Either a b
Right (Pos
i Pos -> [Pos] -> NonEmpty Pos
forall a. a -> [a] -> NonEmpty a
:| [Pos]
is)
[] -> String -> Either String (NonEmpty Pos)
forall a. HasCallStack => String -> a
programmError String
"ValidateNestedListC: ('S 'Z): empty list of indices"
instance ValidateNestedListC x ( 'S n) => ValidateNestedListC [x] ( 'S ( 'S n)) where
validateNestedListC :: [Pos] -> [x] -> [[x]] -> Either String (NonEmpty Pos)
validateNestedListC [Pos]
ixes [] [[x]]
_ = String -> Either String (NonEmpty Pos)
forall a b. a -> Either a b
Left (String -> Either String (NonEmpty Pos))
-> String -> Either String (NonEmpty Pos)
forall a b. (a -> b) -> a -> b
$ String
"validateNestedListC: ixes=" String -> String -> String
forall a. [a] -> [a] -> [a]
++ [Pos] -> String
forall a. Show a => a -> String
show [Pos]
ixes String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
":no data!"
validateNestedListC [Pos]
ixes x :: [x]
x@(x
n : [x]
ns) [[x]]
xs =
let cs :: [Maybe Ordering]
cs = (CLCount x -> Maybe Ordering) -> [CLCount x] -> [Maybe Ordering]
forall a b. (a -> b) -> [a] -> [b]
map CLCount x -> Maybe Ordering
forall b. CLCount b -> Maybe Ordering
clOrdering ([CLCount x] -> [Maybe Ordering])
-> [CLCount x] -> [Maybe Ordering]
forall a b. (a -> b) -> a -> b
$ [x] -> [[x]] -> [CLCount x]
forall a b (t :: * -> *) (u :: * -> *).
(Foldable t, Foldable u) =>
t a -> [u b] -> [CLCount b]
compareLengths [x]
x [[x]]
xs
in if (Maybe Ordering -> Bool) -> [Maybe Ordering] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (Ordering -> Maybe Ordering
forall a. a -> Maybe a
Just Ordering
EQ Maybe Ordering -> Maybe Ordering -> Bool
forall a. Eq a => a -> a -> Bool
==) [Maybe Ordering]
cs
then
let zs :: [x]
zs = [x]
ns [x] -> [x] -> [x]
forall a. Semigroup a => a -> a -> a
<> [[x]] -> [x]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [[x]]
xs
in [Pos] -> x -> [x] -> Either String (NonEmpty Pos)
forall x (y :: Peano).
ValidateNestedListC x y =>
[Pos] -> x -> [x] -> Either String (NonEmpty Pos)
validateNestedListC @x @( 'S n) ([Pos]
ixes [Pos] -> Pos -> [Pos]
forall a. [a] -> a -> [a]
`snocL` NonEmpty x -> Pos
forall (t :: * -> *) a. Foldable1 t => t a -> Pos
lengthP (x
n x -> [x] -> NonEmpty x
forall a. a -> [a] -> NonEmpty a
:| [x]
ns)) x
n [x]
zs
else String -> Either String (NonEmpty Pos)
forall a b. a -> Either a b
Left (String -> Either String (NonEmpty Pos))
-> String -> Either String (NonEmpty Pos)
forall a b. (a -> b) -> a -> b
$ String
"validateNestedListC: lengths=" String -> String -> String
forall a. [a] -> [a] -> [a]
++ [Int] -> String
forall a. Show a => a -> String
show (([x] -> Int) -> [[x]] -> [Int]
forall a b. (a -> b) -> [a] -> [b]
map [x] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length ([x]
x [x] -> [[x]] -> [[x]]
forall a. a -> [a] -> [a]
: [[x]]
xs)) String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" ixes=" String -> String -> String
forall a. [a] -> [a] -> [a]
++ [Pos] -> String
forall a. Show a => a -> String
show [Pos]
ixes
data Peano = Z | S !Peano deriving stock (Eq Peano
Eq Peano
-> (Peano -> Peano -> Ordering)
-> (Peano -> Peano -> Bool)
-> (Peano -> Peano -> Bool)
-> (Peano -> Peano -> Bool)
-> (Peano -> Peano -> Bool)
-> (Peano -> Peano -> Peano)
-> (Peano -> Peano -> Peano)
-> Ord Peano
Peano -> Peano -> Bool
Peano -> Peano -> Ordering
Peano -> Peano -> Peano
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
min :: Peano -> Peano -> Peano
$cmin :: Peano -> Peano -> Peano
max :: Peano -> Peano -> Peano
$cmax :: Peano -> Peano -> Peano
>= :: Peano -> Peano -> Bool
$c>= :: Peano -> Peano -> Bool
> :: Peano -> Peano -> Bool
$c> :: Peano -> Peano -> Bool
<= :: Peano -> Peano -> Bool
$c<= :: Peano -> Peano -> Bool
< :: Peano -> Peano -> Bool
$c< :: Peano -> Peano -> Bool
compare :: Peano -> Peano -> Ordering
$ccompare :: Peano -> Peano -> Ordering
$cp1Ord :: Eq Peano
Ord, Int -> Peano -> String -> String
[Peano] -> String -> String
Peano -> String
(Int -> Peano -> String -> String)
-> (Peano -> String) -> ([Peano] -> String -> String) -> Show Peano
forall a.
(Int -> a -> String -> String)
-> (a -> String) -> ([a] -> String -> String) -> Show a
showList :: [Peano] -> String -> String
$cshowList :: [Peano] -> String -> String
show :: Peano -> String
$cshow :: Peano -> String
showsPrec :: Int -> Peano -> String -> String
$cshowsPrec :: Int -> Peano -> String -> String
Show, Peano -> Peano -> Bool
(Peano -> Peano -> Bool) -> (Peano -> Peano -> Bool) -> Eq Peano
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Peano -> Peano -> Bool
$c/= :: Peano -> Peano -> Bool
== :: Peano -> Peano -> Bool
$c== :: Peano -> Peano -> Bool
Eq)
type NatToPeanoT :: Nat -> Peano
type family NatToPeanoT n where
NatToPeanoT 0 = 'Z
NatToPeanoT n = 'S (NatToPeanoT (n GN.- 1))
type PeanoToNatT :: Peano -> Nat
type family PeanoToNatT n where
PeanoToNatT 'Z = 0
PeanoToNatT ( 'S n) = 1 GN.+ PeanoToNatT n
type ListNST :: [Nat] -> Type -> Type
type family ListNST ns a where
ListNST '[] _ = GL.TypeError ( 'GL.Text "ListNST: empty indices")
ListNST '[_] a = [a]
ListNST (_ ': n1 ': ns) a = [ListNST (n1 ': ns) a]
type NonEmptyNST :: [Nat] -> Type -> Type
type family NonEmptyNST ns a where
NonEmptyNST '[] _ = GL.TypeError ( 'GL.Text "NonEmptyNST: empty indices")
NonEmptyNST '[_] a = NonEmpty a
NonEmptyNST (_ ': n1 ': ns) a = NonEmpty (NonEmptyNST (n1 ': ns) a)
nestedNonEmptyToList :: forall ns a. NestedListC ns => NonEmptyNST ns a -> Either String (ListNST ns a)
nestedNonEmptyToList :: NonEmptyNST ns a -> Either String (ListNST ns a)
nestedNonEmptyToList = Proxy a -> NonEmptyNST ns a -> Either String (ListNST ns a)
forall (ns :: [Nat]) (proxy :: * -> *) a.
NestedListC ns =>
proxy a -> NonEmptyNST ns a -> Either String (ListNST ns a)
nestedNonEmptyToListC @ns (Proxy a
forall k (t :: k). Proxy t
Proxy @a)
nestedListToNonEmpty :: forall ns a. NestedListC ns => ListNST ns a -> Either String (NonEmptyNST ns a)
nestedListToNonEmpty :: ListNST ns a -> Either String (NonEmptyNST ns a)
nestedListToNonEmpty = Proxy a -> ListNST ns a -> Either String (NonEmptyNST ns a)
forall (ns :: [Nat]) (proxy :: * -> *) a.
NestedListC ns =>
proxy a -> ListNST ns a -> Either String (NonEmptyNST ns a)
nestedListToNonEmptyC @ns @_ @a Proxy a
forall k (t :: k). Proxy t
Proxy
type NestedListC :: [Nat] -> Constraint
class NestedListC ns where
nestedListToNonEmptyC :: proxy a -> ListNST ns a -> Either String (NonEmptyNST ns a)
nestedNonEmptyToListC :: proxy a -> NonEmptyNST ns a -> Either String (ListNST ns a)
flattenNestedListC :: proxy a -> ListNST ns a -> Either String [a]
instance GL.TypeError ( 'GL.Text "NestedListC '[]: empty indices") => NestedListC '[] where
nestedListToNonEmptyC :: proxy a -> ListNST '[] a -> Either String (NonEmptyNST '[] a)
nestedListToNonEmptyC = String
-> proxy a -> (TypeError ...) -> Either String (TypeError ...)
forall a. HasCallStack => String -> a
compileError String
"NestedListC '[]:nestedListToNonEmptyC"
nestedNonEmptyToListC :: proxy a -> NonEmptyNST '[] a -> Either String (ListNST '[] a)
nestedNonEmptyToListC = String
-> proxy a -> (TypeError ...) -> Either String (TypeError ...)
forall a. HasCallStack => String -> a
compileError String
"NestedListC '[]:nestedNonEmptyToListC"
flattenNestedListC :: proxy a -> ListNST '[] a -> Either String [a]
flattenNestedListC = String -> proxy a -> (TypeError ...) -> Either String [a]
forall a. HasCallStack => String -> a
compileError String
"NestedListC '[]:flattenNestedListC"
instance PosC n => NestedListC '[n] where
nestedListToNonEmptyC :: proxy a -> ListNST '[n] a -> Either String (NonEmptyNST '[n] a)
nestedListToNonEmptyC proxy a
_ = \case
[] -> String -> Either String (NonEmpty a)
forall a b. a -> Either a b
Left String
"nestedListToNonEmptyC 'SZ no data"
x : xs -> String -> Either String (NonEmpty a) -> Either String (NonEmpty a)
forall a. String -> Either String a -> Either String a
lmsg String
"nestedListToNonEmptyC 'SZ" (Either String (NonEmpty a) -> Either String (NonEmpty a))
-> Either String (NonEmpty a) -> Either String (NonEmpty a)
forall a b. (a -> b) -> a -> b
$ Pos -> NonEmpty a -> Either String (NonEmpty a)
forall a. Pos -> NonEmpty a -> Either String (NonEmpty a)
lengthExact1 (PosC n => Pos
forall (n :: Nat). PosC n => Pos
fromNP @n) (a
x a -> [a] -> NonEmpty a
forall a. a -> [a] -> NonEmpty a
:| [a]
xs)
nestedNonEmptyToListC :: proxy a -> NonEmptyNST '[n] a -> Either String (ListNST '[n] a)
nestedNonEmptyToListC proxy a
_ NonEmptyNST '[n] a
lst = NonEmpty a -> [a]
forall a. NonEmpty a -> [a]
N.toList (NonEmpty a -> [a])
-> Either String (NonEmpty a) -> Either String [a]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> String -> Either String (NonEmpty a) -> Either String (NonEmpty a)
forall a. String -> Either String a -> Either String a
lmsg String
"nestedNonEmptyToListC 'SZ" (Pos -> NonEmpty a -> Either String (NonEmpty a)
forall a. Pos -> NonEmpty a -> Either String (NonEmpty a)
lengthExact1 (PosC n => Pos
forall (n :: Nat). PosC n => Pos
fromNP @n) NonEmpty a
NonEmptyNST '[n] a
lst)
flattenNestedListC :: proxy a -> ListNST '[n] a -> Either String [a]
flattenNestedListC proxy a
_ = \case
[] -> String -> Either String [a]
forall a b. a -> Either a b
Left String
"flattenNestedListC 'SZ no data"
x : xs -> String -> Either String [a] -> Either String [a]
forall a. String -> Either String a -> Either String a
lmsg String
"flattenNestedListC 'SZ" (Either String [a] -> Either String [a])
-> Either String [a] -> Either String [a]
forall a b. (a -> b) -> a -> b
$ Int -> [a] -> Either String [a]
forall a. Int -> [a] -> Either String [a]
lengthExact (PosC n => Int
forall (n :: Nat). PosC n => Int
fromN @n) (a
x a -> [a] -> [a]
forall a. a -> [a] -> [a]
: [a]
xs)
instance (PosC n, NestedListC (n1 ': ns)) => NestedListC (n ': n1 ': ns) where
nestedListToNonEmptyC :: proxy a
-> ListNST (n : n1 : ns) a
-> Either String (NonEmptyNST (n : n1 : ns) a)
nestedListToNonEmptyC proxy a
p = \case
[] -> String -> Either String (NonEmpty (NonEmptyNST (n1 : ns) a))
forall a b. a -> Either a b
Left String
"nestedListToNonEmptyC 'SS no data"
x : xs -> do
NonEmpty (ListNST (n1 : ns) a)
ys <- String
-> Either String (NonEmpty (ListNST (n1 : ns) a))
-> Either String (NonEmpty (ListNST (n1 : ns) a))
forall a. String -> Either String a -> Either String a
lmsg String
"nestedListToNonEmptyC 'SS" (Either String (NonEmpty (ListNST (n1 : ns) a))
-> Either String (NonEmpty (ListNST (n1 : ns) a)))
-> Either String (NonEmpty (ListNST (n1 : ns) a))
-> Either String (NonEmpty (ListNST (n1 : ns) a))
forall a b. (a -> b) -> a -> b
$ Pos
-> NonEmpty (ListNST (n1 : ns) a)
-> Either String (NonEmpty (ListNST (n1 : ns) a))
forall a. Pos -> NonEmpty a -> Either String (NonEmpty a)
lengthExact1 (PosC n => Pos
forall (n :: Nat). PosC n => Pos
fromNP @n) (ListNST (n1 : ns) a
x ListNST (n1 : ns) a
-> [ListNST (n1 : ns) a] -> NonEmpty (ListNST (n1 : ns) a)
forall a. a -> [a] -> NonEmpty a
:| [ListNST (n1 : ns) a]
xs)
(ListNST (n1 : ns) a -> Either String (NonEmptyNST (n1 : ns) a))
-> NonEmpty (ListNST (n1 : ns) a)
-> Either String (NonEmpty (NonEmptyNST (n1 : ns) a))
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse (proxy a
-> ListNST (n1 : ns) a -> Either String (NonEmptyNST (n1 : ns) a)
forall (ns :: [Nat]) (proxy :: * -> *) a.
NestedListC ns =>
proxy a -> ListNST ns a -> Either String (NonEmptyNST ns a)
nestedListToNonEmptyC @(n1 ': ns) proxy a
p) NonEmpty (ListNST (n1 : ns) a)
ys
nestedNonEmptyToListC :: proxy a
-> NonEmptyNST (n : n1 : ns) a
-> Either String (ListNST (n : n1 : ns) a)
nestedNonEmptyToListC proxy a
p NonEmptyNST (n : n1 : ns) a
lst = do
NonEmpty (NonEmptyNST (n1 : ns) a)
xs <- String
-> Either String (NonEmpty (NonEmptyNST (n1 : ns) a))
-> Either String (NonEmpty (NonEmptyNST (n1 : ns) a))
forall a. String -> Either String a -> Either String a
lmsg String
"nestedNonEmptyToListC 'SS" (Either String (NonEmpty (NonEmptyNST (n1 : ns) a))
-> Either String (NonEmpty (NonEmptyNST (n1 : ns) a)))
-> Either String (NonEmpty (NonEmptyNST (n1 : ns) a))
-> Either String (NonEmpty (NonEmptyNST (n1 : ns) a))
forall a b. (a -> b) -> a -> b
$ Pos
-> NonEmpty (NonEmptyNST (n1 : ns) a)
-> Either String (NonEmpty (NonEmptyNST (n1 : ns) a))
forall a. Pos -> NonEmpty a -> Either String (NonEmpty a)
lengthExact1 (PosC n => Pos
forall (n :: Nat). PosC n => Pos
fromNP @n) NonEmpty (NonEmptyNST (n1 : ns) a)
NonEmptyNST (n : n1 : ns) a
lst
NonEmpty (ListNST (n1 : ns) a) -> [ListNST (n1 : ns) a]
forall a. NonEmpty a -> [a]
N.toList (NonEmpty (ListNST (n1 : ns) a) -> [ListNST (n1 : ns) a])
-> Either String (NonEmpty (ListNST (n1 : ns) a))
-> Either String [ListNST (n1 : ns) a]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (NonEmptyNST (n1 : ns) a -> Either String (ListNST (n1 : ns) a))
-> NonEmpty (NonEmptyNST (n1 : ns) a)
-> Either String (NonEmpty (ListNST (n1 : ns) a))
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse (proxy a
-> NonEmptyNST (n1 : ns) a -> Either String (ListNST (n1 : ns) a)
forall (ns :: [Nat]) (proxy :: * -> *) a.
NestedListC ns =>
proxy a -> NonEmptyNST ns a -> Either String (ListNST ns a)
nestedNonEmptyToListC @(n1 ': ns) proxy a
p) NonEmpty (NonEmptyNST (n1 : ns) a)
xs
flattenNestedListC :: proxy a -> ListNST (n : n1 : ns) a -> Either String [a]
flattenNestedListC proxy a
p = \case
[] -> String -> Either String [a]
forall a b. a -> Either a b
Left String
"flattenNestedListC 'SS no data"
x : xs -> do
[ListNST (n1 : ns) a]
ys <- String
-> Either String [ListNST (n1 : ns) a]
-> Either String [ListNST (n1 : ns) a]
forall a. String -> Either String a -> Either String a
lmsg String
"flattenNestedListC 'SS" (Either String [ListNST (n1 : ns) a]
-> Either String [ListNST (n1 : ns) a])
-> Either String [ListNST (n1 : ns) a]
-> Either String [ListNST (n1 : ns) a]
forall a b. (a -> b) -> a -> b
$ Int -> [ListNST (n1 : ns) a] -> Either String [ListNST (n1 : ns) a]
forall a. Int -> [a] -> Either String [a]
lengthExact (PosC n => Int
forall (n :: Nat). PosC n => Int
fromN @n) (ListNST (n1 : ns) a
x ListNST (n1 : ns) a
-> [ListNST (n1 : ns) a] -> [ListNST (n1 : ns) a]
forall a. a -> [a] -> [a]
: [ListNST (n1 : ns) a]
xs)
[[a]] -> [a]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat ([[a]] -> [a]) -> Either String [[a]] -> Either String [a]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (ListNST (n1 : ns) a -> Either String [a])
-> [ListNST (n1 : ns) a] -> Either String [[a]]
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse (proxy a -> ListNST (n1 : ns) a -> Either String [a]
forall (ns :: [Nat]) (proxy :: * -> *) a.
NestedListC ns =>
proxy a -> ListNST ns a -> Either String [a]
flattenNestedListC @(n1 ': ns) proxy a
p) [ListNST (n1 : ns) a]
ys
type ListTupleT :: Nat -> Type -> Type
type family ListTupleT n a = result | result -> n a where
ListTupleT 1 a = One a
ListTupleT 2 a = (a, a)
ListTupleT 3 a = (a, a, a)
ListTupleT 4 a = (a, a, a, a)
ListTupleT 5 a = (a, a, a, a, a)
ListTupleT 6 a = (a, a, a, a, a, a)
ListTupleT 7 a = (a, a, a, a, a, a, a)
ListTupleT 8 a = (a, a, a, a, a, a, a, a)
ListTupleT 9 a = (a, a, a, a, a, a, a, a, a)
ListTupleT 10 a = (a, a, a, a, a, a, a, a, a, a)
ListTupleT 11 a = (a, a, a, a, a, a, a, a, a, a, a)
ListTupleT 12 a = (a, a, a, a, a, a, a, a, a, a, a, a)
ListTupleT 13 a = (a, a, a, a, a, a, a, a, a, a, a, a, a)
ListTupleT 14 a = (a, a, a, a, a, a, a, a, a, a, a, a, a, a)
ListTupleT 15 a = (a, a, a, a, a, a, a, a, a, a, a, a, a, a, a)
ListTupleT 16 a = (a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a)
ListTupleT 17 a = (a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a)
ListTupleT 18 a = (a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a)
ListTupleT 19 a = (a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a)
ListTupleT 20 a = (a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a)
type NN :: Nat -> [Nat]
type NN n = NN' '[] n
type NN' :: [Nat] -> Nat -> [Nat]
type family NN' ns n where
NN' ns 0 = ns
NN' ns n = NN' (GN.Mod n 10 ': ns) (GN.Div n 10)
type D1 :: Nat -> [Nat]
type D1 a = '[a]
type D2 :: Nat -> Nat -> [Nat]
type D2 a b = '[a, b]
type D3 :: Nat -> Nat -> Nat -> [Nat]
type D3 a b c = '[a, b, c]
type D4 :: Nat -> Nat -> Nat -> Nat -> [Nat]
type D4 a b c d = '[a, b, c, d]
type D5 :: Nat -> Nat -> Nat -> Nat -> Nat -> [Nat]
type D5 a b c d e = '[a, b, c, d, e]
type D6 :: Nat -> Nat -> Nat -> Nat -> Nat -> Nat -> [Nat]
type D6 a b c d e f = '[a, b, c, d, e, f]
type D7 :: Nat -> Nat -> Nat -> Nat -> Nat -> Nat -> Nat -> [Nat]
type D7 a b c d e f g = '[a, b, c, d, e, f, g]
type D8 :: Nat -> Nat -> Nat -> Nat -> Nat -> Nat -> Nat -> Nat -> [Nat]
type D8 a b c d e f g h = '[a, b, c, d, e, f, g, h]
type D9 :: Nat -> Nat -> Nat -> Nat -> Nat -> Nat -> Nat -> Nat -> Nat -> [Nat]
type D9 a b c d e f g h i = '[a, b, c, d, e, f, g, h, i]
type D10 :: Nat -> Nat -> Nat -> Nat -> Nat -> Nat -> Nat -> Nat -> Nat -> Nat -> [Nat]
type D10 a b c d e f g h i j = '[a, b, c, d, e, f, g, h, i, j]