{-# LANGUAGE UndecidableInstances, FlexibleInstances, FlexibleContexts #-}
{-# LANGUAGE Trustworthy, TypeFamilies, TypeOperators, OverloadedLists #-}
module SDP.Finite
(
E (..), (:&) (..),
I1, I2, I3, I4, I5, I6, I7, I8, I9, I10, I11, I12, I13, I14, I15,
ind2, ind3, ind4, ind5, ind6, ind7, ind8, ind9,
ind10, ind11, ind12, ind13, ind14, ind15
)
where
import Prelude ( (++) )
import SDP.SafePrelude
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 ()
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 []
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
succ :: (E :& i) -> E :& i
succ = \ [Item (E :& i)
e] -> [i -> i
forall a. Enum a => a -> a
succ i
Item (E :& i)
e]
pred :: (E :& i) -> E :& i
pred = \ [Item (E :& i)
e] -> [i -> i
forall a. Enum a => a -> a
pred i
Item (E :& i)
e]
toEnum :: Int -> E :& i
toEnum = \ Int
n -> [Int -> i
forall a. Enum a => Int -> a
toEnum Int
n]
fromEnum :: (E :& i) -> Int
fromEnum = \ [Item (E :& i)
e] -> i -> Int
forall a. Enum a => a -> Int
fromEnum i
Item (E :& i)
e
enumFrom :: (E :& i) -> [E :& i]
enumFrom = \ [Item (E :& i)
f] -> [ [i
Item (E :& i)
e] | i
e <- [Item [i]
Item (E :& i)
f ..] ]
enumFromTo :: (E :& i) -> (E :& i) -> [E :& i]
enumFromTo = \ [Item (E :& i)
f] [Item (E :& i)
l] -> [ [i
Item (E :& i)
e] | i
e <- [Item [i]
Item (E :& i)
f .. Item [i]
Item (E :& i)
l] ]
enumFromThen :: (E :& i) -> (E :& i) -> [E :& i]
enumFromThen = \ [Item (E :& i)
f] [Item (E :& i)
n] -> [ [i
Item (E :& i)
e] | i
e <- [Item [i]
Item (E :& i)
f, Item [i]
Item (E :& i)
n ..] ]
enumFromThenTo :: (E :& i) -> (E :& i) -> (E :& i) -> [E :& i]
enumFromThenTo = \ [Item (E :& i)
f] [Item (E :& i)
n] [Item (E :& i)
l] -> [ [i
Item (E :& i)
e] | i
e <- [Item [i]
Item (E :& i)
f, Item [i]
Item (E :& i)
n .. Item [i]
Item (E :& 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
instance (IsList (i' :& i), E.Item (i' :& i) ~~ i, Show i) => Show (i' :& i)
where
showsPrec :: Int -> (i' :& i) -> ShowS
showsPrec Int
p = Int -> [i] -> ShowS
forall a. Show a => Int -> a -> ShowS
showsPrec Int
p ([i] -> ShowS) -> ((i' :& i) -> [i]) -> (i' :& i) -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (i' :& 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 [i]
i] = E
E E -> i -> E :& i
forall tail head. tail -> head -> tail :& head
:& i
Item [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 [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
Item [i]
i]
fromList :: [Item ((i' :& i) :& i)] -> (i' :& i) :& i
fromList = (([i] -> i -> (i' :& i) :& i) -> ([i], i) -> (i' :& i) :& i
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry (([i] -> i -> (i' :& i) :& i) -> ([i], i) -> (i' :& i) :& i)
-> ([i] -> i -> (i' :& i) :& 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)
-> ([i] -> i' :& i) -> [i] -> i -> (i' :& i) :& i
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [i] -> i' :& i
forall l. IsList l => [Item l] -> l
E.fromList) (([i], i) -> (i' :& i) :& i)
-> ([i] -> ([i], i)) -> [i] -> (i' :& i) :& i
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [i] -> ([i], i)
forall i. [i] -> ([i], i)
unsnoc
type I1 i = E :& i
type I2 i = E :& i :& i
type I3 i = (I2 i) :& i
type I4 i = (I3 i) :& i
type I5 i = (I4 i) :& i
type I6 i = (I5 i) :& i
type I7 i = (I6 i) :& i
type I8 i = (I7 i) :& i
type I9 i = (I8 i) :& i
type I10 i = (I9 i) :& i
type I11 i = (I10 i) :& i
type I12 i = (I11 i) :& i
type I13 i = (I12 i) :& i
type I14 i = (I13 i) :& i
type I15 i = (I14 i) :& i
ind2 :: i -> i -> I2 i
ind3 :: i -> i -> i -> I3 i
ind4 :: i -> i -> i -> i -> I4 i
ind5 :: i -> i -> i -> i -> i -> I5 i
ind6 :: i -> i -> i -> i -> i -> i -> I6 i
ind7 :: i -> i -> i -> i -> i -> i -> i -> I7 i
ind8 :: i -> i -> i -> i -> i -> i -> i -> i -> I8 i
ind9 :: i -> i -> i -> i -> i -> i -> i -> i -> i -> I9 i
ind10 :: i -> i -> i -> i -> i -> i -> i -> i -> i -> i -> I10 i
ind11 :: i -> i -> i -> i -> i -> i -> i -> i -> i -> i -> i -> I11 i
ind12 :: i -> i -> i -> i -> i -> i -> i -> i -> i -> i -> i -> i -> I12 i
ind13 :: i -> i -> i -> i -> i -> i -> i -> i -> i -> i -> i -> i -> i -> I13 i
ind14 :: i -> i -> i -> i -> i -> i -> i -> i -> i -> i -> i -> i -> i -> i -> I14 i
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 = [i
Item (I2 i)
a,i
Item (I2 i)
b]
ind3 :: i -> i -> i -> I3 i
ind3 i
a i
b i
c = [i
Item (I3 i)
a,i
Item (I3 i)
b,i
Item (I3 i)
c]
ind4 :: i -> i -> i -> i -> I4 i
ind4 i
a i
b i
c i
d = [i
Item (I4 i)
a,i
Item (I4 i)
b,i
Item (I4 i)
c,i
Item (I4 i)
d]
ind5 :: i -> i -> i -> i -> i -> I5 i
ind5 i
a i
b i
c i
d i
e = [i
Item (I5 i)
a,i
Item (I5 i)
b,i
Item (I5 i)
c,i
Item (I5 i)
d,i
Item (I5 i)
e]
ind6 :: i -> i -> i -> i -> i -> i -> I6 i
ind6 i
a i
b i
c i
d i
e i
f = [i
Item (I6 i)
a,i
Item (I6 i)
b,i
Item (I6 i)
c,i
Item (I6 i)
d,i
Item (I6 i)
e,i
Item (I6 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 = [i
Item (I7 i)
a,i
Item (I7 i)
b,i
Item (I7 i)
c,i
Item (I7 i)
d,i
Item (I7 i)
e,i
Item (I7 i)
f,i
Item (I7 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 = [i
Item (I8 i)
a,i
Item (I8 i)
b,i
Item (I8 i)
c,i
Item (I8 i)
d,i
Item (I8 i)
e,i
Item (I8 i)
f,i
Item (I8 i)
g,i
Item (I8 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 = [i
Item (I9 i)
a,i
Item (I9 i)
b,i
Item (I9 i)
c,i
Item (I9 i)
d,i
Item (I9 i)
e,i
Item (I9 i)
f,i
Item (I9 i)
g,i
Item (I9 i)
h,i
Item (I9 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 = [i
Item (I10 i)
a,i
Item (I10 i)
b,i
Item (I10 i)
c,i
Item (I10 i)
d,i
Item (I10 i)
e,i
Item (I10 i)
f,i
Item (I10 i)
g,i
Item (I10 i)
h,i
Item (I10 i)
i,i
Item (I10 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 = [i
Item (I11 i)
a,i
Item (I11 i)
b,i
Item (I11 i)
c,i
Item (I11 i)
d,i
Item (I11 i)
e,i
Item (I11 i)
f,i
Item (I11 i)
g,i
Item (I11 i)
h,i
Item (I11 i)
i,i
Item (I11 i)
j,i
Item (I11 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 = [i
Item (I12 i)
a,i
Item (I12 i)
b,i
Item (I12 i)
c,i
Item (I12 i)
d,i
Item (I12 i)
e,i
Item (I12 i)
f,i
Item (I12 i)
g,i
Item (I12 i)
h,i
Item (I12 i)
i,i
Item (I12 i)
j,i
Item (I12 i)
k,i
Item (I12 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 = [i
Item (I13 i)
a,i
Item (I13 i)
b,i
Item (I13 i)
c,i
Item (I13 i)
d,i
Item (I13 i)
e,i
Item (I13 i)
f,i
Item (I13 i)
g,i
Item (I13 i)
h,i
Item (I13 i)
i,i
Item (I13 i)
j,i
Item (I13 i)
k,i
Item (I13 i)
l,i
Item (I13 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 = [i
Item (I14 i)
a,i
Item (I14 i)
b,i
Item (I14 i)
c,i
Item (I14 i)
d,i
Item (I14 i)
e,i
Item (I14 i)
f,i
Item (I14 i)
g,i
Item (I14 i)
h,i
Item (I14 i)
i,i
Item (I14 i)
j,i
Item (I14 i)
k,i
Item (I14 i)
l,i
Item (I14 i)
m,i
Item (I14 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 = [i
Item (I15 i)
a,i
Item (I15 i)
b,i
Item (I15 i)
c,i
Item (I15 i)
d,i
Item (I15 i)
e,i
Item (I15 i)
f,i
Item (I15 i)
g,i
Item (I15 i)
h,i
Item (I15 i)
i,i
Item (I15 i)
j,i
Item (I15 i)
k,i
Item (I15 i)
l,i
Item (I15 i)
m,i
Item (I15 i)
n,i
Item (I15 i)
o]
unsnoc :: [i] -> ([i], i)
unsnoc :: [i] -> ([i], i)
unsnoc [Item [i]
i] = ([], i
Item [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"