-- Required for class constraints of form: c (ValueType t) :: Constraint
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE DefaultSignatures #-}

module Language.Hasmtlib.Orderable where

import Prelude hiding (not, (&&), (||))
import Language.Hasmtlib.Internal.Expr
import Language.Hasmtlib.Type.SMTSort
import Language.Hasmtlib.Equatable
import Language.Hasmtlib.Iteable
import Language.Hasmtlib.Boolean
import Data.Int
import Data.Word
import Data.Void
import Data.Tree (Tree)
import Data.Monoid (Sum, Product, First, Last, Dual)
import Data.Functor.Identity (Identity)
import Numeric.Natural
import GHC.Generics
import GHC.TypeNats

-- | Compare two as as SMT-Expression.
--
--   You can derive an instance of this class if your type is 'Generic'.
--
-- @
-- x <- var @RealSort
-- y <- var
-- assert $ x >? y
-- assert $ x === min' 42 100
-- @
--
class Equatable a => Orderable a where
  (<=?) :: a -> a -> Expr BoolSort
  default (<=?) :: (Generic a, GOrderable (Rep a)) => a -> a -> Expr BoolSort
  a
x <=? a
y = a -> Rep a Any
forall x. a -> Rep a x
forall a x. Generic a => a -> Rep a x
from a
x Rep a Any -> Rep a Any -> Expr 'BoolSort
forall a. Rep a a -> Rep a a -> Expr 'BoolSort
forall {k} (f :: k -> *) (a :: k).
GOrderable f =>
f a -> f a -> Expr 'BoolSort
<=?# a -> Rep a Any
forall x. a -> Rep a x
forall a x. Generic a => a -> Rep a x
from a
y

  (>=?) :: a -> a -> Expr BoolSort
  a
x >=? a
y = a
y a -> a -> Expr 'BoolSort
forall a. Orderable a => a -> a -> Expr 'BoolSort
<=? a
x

  (<?)  :: a -> a -> Expr BoolSort
  a
x <? a
y = Expr 'BoolSort -> Expr 'BoolSort
forall b. Boolean b => b -> b
not (Expr 'BoolSort -> Expr 'BoolSort)
-> Expr 'BoolSort -> Expr 'BoolSort
forall a b. (a -> b) -> a -> b
$ a
y a -> a -> Expr 'BoolSort
forall a. Orderable a => a -> a -> Expr 'BoolSort
<=? a
x

  (>?)  :: a -> a -> Expr BoolSort
  a
x >? a
y = Expr 'BoolSort -> Expr 'BoolSort
forall b. Boolean b => b -> b
not (Expr 'BoolSort -> Expr 'BoolSort)
-> Expr 'BoolSort -> Expr 'BoolSort
forall a b. (a -> b) -> a -> b
$ a
x a -> a -> Expr 'BoolSort
forall a. Orderable a => a -> a -> Expr 'BoolSort
<=? a
y

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

-- | Minimum of two as SMT-Expression.
min' :: (Orderable a, Iteable (Expr BoolSort) a) => a -> a -> a
min' :: forall a. (Orderable a, Iteable (Expr 'BoolSort) a) => a -> a -> a
min' a
x a
y = Expr 'BoolSort -> a -> a -> a
forall b a. Iteable b a => b -> a -> a -> a
ite (a
x a -> a -> Expr 'BoolSort
forall a. Orderable a => a -> a -> Expr 'BoolSort
<=? a
y) a
x a
y

-- | Maximum of two as SMT-Expression.
max' :: (Orderable a, Iteable (Expr BoolSort) a) => a -> a -> a
max' :: forall a. (Orderable a, Iteable (Expr 'BoolSort) a) => a -> a -> a
max' a
x a
y = Expr 'BoolSort -> a -> a -> a
forall b a. Iteable b a => b -> a -> a -> a
ite (a
y a -> a -> Expr 'BoolSort
forall a. Orderable a => a -> a -> Expr 'BoolSort
<=? a
x) a
x a
y

instance Orderable (Expr IntSort) where
  <? :: Expr 'IntSort -> Expr 'IntSort -> Expr 'BoolSort
