{-# LANGUAGE DeriveDataTypeable  #-}
{-# LANGUAGE DeriveFoldable      #-}
{-# LANGUAGE DeriveFunctor       #-}
{-# LANGUAGE DeriveGeneric       #-}
{-# LANGUAGE DeriveTraversable   #-}
{-# LANGUAGE FlexibleContexts    #-}
{-# LANGUAGE Safe                #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeOperators       #-}
----------------------------------------------------------------------------
-- |
-- Module      :  Algebra.Lattice.Lexicographic
-- Copyright   :  (C) 2010-2015 Maximilian Bolingbroke, 2015-2019 Oleg Grenrus
-- License     :  BSD-3-Clause (see the file LICENSE)
--
-- Maintainer  :  Oleg Grenrus <oleg.grenrus@iki.fi>
--
----------------------------------------------------------------------------
module Algebra.Lattice.Lexicographic (
    Lexicographic(..)
  ) where

import Prelude ()
import Prelude.Compat

import Algebra.Lattice
import Algebra.PartialOrd

import Control.DeepSeq       (NFData (..))
import Control.Monad         (ap, liftM2)
import Data.Data             (Data, Typeable)
import Data.Hashable         (Hashable (..))
import Data.Universe.Class   (Finite (..), Universe (..))
import Data.Universe.Helpers (Natural, Tagged, retag)
import GHC.Generics          (Generic, Generic1)

import qualified Test.QuickCheck as QC

--
-- Lexicographic
--

-- | A pair lattice with a lexicographic ordering.  This means in
-- a join the second component of the resulting pair is the second
-- component of the pair with the larger first component.  If the
-- first components are equal, then the second components will be
-- joined.  The meet is similar only it prefers the smaller first
-- component.
--
-- An application of this type is versioning.  For example, a
-- Last-Writer-Wins register would look like
-- @'Lexicographic' ('Algebra.Lattice.Ordered.Ordered' Timestamp) v@ where the lattice
-- structure handles the, presumably rare, case of matching
-- @Timestamp@s.  Typically this is done in an arbitary, but
-- deterministic manner.
data Lexicographic k v = Lexicographic !k !v
  deriving ( Lexicographic k v -> Lexicographic k v -> Bool
(Lexicographic k v -> Lexicographic k v -> Bool)
-> (Lexicographic k v -> Lexicographic k v -> Bool)
-> Eq (Lexicographic k v)
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
forall k v.
(Eq k, Eq v) =>
Lexicographic k v -> Lexicographic k v -> Bool
/= :: Lexicographic k v -> Lexicographic k v -> Bool
$c/= :: forall k v.
(Eq k, Eq v) =>
Lexicographic k v -> Lexicographic k v -> Bool
== :: Lexicographic k v -> Lexicographic k v -> Bool
$c== :: forall k v.
(Eq k, Eq v) =>
Lexicographic k v -> Lexicographic k v -> Bool
Eq, Eq (Lexicographic k v)
Eq (Lexicographic k v)
-> (Lexicographic k v -> Lexicographic k v -> Ordering)
-> (Lexicographic k v -> Lexicographic k v -> Bool)
-> (Lexicographic k v -> Lexicographic k v -> Bool)
-> (Lexicographic k v -> Lexicographic k v -> Bool)
-> (Lexicographic k v -> Lexicographic k v -> Bool)
-> (Lexicographic k v -> Lexicographic k v -> Lexicographic k v)
-> (Lexicographic k v -> Lexicographic k v -> Lexicographic k v)
-> Ord (Lexicographic k v)
Lexicographic k v -> Lexicographic k v -> Bool
Lexicographic k v -> Lexicographic k v -> Ordering
Lexicographic k v -> Lexicographic k v -> Lexicographic k v
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 k v. (Ord k, Ord v) => Eq (Lexicographic k v)
forall k v.
(Ord k, Ord v) =>
Lexicographic k v -> Lexicographic k v -> Bool
forall k v.
(Ord k, Ord v) =>
Lexicographic k v -> Lexicographic k v -> Ordering
forall k v.
(Ord k, Ord v) =>
Lexicographic k v -> Lexicographic k v -> Lexicographic k v
min :: Lexicographic k v -> Lexicographic k v -> Lexicographic k v
$cmin :: forall k v.
(Ord k, Ord v) =>
Lexicographic k v -> Lexicographic k v -> Lexicographic k v
max :: Lexicographic k v -> Lexicographic k v -> Lexicographic k v
$cmax :: forall k v.
(Ord k, Ord v) =>
Lexicographic k v -> Lexicographic k v -> Lexicographic k v
>= :: Lexicographic k v -> Lexicographic k v -> Bool
$c>= :: forall k v.
(Ord k, Ord v) =>
Lexicographic k v -> Lexicographic k v -> Bool
> :: Lexicographic k v -> Lexicographic k v -> Bool
$c> :: forall k v.
(Ord k, Ord v) =>
Lexicographic k v -> Lexicographic k v -> Bool
<= :: Lexicographic k v -> Lexicographic k v -> Bool
$c<= :: forall k v.
(Ord k, Ord v) =>
Lexicographic k v -> Lexicographic k v -> Bool
< :: Lexicographic k v -> Lexicographic k v -> Bool
$c< :: forall k v.
(Ord k, Ord v) =>
Lexicographic k v -> Lexicographic k v -> Bool
compare :: Lexicographic k v -> Lexicographic k v -> Ordering
$ccompare :: forall k v.
(Ord k, Ord v) =>
Lexicographic k v -> Lexicographic k v -> Ordering
$cp1Ord :: forall k v. (Ord k, Ord v) => Eq (Lexicographic k v)
Ord, Int -> Lexicographic k v -> ShowS
[Lexicographic k v] -> ShowS
Lexicographic k v -> String
(Int -> Lexicographic k v -> ShowS)
-> (Lexicographic k v -> String)
-> ([Lexicographic k v] -> ShowS)
-> Show (Lexicographic k v)
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
forall k v. (Show k, Show v) => Int -> Lexicographic k v -> ShowS
forall k v. (Show k, Show v) => [Lexicographic k v] -> ShowS
forall k v. (Show k, Show v) => Lexicographic k v -> String
showList :: [Lexicographic k v] -> ShowS
$cshowList :: forall k v. (Show k, Show v) => [Lexicographic k v] -> ShowS
show :: Lexicographic k v -> String
$cshow :: forall k v. (Show k, Show v) => Lexicographic k v -> String
showsPrec :: Int -> Lexicographic k v -> ShowS
$cshowsPrec :: forall k v. (Show k, Show v) => Int -> Lexicographic k v -> ShowS
Show, ReadPrec [Lexicographic k v]
ReadPrec (Lexicographic k v)
Int -> ReadS (Lexicographic k v)
ReadS [Lexicographic k v]
(Int -> ReadS (Lexicographic k v))
-> ReadS [Lexicographic k v]
-> ReadPrec (Lexicographic k v)
-> ReadPrec [Lexicographic k v]
-> Read (Lexicographic k v)
forall a.
(Int -> ReadS a)
-> ReadS [a] -> ReadPrec a -> ReadPrec [a] -> Read a
forall k v. (Read k, Read v) => ReadPrec [Lexicographic k v]
forall k v. (Read k, Read v) => ReadPrec (Lexicographic k v)
forall k v. (Read k, Read v) => Int -> ReadS (Lexicographic k v)
forall k v. (Read k, Read v) => ReadS [Lexicographic k v]
readListPrec :: ReadPrec [Lexicographic k v]
$creadListPrec :: forall k v. (Read k, Read v) => ReadPrec [Lexicographic k v]
readPrec :: ReadPrec (Lexicographic k v)
$creadPrec :: forall k v. (Read k, Read v) => ReadPrec (Lexicographic k v)
readList :: ReadS [Lexicographic k v]
$creadList :: forall k v. (Read k, Read v) => ReadS [Lexicographic k v]
readsPrec :: Int -> ReadS (Lexicographic k v)
$creadsPrec :: forall k v. (Read k, Read v) => Int -> ReadS (Lexicographic k v)
Read, Typeable (Lexicographic k v)
DataType
Constr
Typeable (Lexicographic k v)
-> (forall (c :: * -> *).
    (forall d b. Data d => c (d -> b) -> d -> c b)
    -> (forall g. g -> c g)
    -> Lexicographic k v
    -> c (Lexicographic k v))
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c (Lexicographic k v))
-> (Lexicographic k v -> Constr)
-> (Lexicographic k v -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c (Lexicographic k v)))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e))
    -> Maybe (c (Lexicographic k v)))
-> ((forall b. Data b => b -> b)
    -> Lexicographic k v -> Lexicographic k v)
-> (forall r r'.
    (r -> r' -> r)
    -> r -> (forall d. Data d => d -> r') -> Lexicographic k v -> r)
-> (forall r r'.
    (r' -> r -> r)
    -> r -> (forall d. Data d => d -> r') -> Lexicographic k v -> r)
-> (forall u.
    (forall d. Data d => d -> u) -> Lexicographic k v -> [u])
-> (forall u.
    Int -> (forall d. Data d => d -> u) -> Lexicographic k v -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d)
    -> Lexicographic k v -> m (Lexicographic k v))
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d)
    -> Lexicographic k v -> m (Lexicographic k v))
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d)
    -> Lexicographic k v -> m (Lexicographic k v))
-> Data (Lexicographic k v)
Lexicographic k v -> DataType
Lexicographic k v -> Constr
(forall b. Data b => b -> b)
-> Lexicographic k v -> Lexicographic k v
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g)
-> Lexicographic k v
-> c (Lexicographic k v)
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (Lexicographic k v)
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c (Lexicographic k v))
forall a.
Typeable a
-> (forall (c :: * -> *).
    (forall d b. Data d => c (d -> b) -> d -> c b)
    -> (forall g. g -> c g) -> a -> c a)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c a)
-> (a -> Constr)
-> (a -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c a))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c a))
-> ((forall b. Data b => b -> b) -> a -> a)
-> (forall r r'.
    (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall r r'.
    (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall u. (forall d. Data d => d -> u) -> a -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> a -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> Data a
forall u.
Int -> (forall d. Data d => d -> u) -> Lexicographic k v -> u
forall u. (forall d. Data d => d -> u) -> Lexicographic k v -> [u]
forall k v. (Data k, Data v) => Typeable (Lexicographic k v)
forall k v. (Data k, Data v) => Lexicographic k v -> DataType
forall k v. (Data k, Data v) => Lexicographic k v -> Constr
forall k v.
(Data k, Data v) =>
(forall b. Data b => b -> b)
-> Lexicographic k v -> Lexicographic k v
forall k v u.
(Data k, Data v) =>
Int -> (forall d. Data d => d -> u) -> Lexicographic k v -> u
forall k v u.
(Data k, Data v) =>
(forall d. Data d => d -> u) -> Lexicographic k v -> [u]
forall k v r r'.
(Data k, Data v) =>
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> Lexicographic k v -> r
forall k v r r'.
(Data k, Data v) =>
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> Lexicographic k v -> r
forall k v (m :: * -> *).
(Data k, Data v, Monad m) =>
(forall d. Data d => d -> m d)
-> Lexicographic k v -> m (Lexicographic k v)
forall k v (m :: * -> *).
(Data k, Data v, MonadPlus m) =>
(forall d. Data d => d -> m d)
-> Lexicographic k v -> m (Lexicographic k v)
forall k v (c :: * -> *).
(Data k, Data v) =>
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (Lexicographic k v)
forall k v (c :: * -> *).
(Data k, Data v) =>
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g)
-> Lexicographic k v
-> c (Lexicographic k v)
forall k v (t :: * -> *) (c :: * -> *).
(Data k, Data v, Typeable t) =>
(forall d. Data d => c (t d)) -> Maybe (c (Lexicographic k v))
forall k v (t :: * -> * -> *) (c :: * -> *).
(Data k, Data v, Typeable t) =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c (Lexicographic k v))
forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> Lexicographic k v -> r
forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> Lexicographic k v -> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d)
-> Lexicographic k v -> m (Lexicographic k v)
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d)
-> Lexicographic k v -> m (Lexicographic k v)
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (Lexicographic k v)
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g)
-> Lexicographic k v
-> c (Lexicographic k v)
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c (Lexicographic k v))
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c (Lexicographic k v))
$cLexicographic :: Constr
$tLexicographic :: DataType
gmapMo :: (forall d. Data d => d -> m d)
-> Lexicographic k v -> m (Lexicographic k v)
$cgmapMo :: forall k v (m :: * -> *).
(Data k, Data v, MonadPlus m) =>
(forall d. Data d => d -> m d)
-> Lexicographic k v -> m (Lexicographic k v)
gmapMp :: (forall d. Data d => d -> m d)
-> Lexicographic k v -> m (Lexicographic k v)
$cgmapMp :: forall k v (m :: * -> *).
(Data k, Data v, MonadPlus m) =>
(forall d. Data d => d -> m d)
-> Lexicographic k v -> m (Lexicographic k v)
gmapM :: (forall d. Data d => d -> m d)
-> Lexicographic k v -> m (Lexicographic k v)
$cgmapM :: forall k v (m :: * -> *).
(Data k, Data v, Monad m) =>
(forall d. Data d => d -> m d)
-> Lexicographic k v -> m (Lexicographic k v)
gmapQi :: Int -> (forall d. Data d => d -> u) -> Lexicographic k v -> u
$cgmapQi :: forall k v u.
(Data k, Data v) =>
Int -> (forall d. Data d => d -> u) -> Lexicographic k v -> u
gmapQ :: (forall d. Data d => d -> u) -> Lexicographic k v -> [u]
$cgmapQ :: forall k v u.
(Data k, Data v) =>
(forall d. Data d => d -> u) -> Lexicographic k v -> [u]
gmapQr :: (r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> Lexicographic k v -> r
$cgmapQr :: forall k v r r'.
(Data k, Data v) =>
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> Lexicographic k v -> r
gmapQl :: (r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> Lexicographic k v -> r
$cgmapQl :: forall k v r r'.
(Data k, Data v) =>
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> Lexicographic k v -> r
gmapT :: (forall b. Data b => b -> b)
-> Lexicographic k v -> Lexicographic k v
$cgmapT :: forall k v.
(Data k, Data v) =>
(forall b. Data b => b -> b)
-> Lexicographic k v -> Lexicographic k v
dataCast2 :: (forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c (Lexicographic k v))
$cdataCast2 :: forall k v (t :: * -> * -> *) (c :: * -> *).
(Data k, Data v, Typeable t) =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c (Lexicographic k v))
dataCast1 :: (forall d. Data d => c (t d)) -> Maybe (c (Lexicographic k v))
$cdataCast1 :: forall k v (t :: * -> *) (c :: * -> *).
(Data k, Data v, Typeable t) =>
(forall d. Data d => c (t d)) -> Maybe (c (Lexicographic k v))
dataTypeOf :: Lexicographic k v -> DataType
$cdataTypeOf :: forall k v. (Data k, Data v) => Lexicographic k v -> DataType
toConstr :: Lexicographic k v -> Constr
$ctoConstr :: forall k v. (Data k, Data v) => Lexicographic k v -> Constr
gunfold :: (forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (Lexicographic k v)
$cgunfold :: forall k v (c :: * -> *).
(Data k, Data v) =>
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (Lexicographic k v)
gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g)
-> Lexicographic k v
-> c (Lexicographic k v)
$cgfoldl :: forall k v (c :: * -> *).
(Data k, Data v) =>
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g)
-> Lexicographic k v
-> c (Lexicographic k v)
$cp1Data :: forall k v. (Data k, Data v) => Typeable (Lexicographic k v)
Data, Typeable, (forall x. Lexicographic k v -> Rep (Lexicographic k v) x)
-> (forall x. Rep (Lexicographic k v) x -> Lexicographic k v)
-> Generic (Lexicographic k v)
forall x. Rep (Lexicographic k v) x -> Lexicographic k v
forall x. Lexicographic k v -> Rep (Lexicographic k v) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall k v x. Rep (Lexicographic k v) x -> Lexicographic k v
forall k v x. Lexicographic k v -> Rep (Lexicographic k v) x
$cto :: forall k v x. Rep (Lexicographic k v) x -> Lexicographic k v
$cfrom :: forall k v x. Lexicographic k v -> Rep (Lexicographic k v) x
Generic, a -> Lexicographic k b -> Lexicographic k a
(a -> b) -> Lexicographic k a -> Lexicographic k b
(forall a b. (a -> b) -> Lexicographic k a -> Lexicographic k b)
-> (forall a b. a -> Lexicographic k b -> Lexicographic k a)
-> Functor (Lexicographic k)
forall a b. a -> Lexicographic k b -> Lexicographic k a
forall a b. (a -> b) -> Lexicographic k a -> Lexicographic k b
forall k a b. a -> Lexicographic k b -> Lexicographic k a
forall k a b. (a -> b) -> Lexicographic k a -> Lexicographic k b
forall (f :: * -> *).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
<$ :: a -> Lexicographic k b -> Lexicographic k a
$c<$ :: forall k a b. a -> Lexicographic k b -> Lexicographic k a
fmap :: (a -> b) -> Lexicographic k a -> Lexicographic k b
$cfmap :: forall k a b. (a -> b) -> Lexicographic k a -> Lexicographic k b
Functor, Lexicographic k a -> Bool
(a -> m) -> Lexicographic k a -> m
(a -> b -> b) -> b -> Lexicographic k a -> b
(forall m. Monoid m => Lexicographic k m -> m)
-> (forall m a. Monoid m => (a -> m) -> Lexicographic k a -> m)
-> (forall m a. Monoid m => (a -> m) -> Lexicographic k a -> m)
-> (forall a b. (a -> b -> b) -> b -> Lexicographic k a -> b)
-> (forall a b. (a -> b -> b) -> b -> Lexicographic k a -> b)
-> (forall b a. (b -> a -> b) -> b -> Lexicographic k a -> b)
-> (forall b a. (b -> a -> b) -> b -> Lexicographic k a -> b)
-> (forall a. (a -> a -> a) -> Lexicographic k a -> a)
-> (forall a. (a -> a -> a) -> Lexicographic k a -> a)
-> (forall a. Lexicographic k a -> [a])
-> (forall a. Lexicographic k a -> Bool)
-> (forall a. Lexicographic k a -> Int)
-> (forall a. Eq a => a -> Lexicographic k a -> Bool)
-> (forall a. Ord a => Lexicographic k a -> a)
-> (forall a. Ord a => Lexicographic k a -> a)
-> (forall a. Num a => Lexicographic k a -> a)
-> (forall a. Num a => Lexicographic k a -> a)
-> Foldable (Lexicographic k)
forall a. Eq a => a -> Lexicographic k a -> Bool
forall a. Num a => Lexicographic k a -> a
forall a. Ord a => Lexicographic k a -> a
forall m. Monoid m => Lexicographic k m -> m
forall a. Lexicographic k a -> Bool
forall a. Lexicographic k a -> Int
forall a. Lexicographic k a -> [a]
forall a. (a -> a -> a) -> Lexicographic k a -> a
forall k a. Eq a => a -> Lexicographic k a -> Bool
forall k a. Num a => Lexicographic k a -> a
forall k a. Ord a => Lexicographic k a -> a
forall m a. Monoid m => (a -> m) -> Lexicographic k a -> m
forall k m. Monoid m => Lexicographic k m -> m
forall k a. Lexicographic k a -> Bool
forall k a. Lexicographic k a -> Int
forall k a. Lexicographic k a -> [a]
forall b a. (b -> a -> b) -> b -> Lexicographic k a -> b
forall a b. (a -> b -> b) -> b -> Lexicographic k a -> b
forall k a. (a -> a -> a) -> Lexicographic k a -> a
forall k m a. Monoid m => (a -> m) -> Lexicographic k a -> m
forall k b a. (b -> a -> b) -> b -> Lexicographic k a -> b
forall k a b. (a -> b -> b) -> b -> Lexicographic k a -> b
forall (t :: * -> *).
(forall m. Monoid m => t m -> m)
-> (forall m a. Monoid m => (a -> m) -> t a -> m)
-> (forall m a. Monoid m => (a -> m) -> t a -> m)
-> (forall a b. (a -> b -> b) -> b -> t a -> b)
-> (forall a b. (a -> b -> b) -> b -> t a -> b)
-> (forall b a. (b -> a -> b) -> b -> t a -> b)
-> (forall b a. (b -> a -> b) -> b -> t a -> b)
-> (forall a. (a -> a -> a) -> t a -> a)
-> (forall a. (a -> a -> a) -> t a -> a)
-> (forall a. t a -> [a])
-> (forall a. t a -> Bool)
-> (forall a. t a -> Int)
-> (forall a. Eq a => a -> t a -> Bool)
-> (forall a. Ord a => t a -> a)
-> (forall a. Ord a => t a -> a)
-> (forall a. Num a => t a -> a)
-> (forall a. Num a => t a -> a)
-> Foldable t
product :: Lexicographic k a -> a
$cproduct :: forall k a. Num a => Lexicographic k a -> a
sum :: Lexicographic k a -> a
$csum :: forall k a. Num a => Lexicographic k a -> a
minimum :: Lexicographic k a -> a
$cminimum :: forall k a. Ord a => Lexicographic k a -> a
maximum :: Lexicographic k a -> a
$cmaximum :: forall k a. Ord a => Lexicographic k a -> a
elem :: a -> Lexicographic k a -> Bool
$celem :: forall k a. Eq a => a -> Lexicographic k a -> Bool
length :: Lexicographic k a -> Int
$clength :: forall k a. Lexicographic k a -> Int
null :: Lexicographic k a -> Bool
$cnull :: forall k a. Lexicographic k a -> Bool
toList :: Lexicographic k a -> [a]
$ctoList :: forall k a. Lexicographic k a -> [a]
foldl1 :: (a -> a -> a) -> Lexicographic k a -> a
$cfoldl1 :: forall k a. (a -> a -> a) -> Lexicographic k a -> a
foldr1 :: (a -> a -> a) -> Lexicographic k a -> a
$cfoldr1 :: forall k a. (a -> a -> a) -> Lexicographic k a -> a
foldl' :: (b -> a -> b) -> b -> Lexicographic k a -> b
$cfoldl' :: forall k b a. (b -> a -> b) -> b -> Lexicographic k a -> b
foldl :: (b -> a -> b) -> b -> Lexicographic k a -> b
$cfoldl :: forall k b a. (b -> a -> b) -> b -> Lexicographic k a -> b
foldr' :: (a -> b -> b) -> b -> Lexicographic k a -> b
$cfoldr' :: forall k a b. (a -> b -> b) -> b -> Lexicographic k a -> b
foldr :: (a -> b -> b) -> b -> Lexicographic k a -> b
$cfoldr :: forall k a b. (a -> b -> b) -> b -> Lexicographic k a -> b
foldMap' :: (a -> m) -> Lexicographic k a -> m
$cfoldMap' :: forall k m a. Monoid m => (a -> m) -> Lexicographic k a -> m
foldMap :: (a -> m) -> Lexicographic k a -> m
$cfoldMap :: forall k m a. Monoid m => (a -> m) -> Lexicographic k a -> m
fold :: Lexicographic k m -> m
$cfold :: forall k m. Monoid m => Lexicographic k m -> m
Foldable, Functor (Lexicographic k)
Foldable (Lexicographic k)
Functor (Lexicographic k)
-> Foldable (Lexicographic k)
-> (forall (f :: * -> *) a b.
    Applicative f =>
    (a -> f b) -> Lexicographic k a -> f (Lexicographic k b))
