{-# LANGUAGE Trustworthy, TypeFamilies, TypeOperators #-}
{-# LANGUAGE UndecidableInstances, FlexibleInstances #-}

{- |
    Module      :  SDP.Finite
    Copyright   :  (c) Andrey Mulik 2019-2021
    License     :  BSD-style
    Maintainer  :  work.a.mulik@gmail.com
    Portability :  non-portable (GHC extensions)
    
    "SDP.Finite" provide generalized finite-dimensional index type (':&') based
    on @repa@ @(:.)@.
    
    Since @sdp-0.2@, for (':&') available @OverloadedLists@-based syntactic sugar.
    For example, instead of the inconvenient @es!(ind4 0 1 2 3)@ or just awful
    @es!(E:&0:&1:&1:&2:&3)@ you can write: @es![0, 1, 2, 3]@.
    
    Note that @OverloadedLists@ instances requires a strictly defined number of
    subindexes.
-}
module SDP.Finite
(
  -- * Generalized index
  E (..), (:&) (..),
  
  -- * Type synonyms
  I1, I2, I3, I4, I5, I6, I7, I8, I9, I10, I11, I12, I13, I14, I15,
  
  -- * Old constructors
  ind2,  ind3,  ind4,  ind5,  ind6,  ind7,  ind8,  ind9,
  ind10, ind11, ind12, ind13, ind14, ind15
)
where

import Prelude ( (++) )
import SDP.SafePrelude
import SDP.Nullable

import Data.Default.Class

import GHC.Types
import GHC.Read

import qualified GHC.Exts as E
import GHC.Exts ( IsList )

import Control.Exception.SDP

default ()

--------------------------------------------------------------------------------

{- Zero-dimensional type. -}

-- | Service type, that represents zero-dimensional index.
data E = E deriving ( E -> E -> Bool
(E -> E -> Bool) -> (E -> E -> Bool) -> Eq E
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: E -> E -> Bool
$c/= :: E -> E -> Bool
== :: E -> E -> Bool
$c== :: E -> E -> Bool
Eq, Eq E
Eq E
-> (E -> E -> Ordering)
-> (E -> E -> Bool)
-> (E -> E -> Bool)
-> (E -> E -> Bool)
-> (E -> E -> Bool)
-> (E -> E -> E)
-> (E -> E -> E)
-> Ord E
E -> E -> Bool
E -> E -> Ordering
E -> E -> E
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 :: E -> E -> E
$cmin :: E -> E -> E
max :: E -> E -> E
$cmax :: E -> E -> E
>= :: E -> E -> Bool
$c>= :: E -> E -> Bool
> :: E -> E -> Bool
$c> :: E -> E -> Bool
<= :: E -> E -> Bool
$c<= :: E -> E -> Bool
< :: E -> E -> Bool
$c< :: E -> E -> Bool
compare :: E -> E -> Ordering
$ccompare :: E -> E -> Ordering
$cp1Ord :: Eq E
Ord, Int -> E -> ShowS
[E] -> ShowS
E -> String
(Int -> E -> ShowS) -> (E -> String) -> ([E] -> ShowS) -> Show E
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [E] -> ShowS
$cshowList :: [E] -> ShowS
show :: E -> String
$cshow :: E -> String
showsPrec :: Int -> E -> ShowS
$cshowsPrec :: Int -> E -> ShowS
Show, ReadPrec [E]
ReadPrec E
Int -> ReadS E
ReadS [E]
(Int -> ReadS E)
-> ReadS [E] -> ReadPrec E -> ReadPrec [E] -> Read E
forall a.
(Int -> ReadS a)
-> ReadS [a] -> ReadPrec a -> ReadPrec [a] -> Read a
readListPrec :: ReadPrec [E]
$creadListPrec :: ReadPrec [E]
readPrec :: ReadPrec E
$creadPrec :: ReadPrec E
readList :: ReadS [E]
$creadList :: ReadS [E]
readsPrec :: Int -> ReadS E
$creadsPrec :: Int -> ReadS E
Read )

instance Default E where def :: E
def = E
E

instance IsList E
  where
    type Item E = E
    
    fromList :: [Item E] -> E
fromList = E -> [E] -> E
forall a b. a -> b -> a
const E
E
    toList :: E -> [Item E]
toList   = [E] -> E -> [E]
forall a b. a -> b -> a
const []

-- | @since 0.2.1
instance Nullable E where lzero :: E
lzero = E
E; isNull :: E -> Bool
isNull = Bool -> E -> Bool
forall a b. a -> b -> a
const Bool
True

--------------------------------------------------------------------------------

{- N-dimensional index type. -}

{- |
  N-dimensional index type. The type (head :& tail) allows working with any
  finite dimension number.
-}
data tail :& head = !tail :& !head deriving ( (tail :& head) -> (tail :& head) -> Bool
((tail :& head) -> (tail :& head) -> Bool)
-> ((tail :& head) -> (tail :& head) -> Bool) -> Eq (tail :& head)
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
forall tail head.
(Eq tail, Eq head) =>
(tail :& head) -> (tail :& head) -> Bool
/= :: (tail :& head) -> (tail :& head) -> Bool
$c/= :: forall tail head.
(Eq tail, Eq head) =>
(tail :& head) -> (tail :& head) -> Bool
== :: (tail :& head) -> (tail :& head) -> Bool
$c== :: forall tail head.
(Eq tail, Eq head) =>
(tail :& head) -> (tail :& head) -> Bool
Eq, Eq (tail :& head)
Eq (tail :& head)
-> ((tail :& head) -> (tail :& head) -> Ordering)
-> ((tail :& head) -> (tail :& head) -> Bool)
-> ((tail :& head) -> (tail :& head) -> Bool)
-> ((tail :& head) -> (tail :& head) -> Bool)
-> ((tail :& head) -> (tail :& head) -> Bool)
-> ((tail :& head) -> (tail :& head) -> tail :& head)
-> ((tail :& head) -> (tail :& head) -> tail :& head)
-> Ord (tail :& head)
(tail :& head) -> (tail :& head) -> Bool
(tail :& head) -> (tail :& head) -> Ordering
(tail :& head) -> (tail :& head) -> tail :& head
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
forall tail head. (Ord tail, Ord head) => Eq (tail :& head)
forall tail head.
(Ord tail, Ord head) =>
(tail :& head) -> (tail :& head) -> Bool
forall tail head.
(Ord tail, Ord head) =>
(tail :& head) -> (tail :& head) -> Ordering
forall tail head.
(Ord tail, Ord head) =>
(tail :& head) -> (tail :& head) -> tail :& head
min :: (tail :& head) -> (tail :& head) -> tail :& head
$cmin :: forall tail head.
(Ord tail, Ord head) =>
(tail :& head) -> (tail :& head) -> tail :& head
max :: (tail :& head) -> (tail :& head) -> tail :& head
$cmax :: forall tail head.
(Ord tail, Ord head) =>
(tail :& head) -> (tail :& head) -> tail :& head
>= :: (tail :& head) -> (tail :& head) -> Bool
$c>= :: forall tail head.
(Ord tail, Ord head) =>
(tail :& head) -> (tail :& head) -> Bool
> :: (tail :& head) -> (tail :& head) -> Bool
$c> :: forall tail head.
(Ord tail, Ord head) =>
(tail :& head) -> (tail :& head) -> Bool
<= :: (tail :& head) -> (tail :& head) -> Bool
$c<= :: forall tail head.
(Ord tail, Ord head) =>
(tail :& head) -> (tail :& head) -> Bool
< :: (tail :& head) -> (tail :& head) -> Bool
$c< :: forall tail head.
(Ord tail, Ord head) =>
(tail :& head) -> (tail :& head) -> Bool
compare :: (tail :& head) -> (tail :& head) -> Ordering
$ccompare :: forall tail head.
(Ord tail, Ord head) =>
(tail :& head) -> (tail :& head) -> Ordering
$cp1Ord :: forall tail head. (Ord tail, Ord head) => Eq (tail :& head)
Ord )

instance (Enum i) => Enum (E :& i)
  where
    fromEnum :: (E :& i) -> Int
fromEnum (E
E :& i
e) = i -> Int
forall a. Enum a => a -> Int
fromEnum  i
e
    succ :: (E :& i) -> E :& i
succ     (E
E :& i
e) = E
E E -> i -> E :& i
forall tail head. tail -> head -> tail :& head
:& i -> i
forall a. Enum a => a -> a
succ i
e
    pred :: (E :& i) -> E :& i
pred     (E
E :& i
e) = E
E E -> i -> E :& i
forall tail head. tail -> head -> tail :& head
:& i -> i
forall a. Enum a => a -> a
pred i
e
    
    toEnum :: Int -> E :& i
toEnum = (E
E E -> i -> E :& i
forall tail head. tail -> head -> tail :& head
:&) (i -> E :& i) -> (Int -> i) -> Int -> E :& i
forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. Int -> i
forall a. Enum a => Int -> a
toEnum
    
    enumFrom :: (E :& i) -> [E :& i]
enumFrom                (E
E :& i
f)          = (E
E E -> i -> E :& i
forall tail head. tail -> head -> tail :& head
:&) (i -> E :& i) -> [i] -> [E :& i]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [i
f ..]
    enumFromTo :: (E :& i) -> (E :& i) -> [E :& i]
enumFromTo         (E
E :& i
f) (E
E :& i
l)      = (E
E E -> i -> E :& i
forall tail head. tail -> head -> tail :& head
:&) (i -> E :& i) -> [i] -> [E :& i]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [i
f .. i
l]
    enumFromThen :: (E :& i) -> (E :& i) -> [E :& i]
enumFromThen       (E
E :& i
f)  (E
E :& i
n)     = (E
E E -> i -> E :& i
forall tail head. tail -> head -> tail :& head
:&) (i -> E :& i) -> [i] -> [E :& i]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [i
f, i
n ..]
    enumFromThenTo :: (E :& i) -> (E :& i) -> (E :& i) -> [E :& i]
enumFromThenTo (E
E :& i
f) (E
E :& i
n) (E
E :& i
l) = (E
E E -> i -> E :& i
forall tail head. tail -> head -> tail :& head
:&) (i -> E :& i) -> [i] -> [E :& i]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [i
f, i
n .. i
l]

instance (Default d, Default d') => Default (d :& d') where def :: d :& d'
def = d
forall a. Default a => a
def d -> d' -> d :& d'
forall tail head. tail -> head -> tail :& head
:& d'
forall a. Default a => a
def

--------------------------------------------------------------------------------

{- Overloaded indices. -}

instance (IsList (i' :& i), E.Item (i' :& i) ~~ i, Show i) => Show (i' :& i)
  where
    showsPrec :: Int -> (i' :& i) -> ShowS
showsPrec Int
p = Int -> [Item (i' :& i)] -> ShowS
forall a. Show a => Int -> a -> ShowS
showsPrec Int
p ([Item (i' :& i)] -> ShowS)
-> ((i' :& i) -> [Item (i' :& i)]) -> (i' :& i) -> ShowS
forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. (i' :& i) -> [Item (i' :& i)]
forall l. IsList l => l -> [Item l]
E.toList

instance (IsList (i' :& i), E.Item (i' :& i) ~~ i, Read i) => Read (i' :& i)
  where
    readPrec :: ReadPrec (i' :& i)
readPrec = [i] -> i' :& i
forall l. IsList l => [Item l] -> l
E.fromList ([i] -> i' :& i) -> ReadPrec [i] -> ReadPrec (i' :& i)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ReadPrec [i]
forall a. Read a => ReadPrec a
readPrec

instance IsList (E :& i)
  where
    type Item (E :& i) = i
    
    fromList :: [Item (E :& i)] -> E :& i
fromList [Item (E :& i)
i] = E
E E -> i -> E :& i
forall tail head. tail -> head -> tail :& head
:& i
Item (E :& i)
i
    fromList  [Item (E :& i)]
_  = IndexException -> E :& i
forall a e. Exception e => e -> a
throw (IndexException -> E :& i) -> IndexException -> E :& i
forall a b. (a -> b) -> a -> b
$ String -> IndexException
UnexpectedRank String
"in SDP.Finite.fromList"
    
    toList :: (E :& i) -> [Item (E :& i)]
toList (E
E :& i
i) = [i
Item (E :& i)
i]

instance (E.Item (i' :& i) ~~ i, IsList (i' :& i)) => IsList (i' :& i :& i)
  where
    type Item (i' :& i :& i) = i
    
    toList :: ((i' :& i) :& i) -> [Item ((i' :& i) :& i)]
toList (i' :& i
i' :& i
i) = (i' :& i) -> [Item (i' :& i)]
forall l. IsList l => l -> [Item l]
E.toList i' :& i
i' [i] -> [i] -> [i]
forall a. [a] -> [a] -> [a]
++ [i
i]
    
    fromList :: [Item ((i' :& i) :& i)] -> (i' :& i) :& i
fromList = (([Item (i' :& i)] -> i -> (i' :& i) :& i)
-> ([Item (i' :& i)], i) -> (i' :& i) :& i
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry (([Item (i' :& i)] -> i -> (i' :& i) :& i)
 -> ([Item (i' :& i)], i) -> (i' :& i) :& i)
-> ([Item (i' :& i)] -> i -> (i' :& i) :& i)
-> ([Item (i' :& i)], i)
-> (i' :& i) :& i
forall a b. (a -> b) -> a -> b
$ (i' :& i) -> i -> (i' :& i) :& i
forall tail head. tail -> head -> tail :& head
(:&) ((i' :& i) -> i -> (i' :& i) :& i)
-> ([Item (i' :& i)] -> i' :& i)
-> [Item (i' :& i)]
-> i
-> (i' :& i) :& i
forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. [Item (i' :& i)] -> i' :& i
forall l. IsList l => [Item l] -> l
E.fromList) (([Item (i' :& i)], i) -> (i' :& i) :& i)
-> ([i] -> ([Item (i' :& i)], i)) -> [i] -> (i' :& i) :& i
forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. [i] -> ([Item (i' :& i)], i)
forall i. [i] -> ([i], i)
unsnoc

--------------------------------------------------------------------------------

{- Type synonyms are declared up to 15 dimensions. -}

-- | 1-dimensional index (@(E :& i)@ without @TypeOperators@).
type I1  i = E :& i
-- | 2-dimensional index
type I2  i = E :& i  :& i
-- | 3-dimensional index
type I3  i = (I2  i) :& i
-- | 4-dimensional index
type I4  i = (I3  i) :& i
-- | 5-dimensional index
type I5  i = (I4  i) :& i
-- | 6-dimensional index
type I6  i = (I5  i) :& i
-- | 7-dimensional index
type I7  i = (I6  i) :& i
-- | 8-dimensional index
type I8  i = (I7  i) :& i
-- | 9-dimensional index
type I9  i = (I8  i) :& i
-- | 10-dimensional index
type I10 i = (I9  i) :& i
-- | 11-dimensional index
type I11 i = (I10 i) :& i
-- | 12-dimensional index
type I12 i = (I11 i) :& i
-- | 13-dimensional index
type I13 i = (I12 i) :& i
-- | 14-dimensional index
type I14 i = (I13 i) :& i
-- | 15-dimensional index
type I15 i = (I14 i) :& i

-- | 2-dimensional index constructor.
ind2  :: i -> i                                                                  -> I2  i
-- | 3-dimensional index constructor.
ind3  :: i -> i -> i                                                             -> I3  i
-- | 4-dimensional index constructor.
ind4  :: i -> i -> i -> i                                                        -> I4  i
-- | 5-dimensional index constructor.
ind5  :: i -> i -> i -> i -> i                                                   -> I5  i
-- | 6-dimensional index constructor.
ind6  :: i -> i -> i -> i -> i -> i                                              -> I6  i
-- | 7-dimensional index constructor.
ind7  :: i -> i -> i -> i -> i -> i -> i                                         -> I7  i
-- | 8-dimensional index constructor.
ind8  :: i -> i -> i -> i -> i -> i -> i -> i                                    -> I8  i
-- | 9-dimensional index constructor.
ind9  :: i -> i -> i -> i -> i -> i -> i -> i -> i                               -> I9  i
-- | 10-dimensional index constructor.
ind10 :: i -> i -> i -> i -> i -> i -> i -> i -> i -> i                          -> I10 i
-- | 11-dimensional index constructor.
ind11 :: i -> i -> i -> i -> i -> i -> i -> i -> i -> i -> i                     -> I11 i
-- | 12-dimensional index constructor.
ind12 :: i -> i -> i -> i -> i -> i -> i -> i -> i -> i -> i -> i                -> I12 i
-- | 13-dimensional index constructor.
ind13 :: i -> i -> i -> i -> i -> i -> i -> i -> i -> i -> i -> i -> i           -> I13 i
-- | 14-dimensional index constructor.
ind14 :: i -> i -> i -> i -> i -> i -> i -> i -> i -> i -> i -> i -> i -> i      -> I14 i
-- | 15-dimensional index constructor.
ind15 :: i -> i -> i -> i -> i -> i -> i -> i -> i -> i -> i -> i -> i -> i -> i -> I15 i

ind2 :: i -> i -> I2 i
ind2  i
a i
b                           = E
EE -> i -> E :& i
forall tail head. tail -> head -> tail :& head
:&i
a(E :& i) -> i -> I2 i
forall tail head. tail -> head -> tail :& head
:&i
b
ind3 :: i -> i -> i -> I3 i
ind3  i
a i
b i
c                         = E
EE -> i -> E :& i
forall tail head. tail -> head -> tail :& head
:&i
a(E :& i) -> i -> (E :& i) :& i
forall tail head. tail -> head -> tail :& head
:&i
b((E :& i) :& i) -> i -> I3 i
forall tail head. tail -> head -> tail :& head
:&i
c
ind4 :: i -> i -> i -> i -> I4 i
ind4  i
a i
b i
c i
d                       = E
EE -> i -> E :& i
forall tail head. tail -> head -> tail :& head
:&i
a(E :& i) -> i -> (E :& i) :& i
forall tail head. tail -> head -> tail :& head
:&i
b((E :& i) :& i) -> i -> ((E :& i) :& i) :& i
forall tail head. tail -> head -> tail :& head
:&i
c(((E :& i) :& i) :& i) -> i -> I4 i
forall tail head. tail -> head -> tail :& head
:&i
d
ind5 :: i -> i -> i -> i -> i -> I5 i
ind5  i
a i
b i
c i
d i
e                     = E
EE -> i -> E :& i
forall tail head. tail -> head -> tail :& head
:&i
a(E :& i) -> i -> (E :& i) :& i
forall tail head. tail -> head -> tail :& head
:&i
b((E :& i) :& i) -> i -> ((E :& i) :& i) :& i
forall tail head. tail -> head -> tail :& head
:&i
c(((E :& i) :& i) :& i) -> i -> (((E :& i) :& i) :& i) :& i
forall tail head. tail -> head -> tail :& head
:&i
d((((E :& i) :& i) :& i) :& i) -> i -> I5 i
forall tail head. tail -> head -> tail :& head
:&i
e
ind6 :: i -> i -> i -> i -> i -> i -> I6 i
ind6  i
a i
b i
c i
d i
e i
f                   = E
EE -> i -> E :& i
forall tail head. tail -> head -> tail :& head
:&i
a(E :& i) -> i -> (E :& i) :& i
forall tail head. tail -> head -> tail :& head
:&i
b((E :& i) :& i) -> i -> ((E :& i) :& i) :& i
forall tail head. tail -> head -> tail :& head
:&i
c(((E :& i) :& i) :& i) -> i -> (((E :& i) :& i) :& i) :& i
forall tail head. tail -> head -> tail :& head
:&i
d((((E :& i) :& i) :& i) :& i)
-> i -> ((((E :& i) :& i) :& i) :& i) :& i
forall tail head. tail -> head -> tail :& head
:&i
e(((((E :& i) :& i) :& i) :& i) :& i) -> i -> I6 i
forall tail head. tail -> head -> tail :& head
:&i
f
ind7 :: i -> i -> i -> i -> i -> i -> i -> I7 i
ind7  i
a i
b i
c i
d i
e i
f i
g                 = E
EE -> i -> E :& i
forall tail head. tail -> head -> tail :& head
:&i
a(E :& i) -> i -> (E :& i) :& i
forall tail head. tail -> head -> tail :& head
:&i
b((E :& i) :& i) -> i -> ((E :& i) :& i) :& i
forall tail head. tail -> head -> tail :& head
:&i
c(((E :& i) :& i) :& i) -> i -> (((E :& i) :& i) :& i) :& i
forall tail head. tail -> head -> tail :& head
:&i
d((((E :& i) :& i) :& i) :& i)
-> i -> ((((E :& i) :& i) :& i) :& i) :& i
forall tail head. tail -> head -> tail :& head
:&i
e(((((E :& i) :& i) :& i) :& i) :& i)
-> i -> (((((E :& i) :& i) :& i) :& i) :& i) :& i
forall tail head. tail -> head -> tail :& head
:&i
f((((((E :& i) :& i) :& i) :& i) :& i) :& i) -> i -> I7 i
forall tail head. tail -> head -> tail :& head
:&i
g
ind8 :: i -> i -> i -> i -> i -> i -> i -> i -> I8 i
ind8  i
a i
b i
c i
d i
e i
f i
g i
h               = E
EE -> i -> E :& i
forall tail head. tail -> head -> tail :& head
:&i
a(E :& i) -> i -> (E :& i) :& i
forall tail head. tail -> head -> tail :& head
:&i
b((E :& i) :& i) -> i -> ((E :& i) :& i) :& i
forall tail head. tail -> head -> tail :& head
:&i
c(((E :& i) :& i) :& i) -> i -> (((E :& i) :& i) :& i) :& i
forall tail head. tail -> head -> tail :& head
:&i
d((((E :& i) :& i) :& i) :& i)
-> i -> ((((E :& i) :& i) :& i) :& i) :& i
forall tail head. tail -> head -> tail :& head
:&i
e(((((E :& i) :& i) :& i) :& i) :& i)
-> i -> (((((E :& i) :& i) :& i) :& i) :& i) :& i
forall tail head. tail -> head -> tail :& head
:&i
f((((((E :& i) :& i) :& i) :& i) :& i) :& i)
-> i -> ((((((E :& i) :& i) :& i) :& i) :& i) :& i) :& i
forall tail head. tail -> head -> tail :& head
:&i
g(((((((E :& i) :& i) :& i) :& i) :& i) :& i) :& i) -> i -> I8 i
forall tail head. tail -> head -> tail :& head
:&i
h
ind9 :: i -> i -> i -> i -> i -> i -> i -> i -> i -> I9 i
ind9  i
a i
b i
c i
d i
e i
f i
g i
h i
i             = E
EE -> i -> E :& i
forall tail head. tail -> head -> tail :& head
:&i
a(E :& i) -> i -> (E :& i) :& i
forall tail head. tail -> head -> tail :& head
:&i
b((E :& i) :& i) -> i -> ((E :& i) :& i) :& i
forall tail head. tail -> head -> tail :& head
:&i
c(((E :& i) :& i) :& i) -> i -> (((E :& i) :& i) :& i) :& i
forall tail head. tail -> head -> tail :& head
:&i
d((((E :& i) :& i) :& i) :& i)
-> i -> ((((E :& i) :& i) :& i) :& i) :& i
forall tail head. tail -> head -> tail :& head
:&i
e(((((E :& i) :& i) :& i) :& i) :& i)
-> i -> (((((E :& i) :& i) :& i) :& i) :& i) :& i
forall tail head. tail -> head -> tail :& head
:&i
f((((((E :& i) :& i) :& i) :& i) :& i) :& i)
-> i -> ((((((E :& i) :& i) :& i) :& i) :& i) :& i) :& i
forall tail head. tail -> head -> tail :& head
:&i
g(((((((E :& i) :& i) :& i) :& i) :& i) :& i) :& i)
-> i -> (((((((E :& i) :& i) :& i) :& i) :& i) :& i) :& i) :& i
forall tail head. tail -> head -> tail :& head
:&i
h((((((((E :& i) :& i) :& i) :& i) :& i) :& i) :& i) :& i)
-> i -> I9 i
forall tail head. tail -> head -> tail :& head
:&i
i
ind10 :: i -> i -> i -> i -> i -> i -> i -> i -> i -> i -> I10 i
ind10 i
a i
b i
c i
d i
e i
f i
g i
h i
i i
j           = E
EE -> i -> E :& i
forall tail head. tail -> head -> tail :& head
:&i
a(E :& i) -> i -> (E :& i) :& i
forall tail head. tail -> head -> tail :& head
:&i
b((E :& i) :& i) -> i -> ((E :& i) :& i) :& i
forall tail head. tail -> head -> tail :& head
:&i
c(((E :& i) :& i) :& i) -> i -> (((E :& i) :& i) :& i) :& i
forall tail head. tail -> head -> tail :& head
:&i
d((((E :& i) :& i) :& i) :& i)
-> i -> ((((E :& i) :& i) :& i) :& i) :& i
forall tail head. tail -> head -> tail :& head
:&i
e(((((E :& i) :& i) :& i) :& i) :& i)
-> i -> (((((E :& i) :& i) :& i) :& i) :& i) :& i
forall tail head. tail -> head -> tail :& head
:&i
f((((((E :& i) :& i) :& i) :& i) :& i) :& i)
-> i -> ((((((E :& i) :& i) :& i) :& i) :& i) :& i) :& i
forall tail head. tail -> head -> tail :& head
:&i
g(((((((E :& i) :& i) :& i) :& i) :& i) :& i) :& i)
-> i -> (((((((E :& i) :& i) :& i) :& i) :& i) :& i) :& i) :& i
forall tail head. tail -> head -> tail :& head
:&i
h((((((((E :& i) :& i) :& i) :& i) :& i) :& i) :& i) :& i)
-> i
-> ((((((((E :& i) :& i) :& i) :& i) :& i) :& i) :& i) :& i) :& i
forall tail head. tail -> head -> tail :& head
:&i
i(((((((((E :& i) :& i) :& i) :& i) :& i) :& i) :& i) :& i) :& i)
-> i -> I10 i
forall tail head. tail -> head -> tail :& head
:&i
j
ind11 :: i -> i -> i -> i -> i -> i -> i -> i -> i -> i -> i -> I11 i
ind11 i
a i
b i
c i
d i
e i
f i
g i
h i
i i
j i
k         = E
EE -> i -> E :& i
forall tail head. tail -> head -> tail :& head
:&i
a(E :& i) -> i -> (E :& i) :& i
forall tail head. tail -> head -> tail :& head
:&i
b((E :& i) :& i) -> i -> ((E :& i) :& i) :& i
forall tail head. tail -> head -> tail :& head
:&i
c(((E :& i) :& i) :& i) -> i -> (((E :& i) :& i) :& i) :& i
forall tail head. tail -> head -> tail :& head
:&i
d((((E :& i) :& i) :& i) :& i)
-> i -> ((((E :& i) :& i) :& i) :& i) :& i
forall tail head. tail -> head -> tail :& head
:&i
e(((((E :& i) :& i) :& i) :& i) :& i)
-> i -> (((((E :& i) :& i) :& i) :& i) :& i) :& i
forall tail head. tail -> head -> tail :& head
:&i
f((((((E :& i) :& i) :& i) :& i) :& i) :& i)
-> i -> ((((((E :& i) :& i) :& i) :& i) :& i) :& i) :& i
forall tail head. tail -> head -> tail :& head
:&i
g(((((((E :& i) :& i) :& i) :& i) :& i) :& i) :& i)
-> i -> (((((((E :& i) :& i) :& i) :& i) :& i) :& i) :& i) :& i
forall tail head. tail -> head -> tail :& head
:&i
h((((((((E :& i) :& i) :& i) :& i) :& i) :& i) :& i) :& i)
-> i
-> ((((((((E :& i) :& i) :& i) :& i) :& i) :& i) :& i) :& i) :& i
forall tail head. tail -> head -> tail :& head
:&i
i(((((((((E :& i) :& i) :& i) :& i) :& i) :& i) :& i) :& i) :& i)
-> i
-> (((((((((E :& i) :& i) :& i) :& i) :& i) :& i) :& i) :& i) :& i)
   :& i
forall tail head. tail -> head -> tail :& head
:&i
j((((((((((E :& i) :& i) :& i) :& i) :& i) :& i) :& i) :& i) :& i)
 :& i)
-> i -> I11 i
forall tail head. tail -> head -> tail :& head
:&i
k
ind12 :: i -> i -> i -> i -> i -> i -> i -> i -> i -> i -> i -> i -> I12 i
ind12 i
a i
b i
c i
d i
e i
f i
g i
h i
i i
j i
k i
l       = E
EE -> i -> E :& i
forall tail head. tail -> head -> tail :& head
:&i
a(E :& i) -> i -> (E :& i) :& i
forall tail head. tail -> head -> tail :& head
:&i
b((E :& i) :& i) -> i -> ((E :& i) :& i) :& i
forall tail head. tail -> head -> tail :& head
:&i
c(((E :& i) :& i) :& i) -> i -> (((E :& i) :& i) :& i) :& i
forall tail head. tail -> head -> tail :& head
:&i
d((((E :& i) :& i) :& i) :& i)
-> i -> ((((E :& i) :& i) :& i) :& i) :& i
forall tail head. tail -> head -> tail :& head
:&i
e(((((E :& i) :& i) :& i) :& i) :& i)
-> i -> (((((E :& i) :& i) :& i) :& i) :& i) :& i
forall tail head. tail -> head -> tail :& head
:&i
f((((((E :& i) :& i) :& i) :& i) :& i) :& i)
-> i -> ((((((E :& i) :& i) :& i) :& i) :& i) :& i) :& i
forall tail head. tail -> head -> tail :& head
:&i
g(((((((E :& i) :& i) :& i) :& i) :& i) :& i) :& i)
-> i -> (((((((E :& i) :& i) :& i) :& i) :& i) :& i) :& i) :& i
forall tail head. tail -> head -> tail :& head
:&i
h((((((((E :& i) :& i) :& i) :& i) :& i) :& i) :& i) :& i)
-> i
-> ((((((((E :& i) :& i) :& i) :& i) :& i) :& i) :& i) :& i) :& i
forall tail head. tail -> head -> tail :& head
:&i
i(((((((((E :& i) :& i) :& i) :& i) :& i) :& i) :& i) :& i) :& i)
-> i
-> (((((((((E :& i) :& i) :& i) :& i) :& i) :& i) :& i) :& i) :& i)
   :& i
forall tail head. tail -> head -> tail :& head
:&i
j((((((((((E :& i) :& i) :& i) :& i) :& i) :& i) :& i) :& i) :& i)
 :& i)
-> i
-> ((((((((((E :& i) :& i) :& i) :& i) :& i) :& i) :& i) :& i)
     :& i)
    :& i)
   :& i
forall tail head. tail -> head -> tail :& head
:&i
k(((((((((((E :& i) :& i) :& i) :& i) :& i) :& i) :& i) :& i) :& i)
  :& i)
 :& i)
-> i -> I12 i
forall tail head. tail -> head -> tail :& head
:&i
l
ind13 :: i
-> i
-> i
-> i
-> i
-> i
-> i
-> i
-> i
-> i
-> i
-> i
-> i
-> I13 i
ind13 i
a i
b i
c i
d i
e i
f i
g i
h i
i i
j i
k i
l i
m     = E
EE -> i -> E :& i
forall tail head. tail -> head -> tail :& head
:&i
a(E :& i) -> i -> (E :& i) :& i
forall tail head. tail -> head -> tail :& head
:&i
b((E :& i) :& i) -> i -> ((E :& i) :& i) :& i
forall tail head. tail -> head -> tail :& head
:&i
c(((E :& i) :& i) :& i) -> i -> (((E :& i) :& i) :& i) :& i
forall tail head. tail -> head -> tail :& head
:&i
d((((E :& i) :& i) :& i) :& i)
-> i -> ((((E :& i) :& i) :& i) :& i) :& i
forall tail head. tail -> head -> tail :& head
:&i
e(((((E :& i) :& i) :& i) :& i) :& i)
-> i -> (((((E :& i) :& i) :& i) :& i) :& i) :& i
forall tail head. tail -> head -> tail :& head
:&i
f((((((E :& i) :& i) :& i) :& i) :& i) :& i)
-> i -> ((((((E :& i) :& i) :& i) :& i) :& i) :& i) :& i
forall tail head. tail -> head -> tail :& head
:&i
g(((((((E :& i) :& i) :& i) :& i) :& i) :& i) :& i)
-> i -> (((((((E :& i) :& i) :& i) :& i) :& i) :& i) :& i) :& i
forall tail head. tail -> head -> tail :& head
:&i
h((((((((E :& i) :& i) :& i) :& i) :& i) :& i) :& i) :& i)
-> i
-> ((((((((E :& i) :& i) :& i) :& i) :& i) :& i) :& i) :& i) :& i
forall tail head. tail -> head -> tail :& head
:&i
i(((((((((E :& i) :& i) :& i) :& i) :& i) :& i) :& i) :& i) :& i)
-> i
-> (((((((((E :& i) :& i) :& i) :& i) :& i) :& i) :& i) :& i) :& i)
   :& i
forall tail head. tail -> head -> tail :& head
:&i
j((((((((((E :& i) :& i) :& i) :& i) :& i) :& i) :& i) :& i) :& i)
 :& i)
-> i
-> ((((((((((E :& i) :& i) :& i) :& i) :& i) :& i) :& i) :& i)
     :& i)
    :& i)
   :& i
forall tail head. tail -> head -> tail :& head
:&i
k(((((((((((E :& i) :& i) :& i) :& i) :& i) :& i) :& i) :& i) :& i)
  :& i)
 :& i)
-> i
-> (((((((((((E :& i) :& i) :& i) :& i) :& i) :& i) :& i) :& i)
      :& i)
     :& i)
    :& i)
   :& i
forall tail head. tail -> head -> tail :& head
:&i
l((((((((((((E :& i) :& i) :& i) :& i) :& i) :& i) :& i) :& i) :& i)
   :& i)
  :& i)
 :& i)
-> i -> I13 i
forall tail head. tail -> head -> tail :& head
:&i
m
ind14 :: i
-> i
-> i
-> i
-> i
-> i
-> i
-> i
-> i
-> i
-> i
-> i
-> i
-> i
-> I14 i
ind14 i
a i
b i
c i
d i
e i
f i
g i
h i
i i
j i
k i
l i
m i
n   = E
EE -> i -> E :& i
forall tail head. tail -> head -> tail :& head
:&i
a(E :& i) -> i -> (E :& i) :& i
forall tail head. tail -> head -> tail :& head
:&i
b((E :& i) :& i) -> i -> ((E :& i) :& i) :& i
forall tail head. tail -> head -> tail :& head
:&i
c(((E :& i) :& i) :& i) -> i -> (((E :& i) :& i) :& i) :& i
forall tail head. tail -> head -> tail :& head
:&i
d((((E :& i) :& i) :& i) :& i)
-> i -> ((((E :& i) :& i) :& i) :& i) :& i
forall tail head. tail -> head -> tail :& head
:&i
e(((((E :& i) :& i) :& i) :& i) :& i)
-> i -> (((((E :& i) :& i) :& i) :& i) :& i) :& i
forall tail head. tail -> head -> tail :& head
:&i
f((((((E :& i) :& i) :& i) :& i) :& i) :& i)
-> i -> ((((((E :& i) :& i) :& i) :& i) :& i) :& i) :& i
forall tail head. tail -> head -> tail :& head
:&i
g(((((((E :& i) :& i) :& i) :& i) :& i) :& i) :& i)
-> i -> (((((((E :& i) :& i) :& i) :& i) :& i) :& i) :& i) :& i
forall tail head. tail -> head -> tail :& head
:&i
h((((((((E :& i) :& i) :& i) :& i) :& i) :& i) :& i) :& i)
-> i
-> ((((((((E :& i) :& i) :& i) :& i) :& i) :& i) :& i) :& i) :& i
forall tail head. tail -> head -> tail :& head
:&i
i(((((((((E :& i) :& i) :& i) :& i) :& i) :& i) :& i) :& i) :& i)
-> i
-> (((((((((E :& i) :& i) :& i) :& i) :& i) :& i) :& i) :& i) :& i)
   :& i
forall tail head. tail -> head -> tail :& head
:&i
j((((((((((E :& i) :& i) :& i) :& i) :& i) :& i) :& i) :& i) :& i)
 :& i)
-> i
-> ((((((((((E :& i) :& i) :& i) :& i) :& i) :& i) :& i) :& i)
     :& i)
    :& i)
   :& i
forall tail head. tail -> head -> tail :& head
:&i
k(((((((((((E :& i) :& i) :& i) :& i) :& i) :& i) :& i) :& i) :& i)
  :& i)
 :& i)
-> i
-> (((((((((((E :& i) :& i) :& i) :& i) :& i) :& i) :& i) :& i)
      :& i)
     :& i)
    :& i)
   :& i
forall tail head. tail -> head -> tail :& head
:&i
l((((((((((((E :& i) :& i) :& i) :& i) :& i) :& i) :& i) :& i) :& i)
   :& i)
  :& i)
 :& i)
-> i
-> ((((((((((((E :& i) :& i) :& i) :& i) :& i) :& i) :& i) :& i)
       :& i)
      :& i)
     :& i)
    :& i)
   :& i
forall tail head. tail -> head -> tail :& head
:&i
m(((((((((((((E :& i) :& i) :& i) :& i) :& i) :& i) :& i) :& i)
     :& i)
    :& i)
   :& i)
  :& i)
 :& i)
-> i -> I14 i
forall tail head. tail -> head -> tail :& head
:&i
n
ind15 :: i
-> i
-> i
-> i
-> i
-> i
-> i
-> i
-> i
-> i
-> i
-> i
-> i
-> i
-> i
-> I15 i
ind15 i
a i
b i
c i
d i
e i
f i
g i
h i
i i
j i
k i
l i
m i
n i
o = E
EE -> i -> E :& i
forall tail head. tail -> head -> tail :& head
:&i
a(E :& i) -> i -> (E :& i) :& i
forall tail head. tail -> head -> tail :& head
:&i
b((E :& i) :& i) -> i -> ((E :& i) :& i) :& i
forall tail head. tail -> head -> tail :& head
:&i
c(((E :& i) :& i) :& i) -> i -> (((E :& i) :& i) :& i) :& i
forall tail head. tail -> head -> tail :& head
:&i
d((((E :& i) :& i) :& i) :& i)
-> i -> ((((E :& i) :& i) :& i) :& i) :& i
forall tail head. tail -> head -> tail :& head
:&i
e(((((E :& i) :& i) :& i) :& i) :& i)
-> i -> (((((E :& i) :& i) :& i) :& i) :& i) :& i
forall tail head. tail -> head -> tail :& head
:&i
f((((((E :& i) :& i) :& i) :& i) :& i) :& i)
-> i -> ((((((E :& i) :& i) :& i) :& i) :& i) :& i) :& i
forall tail head. tail -> head -> tail :& head
:&i
g(((((((E :& i) :& i) :& i) :& i) :& i) :& i) :& i)
-> i -> (((((((E :& i) :& i) :& i) :& i) :& i) :& i) :& i) :& i
forall tail head. tail -> head -> tail :& head
:&i
h((((((((E :& i) :& i) :& i) :& i) :& i) :& i) :& i) :& i)
-> i
-> ((((((((E :& i) :& i) :& i) :& i) :& i) :& i) :& i) :& i) :& i
forall tail head. tail -> head -> tail :& head
:&i
i(((((((((E :& i) :& i) :& i) :& i) :& i) :& i) :& i) :& i) :& i)
-> i
-> (((((((((E :& i) :& i) :& i) :& i) :& i) :& i) :& i) :& i) :& i)
   :& i
forall tail head. tail -> head -> tail :& head
:&i
j((((((((((E :& i) :& i) :& i) :& i) :& i) :& i) :& i) :& i) :& i)
 :& i)
-> i
-> ((((((((((E :& i) :& i) :& i) :& i) :& i) :& i) :& i) :& i)
     :& i)
    :& i)
   :& i
forall tail head. tail -> head -> tail :& head
:&i
k(((((((((((E :& i) :& i) :& i) :& i) :& i) :& i) :& i) :& i) :& i)
  :& i)
 :& i)
-> i
-> (((((((((((E :& i) :& i) :& i) :& i) :& i) :& i) :& i) :& i)
      :& i)
     :& i)
    :& i)
   :& i
forall tail head. tail -> head -> tail :& head
:&i
l((((((((((((E :& i) :& i) :& i) :& i) :& i) :& i) :& i) :& i) :& i)
   :& i)
  :& i)
 :& i)
-> i
-> ((((((((((((E :& i) :& i) :& i) :& i) :& i) :& i) :& i) :& i)
       :& i)
      :& i)
     :& i)
    :& i)
   :& i
forall tail head. tail -> head -> tail :& head
:&i
m(((((((((((((E :& i) :& i) :& i) :& i) :& i) :& i) :& i) :& i)
     :& i)
    :& i)
   :& i)
  :& i)
 :& i)
-> i
-> (((((((((((((E :& i) :& i) :& i) :& i) :& i) :& i) :& i) :& i)
        :& i)
       :& i)
      :& i)
     :& i)
    :& i)
   :& i
forall tail head. tail -> head -> tail :& head
:&i
n((((((((((((((E :& i) :& i) :& i) :& i) :& i) :& i) :& i) :& i)
      :& i)
     :& i)
    :& i)
   :& i)
  :& i)
 :& i)
-> i -> I15 i
forall tail head. tail -> head -> tail :& head
:&i
o

unsnoc :: [i] -> ([i], i)
unsnoc :: [i] -> ([i], i)
unsnoc    [i
i]   = ([], i
i)
unsnoc (i
i : [i]
is) = (i
i i -> [i] -> [i]
forall a. a -> [a] -> [a]
:) ([i] -> [i]) -> ([i], i) -> ([i], i)
forall (p :: * -> * -> *) a b c.
Bifunctor p =>
(a -> b) -> p a c -> p b c
`first` [i] -> ([i], i)
forall i. [i] -> ([i], i)
unsnoc [i]
is
unsnoc     [i]
_    = IndexException -> ([i], i)
forall a e. Exception e => e -> a
throw (IndexException -> ([i], i)) -> IndexException -> ([i], i)
forall a b. (a -> b) -> a -> b
$ String -> IndexException
UnexpectedRank String
"in SDP.Finite.fromList"