(<?)     = Expr 'IntSort -> Expr 'IntSort -> Expr 'BoolSort
forall (t1 :: SMTSort).
(Ord (HaskellType t1), KnownSMTSort t1) =>
Expr t1 -> Expr t1 -> Expr 'BoolSort
LTH
  {-# INLINE (<?) #-}
  <=? :: Expr 'IntSort -> Expr 'IntSort -> Expr 'BoolSort
(<=?)    = Expr 'IntSort -> Expr 'IntSort -> Expr 'BoolSort
forall (t1 :: SMTSort).
(Ord (HaskellType t1), KnownSMTSort t1) =>
Expr t1 -> Expr t1 -> Expr 'BoolSort
LTHE
  {-# INLINE (<=?) #-}
  >=? :: Expr 'IntSort -> Expr 'IntSort -> Expr 'BoolSort
(>=?)    = Expr 'IntSort -> Expr 'IntSort -> Expr 'BoolSort
forall (t1 :: SMTSort).
(Ord (HaskellType t1), KnownSMTSort t1) =>
Expr t1 -> Expr t1 -> Expr 'BoolSort
GTHE
  {-# INLINE (>=?) #-}
  >? :: Expr 'IntSort -> Expr 'IntSort -> Expr 'BoolSort
(>?)     = Expr 'IntSort -> Expr 'IntSort -> Expr 'BoolSort
forall (t1 :: SMTSort).
(Ord (HaskellType t1), KnownSMTSort t1) =>
Expr t1 -> Expr t1 -> Expr 'BoolSort
GTH
  {-# INLINE (>?) #-}

instance Orderable (Expr RealSort) where
  <? :: Expr 'RealSort -> Expr 'RealSort -> Expr 'BoolSort
(<?)     = Expr 'RealSort -> Expr 'RealSort -> Expr 'BoolSort
forall (t1 :: SMTSort).
(Ord (HaskellType t1), KnownSMTSort t1) =>
Expr t1 -> Expr t1 -> Expr 'BoolSort
LTH
  {-# INLINE (<?) #-}
  <=? :: Expr 'RealSort -> Expr 'RealSort -> Expr 'BoolSort
(<=?)    = Expr 'RealSort -> Expr 'RealSort -> Expr 'BoolSort
forall (t1 :: SMTSort).
(Ord (HaskellType t1), KnownSMTSort t1) =>
Expr t1 -> Expr t1 -> Expr 'BoolSort
LTHE
  {-# INLINE (<=?) #-}
  >=? :: Expr 'RealSort -> Expr 'RealSort -> Expr 'BoolSort
(>=?)    = Expr 'RealSort -> Expr 'RealSort -> Expr 'BoolSort
forall (t1 :: SMTSort).
(Ord (HaskellType t1), KnownSMTSort t1) =>
Expr t1 -> Expr t1 -> Expr 'BoolSort
GTHE
  {-# INLINE (>=?) #-}
  >? :: Expr 'RealSort -> Expr 'RealSort -> Expr 'BoolSort
(>?)     = Expr 'RealSort -> Expr 'RealSort -> Expr 'BoolSort
forall (t1 :: SMTSort).
(Ord (HaskellType t1), KnownSMTSort t1) =>
Expr t1 -> Expr t1 -> Expr 'BoolSort
GTH
  {-# INLINE (>?) #-}

instance KnownNat n => Orderable (Expr (BvSort n)) where
  <? :: Expr ('BvSort n) -> Expr ('BvSort n) -> Expr 'BoolSort
(<?)     = Expr ('BvSort n) -> Expr ('BvSort n) -> Expr 'BoolSort
forall (n :: Nat).
KnownNat n =>
Expr ('BvSort n) -> Expr ('BvSort n) -> Expr 'BoolSort
BvuLT
  {-# INLINE (<?) #-}
  <=? :: Expr ('BvSort n) -> Expr ('BvSort n) -> Expr 'BoolSort
(<=?)    = Expr ('BvSort n) -> Expr ('BvSort n) -> Expr 'BoolSort
forall (n :: Nat).
KnownNat n =>
Expr ('BvSort n) -> Expr ('BvSort n) -> Expr 'BoolSort
BvuLTHE
  {-# INLINE (<=?) #-}
  >=? :: Expr ('BvSort n) -> Expr ('BvSort n) -> Expr 'BoolSort
(>=?)    = Expr ('BvSort n) -> Expr ('BvSort n) -> Expr 'BoolSort
forall (n :: Nat).
KnownNat n =>
Expr ('BvSort n) -> Expr ('BvSort n) -> Expr 'BoolSort
BvuGTHE
  {-# INLINE (>=?) #-}
  >? :: Expr ('BvSort n) -> Expr ('BvSort n) -> Expr 'BoolSort
(>?)     = Expr ('BvSort n) -> Expr ('BvSort n) -> Expr 'BoolSort
forall (n :: Nat).
KnownNat n =>
Expr ('BvSort n) -> Expr ('BvSort n) -> Expr 'BoolSort
BvuGT
  {-# INLINE (>?) #-}

-- | Lexicographic ordering for '(<?)' and reflexive closure of lexicographic ordering for '(<=?)'
instance Orderable (Expr StringSort) where
  <? :: Expr 'StringSort -> Expr 'StringSort -> Expr 'BoolSort
(<?)     = Expr 'StringSort -> Expr 'StringSort -> Expr 'BoolSort
StrLT
  {-# INLINE (<?) #-}
  <=? :: Expr 'StringSort -> Expr 'StringSort -> Expr 'BoolSort
(<=?)    = Expr 'StringSort -> Expr 'StringSort -> Expr 'BoolSort
StrLTHE
  {-# INLINE (<=?) #-}

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

instance GOrderable U1 where
  U1 a
U1 <?# :: forall (a :: k). U1 a -> U1 a -> Expr 'BoolSort
<?#  U1 a
U1 = Expr 'BoolSort
forall b. Boolean b => b
false
  U1 a
U1 <=?# :: forall (a :: k). U1 a -> U1 a -> Expr 'BoolSort
<=?# U1 a
U1 = Expr 'BoolSort
forall b. Boolean b => b
true

instance GOrderable V1 where
  V1 a
x <?# :: forall (a :: k). V1 a -> V1 a -> Expr 'BoolSort
<?# V1 a
y = V1 a
x V1 a -> Expr 'BoolSort -> Expr 'BoolSort
forall a b. a -> b -> b
`seq` V1 a
y V1 a -> Expr 'BoolSort -> Expr 'BoolSort
forall a b. a -> b -> b
`seq` [Char] -> Expr 'BoolSort
forall a. HasCallStack => [Char] -> a
error [Char]
"GOrderable[V1].<?#"
  V1 a
x <=?# :: forall (a :: k). V1 a -> V1 a -> Expr 'BoolSort
<=?# V1 a
y = V1 a
x V1 a -> Expr 'BoolSort -> Expr 'BoolSort
forall a b. a -> b -> b
`seq` V1 a
y V1 a -> Expr 'BoolSort -> Expr 'BoolSort
forall a b. a -> b -> b
`seq` [Char] -> Expr 'BoolSort
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 :: k). (:*:) f g a -> (:*:) f g a -> Expr 'BoolSort
<?#  (f a
c :*: g a
d) = (f a
a f a -> f a -> Expr 'BoolSort
forall (a :: k). f a -> f a -> Expr 'BoolSort
forall {k} (f :: k -> *) (a :: k).
GOrderable f =>
f a -> f a -> Expr 'BoolSort
<?# f a
c) Expr 'BoolSort -> Expr 'BoolSort -> Expr 'BoolSort
forall b. Boolean b => b -> b -> b
|| (f a
a f a -> f a -> Expr 'BoolSort
forall (a :: k). f a -> f a -> Expr 'BoolSort
forall {k} (f :: k -> *) (a :: k).
GEquatable f =>
f a -> f a -> Expr 'BoolSort
===# f a
c Expr 'BoolSort -> Expr 'BoolSort -> Expr 'BoolSort
forall b. Boolean b => b -> b -> b
&& g a
b g a -> g a -> Expr 'BoolSort
forall (a :: k). g a -> g a -> Expr 'BoolSort
forall {k} (f :: k -> *) (a :: k).
GOrderable f =>
f a -> f a -> Expr 'BoolSort
<?# g a
d)
  (f a
a :*: g a
b) <=?# :: forall (a :: k). (:*:) f g a -> (:*:) f g a -> Expr 'BoolSort
<=?# (f a
c :*: g a
d) = (f a
a f a -> f a -> Expr 'BoolSort
forall (a :: k). f a -> f a -> Expr 'BoolSort
forall {k} (f :: k -> *) (a :: k).
GOrderable f =>
f a -> f a -> Expr 'BoolSort
<?# f a
c) Expr 'BoolSort -> Expr 'BoolSort -> Expr 'BoolSort
forall b. Boolean b => b -> b -> b
|| (f a
a f a -> f a -> Expr 'BoolSort
forall (a :: k). f a -> f a -> Expr 'BoolSort
forall {k} (f :: k -> *) (a :: k).
GEquatable f =>
f a -> f a -> Expr 'BoolSort
===# f a
c Expr 'BoolSort -> Expr 'BoolSort -> Expr 'BoolSort
forall b. Boolean b => b -> b -> b
&& g a
b g a -> g a -> Expr 'BoolSort
forall (a :: k). g a -> g a -> Expr 'BoolSort
forall {k} (f :: k -> *) (a :: k).
GOrderable f =>
f a -> f a -> Expr 'BoolSort
<=?# g a
d)

instance (GOrderable f, GOrderable g) => GOrderable (f :+: g) where
  L1 f a
_ <?# :: forall (a :: k). (:+:) f g a -> (:+:) f g a -> Expr 'BoolSort
<?# R1 g a
_ = Expr 'BoolSort
forall b. Boolean b => b
true
  L1 f a
a <?# L1 f a
b = f a
a f a -> f a -> Expr 'BoolSort
forall (a :: k). f a -> f a -> Expr 'BoolSort
forall {k} (f :: k -> *) (a :: k).
GOrderable f =>
f a -> f a -> Expr 'BoolSort
<?# f a
b
  R1 g a
a <?# R1 g a
b = g a
a g a -> g a -> Expr 'BoolSort
forall (a :: k). g a -> g a -> Expr 'BoolSort
forall {k} (f :: k -> *) (a :: k).
GOrderable f =>
f a -> f a -> Expr 'BoolSort
<?# g a
b
  R1 g a
_ <?# L1 f a
_ = Expr 'BoolSort
forall b. Boolean b => b
false

  L1 f a
_ <=?# :: forall (a :: k). (:+:) f g a -> (:+:) f g a -> Expr 'BoolSort
<=?# R1 g a
_ = Expr 'BoolSort
forall b. Boolean b => b
true
  L1 f a
a <=?# L1 f a
b = f a
a f a -> f a -> Expr 'BoolSort
forall (a :: k). f a -> f a -> Expr 'BoolSort
forall {k} (f :: k -> *) (a :: k).
GOrderable f =>
f a -> f a -> Expr 'BoolSort
<=?# f a
b
  R1 g a
a <=?# R1 g a
b = g a
a g a -> g a -> Expr 'BoolSort
forall (a :: k). g a -> g a -> Expr 'BoolSort
forall {k} (f :: k -> *) (a :: k).
GOrderable f =>
f a -> f a -> Expr 'BoolSort
<=?# g a
b
  R1 g a
_ <=?# L1 f a
_ = Expr 'BoolSort
forall b. Boolean b => b
false

instance GOrderable f => GOrderable (M1 i c f) where
  M1 f a
x <?# :: forall (a :: k). M1 i c f a -> M1 i c f a -> Expr 'BoolSort
<?#  M1 f a
y = f a
x f a -> f a -> Expr 'BoolSort
forall (a :: k). f a -> f a -> Expr 'BoolSort
forall {k} (f :: k -> *) (a :: k).
GOrderable f =>
f a -> f a -> Expr 'BoolSort
<?#  f a
y
  M1 f a
x <=?# :: forall (a :: k). M1 i c f a -> M1 i c f a -> Expr 'BoolSort
<=?# M1 f a
y = f a
x f a -> f a -> Expr 'BoolSort
forall (a :: k). f a -> f a -> Expr 'BoolSort
forall {k} (f :: k -> *) (a :: k).
GOrderable f =>
f a -> f a -> Expr 'BoolSort
<=?# f a
y

instance Orderable a => GOrderable (K1 i a) where
  K1 a
a <?# :: forall (a :: k). K1 i a a -> K1 i a a -> Expr 'BoolSort
<?#  K1 a
b = a
a a -> a -> Expr 'BoolSort
forall a. Orderable a => a -> a -> Expr 'BoolSort
<?  a
b
  K1 a
a <=?# :: forall (a :: k). K1 i a a -> K1 i a a -> Expr 'BoolSort
<=?# K1 a
b = a
a a -> a -> Expr 'BoolSort
forall a. Orderable a => a -> a -> Expr 'BoolSort
<=? a
b

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

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

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 b, Orderable c, Orderable d, Orderable e, Orderable f, Orderable g, Orderable h) => Orderable (a,b,c,d,e,f,g,h)
instance Orderable a => Orderable [a]
instance Orderable a => Orderable (Tree a)
instance Orderable a => Orderable (Maybe a)
instance (Orderable a, Orderable b) => Orderable (Either a b)
instance Orderable a => Orderable (Sum a)
instance Orderable a => Orderable (Product a)
instance Orderable a => Orderable (First a)
instance Orderable a => Orderable (Last a)
instance Orderable a => Orderable (Dual a)
instance Orderable a => Orderable (Identity a)