-> (forall (f :: * -> *) a.
    Applicative f =>
    Lexicographic k (f a) -> f (Lexicographic k a))
-> (forall (m :: * -> *) a b.
    Monad m =>
    (a -> m b) -> Lexicographic k a -> m (Lexicographic k b))
-> (forall (m :: * -> *) a.
    Monad m =>
    Lexicographic k (m a) -> m (Lexicographic k a))
-> Traversable (Lexicographic k)
(a -> f b) -> Lexicographic k a -> f (Lexicographic k b)
forall k. Functor (Lexicographic k)
forall k. Foldable (Lexicographic k)
forall k (m :: * -> *) a.
Monad m =>
Lexicographic k (m a) -> m (Lexicographic k a)
forall k (f :: * -> *) a.
Applicative f =>
Lexicographic k (f a) -> f (Lexicographic k a)
forall k (m :: * -> *) a b.
Monad m =>
(a -> m b) -> Lexicographic k a -> m (Lexicographic k b)
forall k (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> Lexicographic k a -> f (Lexicographic k b)
forall (t :: * -> *).
Functor t
-> Foldable t
-> (forall (f :: * -> *) a b.
    Applicative f =>
    (a -> f b) -> t a -> f (t b))
-> (forall (f :: * -> *) a. Applicative f => t (f a) -> f (t a))
-> (forall (m :: * -> *) a b.
    Monad m =>
    (a -> m b) -> t a -> m (t b))
-> (forall (m :: * -> *) a. Monad m => t (m a) -> m (t a))
-> Traversable t
forall (m :: * -> *) a.
Monad m =>
Lexicographic k (m a) -> m (Lexicographic k a)
forall (f :: * -> *) a.
Applicative f =>
Lexicographic k (f a) -> f (Lexicographic k a)
forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> Lexicographic k a -> m (Lexicographic k b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> Lexicographic k a -> f (Lexicographic k b)
sequence :: Lexicographic k (m a) -> m (Lexicographic k a)
$csequence :: forall k (m :: * -> *) a.
Monad m =>
Lexicographic k (m a) -> m (Lexicographic k a)
mapM :: (a -> m b) -> Lexicographic k a -> m (Lexicographic k b)
$cmapM :: forall k (m :: * -> *) a b.
Monad m =>
(a -> m b) -> Lexicographic k a -> m (Lexicographic k b)
sequenceA :: Lexicographic k (f a) -> f (Lexicographic k a)
$csequenceA :: forall k (f :: * -> *) a.
Applicative f =>
Lexicographic k (f a) -> f (Lexicographic k a)
traverse :: (a -> f b) -> Lexicographic k a -> f (Lexicographic k b)
$ctraverse :: forall k (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> Lexicographic k a -> f (Lexicographic k b)
$cp2Traversable :: forall k. Foldable (Lexicographic k)
$cp1Traversable :: forall k. Functor (Lexicographic k)
Traversable
           , (forall a. Lexicographic k a -> Rep1 (Lexicographic k) a)
-> (forall a. Rep1 (Lexicographic k) a -> Lexicographic k a)
-> Generic1 (Lexicographic k)
forall a. Rep1 (Lexicographic k) a -> Lexicographic k a
forall a. Lexicographic k a -> Rep1 (Lexicographic k) a
forall k a. Rep1 (Lexicographic k) a -> Lexicographic k a
forall k a. Lexicographic k a -> Rep1 (Lexicographic k) a
forall k (f :: k -> *).
(forall (a :: k). f a -> Rep1 f a)
-> (forall (a :: k). Rep1 f a -> f a) -> Generic1 f
$cto1 :: forall k a. Rep1 (Lexicographic k) a -> Lexicographic k a
$cfrom1 :: forall k a. Lexicographic k a -> Rep1 (Lexicographic k) a
Generic1
           )

instance BoundedJoinSemiLattice k => Applicative (Lexicographic k) where
  pure :: a -> Lexicographic k a
pure = a -> Lexicographic k a
forall (m :: * -> *) a. Monad m => a -> m a
return
  <*> :: Lexicographic k (a -> b) -> Lexicographic k a -> Lexicographic k b
(<*>) = Lexicographic k (a -> b) -> Lexicographic k a -> Lexicographic k b
forall (m :: * -> *) a b. Monad m => m (a -> b) -> m a -> m b
ap

-- Essentially the Writer monad.
instance BoundedJoinSemiLattice k => Monad (Lexicographic k) where
  return :: a -> Lexicographic k a
return                   =  k -> a -> Lexicographic k a
forall k v. k -> v -> Lexicographic k v
Lexicographic k
forall a. BoundedJoinSemiLattice a => a
bottom
  Lexicographic k
k a
v >>= :: Lexicographic k a -> (a -> Lexicographic k b) -> Lexicographic k b
>>= a -> Lexicographic k b
f  =
    case a -> Lexicographic k b
f a
v of
      Lexicographic k
k' b
v' -> k -> b -> Lexicographic k b
forall k v. k -> v -> Lexicographic k v
Lexicographic (k
k k -> k -> k
forall a. Lattice a => a -> a -> a
\/ k
k') b
v'

instance (NFData k, NFData v) => NFData (Lexicographic k v) where
  rnf :: Lexicographic k v -> ()
rnf (Lexicographic k
k v
v) = k -> ()
forall a. NFData a => a -> ()
rnf k
k () -> () -> ()
`seq` v -> ()
forall a. NFData a => a -> ()
rnf v
v

instance (Hashable k, Hashable v) => Hashable (Lexicographic k v)

-- Why we have 'bottom', and not @v1 \\/ v2@ in the @otherwise@ clause?
--
-- For example what is the join of @(2, 1)@ and @(3, 2)@
-- in lexicographic divisibility divisibility lattice.
--
-- With @v1 \\/ v2@, we get the upper bound, but not least!
--
-- @
-- (2, 1) `leq` (6, 2)
-- (3, 2) `leq` (6, 2)
-- @
--
-- But @(6, 1) `leq` (6, 2)@, and
--
-- @
-- (2, 1) `leq` (6, 1)
-- (3, 2) `leq` (6, 1)
-- @
--
instance (PartialOrd k, Lattice k, BoundedJoinSemiLattice v, BoundedMeetSemiLattice v) => Lattice (Lexicographic k v) where
  l :: Lexicographic k v
l@(Lexicographic k
k1 v
v1) \/ :: Lexicographic k v -> Lexicographic k v -> Lexicographic k v
\/ r :: Lexicographic k v
r@(Lexicographic k
k2 v
v2)
    | k
k1 k -> k -> Bool
forall a. Eq a => a -> a -> Bool
== k
k2 = k -> v -> Lexicographic k v
forall k v. k -> v -> Lexicographic k v
Lexicographic k
k1 (v
v1 v -> v -> v
forall a. Lattice a => a -> a -> a
\/ v
v2)
    | k
k1 k -> k -> Bool
forall a. PartialOrd a => a -> a -> Bool
`leq` k
k2 = Lexicographic k v
r
    | k
k2 k -> k -> Bool
forall a. PartialOrd a => a -> a -> Bool
`leq` k
k1 = Lexicographic k v
l
    | Bool
otherwise   = k -> v -> Lexicographic k v
forall k v. k -> v -> Lexicographic k v
Lexicographic (k
k1 k -> k -> k
forall a. Lattice a => a -> a -> a
\/ k
k2) v
forall a. BoundedJoinSemiLattice a => a
bottom

  l :: Lexicographic k v
l@(Lexicographic k
k1 v
v1) /\ :: Lexicographic k v -> Lexicographic k v -> Lexicographic k v
/\ r :: Lexicographic k v
r@(Lexicographic k
k2 v
v2)
    | k
k1 k -> k -> Bool
forall a. Eq a => a -> a -> Bool
== k
k2 = k -> v -> Lexicographic k v
forall k v. k -> v -> Lexicographic k v
Lexicographic k
k1 (v
v1 v -> v -> v
forall a. Lattice a => a -> a -> a
/\ v
v2)
    | k
k1 k -> k -> Bool
forall a. PartialOrd a => a -> a -> Bool
`leq` k
k2 = Lexicographic k v
l
    | k
k2 k -> k -> Bool
forall a. PartialOrd a => a -> a -> Bool
`leq` k
k1 = Lexicographic k v
r
    | Bool
otherwise   = k -> v -> Lexicographic k v
forall k v. k -> v -> Lexicographic k v
Lexicographic (k
k1 k -> k -> k
forall a. Lattice a => a -> a -> a
/\ k
k2) v
forall a. BoundedMeetSemiLattice a => a
top

instance (PartialOrd k, BoundedJoinSemiLattice k, BoundedJoinSemiLattice v, BoundedMeetSemiLattice v) => BoundedJoinSemiLattice (Lexicographic k v) where
  bottom :: Lexicographic k v
bottom = k -> v -> Lexicographic k v
forall k v. k -> v -> Lexicographic k v
Lexicographic k
forall a. BoundedJoinSemiLattice a => a
bottom v
forall a. BoundedJoinSemiLattice a => a
bottom

instance (PartialOrd k, BoundedMeetSemiLattice k, BoundedJoinSemiLattice v, BoundedMeetSemiLattice v) => BoundedMeetSemiLattice (Lexicographic k v) where
  top :: Lexicographic k v
top = k -> v -> Lexicographic k v
forall k v. k -> v -> Lexicographic k v
Lexicographic k
forall a. BoundedMeetSemiLattice a => a
top v
forall a. BoundedMeetSemiLattice a => a
top

instance (PartialOrd k, PartialOrd v) => PartialOrd (Lexicographic k v) where
  Lexicographic k
k1 v
v1 leq :: Lexicographic k v -> Lexicographic k v -> Bool
`leq` Lexicographic k
k2 v
v2
    | k
k1   k -> k -> Bool
forall a. Eq a => a -> a -> Bool
==  k
k2 = v
v1 v -> v -> Bool
forall a. PartialOrd a => a -> a -> Bool
`leq` v
v2
    | k
k1 k -> k -> Bool
forall a. PartialOrd a => a -> a -> Bool
`leq` k
k2 = Bool
True
    | Bool
otherwise   = Bool
False -- Incomparable or k2 `leq` k1
  comparable :: Lexicographic k v -> Lexicographic k v -> Bool
comparable (Lexicographic k
k1 v
v1) (Lexicographic k
k2 v
v2)
    | k
k1 k -> k -> Bool
forall a. Eq a => a -> a -> Bool
== k
k2 = v -> v -> Bool
forall a. PartialOrd a => a -> a -> Bool
comparable v
v1 v
v2
    | Bool
otherwise = k -> k -> Bool
forall a. PartialOrd a => a -> a -> Bool
comparable k
k1 k
k2

instance (Universe k, Universe v) => Universe (Lexicographic k v) where
    universe :: [Lexicographic k v]
universe = ((k, v) -> Lexicographic k v) -> [(k, v)] -> [Lexicographic k v]
forall a b. (a -> b) -> [a] -> [b]
map ((k -> v -> Lexicographic k v) -> (k, v) -> Lexicographic k v
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry k -> v -> Lexicographic k v
forall k v. k -> v -> Lexicographic k v
Lexicographic) [(k, v)]
forall a. Universe a => [a]
universe
instance (Finite k, Finite v) => Finite (Lexicographic k v) where
    universeF :: [Lexicographic k v]
universeF = ((k, v) -> Lexicographic k v) -> [(k, v)] -> [Lexicographic k v]
forall a b. (a -> b) -> [a] -> [b]
map ((k -> v -> Lexicographic k v) -> (k, v) -> Lexicographic k v
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry k -> v -> Lexicographic k v
forall k v. k -> v -> Lexicographic k v
Lexicographic) [(k, v)]
forall a. Finite a => [a]
universeF
    cardinality :: Tagged (Lexicographic k v) Natural
cardinality = (Natural -> Natural -> Natural)
-> Tagged (Lexicographic k v) Natural
-> Tagged (Lexicographic k v) Natural
-> Tagged (Lexicographic k v) Natural
forall (m :: * -> *) a1 a2 r.
Monad m =>
(a1 -> a2 -> r) -> m a1 -> m a2 -> m r
liftM2 Natural -> Natural -> Natural
forall a. Num a => a -> a -> a
(*)
        (Tagged k Natural -> Tagged (Lexicographic k v) Natural
forall k1 k2 (s :: k1) b (t :: k2). Tagged s b -> Tagged t b
retag (Tagged k Natural
forall a. Finite a => Tagged a Natural
cardinality :: Tagged k Natural))
        (Tagged v Natural -> Tagged (Lexicographic k v) Natural
forall k1 k2 (s :: k1) b (t :: k2). Tagged s b -> Tagged t b
retag (Tagged v Natural
forall a. Finite a => Tagged a Natural
cardinality :: Tagged v Natural))

instance (QC.Arbitrary k, QC.Arbitrary v) => QC.Arbitrary (Lexicographic k v) where
    arbitrary :: Gen (Lexicographic k v)
arbitrary = (k -> v -> Lexicographic k v) -> (k, v) -> Lexicographic k v
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry k -> v -> Lexicographic k v
forall k v. k -> v -> Lexicographic k v
Lexicographic ((k, v) -> Lexicographic k v)
-> Gen (k, v) -> Gen (Lexicographic k v)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Gen (k, v)
forall a. Arbitrary a => Gen a
QC.arbitrary
    shrink :: Lexicographic k v -> [Lexicographic k v]
shrink (Lexicographic k
k v
v) = (k -> v -> Lexicographic k v) -> (k, v) -> Lexicographic k v
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry k -> v -> Lexicographic k v
forall k v. k -> v -> Lexicographic k v
Lexicographic ((k, v) -> Lexicographic k v) -> [(k, v)] -> [Lexicographic k v]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (k, v) -> [(k, v)]
forall a. Arbitrary a => a -> [a]
QC.shrink (k
k, v
v)

instance (QC.CoArbitrary k, QC.CoArbitrary v) => QC.CoArbitrary (Lexicographic k v) where
    coarbitrary :: Lexicographic k v -> Gen b -> Gen b
coarbitrary (Lexicographic k
k v
v) = (k, v) -> Gen b -> Gen b
forall a b. CoArbitrary a => a -> Gen b -> Gen b
QC.coarbitrary (k
k, v
v)

instance (QC.Function k, QC.Function v) => QC.Function (Lexicographic k v) where
    function :: (Lexicographic k v -> b) -> Lexicographic k v :-> b
function = (Lexicographic k v -> (k, v))
-> ((k, v) -> Lexicographic k v)
-> (Lexicographic k v -> b)
-> Lexicographic k v :-> b
forall b a c.
Function b =>
(a -> b) -> (b -> a) -> (a -> c) -> a :-> c
QC.functionMap (\(Lexicographic k
k v
v) -> (k
k,v
v)) ((k -> v -> Lexicographic k v) -> (k, v) -> Lexicographic k v
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry k -> v -> Lexicographic k v
forall k v. k -> v -> Lexicographic k v
Lexicographic)