{-# LANGUAGE CPP #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE FlexibleContexts #-}
#ifndef HLINT
{-# LANGUAGE DefaultSignatures #-}
#endif
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE UndecidableInstances #-}

{-# OPTIONS_HADDOCK not-home #-}
--------------------------------------------------------------------
-- |
-- Copyright :  © Edward Kmett 2010-2014, Johan Kiviniemi 2013
-- License   :  BSD3
-- Maintainer:  Edward Kmett <ekmett@gmail.com>
-- Stability :  experimental
-- Portability: non-portable
--
--------------------------------------------------------------------
module Ersatz.Orderable
  ( Orderable(..)
  , GOrderable(..)
  ) where

import Prelude hiding ((&&),(||),not,and,or,all,any)

import Data.Foldable (toList)
import Data.Int
import Data.Void
import Data.Word
import Ersatz.Bit
import Ersatz.Equatable
import GHC.Generics
import Numeric.Natural
import qualified Data.IntMap as IntMap
import qualified Data.Map as Map
import qualified Data.Sequence as Seq
import qualified Data.Tree as Tree

infix  4 <?, <=?, >=?, >?

-- | Instances for this class for arbitrary types can be automatically derived from 'Generic'.
class Equatable t => Orderable t where
  -- | Compare for less-than within the SAT problem.
  (<?)  :: t -> t -> Bit

  -- | Compare for less-than or equal-to within the SAT problem.
  (<=?) :: t -> t -> Bit
  t
x <=? t
y = t
x forall t. Equatable t => t -> t -> Bit
=== t
y forall b. Boolean b => b -> b -> b
|| t
x forall t. Orderable t => t -> t -> Bit
<? t
y
#ifndef HLINT
  default (<?) :: (Generic t, GOrderable (Rep t)) => t -> t -> Bit
  t
a <? t
b = forall a x. Generic a => a -> Rep a x
from t
a forall (f :: * -> *) a. GOrderable f => f a -> f a -> Bit
<?# forall a x. Generic a => a -> Rep a x
from t
b
#endif

  -- | Compare for greater-than or equal-to within the SAT problem.
  (>=?) :: t -> t -> Bit
  t
x >=? t
y = t
y forall t. Orderable t => t -> t -> Bit
<=? t
x

  -- | Compare for greater-than within the SAT problem.
  (>?) :: t -> t -> Bit
  t
x >? t
y = t
y forall t. Orderable t => t -> t -> Bit
<? t
x


instance Orderable Bit where
  Bit
a <? :: Bit -> Bit -> Bit
<?  Bit
b = forall b. Boolean b => b -> b
not Bit
a forall b. Boolean b => b -> b -> b
&& Bit
b
  Bit
a <=? :: Bit -> Bit -> Bit
<=? Bit
b = forall b. Boolean b => b -> b
not Bit
a forall b. Boolean b => b -> b -> b
|| Bit
b

-- | Compare by lexicographic order on sorted key-value pairs
instance (Ord k, Orderable v) => Orderable (Map.Map k v) where
  Map k v
x <? :: Map k v -> Map k v -> Bit
<?  Map k v
y = forall k v. (Ord k, Orderable v) => [(k, v)] -> [(k, v)] -> Bit
assocsLt (forall k a. Map k a -> [(k, a)]
Map.assocs Map k v
x) (forall k a. Map k a -> [(k, a)]
Map.assocs Map k v
y)
  Map k v
x <=? :: Map k v -> Map k v -> Bit
<=? Map k v
y = forall k v. (Ord k, Orderable v) => [(k, v)] -> [(k, v)] -> Bit
assocsLe (forall k a. Map k a -> [(k, a)]
Map.assocs Map k v
x) (forall k a. Map k a -> [(k, a)]
Map.assocs Map k v
y)

-- | Compare by lexicographic order on sorted key-value pairs
instance Orderable v => Orderable (IntMap.IntMap v) where
  IntMap v
x <? :: IntMap v -> IntMap v -> Bit
<?  IntMap v
y = forall k v. (Ord k, Orderable v) => [(k, v)] -> [(k, v)] -> Bit
assocsLt (forall a. IntMap a -> [(Int, a)]
IntMap.assocs IntMap v
x) (forall a. IntMap a -> [(Int, a)]
IntMap.assocs IntMap v
y)
  IntMap v
x <=? :: IntMap v -> IntMap v -> Bit
<=? IntMap v
y = forall k v. (Ord k, Orderable v) => [(k, v)] -> [(k, v)] -> Bit
assocsLe (forall a. IntMap a -> [(Int, a)]
IntMap.assocs IntMap v
x) (forall a. IntMap a -> [(Int, a)]
IntMap.assocs IntMap v
y)

assocsLt :: (Ord k, Orderable v) => [(k,v)] -> [(k,v)] -> Bit
assocsLt :: forall k v. (Ord k, Orderable v) => [(k, v)] -> [(k, v)] -> Bit
assocsLt [(k, v)]
_ [] = forall b. Boolean b => b
false
assocsLt [] [(k, v)]
_ = forall b. Boolean b => b
true
assocsLt ((k
k1,v
v1):[(k, v)]
xs) ((k
k2,v
v2):[(k, v)]
ys) =
  case forall a. Ord a => a -> a -> Ordering
compare k
k1 k
k2 of
    Ordering
LT -> forall b. Boolean b => b
true
    Ordering
GT -> forall b. Boolean b => b
false
    Ordering
EQ -> v
v1 forall t. Orderable t => t -> t -> Bit
<? v
v2 forall b. Boolean b => b -> b -> b
|| v
v1 forall t. Equatable t => t -> t -> Bit
=== v
v2 forall b. Boolean b => b -> b -> b
&& forall k v. (Ord k, Orderable v) => [(k, v)] -> [(k, v)] -> Bit
assocsLt [(k, v)]
xs [(k, v)]
ys

assocsLe :: (Ord k, Orderable v) => [(k,v)] -> [(k,v)] -> Bit
assocsLe :: forall k v. (Ord k, Orderable v) => [(k, v)] -> [(k, v)] -> Bit
assocsLe [] [(k, v)]
_ = forall b. Boolean b => b
true
assocsLe [(k, v)]
_ [] = forall b. Boolean b => b
false
assocsLe ((k
k1,v
v1):[(k, v)]
xs) ((k
k2,v
v2):[(k, v)]
ys) =
  case forall a. Ord a => a -> a -> Ordering
compare k
k1 k
k2 of
    Ordering
LT -> forall b. Boolean b => b
true
    Ordering
GT -> forall b. Boolean b => b
false
    Ordering
EQ -> v
v1 forall t. Orderable t => t -> t -> Bit
<? v
v2 forall b. Boolean b => b -> b -> b
|| v
v1 forall t. Equatable t => t -> t -> Bit
=== v
v2 forall b. Boolean b => b -> b -> b
&& forall k v. (Ord k, Orderable v) => [(k, v)] -> [(k, v)] -> Bit
assocsLe [(k, v)]
xs [(k, v)]
ys

-- | Compare by lexicographic order on elements
instance Orderable v => Orderable (Seq.Seq v) where
  Seq v
x <? :: Seq v -> Seq v -> Bit
<?  Seq v
y = forall (t :: * -> *) a. Foldable t => t a -> [a]
toList Seq v
x forall t. Orderable t => t -> t -> Bit
<?  forall (t :: * -> *) a. Foldable t => t a -> [a]
toList Seq v
y
  Seq v
x <=? :: Seq v -> Seq v -> Bit
<=? Seq v
y = forall (t :: * -> *) a. Foldable t => t a -> [a]
toList Seq v
x forall t. Orderable t => t -> t -> Bit
<=? forall (t :: * -> *) a. Foldable t => t a -> [a]
toList Seq v
y

-- | Compare by lexicographic order on: root node, list of children
instance Orderable a => Orderable (Tree.Tree a) where
  Tree.Node a
x [Tree a]
xs <? :: Tree a -> Tree a -> Bit
<?  Tree.Node a
y [Tree a]
ys = (a
x,[Tree a]
xs) forall t. Orderable t => t -> t -> Bit
<?  (a
y,[Tree a]
ys)
  Tree.Node a
x [Tree a]
xs <=? :: Tree a -> Tree a -> Bit
<=? Tree.Node a
y [Tree a]
ys = (a
x,[Tree a]
xs) forall t. Orderable t => t -> t -> Bit
<=? (a
y,[Tree a]
ys)

instance (Orderable a, Orderable b) => Orderable (a,b)
instance (Orderable a, Orderable b, Orderable c) => Orderable (a,b,c)
instance (Orderable a, Orderable b, Orderable c, Orderable d) => Orderable (a,b,c,d)
instance (Orderable a, Orderable b, Orderable c, Orderable d, Orderable e) => Orderable (a,b,c,d,e)
instance (Orderable a, Orderable b, Orderable c, Orderable d, Orderable e, Orderable f) => Orderable (a,b,c,d,e,f)
instance (Orderable a, Orderable b, Orderable c, Orderable d, Orderable e, Orderable f, Orderable g) => Orderable (a,b,c,d,e,f,g)
instance Orderable a => Orderable (Maybe a)
instance (Orderable a, Orderable b) => Orderable (Either a b)

-- | Lexicographic order
instance Orderable a => Orderable [a] where
#ifndef HLINT
  []   <? :: [a] -> [a] -> Bit
<? []   = forall b. Boolean b => b
false
  a
x:[a]
xs <? a
y:[a]
ys = a
x forall t. Equatable t => t -> t -> Bit
=== a
y forall b. Boolean b => b -> b -> b
&& [a]
xs forall t. Orderable t => t -> t -> Bit
<? [a]
ys
              forall b. Boolean b => b -> b -> b
|| a
x forall t. Orderable t => t -> t -> Bit
<?  a
y
  []   <? [a]
_    = forall b. Boolean b => b
true
  [a]
_    <? []   = forall b. Boolean b => b
false

  []   <=? :: [a] -> [a] -> Bit
<=? [a]
_    = forall b. Boolean b => b
true
  a
x:[a]
xs <=? a
y:[a]
ys = a
x forall t. Equatable t => t -> t -> Bit
=== a
y forall b. Boolean b => b -> b -> b
&& [a]
xs forall t. Orderable t => t -> t -> Bit
<=? [a]
ys
               forall b. Boolean b => b -> b -> b
|| a
x forall t. Orderable t => t -> t -> Bit
<?  a
y
  [a]
_    <=? []   = forall b. Boolean b => b
false
#endif

class GEquatable f => GOrderable f where
  (<?#) :: f a -> f a -> Bit
  (<=?#) :: f a -> f a -> Bit

instance GOrderable U1 where
  U1 a
U1 <?# :: forall a. U1 a -> U1 a -> Bit
<?#  U1 a
U1 = forall b. Boolean b => b
false
  U1 a
U1 <=?# :: forall a. U1 a -> U1 a -> Bit
<=?# U1 a
U1 = forall b. Boolean b => b
true

instance GOrderable V1 where
  V1 a
x <?# :: forall a. V1 a -> V1 a -> Bit
<?# V1 a
y = V1 a
x seq :: forall a b. a -> b -> b
`seq` V1 a
y seq :: forall a b. a -> b -> b
`seq` forall a. HasCallStack => [Char] -> a
error [Char]
"GOrderable[V1].<?#"
  V1 a
x <=?# :: forall a. V1 a -> V1 a -> Bit
<=?# V1 a
y = V1 a
x seq :: forall a b. a -> b -> b
`seq` V1 a
y seq :: forall a b. a -> b -> b
`seq` forall a. HasCallStack => [Char] -> a
error [Char]
"GOrderable[V1].<=?#"

instance (GOrderable f, GOrderable g) => GOrderable (f :*: g) where
  (f a
a :*: g a
b) <?# :: forall a. (:*:) f g a -> (:*:) f g a -> Bit
<?#  (f a
c :*: g a
d) = (f a
a forall (f :: * -> *) a. GOrderable f => f a -> f a -> Bit
<?# f a
c) forall b. Boolean b => b -> b -> b
|| (f a
a forall (f :: * -> *) a. GEquatable f => f a -> f a -> Bit
===# f a
c forall b. Boolean b => b -> b -> b
&& g a
b forall (f :: * -> *) a. GOrderable f => f a -> f a -> Bit
<?# g a
d)
  (f a
a :*: g a
b) <=?# :: forall a. (:*:) f g a -> (:*:) f g a -> Bit
<=?# (f a
c :*: g a
d) = (f a
a forall (f :: * -> *) a. GOrderable f => f a -> f a -> Bit
<?# f a
c) forall b. Boolean b => b -> b -> b
|| (f a
a forall (f :: * -> *) a. GEquatable f => f a -> f a -> Bit
===# f a
c forall b. Boolean b => b -> b -> b
&& g a
b forall (f :: * -> *) a. GOrderable f => f a -> f a -> Bit
<=?# g a
d)

instance (GOrderable f, GOrderable g) => GOrderable (f :+: g) where
  L1 f a
_ <?# :: forall a. (:+:) f g a -> (:+:) f g a -> Bit
<?# R1 g a
_ = forall b. Boolean b => b
true
  L1 f a
a <?# L1 f a
b = f a
a forall (f :: * -> *) a. GOrderable f => f a -> f a -> Bit
<?# f a
b
  R1 g a
a <?# R1 g a
b = g a
a forall (f :: * -> *) a. GOrderable f => f a -> f a -> Bit
<?# g a
b
  R1 g a
_ <?# L1 f a
_ = forall b. Boolean b => b
false

  L1 f a
_ <=?# :: forall a. (:+:) f g a -> (:+:) f g a -> Bit
<=?# R1 g a
_ = forall b. Boolean b => b
true
  L1 f a
a <=?# L1 f a
b = f a
a forall (f :: * -> *) a. GOrderable f => f a -> f a -> Bit
<=?# f a
b
  R1 g a
a <=?# R1 g a
b = g a
a forall (f :: * -> *) a. GOrderable f => f a -> f a -> Bit
<=?# g a
b
  R1 g a
_ <=?# L1 f a
_ = forall b. Boolean b => b
false

instance GOrderable f => GOrderable (M1 i c f) where
  M1 f a
x <?# :: forall a. M1 i c f a -> M1 i c f a -> Bit
<?#  M1 f a
y = f a
x forall (f :: * -> *) a. GOrderable f => f a -> f a -> Bit
<?#  f a
y
  M1 f a
x <=?# :: forall a. M1 i c f a -> M1 i c f a -> Bit
<=?# M1 f a
y = f a
x forall (f :: * -> *) a. GOrderable f => f a -> f a -> Bit
<=?# f a
y

instance Orderable a => GOrderable (K1 i a) where
  K1 a
a <?# :: forall a. K1 i a a -> K1 i a a -> Bit
<?#  K1 a
b = a
a forall t. Orderable t => t -> t -> Bit
<?  a
b
  K1 a
a <=?# :: forall a. K1 i a a -> K1 i a a -> Bit
<=?# K1 a
b = a
a forall t. Orderable t => t -> t -> Bit
<=? a
b

-- Boring instances that end up being useful when deriving Orderable with Generics

instance Orderable ()       where ()
_ <? :: () -> () -> Bit
<?  ()
_ = forall b. Boolean b => b
false
                                  ()
_ <=? :: () -> () -> Bit
<=? ()
_ = forall b. Boolean b => b
true
instance Orderable Void     where Void
x <? :: Void -> Void -> Bit
<?  Void
y = Void
x seq :: forall a b. a -> b -> b
`seq` Void
y seq :: forall a b. a -> b -> b
`seq` forall a. HasCallStack => [Char] -> a
error [Char]
"Orderable[Void].<?"
                                  Void
x <=? :: Void -> Void -> Bit
<=? Void
y = Void
x seq :: forall a b. a -> b -> b
`seq` Void
y seq :: forall a b. a -> b -> b
`seq` forall a. HasCallStack => [Char] -> a
error [Char]
"Orderable[Void].<=?"
instance Orderable Int      where Int
x <? :: Int -> Int -> Bit
<?  Int
y = forall b. Boolean b => Bool -> b
bool (Int
x forall a. Ord a => a -> a -> Bool
<  Int
y)
                                  Int
x <=? :: Int -> Int -> Bit
<=? Int
y = forall b. Boolean b => Bool -> b
bool (Int
x forall a. Ord a => a -> a -> Bool
<= Int
y)
instance Orderable Integer  where Integer
x <? :: Integer -> Integer -> Bit
<?  Integer
y = forall b. Boolean b => Bool -> b
bool (Integer
x forall a. Ord a => a -> a -> Bool
<  Integer
y)
                                  Integer
x <=? :: Integer -> Integer -> Bit
<=? Integer
y = forall b. Boolean b => Bool -> b
bool (Integer
x forall a. Ord a => a -> a -> Bool
<= Integer
y)
instance Orderable Natural  where Natural
x <? :: Natural -> Natural -> Bit
<?  Natural
y = forall b. Boolean b => Bool -> b
bool (Natural
x forall a. Ord a => a -> a -> Bool
<  Natural
y)
                                  Natural
x <=? :: Natural -> Natural -> Bit
<=? Natural
y = forall b. Boolean b => Bool -> b
bool (Natural
x forall a. Ord a => a -> a -> Bool
<= Natural
y)
instance Orderable Word     where Word
x <? :: Word -> Word -> Bit
<?  Word
y = forall b. Boolean b => Bool -> b
bool (Word
x forall a. Ord a => a -> a -> Bool
<  Word
y)
                                  Word
x <=? :: Word -> Word -> Bit
<=? Word
y = forall b. Boolean b => Bool -> b
bool (Word
x forall a. Ord a => a -> a -> Bool
<= Word
y)
instance Orderable Word8    where Word8
x <? :: Word8 -> Word8 -> Bit
<?  Word8
y = forall b. Boolean b => Bool -> b
bool (Word8
x forall a. Ord a => a -> a -> Bool
<  Word8
y)
                                  Word8
x <=? :: Word8 -> Word8 -> Bit
<=? Word8
y = forall b. Boolean b => Bool -> b
bool (Word8
x forall a. Ord a => a -> a -> Bool
<= Word8
y)
instance Orderable Word16   where Word16
x <? :: Word16 -> Word16 -> Bit
<?  Word16
y = forall b. Boolean b => Bool -> b
bool (Word16
x forall a. Ord a => a -> a -> Bool
<  Word16
y)
                                  Word16
x <=? :: Word16 -> Word16 -> Bit
<=? Word16
y = forall b. Boolean b => Bool -> b
bool (Word16
x forall a. Ord a => a -> a -> Bool
<= Word16
y)
instance Orderable Word32   where Word32
x <? :: Word32 -> Word32 -> Bit
<?  Word32
y = forall b. Boolean b => Bool -> b
bool (Word32
x forall a. Ord a => a -> a -> Bool
<  Word32
y)
                                  Word32
x <=? :: Word32 -> Word32 -> Bit
<=? Word32
y = forall b. Boolean b => Bool -> b
bool (Word32
x forall a. Ord a => a -> a -> Bool
<= Word32
y)
instance Orderable Word64   where Word64
x <? :: Word64 -> Word64 -> Bit
<?  Word64
y = forall b. Boolean b => Bool -> b
bool (Word64
x forall a. Ord a => a -> a -> Bool
<  Word64
y)
                                  Word64
x <=? :: Word64 -> Word64 -> Bit
<=? Word64
y = forall b. Boolean b => Bool -> b
bool (Word64
x forall a. Ord a => a -> a -> Bool
<= Word64
y)
instance Orderable Int8     where Int8
x <? :: Int8 -> Int8 -> Bit
<?  Int8
y = forall b. Boolean b => Bool -> b
bool (Int8
x forall a. Ord a => a -> a -> Bool
<  Int8
y)
                                  Int8
x <=? :: Int8 -> Int8 -> Bit
<=? Int8
y = forall b. Boolean b => Bool -> b
bool (Int8
x forall a. Ord a => a -> a -> Bool
<= Int8
y)
instance Orderable Int16    where Int16
x <? :: Int16 -> Int16 -> Bit
<?  Int16
y = forall b. Boolean b => Bool -> b
bool (Int16
x forall a. Ord a => a -> a -> Bool
<  Int16
y)
                                  Int16
x <=? :: Int16 -> Int16 -> Bit
<=? Int16
y = forall b. Boolean b => Bool -> b
bool (Int16
x forall a. Ord a => a -> a -> Bool
<= Int16
y)
instance Orderable Int32    where Int32
x <? :: Int32 -> Int32 -> Bit
<?  Int32
y = forall b. Boolean b => Bool -> b
bool (Int32
x forall a. Ord a => a -> a -> Bool
<  Int32
y)
                                  Int32
x <=? :: Int32 -> Int32 -> Bit
<=? Int32
y = forall b. Boolean b => Bool -> b
bool (Int32
x forall a. Ord a => a -> a -> Bool
<= Int32
y)
instance Orderable Int64    where Int64
x <? :: Int64 -> Int64 -> Bit
<?  Int64
y = forall b. Boolean b => Bool -> b
bool (Int64
x forall a. Ord a => a -> a -> Bool
<  Int64
y)
                                  Int64
x <=? :: Int64 -> Int64 -> Bit
<=? Int64
y = forall b. Boolean b => Bool -> b
bool (Int64
x forall a. Ord a => a -> a -> Bool
<= Int64
y)
instance Orderable Char     where Char
x <? :: Char -> Char -> Bit
<?  Char
y = forall b. Boolean b => Bool -> b
bool (Char
x forall a. Ord a => a -> a -> Bool
<  Char
y)
                                  Char
x <=? :: Char -> Char -> Bit
<=? Char
y = forall b. Boolean b => Bool -> b
bool (Char
x forall a. Ord a => a -> a -> Bool
<= Char
y)
instance Orderable Float    where Float
x <? :: Float -> Float -> Bit
<?  Float
y = forall b. Boolean b => Bool -> b
bool (Float
x forall a. Ord a => a -> a -> Bool
<  Float
y)
                                  Float
x <=? :: Float -> Float -> Bit
<=? Float
y = forall b. Boolean b => Bool -> b
bool (Float
x forall a. Ord a => a -> a -> Bool
<= Float
y)
instance Orderable Double   where Double
x <? :: Double -> Double -> Bit
<?  Double
y = forall b. Boolean b => Bool -> b
bool (Double
x forall a. Ord a => a -> a -> Bool
<  Double
y)
                                  Double
x <=? :: Double -> Double -> Bit
<=? Double
y = forall b. Boolean b => Bool -> b
bool (Double
x forall a. Ord a => a -> a -> Bool
<= Double
y)
instance Orderable Ordering where Ordering
x <? :: Ordering -> Ordering -> Bit
<?  Ordering
y = forall b. Boolean b => Bool -> b
bool (Ordering
x forall a. Ord a => a -> a -> Bool
<  Ordering
y)
                                  Ordering
x <=? :: Ordering -> Ordering -> Bit
<=? Ordering
y = forall b. Boolean b => Bool -> b
bool (Ordering
x forall a. Ord a => a -> a -> Bool
<= Ordering
y)
instance Orderable Bool     where Bool
x <? :: Bool -> Bool -> Bit
<?  Bool
y = forall b. Boolean b => Bool -> b
bool (Bool
x forall a. Ord a => a -> a -> Bool
<  Bool
y)
                                  Bool
x <=? :: Bool -> Bool -> Bit
<=? Bool
y = forall b. Boolean b => Bool -> b
bool (Bool
x forall a. Ord a => a -> a -> Bool
<= Bool
y)