{-# 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
Description : Nat helper methods
Copyright   : (c) Grant Weyburne, 2022
License     : BSD-3
-}
module Cybus.NatHelper (
  -- * peano
  NatToPeanoT,
  PeanoToNatT,
  Peano (..),

  -- * arithmetic
  DiffT,
  DiffTC,
  FacT,
  type (<=!),
  type (<!),
  LTEQT,

  -- * matrix dimension synonyms
  D1,
  D2,
  D3,
  D4,
  D5,
  D6,
  D7,
  D8,
  D9,
  D10,

  -- * matrix helpers
  ProductT,
  NN,
  NN',
  ReverseT,
  ListTupleT,

  -- * list and nonempty conversions
  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)

-- | get the factorial of a 'Nat'
type FacT :: Nat -> Nat
type family FacT x where
  FacT 0 = 1
  FacT 1 = 1
  FacT n = n GN.* FacT (n GN.- 1)

-- | constraint for ensuring that "i" <= "n"
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
  )

-- | constraint for ensuring that "i" <= "n" with a custom error message
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
  )

-- | constraint for ensuring that "i" <= "n"
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
  )

-- | constraint for positive numbers
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

-- | constraint for DiffC with better error messages
type DiffTC :: Nat -> Nat -> Nat -> Constraint
type DiffTC i j n = (i <=! j, j <=! n)

-- | find the number of N between "i" and "j" while ensuring i<=j and j<=n
type DiffT :: Nat -> Nat -> Nat -> Nat
type DiffT i j n = j GN.+ 1 GN.- i

-- | reverse a type level list
type ReverseT :: forall k. [k] -> [k]
type family ReverseT ns where
  ReverseT (n ': ns) = ReverseT' (n ': ns) '[]

-- | used by 'ReverseT'
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)

-- | product of a type level list as a 'Nat'
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)

-- | extracts the dimensions of a nested list
type ValidateNestedListT :: Type -> Peano
type family ValidateNestedListT x where
  ValidateNestedListT [x] = 'S (ValidateNestedListT x)
  ValidateNestedListT _ = 'S 'Z

-- | extracts the dimensions of a nested nonempty list
type ValidateNestedNonEmptyT :: Type -> Peano
type family ValidateNestedNonEmptyT x where
  ValidateNestedNonEmptyT (NonEmpty x) = 'S (ValidateNestedNonEmptyT x)
  ValidateNestedNonEmptyT _ = 'S 'Z

-- | validate that the nested nonempty list is consistent in size along all dimensions
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 []

-- | validate that the nested list is consistent in size along all dimensions
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 []

-- | extracts the dimensions of a nested nonempty list: doesnt allow empty dimensions
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)

-- | extracts the dimensions of a nested list: doesnt allow empty dimensions
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

-- | peano numbers for converting between 'Nat' and peano
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)

-- | convert Nat to Peano
type NatToPeanoT :: Nat -> Peano
type family NatToPeanoT n where
  NatToPeanoT 0 = 'Z
  NatToPeanoT n = 'S (NatToPeanoT (n GN.- 1))

-- | convert Peano to Nat
type PeanoToNatT :: Peano -> Nat
type family PeanoToNatT n where
  PeanoToNatT 'Z = 0
  PeanoToNatT ( 'S n) = 1 GN.+ PeanoToNatT n

-- | convert a matrix index into nested lists
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]

-- | convert a matrix index into nested lists
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)

-- | convert a nested nonempty list into a nested list
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)

-- | convert a nested list into a nested nonempty list
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

-- | methods for working with nested lists
type NestedListC :: [Nat] -> Constraint
class NestedListC ns where
  -- | convert a nested list to a nested nonempty list
  nestedListToNonEmptyC :: proxy a -> ListNST ns a -> Either String (NonEmptyNST ns a)

  -- | convert a nested nonempty list to a nested list
  nestedNonEmptyToListC :: proxy a -> NonEmptyNST ns a -> Either String (ListNST ns a) -- need a proxy to make it work and find the correct '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

-- mapM_ (putStrLn . genListTupleT) [2..20]  -- to generate from two onwards

-- | translates a type of size "n" to a tuple of size "n"
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)

-- | generates a list of indices using each digit of the given 'Nat'
type NN :: Nat -> [Nat]
type NN n = NN' '[] n

-- | generates a list of indices using the individual digits of the given 'Nat'
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)

-- | matrix dimension of degree 1
type D1 :: Nat -> [Nat]
type D1 a = '[a]

-- | matrix dimension of degree 2
type D2 :: Nat -> Nat -> [Nat]
type D2 a b = '[a, b]

-- | matrix dimension of degree 3
type D3 :: Nat -> Nat -> Nat -> [Nat]
type D3 a b c = '[a, b, c]

-- | matrix dimension of degree 4
type D4 :: Nat -> Nat -> Nat -> Nat -> [Nat]
type D4 a b c d = '[a, b, c, d]

-- | matrix dimension of degree 5
type D5 :: Nat -> Nat -> Nat -> Nat -> Nat -> [Nat]
type D5 a b c d e = '[a, b, c, d, e]

-- | matrix dimension of degree 6
type D6 :: Nat -> Nat -> Nat -> Nat -> Nat -> Nat -> [Nat]
type D6 a b c d e f = '[a, b, c, d, e, f]

-- | matrix dimension of degree 7
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]

-- | matrix dimension of degree 8
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]

-- | matrix dimension of degree 9
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]

-- | matrix dimension of degree 10
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]