{-# 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 Ersatz.Bit
import Ersatz.Equatable
import GHC.Generics

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 t -> t -> Bit
forall t. Equatable t => t -> t -> Bit
=== t
y Bit -> Bit -> Bit
forall b. Boolean b => b -> b -> b
|| t
x t -> t -> Bit
forall t. Orderable t => t -> t -> Bit
<? t
y
#ifndef HLINT
  default (<?) :: (Generic t, GOrderable (Rep t)) => t -> t -> Bit
  t
a <? t
b = t -> Rep t Any
forall a x. Generic a => a -> Rep a x
from t
a Rep t Any -> Rep t Any -> Bit
forall (f :: * -> *) a. GOrderable f => f a -> f a -> Bit
<?# t -> Rep t Any
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 t -> t -> Bit
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 t -> t -> Bit
forall t. Orderable t => t -> t -> Bit
<? t
x


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

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

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

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

instance (GOrderable f, GOrderable g) => GOrderable (f :*: g) where
  (f a
a :*: g a
b) <?# :: (:*:) f g a -> (:*:) f g a -> Bit
<?#  (f a
c :*: g a
d) = (f a
a f a -> f a -> Bit
forall (f :: * -> *) a. GOrderable f => f a -> f a -> Bit
<?# f a
c) Bit -> Bit -> Bit
forall b. Boolean b => b -> b -> b
|| (f a
a f a -> f a -> Bit
forall (f :: * -> *) a. GEquatable f => f a -> f a -> Bit
===# f a
c Bit -> Bit -> Bit
forall b. Boolean b => b -> b -> b
&& g a
b g a -> g a -> Bit
forall (f :: * -> *) a. GOrderable f => f a -> f a -> Bit
<?# g a
d)
  (f a
a :*: g a
b) <=?# :: (:*:) f g a -> (:*:) f g a -> Bit
<=?# (f a
c :*: g a
d) = (f a
a f a -> f a -> Bit
forall (f :: * -> *) a. GOrderable f => f a -> f a -> Bit
<?# f a
c) Bit -> Bit -> Bit
forall b. Boolean b => b -> b -> b
|| (f a
a f a -> f a -> Bit
forall (f :: * -> *) a. GEquatable f => f a -> f a -> Bit
===# f a
c Bit -> Bit -> Bit
forall b. Boolean b => b -> b -> b
&& g a
b g a -> g a -> Bit
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
_ <?# :: (:+:) f g a -> (:+:) f g a -> Bit
<?# R1 g a
_ = Bit
forall b. Boolean b => b
true
  L1 f a
a <?# L1 f a
b = f a
a f a -> f a -> Bit
forall (f :: * -> *) a. GOrderable f => f a -> f a -> Bit
<?# f a
b
  R1 g a
a <?# R1 g a
b = g a
a g a -> g a -> Bit
forall (f :: * -> *) a. GOrderable f => f a -> f a -> Bit
<?# g a
b
  R1 g a
_ <?# L1 f a
_ = Bit
forall b. Boolean b => b
false

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

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

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