-- 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.Equatable
import Language.Hasmtlib.Iteable
import Language.Hasmtlib.Boolean
import Data.Int
import Data.Word
import Data.Void
import Numeric.Natural
import GHC.Generics
import GHC.TypeNats

-- | Compare two as as SMT-Expression.
-- 
-- @
-- 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 (>?) #-}
  
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)