    -- Copyright (c) 2011, David Amos. All rights reserved.

    {-# LANGUAGE NoMonomorphismRestriction #-}

    module Math.Combinatorics.Poset where

    import Math.Common.ListSet as LS -- set operations on strictly ascending lists
    import Math.Core.Utils -- for set/multiset operations on ordered lists
    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
    -- import qualified Data.Set as S

    -- |A poset is represented as a pair (set,po), where set is the underlying set of the poset, and po is the partial order relation
    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]
    -- There may be ways to avoid comparing every pair
    -- If we could calculate the coverGraph without comparing every pair,
    -- then it would be sufficient to test whether their cover graphs are equal

    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"

    -- Most of the posets we will deal with are in fact lattices, meaning that any two elements
    -- have a meet (greatest lower bound) and join (least upper bound)

    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]

    -- LINEAR ORDER POSET
    -- This is of course a lattice, with meet = min, join = max

    -- |A chain is a poset in which every pair of elements is comparable (ie either x <= y or y <= x).
    -- It is therefore a linear or total order.
    -- chainN n is the poset consisting of the numbers [1..n] ordered by (<=)
    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
    (<=) )

    -- hasseN n = DG [1..n] [(i,i+1) | i <- [1..n-1]]

    -- |An antichain is a poset in which distinct elements are incomparable.
    -- antichainN n is the poset consisting of [1..n], with x <= y only when x == y.
    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
    (==) )

    -- LATTICE OF (POSITIVE) DIVISORS OF N

    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] ]
    -- The toSet call sorts, and deduplicates if n is a square
    -- divisors n | n >= 1 = [a | a <- [1..n], a `divides` n]

    -- |posetD n is the lattice of (positive) divisors of n
    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 )

    -- LATTICE OF SUBSETS OF [1..N] ORDERED BY INCLUSION
    -- (Boolean lattice)

    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

    {-
    -- subset test for sorted lists
    isSubset (x:xs) (y:ys) =
        case compare x y of
        LT -> False
        EQ -> isSubset xs ys
        GT -> isSubset (x:xs) ys
    isSubset [] _ = True
    isSubset _ [] = False
    -}

    -- |posetB n is the lattice of subsets of [1..n] ordered by inclusion
    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 )

    -- LATTICE OF SET PARTITIONS OF [1..N] ORDERED BY REFINEMENT

    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]
    -- if the input is sorted, then so is the output

    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]
    -- if we know that a and b are appropriately sorted, then this can probably be done more efficiently

    -- |posetP n is the lattice of set partitions of [1..n], ordered by refinement
    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 )

    -- muP n = ...
    -- see van Lint and Wilson p336

    -- LATTICE OF INTERVAL PARTITIONS OF [1..N] ORDERED BY REFINEMENT
    -- Interval partitions of [1..n] correspond to compositions of n

    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]
    -- we're guaranteed that x+1 is at the head of the head

    -- LATTICE OF INTEGER PARTITIONS OF N ORDERED BY REFINEMENT

    -- For example, integerPartitions 5 -> [ [5], [4,1], [3,2], [3,1,1], [2,2,1], [2,1,1,1], [1,1,1,1,1] ]
    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)

    {-
    -- In theory it feels like this ought to be faster for large n, but in practice it's unclear
    isIPRefinement2 ys xs = isIPRefinement (ys \\ xs) (xs \\ ys)
        where (\\) = diffDesc
    -}

    -- |posetIP n is the poset of integer partitions of n, ordered by refinement
    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)

    -- Could also implement the Young lattice (or the part up to n)
    -- Of integer partitions <= n, ordered by inclusion
    -- Kassel, Turaev, Braid Groups, p202

    -- INTEGER COMPOSITIONS

    -- LATTICE OF SUBSPACES OF Fq^n

    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]
    -- note that flatsPG returns the subspaces as a matrix of row vectors in reduced row echelon form

    -- inSpanRE m v returns whether the vector v is in the span of the rows of the matrix m, where m is required to be in row echelon form
    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

    -- This is the projective geometry PG(n,q)
    -- |posetL n fq is the lattice of subspaces of the vector space Fq^n, ordered by inclusion.
    -- Subspaces are represented by their reduced row echelon form.
    -- Example usage: posetL 2 f3
    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 )

    -- choose n k = product [n-k+1..n] `div` product [1..k]

    -- NEW FROM OLD CONSTRUCTIONS

    -- |The subposet of a poset satisfying a predicate
    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)

    -- |The direct sum of two posets
    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

    -- |The direct product of two posets
    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) )

    -- |The dual of a poset
    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

    -- ANALYSIS OF POSETS

    -- |Given a poset (X,<=), we say that y covers x, written x -< y, if x < y and there is no z in X with x < z < y.
    -- The Hasse digraph of a poset is the digraph whose vertices are the elements of the poset,
    -- with an edge between every pair (x,y) with x -< y.
    -- The Hasse digraph can be represented diagrammatically as a Hasse diagram, by drawing x below y whenever x -< y.
    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]
    -- The partial order can be recovered as the transitive closure of the covers relation
    -- !! Can we construct the cover graph without having to compare every pair ??

    -- If we know in advance the poset we're interested in,
    -- then we're probably better off constructing the Hasse digraph directly

    -- (In effect, the transitive closure of the edge relation)
    -- |Given a DAG (directed acyclic graph), return the poset consisting of the vertices of the DAG, ordered by reachability.
    -- This can be used to recover a poset from its Hasse digraph.
    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') -- \u v -> tc M.! (u,v)
        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]
    -- !! looks like we could memoise more than we are doing

    {-
    -- For example:
    > let poset = posetB 3 in poset == reachabilityPoset (hasseDigraph poset)
    True
    -}

    -- This definition is incorrect. This is an order embedding. Order preserving only requires the rightward implication.
    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 ]

    -- Find all order isomorphisms between two posets
    -- This is the most naive algorithm, and should not be used on larger posets
    -- For example, already on the following, this takes forever compared to almost instant for orderIsos:
    -- > head $ orderIsos01 (posetD $ 8*9*25*49) (posetD $ 4*27*25*121)
    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 ] ]

    -- |Are the two posets order-isomorphic?
    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)

    -- For small posets, it may be that the up-front cost of calculating the hasseDigraph and heightPartitionDAG
    -- are not justified.
    -- |Find all order isomorphisms between two posets
    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 ] ]
    -- A variant on this algorithm would use the Hasse digraph rather than the partial order in the test on the last line
    -- This might be faster, depending how expensive the partial order comparison function is
    -- In effect though, it would then be a DAG isomorphism function

    -- The order automorphisms of a poset
    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
    -- This returns all automorphisms
    -- What we really want is to return generators of the permutation group

    -- |A linear extension of a poset is a linear ordering of the elements which extends the partial order.
    -- Equivalently, it is an ordering [x1..xn] of the underlying set, such that if xi <= xj then i <= j.
    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')

    -- |Linear extensions of a poset
    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