{-# LANGUAGE NoMonomorphismRestriction #-}
module Math.Combinatorics.Poset where
import Math.Common.ListSet as LS
import Math.Core.Utils
import Math.Core.Field
import Math.Combinatorics.FiniteGeometry
import Math.Algebra.LinearAlgebra
import Math.Combinatorics.Digraph
import Data.List as L
import qualified Data.Map as M
newtype Poset t = Poset ([t], t -> t -> Bool)
instance Eq t => Eq (Poset t) where
Poset (set :: [t]
set,po :: t -> t -> Bool
po) == :: Poset t -> Poset t -> Bool
== Poset (set' :: [t]
set',po' :: t -> t -> Bool
po') =
[t]
set [t] -> [t] -> Bool
forall a. Eq a => a -> a -> Bool
== [t]
set' Bool -> Bool -> Bool
&& [Bool] -> Bool
forall (t :: * -> *). Foldable t => t Bool -> Bool
and [t -> t -> Bool
po t
x t
y Bool -> Bool -> Bool
forall a. Eq a => a -> a -> Bool
== t -> t -> Bool
po' t
x t
y | t
x <- [t]
set, t
y <- [t]
set]
instance Show t => Show (Poset t) where
show :: Poset t -> String
show (Poset (set :: [t]
set,po :: t -> t -> Bool
po)) = "Poset " String -> ShowS
forall a. [a] -> [a] -> [a]
++ [t] -> String
forall a. Show a => a -> String
show [t]
set
implies :: Bool -> Bool -> Bool
implies p :: Bool
p q :: Bool
q = Bool
q Bool -> Bool -> Bool
|| Bool -> Bool
not Bool
p
isReflexive :: ([t], t -> t -> Bool) -> Bool
isReflexive (set :: [t]
set,po :: t -> t -> Bool
po) = [Bool] -> Bool
forall (t :: * -> *). Foldable t => t Bool -> Bool
and [t
x t -> t -> Bool
`po` t
x | t
x <- [t]
set]
isAntisymmetric :: ([a], a -> a -> Bool) -> Bool
isAntisymmetric (set :: [a]
set,po :: a -> a -> Bool
po) = [Bool] -> Bool
forall (t :: * -> *). Foldable t => t Bool -> Bool
and [((a
x a -> a -> Bool
`po` a
y) Bool -> Bool -> Bool
&& (a
y a -> a -> Bool
`po` a
x)) Bool -> Bool -> Bool
`implies` (a
x a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== a
y) | a
x <- [a]
set, a
y <- [a]
set]
isTransitive :: ([t], t -> t -> Bool) -> Bool
isTransitive (set :: [t]
set,po :: t -> t -> Bool
po) = [Bool] -> Bool
forall (t :: * -> *). Foldable t => t Bool -> Bool
and [((t
x t -> t -> Bool
`po` t
y) Bool -> Bool -> Bool
&& (t
y t -> t -> Bool
`po` t
z)) Bool -> Bool -> Bool
`implies` (t
x t -> t -> Bool
`po` t
z) | t
x <- [t]
set, t
y <- [t]
set, t
z <- [t]
set]
isPoset :: ([t], t -> t -> Bool) -> Bool
isPoset poset :: ([t], t -> t -> Bool)
poset = ([t], t -> t -> Bool) -> Bool
forall t. ([t], t -> t -> Bool) -> Bool
isReflexive ([t], t -> t -> Bool)
poset Bool -> Bool -> Bool
&& ([t], t -> t -> Bool) -> Bool
forall a. Eq a => ([a], a -> a -> Bool) -> Bool
isAntisymmetric ([t], t -> t -> Bool)
poset Bool -> Bool -> Bool
&& ([t], t -> t -> Bool) -> Bool
forall t. ([t], t -> t -> Bool) -> Bool
isTransitive ([t], t -> t -> Bool)
poset
poset :: ([t], t -> t -> Bool) -> Poset t
poset (set :: [t]
set,po :: t -> t -> Bool
po)
| ([t], t -> t -> Bool) -> Bool
forall a. Eq a => ([a], a -> a -> Bool) -> Bool
isPoset ([t]
set,t -> t -> Bool
po) = ([t], t -> t -> Bool) -> Poset t
forall t. ([t], t -> t -> Bool) -> Poset t
Poset ([t]
set,t -> t -> Bool
po)
| Bool
otherwise = String -> Poset t
forall a. HasCallStack => String -> a
error "poset: Not a partial order"
intervals :: Poset b -> [(b, b)]
intervals (Poset (set :: [b]
set,po :: b -> b -> Bool
po)) = [(b
a,b
b) | b
a <- [b]
set, b
b <- [b]
set, b
a b -> b -> Bool
`po` b
b]
interval :: Poset a -> (a, a) -> [a]
interval (Poset (set :: [a]
set,po :: a -> a -> Bool
po)) (x :: a
x,z :: a
z) = [a
y | a
y <- [a]
set, a
x a -> a -> Bool
`po` a
y, a
y a -> a -> Bool
`po` a
z]
chainN :: Int -> Poset Int
chainN :: Int -> Poset Int
chainN n :: Int
n = ([Int], Int -> Int -> Bool) -> Poset Int
forall t. ([t], t -> t -> Bool) -> Poset t
Poset ( [1..Int
n], Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
(<=) )
antichainN :: Int -> Poset Int
antichainN :: Int -> Poset Int
antichainN n :: Int
n = ([Int], Int -> Int -> Bool) -> Poset Int
forall t. ([t], t -> t -> Bool) -> Poset t
Poset ( [1..Int
n], Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
(==) )
divides :: a -> a -> Bool
divides a :: a
a b :: a
b = a
b a -> a -> a
forall a. Integral a => a -> a -> a
`rem` a
a a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== 0
divisors :: a -> [a]
divisors n :: a
n = [a] -> [a]
forall a. Ord a => [a] -> [a]
toSet [ a
d' | a
d <- (a -> Bool) -> [a] -> [a]
forall a. (a -> Bool) -> [a] -> [a]
takeWhile (\d :: a
d -> a
da -> a -> a
forall a. Num a => a -> a -> a
*a
d a -> a -> Bool
forall a. Ord a => a -> a -> Bool
<= a
n) [1..],
let (q :: a
q,r :: a
r) = a
n a -> a -> (a, a)
forall a. Integral a => a -> a -> (a, a)
`quotRem` a
d, a
r a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== 0,
a
d' <- [a
d,a
q] ]
posetD :: Int -> Poset Int
posetD :: Int -> Poset Int
posetD n :: Int
n | Int
n Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>= 1 = ([Int], Int -> Int -> Bool) -> Poset Int
forall t. ([t], t -> t -> Bool) -> Poset t
Poset ( Int -> [Int]
forall a. Integral a => a -> [a]
divisors Int
n, Int -> Int -> Bool
forall a. Integral a => a -> a -> Bool
divides )
powerset :: [a] -> [[a]]
powerset [] = [[]]
powerset (x :: a
x:xs :: [a]
xs) = let p :: [[a]]
p = [a] -> [[a]]
powerset [a]
xs in [[a]]
p [[a]] -> [[a]] -> [[a]]
forall a. [a] -> [a] -> [a]
++ ([a] -> [a]) -> [[a]] -> [[a]]
forall a b. (a -> b) -> [a] -> [b]
map (a
xa -> [a] -> [a]
forall a. a -> [a] -> [a]
:) [[a]]
p
posetB :: Int -> Poset [Int]
posetB :: Int -> Poset [Int]
posetB n :: Int
n = ([[Int]], [Int] -> [Int] -> Bool) -> Poset [Int]
forall t. ([t], t -> t -> Bool) -> Poset t
Poset ( [Int] -> [[Int]]
forall a. [a] -> [[a]]
powerset [1..Int
n], [Int] -> [Int] -> Bool
forall a. Ord a => [a] -> [a] -> Bool
LS.isSubset )
partitions :: [a] -> [[[a]]]
partitions [] = [[]]
partitions [x :: a
x] = [[[a
x]]]
partitions (x :: a
x:xs :: [a]
xs) = let ps :: [[[a]]]
ps = [a] -> [[[a]]]
partitions [a]
xs in
([[a]] -> [[a]]) -> [[[a]]] -> [[[a]]]
forall a b. (a -> b) -> [a] -> [b]
map ([a
x][a] -> [[a]] -> [[a]]
forall a. a -> [a] -> [a]
:) [[[a]]]
ps [[[a]]] -> [[[a]]] -> [[[a]]]
forall a. [a] -> [a] -> [a]
++ [ (a
xa -> [a] -> [a]
forall a. a -> [a] -> [a]
:[a]
cell)[a] -> [[a]] -> [[a]]
forall a. a -> [a] -> [a]
:[[a]]
p' | [[a]]
p <- [[[a]]]
ps, (cell :: [a]
cell,p' :: [[a]]
p') <- [[a]] -> [([a], [[a]])]
forall a. [a] -> [(a, [a])]
picks [[a]]
p]
isRefinement :: [[a]] -> [[a]] -> Bool
isRefinement a :: [[a]]
a b :: [[a]]
b = [Bool] -> Bool
forall (t :: * -> *). Foldable t => t Bool -> Bool
and [[Bool] -> Bool
forall (t :: * -> *). Foldable t => t Bool -> Bool
or [[a]
acell [a] -> [a] -> Bool
forall a. Ord a => [a] -> [a] -> Bool
`isSubset` [a]
bcell | [a]
bcell <- [[a]]
b] | [a]
acell <- [[a]]
a]
posetP :: Int -> Poset [[Int]]
posetP :: Int -> Poset [[Int]]
posetP n :: Int
n = ([[[Int]]], [[Int]] -> [[Int]] -> Bool) -> Poset [[Int]]
forall t. ([t], t -> t -> Bool) -> Poset t
Poset ( [Int] -> [[[Int]]]
forall a. [a] -> [[[a]]]
partitions [1..Int
n], [[Int]] -> [[Int]] -> Bool
forall a. Ord a => [[a]] -> [[a]] -> Bool
isRefinement )
intervalPartitions :: [a] -> [[[a]]]
intervalPartitions xs :: [a]
xs = ([[a]] -> Bool) -> [[[a]]] -> [[[a]]]
forall a. (a -> Bool) -> [a] -> [a]
filter (([a] -> Bool) -> [[a]] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all [a] -> Bool
forall a. (Eq a, Num a) => [a] -> Bool
isInterval) ([a] -> [[[a]]]
forall a. [a] -> [[[a]]]
partitions [a]
xs)
isInterval :: [a] -> Bool
isInterval (x1 :: a
x1:x2 :: a
x2:xs :: [a]
xs) = a
x1a -> a -> a
forall a. Num a => a -> a -> a
+1 a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== a
x2 Bool -> Bool -> Bool
&& [a] -> Bool
isInterval (a
x2a -> [a] -> [a]
forall a. a -> [a] -> [a]
:[a]
xs)
isInterval _ = Bool
True
intervalPartitions2 :: [a] -> [[[a]]]
intervalPartitions2 [] = [[]]
intervalPartitions2 [x :: a
x] = [[[a
x]]]
intervalPartitions2 (x :: a
x:xs :: [a]
xs) = let ips :: [[[a]]]
ips = [a] -> [[[a]]]
intervalPartitions2 [a]
xs in
([[a]] -> [[a]]) -> [[[a]]] -> [[[a]]]
forall a b. (a -> b) -> [a] -> [b]
map ([a
x][a] -> [[a]] -> [[a]]
forall a. a -> [a] -> [a]
:) [[[a]]]
ips [[[a]]] -> [[[a]]] -> [[[a]]]
forall a. [a] -> [a] -> [a]
++ [ (a
xa -> [a] -> [a]
forall a. a -> [a] -> [a]
:[a]
head)[a] -> [[a]] -> [[a]]
forall a. a -> [a] -> [a]
:[[a]]
tail | (head :: [a]
head:tail :: [[a]]
tail) <- [[[a]]]
ips]
integerPartitions :: a -> [[a]]
integerPartitions n :: a
n | a
n a -> a -> Bool
forall a. Ord a => a -> a -> Bool
>= 0 = a -> a -> [[a]]
forall a. (Num a, Ord a) => a -> a -> [[a]]
ips a
n a
n where
ips :: a -> a -> [[a]]
ips 0 _ = [[]]
ips _ 0 = []
ips n :: a
n m :: a
m | a
m a -> a -> Bool
forall a. Ord a => a -> a -> Bool
<= a
n = ([a] -> [a]) -> [[a]] -> [[a]]
forall a b. (a -> b) -> [a] -> [b]
map (a
ma -> [a] -> [a]
forall a. a -> [a] -> [a]
:) (a -> a -> [[a]]
ips (a
na -> a -> a
forall a. Num a => a -> a -> a
-a
m) a
m) [[a]] -> [[a]] -> [[a]]
forall a. [a] -> [a] -> [a]
++ a -> a -> [[a]]
ips a
n (a
ma -> a -> a
forall a. Num a => a -> a -> a
-1)
| Bool
otherwise = a -> a -> [[a]]
ips a
n a
n
isIPRefinement :: [a] -> [a] -> Bool
isIPRefinement ys :: [a]
ys xs :: [a]
xs = [a] -> [a] -> Bool
forall a. (Ord a, Num a) => [a] -> [a] -> Bool
dfs [a]
xs [a]
ys
where dfs :: [a] -> [a] -> Bool
dfs (x :: a
x:xs :: [a]
xs) (y :: a
y:ys :: [a]
ys) | a
x a -> a -> Bool
forall a. Ord a => a -> a -> Bool
< a
y = Bool
False
| a
x a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== a
y = [a] -> [a] -> Bool
dfs [a]
xs [a]
ys
| Bool
otherwise = [Bool] -> Bool
forall (t :: * -> *). Foldable t => t Bool -> Bool
or [[a] -> [a] -> Bool
dfs [a]
xs' [a]
ys' | (y' :: a
y', ys' :: [a]
ys') <- [a] -> [(a, [a])]
forall a. [a] -> [(a, [a])]
picks (a
ya -> [a] -> [a]
forall a. a -> [a] -> [a]
:[a]
ys),
let xs' :: [a]
xs' = a -> [a] -> [a]
forall a. Ord a => a -> [a] -> [a]
insertDesc (a
xa -> a -> a
forall a. Num a => a -> a -> a
-a
y') [a]
xs]
dfs [] [] = Bool
True
insertDesc :: a -> [a] -> [a]
insertDesc = (a -> a -> Ordering) -> a -> [a] -> [a]
forall a. (a -> a -> Ordering) -> a -> [a] -> [a]
L.insertBy ((a -> a -> Ordering) -> a -> a -> Ordering
forall a b c. (a -> b -> c) -> b -> a -> c
flip a -> a -> Ordering
forall a. Ord a => a -> a -> Ordering
compare)
posetIP :: Int -> Poset [Int]
posetIP :: Int -> Poset [Int]
posetIP n :: Int
n = ([[Int]], [Int] -> [Int] -> Bool) -> Poset [Int]
forall t. ([t], t -> t -> Bool) -> Poset t
Poset (Int -> [[Int]]
forall a. (Ord a, Num a) => a -> [[a]]
integerPartitions Int
n, [Int] -> [Int] -> Bool
forall a. (Ord a, Num a) => [a] -> [a] -> Bool
isIPRefinement)
subspaces :: [a] -> Int -> [[[a]]]
subspaces fq :: [a]
fq n :: Int
n = [] [[a]] -> [[[a]]] -> [[[a]]]
forall a. a -> [a] -> [a]
: (Int -> [[[a]]]) -> [Int] -> [[[a]]]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (Int -> [a] -> Int -> [[[a]]]
forall a. (Eq a, Num a) => Int -> [a] -> Int -> [[[a]]]
flatsPG (Int
nInt -> Int -> Int
forall a. Num a => a -> a -> a
-1) [a]
fq) [0..Int
nInt -> Int -> Int
forall a. Num a => a -> a -> a
-1]
isSubspace :: t [a] -> [[a]] -> Bool
isSubspace s1 :: t [a]
s1 s2 :: [[a]]
s2 = ([a] -> Bool) -> t [a] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all ([[a]] -> [a] -> Bool
forall a. (Eq a, Num a) => [[a]] -> [a] -> Bool
inSpanRE [[a]]
s2) t [a]
s1
posetL :: (Eq fq, Num fq) => Int -> [fq] -> Poset [[fq]]
posetL :: Int -> [fq] -> Poset [[fq]]
posetL n :: Int
n fq :: [fq]
fq = ([[[fq]]], [[fq]] -> [[fq]] -> Bool) -> Poset [[fq]]
forall t. ([t], t -> t -> Bool) -> Poset t
Poset ( [fq] -> Int -> [[[fq]]]
forall a. (Eq a, Num a) => [a] -> Int -> [[[a]]]
subspaces [fq]
fq Int
n, [[fq]] -> [[fq]] -> Bool
forall (t :: * -> *) a.
(Foldable t, Eq a, Num a) =>
t [a] -> [[a]] -> Bool
isSubspace )
subposet :: Poset a -> (a -> Bool) -> Poset a
subposet :: Poset a -> (a -> Bool) -> Poset a
subposet (Poset (set :: [a]
set,po :: a -> a -> Bool
po)) p :: a -> Bool
p = ([a], a -> a -> Bool) -> Poset a
forall t. ([t], t -> t -> Bool) -> Poset t
Poset ((a -> Bool) -> [a] -> [a]
forall a. (a -> Bool) -> [a] -> [a]
filter a -> Bool
p [a]
set, a -> a -> Bool
po)
dsum :: Poset a -> Poset b -> Poset (Either a b)
dsum :: Poset a -> Poset b -> Poset (Either a b)
dsum (Poset (setA :: [a]
setA,poA :: a -> a -> Bool
poA)) (Poset (setB :: [b]
setB,poB :: b -> b -> Bool
poB)) = ([Either a b], Either a b -> Either a b -> Bool)
-> Poset (Either a b)
forall t. ([t], t -> t -> Bool) -> Poset t
Poset ([Either a b]
set,Either a b -> Either a b -> Bool
po)
where set :: [Either a b]
set = (a -> Either a b) -> [a] -> [Either a b]
forall a b. (a -> b) -> [a] -> [b]
map a -> Either a b
forall a b. a -> Either a b
Left [a]
setA [Either a b] -> [Either a b] -> [Either a b]
forall a. [a] -> [a] -> [a]
++ (b -> Either a b) -> [b] -> [Either a b]
forall a b. (a -> b) -> [a] -> [b]
map b -> Either a b
forall a b. b -> Either a b
Right [b]
setB
po :: Either a b -> Either a b -> Bool
po (Left a1 :: a
a1) (Left a2 :: a
a2) = a -> a -> Bool
poA a
a1 a
a2
po (Right b1 :: b
b1) (Right b2 :: b
b2) = b -> b -> Bool
poB b
b1 b
b2
po _ _ = Bool
False
dprod :: Poset a -> Poset b -> Poset (a,b)
dprod :: Poset a -> Poset b -> Poset (a, b)
dprod (Poset (setA :: [a]
setA,poA :: a -> a -> Bool
poA)) (Poset (setB :: [b]
setB,poB :: b -> b -> Bool
poB)) =
([(a, b)], (a, b) -> (a, b) -> Bool) -> Poset (a, b)
forall t. ([t], t -> t -> Bool) -> Poset t
Poset ( [(a
a,b
b) | a
a <- [a]
setA, b
b <- [b]
setB], \(a1 :: a
a1,b1 :: b
b1) (a2 :: a
a2,b2 :: b
b2) -> (a
a1 a -> a -> Bool
`poA` a
a2) Bool -> Bool -> Bool
&& (b
b1 b -> b -> Bool
`poB` b
b2) )
dual :: Poset a -> Poset a
dual :: Poset a -> Poset a
dual (Poset (set :: [a]
set, po :: a -> a -> Bool
po)) = ([a], a -> a -> Bool) -> Poset a
forall t. ([t], t -> t -> Bool) -> Poset t
Poset ([a]
set, a -> a -> Bool
po')
where po' :: a -> a -> Bool
po' x :: a
x y :: a
y = a -> a -> Bool
po a
y a
x
hasseDigraph :: (Eq a) => Poset a -> Digraph a
hasseDigraph :: Poset a -> Digraph a
hasseDigraph (Poset (set :: [a]
set,po :: a -> a -> Bool
po)) = [a] -> [(a, a)] -> Digraph a
forall v. [v] -> [(v, v)] -> Digraph v
DG [a]
set [(a
x,a
y) | a
x <- [a]
set, a
y <- [a]
set, a
x a -> a -> Bool
-< a
y]
where x :: a
x -< :: a -> a -> Bool
-< y :: a
y = a
x a -> a -> Bool
forall a. Eq a => a -> a -> Bool
/= a
y Bool -> Bool -> Bool
&& a
x a -> a -> Bool
`po` a
y Bool -> Bool -> Bool
&& [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [a
z | a
z <- [a]
set, a
x a -> a -> Bool
`po` a
z, a
x a -> a -> Bool
forall a. Eq a => a -> a -> Bool
/= a
z, a
z a -> a -> Bool
`po` a
y, a
z a -> a -> Bool
forall a. Eq a => a -> a -> Bool
/= a
y]
reachabilityPoset :: (Ord a) => Digraph a -> Poset a
reachabilityPoset :: Digraph a -> Poset a
reachabilityPoset (DG vs :: [a]
vs es :: [(a, a)]
es) = ([a], a -> a -> Bool) -> Poset a
forall t. ([t], t -> t -> Bool) -> Poset t
Poset ([a]
vs,a -> a -> Bool
tc')
where tc :: Map (a, a) Bool
tc = [((a, a), Bool)] -> Map (a, a) Bool
forall k a. Ord k => [(k, a)] -> Map k a
M.fromList [ ((a
u,a
v), a -> a -> Bool
tc' a
u a
v) | a
u <- [a]
vs, a
v <- [a]
vs]
tc' :: a -> a -> Bool
tc' u :: a
u v :: a
v | a
u a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== a
v = Bool
True
| Bool
otherwise = [Bool] -> Bool
forall (t :: * -> *). Foldable t => t Bool -> Bool
or [Map (a, a) Bool
tc Map (a, a) Bool -> (a, a) -> Bool
forall k a. Ord k => Map k a -> k -> a
M.! (a
w,a
v) | a
w <- a -> [a]
successors a
u]
successors :: a -> [a]
successors u :: a
u = [a
v | (u' :: a
u',v :: a
v) <- [(a, a)]
es, a
u' a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== a
u]
isOrderPreserving :: (a -> b) -> Poset a -> Poset b -> Bool
isOrderPreserving :: (a -> b) -> Poset a -> Poset b -> Bool
isOrderPreserving f :: a -> b
f (Poset (seta :: [a]
seta,poa :: a -> a -> Bool
poa)) (Poset (setb :: [b]
setb,pob :: b -> b -> Bool
pob)) =
[Bool] -> Bool
forall (t :: * -> *). Foldable t => t Bool -> Bool
and [ a
x a -> a -> Bool
`poa` a
y Bool -> Bool -> Bool
forall a. Eq a => a -> a -> Bool
== a -> b
f a
x b -> b -> Bool
`pob` a -> b
f a
y | a
x <- [a]
seta, a
y <- [a]
seta ]
orderIsos01 :: Poset a -> Poset a -> [[(a, a)]]
orderIsos01 (Poset (seta :: [a]
seta,poa :: a -> a -> Bool
poa)) (Poset (setb :: [a]
setb,pob :: a -> a -> Bool
pob))
| [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [a]
seta Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
/= [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [a]
setb = []
| Bool
otherwise = [(a, a)] -> [a] -> [a] -> [[(a, a)]]
orderIsos' [] [a]
seta [a]
setb
where orderIsos' :: [(a, a)] -> [a] -> [a] -> [[(a, a)]]
orderIsos' xys :: [(a, a)]
xys [] [] = [[(a, a)]
xys]
orderIsos' xys :: [(a, a)]
xys (x :: a
x:xs :: [a]
xs) ys :: [a]
ys =
[[[(a, a)]]] -> [[(a, a)]]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [ [(a, a)] -> [a] -> [a] -> [[(a, a)]]
orderIsos' ((a
x,a
y)(a, a) -> [(a, a)] -> [(a, a)]
forall a. a -> [a] -> [a]
:[(a, a)]
xys) [a]
xs [a]
ys'
| (y :: a
y,ys' :: [a]
ys') <- [a] -> [(a, [a])]
forall a. [a] -> [(a, [a])]
picks [a]
ys,
[Bool] -> Bool
forall (t :: * -> *). Foldable t => t Bool -> Bool
and [ (a
x a -> a -> Bool
`poa` a
x', a
x' a -> a -> Bool
`poa` a
x) (Bool, Bool) -> (Bool, Bool) -> Bool
forall a. Eq a => a -> a -> Bool
== (a
y a -> a -> Bool
`pob` a
y', a
y' a -> a -> Bool
`pob` a
y) | (x' :: a
x',y' :: a
y') <- [(a, a)]
xys ] ]
isOrderIso :: (Ord a, Ord b) => Poset a -> Poset b -> Bool
isOrderIso :: Poset a -> Poset b -> Bool
isOrderIso poseta :: Poset a
poseta posetb :: Poset b
posetb = (Bool -> Bool
not (Bool -> Bool) -> ([[(a, b)]] -> Bool) -> [[(a, b)]] -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [[(a, b)]] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null) (Poset a -> Poset b -> [[(a, b)]]
forall a b. (Ord a, Ord b) => Poset a -> Poset b -> [[(a, b)]]
orderIsos Poset a
poseta Poset b
posetb)
orderIsos :: (Ord a, Ord b) => Poset a -> Poset b -> [[(a,b)]]
orderIsos :: Poset a -> Poset b -> [[(a, b)]]
orderIsos posetA :: Poset a
posetA@(Poset (_,poa :: a -> a -> Bool
poa)) posetB :: Poset b
posetB@(Poset (_,pob :: b -> b -> Bool
pob))
| ([a] -> Int) -> [[a]] -> [Int]
forall a b. (a -> b) -> [a] -> [b]
map [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [[a]]
heightPartA [Int] -> [Int] -> Bool
forall a. Eq a => a -> a -> Bool
/= ([b] -> Int) -> [[b]] -> [Int]
forall a b. (a -> b) -> [a] -> [b]
map [b] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [[b]]
heightPartB = []
| Bool
otherwise = [(a, b)] -> [[a]] -> [[b]] -> [[(a, b)]]
dfs [] [[a]]
heightPartA [[b]]
heightPartB
where heightPartA :: [[a]]
heightPartA = Digraph a -> [[a]]
forall k. Ord k => Digraph k -> [[k]]
heightPartitionDAG (Poset a -> Digraph a
forall a. Eq a => Poset a -> Digraph a
hasseDigraph Poset a
posetA)
heightPartB :: [[b]]
heightPartB = Digraph b -> [[b]]
forall k. Ord k => Digraph k -> [[k]]
heightPartitionDAG (Poset b -> Digraph b
forall a. Eq a => Poset a -> Digraph a
hasseDigraph Poset b
posetB)
dfs :: [(a, b)] -> [[a]] -> [[b]] -> [[(a, b)]]
dfs xys :: [(a, b)]
xys [] [] = [[(a, b)]
xys]
dfs xys :: [(a, b)]
xys ([]:las :: [[a]]
las) ([]:lbs :: [[b]]
lbs) = [(a, b)] -> [[a]] -> [[b]] -> [[(a, b)]]
dfs [(a, b)]
xys [[a]]
las [[b]]
lbs
dfs xys :: [(a, b)]
xys ((x :: a
x:xs :: [a]
xs):las :: [[a]]
las) (ys :: [b]
ys:lbs :: [[b]]
lbs) =
[[[(a, b)]]] -> [[(a, b)]]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [ [(a, b)] -> [[a]] -> [[b]] -> [[(a, b)]]
dfs ((a
x,b
y)(a, b) -> [(a, b)] -> [(a, b)]
forall a. a -> [a] -> [a]
:[(a, b)]
xys) ([a]
xs[a] -> [[a]] -> [[a]]
forall a. a -> [a] -> [a]
:[[a]]
las) ([b]
ys' [b] -> [[b]] -> [[b]]
forall a. a -> [a] -> [a]
: [[b]]
lbs)
| (y :: b
y,ys' :: [b]
ys') <- [b] -> [(b, [b])]
forall a. [a] -> [(a, [a])]
picks [b]
ys,
[Bool] -> Bool
forall (t :: * -> *). Foldable t => t Bool -> Bool
and [ (a
x a -> a -> Bool
`poa` a
x', a
x' a -> a -> Bool
`poa` a
x) (Bool, Bool) -> (Bool, Bool) -> Bool
forall a. Eq a => a -> a -> Bool
== (b
y b -> b -> Bool
`pob` b
y', b
y' b -> b -> Bool
`pob` b
y) | (x' :: a
x',y' :: b
y') <- [(a, b)]
xys ] ]
orderAuts1 :: Poset b -> [[(b, b)]]
orderAuts1 poset :: Poset b
poset = Poset b -> Poset b -> [[(b, b)]]
forall a b. (Ord a, Ord b) => Poset a -> Poset b -> [[(a, b)]]
orderIsos Poset b
poset Poset b
poset
isLinext :: Poset t -> [t] -> Bool
isLinext (Poset (set :: [t]
set,po :: t -> t -> Bool
po)) set' :: [t]
set' = ((t, t) -> Bool) -> [(t, t)] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (\(x :: t
x,y :: t
y) -> Bool -> Bool
not (t
y t -> t -> Bool
`po` t
x)) ([t] -> [(t, t)]
forall t. [t] -> [(t, t)]
pairs [t]
set')
linexts :: Poset t -> [[t]]
linexts (Poset (set :: [t]
set,po :: t -> t -> Bool
po)) = [[t]] -> [t] -> [[t]]
linexts' [[]] [t]
set
where linexts' :: [[t]] -> [t] -> [[t]]
linexts' lss :: [[t]]
lss (r :: t
r:rs :: [t]
rs) =
let lss' :: [[t]]
lss' = [ [t]
lts [t] -> [t] -> [t]
forall a. [a] -> [a] -> [a]
++ [t
r] [t] -> [t] -> [t]
forall a. [a] -> [a] -> [a]
++ [t]
gts
| [t]
ls <- [[t]]
lss,
let ls' :: [t]
ls' = (t -> Bool) -> [t] -> [t]
forall a. (a -> Bool) -> [a] -> [a]
takeWhile (Bool -> Bool
not (Bool -> Bool) -> (t -> Bool) -> t -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (t
r t -> t -> Bool
`po`)) [t]
ls,
(lts :: [t]
lts,gts :: [t]
gts) <- [[t]] -> [[t]] -> [([t], [t])]
forall a b. [a] -> [b] -> [(a, b)]
zip ([t] -> [[t]]
forall a. [a] -> [[a]]
inits [t]
ls') ([t] -> [[t]]
forall a. [a] -> [[a]]
tails [t]
ls),
(t -> Bool) -> [t] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (Bool -> Bool
not (Bool -> Bool) -> (t -> Bool) -> t -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (t -> t -> Bool
`po` t
r)) [t]
gts ]
in [[t]] -> [t] -> [[t]]
linexts' [[t]]
lss' [t]
rs
linexts' lss :: [[t]]
lss [] = [[t]]
lss