{-# 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
  NS,
  Product1T,
  NN,
  NN',
  Reverse1T,
  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)
import qualified GHC.TypeNats as GN
import Primus.Error
import Primus.Fold
import Primus.List
import Primus.NonEmpty
import Primus.One
import qualified Primus.TypeLevel as TP (Cons1T, 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 =
  ( TP.FailUnless
      (i GN.<=? n)
      ( 'GL.Text "i>n"
          'GL.:<>: 'GL.Text ": i="
          'GL.:<>: 'GL.ShowType i
          'GL.:<>: 'GL.Text " n="
          'GL.:<>: 'GL.ShowType n
      )
  , PosT i
  )

-- | constraint for ensuring that "i" <= "n" with a custom error message
type LTEQT :: GL.ErrorMessage -> Nat -> Nat -> Constraint
type LTEQT msg i n =
  ( TP.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
      )
  , PosT i
  )

-- | constraint for ensuring that "i" <= "n"
type (<!) :: Nat -> Nat -> Constraint
type i <! n =
  ( TP.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
      )
  , GN.KnownNat i
  )

-- | 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

-- | product of a type level nonempty list as a 'Nat'
type Product1T :: NonEmpty Nat -> Nat
type family Product1T ns where
  Product1T (n ':| '[]) = n
  Product1T (n ':| n1 ': ns) = n GN.* Product1T (n1 ':| ns)

-- | convert a list of 'Nat' into a nonempty list of 'Nat'
type NS :: [Nat] -> NonEmpty Nat
type family NS ns where
  NS '[] = GL.TypeError ( 'GL.Text "NS: must have at least one Nat value for NonEmpty Nat")
  NS (n ': '[]) = n ':| '[]
  NS (n ': m ': ns) = TP.Cons1T n (NS (m ': ns))

-- | used for reversing the indices of a matrix using type level list of nonempty indices
type Reverse1T :: forall k. NonEmpty k -> NonEmpty k
type family Reverse1T ns where
  Reverse1T (n ':| ns) = Reverse1T' (n ': ns) '[]

-- | used by 'Reverse1T'
type Reverse1T' :: forall k. [k] -> [k] -> NonEmpty k
type family Reverse1T' ns ret where
  Reverse1T' '[] (r ': rs) = r ':| rs
  Reverse1T' (n ': ns) ret = Reverse1T' ns (n ': ret)

-- | 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 (NonEmpty x) -> [CLCount x]
forall (t :: * -> *) a. Foldable t => NonEmpty (t a) -> [CLCount a]
compareLengths (NonEmpty x
x NonEmpty x -> [NonEmpty x] -> NonEmpty (NonEmpty x)
forall a. a -> [a] -> NonEmpty a
:| [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
$ NonEmpty [x] -> [CLCount x]
forall (t :: * -> *) a. Foldable t => NonEmpty (t a) -> [CLCount a]
compareLengths ([x]
x [x] -> [[x]] -> NonEmpty [x]
forall a. a -> [a] -> NonEmpty a
:| [[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 :: NonEmpty Nat -> Type -> Type
type family ListNST ns a where
  ListNST (_ ':| '[]) a = [a]
  ListNST (_ ':| n1 ': ns) a = [ListNST (n1 ':| ns) a]

-- | convert a matrix index into nested lists
type NonEmptyNST :: NonEmpty Nat -> Type -> Type
type family NonEmptyNST ns a where
  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 :: NonEmpty 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 :: NonEmpty 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 :: NonEmpty 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 PosT 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 (PosT n => Pos
forall (n :: Nat). PosT 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 (PosT n => Pos
forall (n :: Nat). PosT 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 (PosT n => Int
forall (n :: Nat). PosT n => Int
fromN @n) (a
x a -> [a] -> [a]
forall a. a -> [a] -> [a]
: [a]
xs)

instance (PosT 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 (PosT n => Pos
forall (n :: Nat). PosT 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 :: NonEmpty 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 (PosT n => Pos
forall (n :: Nat). PosT 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 :: NonEmpty 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 (PosT n => Int
forall (n :: Nat). PosT 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 :: NonEmpty 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 nonempty list of indices using each digit of the given 'Nat'
type NN :: Nat -> NonEmpty Nat
type NN n = NS (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 -> NonEmpty Nat
type D1 a = a ':| '[]

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

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

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

-- | matrix dimension of degree 5
type D5 :: Nat -> Nat -> Nat -> Nat -> Nat -> NonEmpty 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 -> NonEmpty 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 -> NonEmpty 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 -> NonEmpty 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 -> NonEmpty 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 -> NonEmpty Nat
type D10 a b c d e f g h i j = a ':| '[b, c, d, e, f, g, h, i, j]