{-# LANGUAGE ConstraintKinds     #-}
{-# LANGUAGE FlexibleContexts    #-}
{-# LANGUAGE FlexibleInstances   #-}
{-# LANGUAGE GADTs               #-}
{-# LANGUAGE PatternSynonyms     #-}
{-# LANGUAGE RebindableSyntax    #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TemplateHaskell     #-}
{-# LANGUAGE TypeApplications    #-}
{-# LANGUAGE TypeFamilies        #-}
{-# LANGUAGE TypeOperators       #-}
{-# LANGUAGE ViewPatterns        #-}
{-# OPTIONS_GHC -fno-warn-orphans #-}
-- |
-- Module      : Data.Array.Accelerate.Classes.Ord
-- Copyright   : [2016..2020] The Accelerate Team
-- License     : BSD3
--
-- Maintainer  : Trevor L. McDonell <trevor.mcdonell@gmail.com>
-- Stability   : experimental
-- Portability : non-portable (GHC extensions)
--

module Data.Array.Accelerate.Classes.Ord (

  Ord(..),
  Ordering(..), pattern LT_, pattern EQ_, pattern GT_,

) where

import Data.Array.Accelerate.Analysis.Match
import Data.Array.Accelerate.Pattern
import Data.Array.Accelerate.Pattern.Ordering
import Data.Array.Accelerate.Representation.Tag
import Data.Array.Accelerate.Smart
import Data.Array.Accelerate.Sugar.Elt
import Data.Array.Accelerate.Sugar.Shape
import Data.Array.Accelerate.Type

-- We must hide (==), as that operator is used for the literals 0, 1 and 2 in the pattern synonyms for Ordering.
-- As RebindableSyntax is enabled, a literal pattern is compiled to a call to (==), meaning that the Prelude.(==) should be in scope as (==).
import Data.Array.Accelerate.Classes.Eq                             hiding ( (==) )
import qualified Data.Array.Accelerate.Classes.Eq                   as A

import Data.Char
import Language.Haskell.TH.Extra                                    hiding ( Exp )
import Prelude                                                      ( ($), (>>=), Ordering(..), Num(..), Maybe(..), String, show, error, unlines, return, concat, map, mapM )
import Text.Printf
import qualified Prelude                                            as P


infix 4 <
infix 4 >
infix 4 <=
infix 4 >=

-- | The 'Ord' class for totally ordered datatypes
--
class Eq a => Ord a where
  {-# MINIMAL (<=) | compare #-}
  (<)     :: Exp a -> Exp a -> Exp Bool
  (>)     :: Exp a -> Exp a -> Exp Bool
  (<=)    :: Exp a -> Exp a -> Exp Bool
  (>=)    :: Exp a -> Exp a -> Exp Bool
  min     :: Exp a -> Exp a -> Exp a
  max     :: Exp a -> Exp a -> Exp a
  compare :: Exp a -> Exp a -> Exp Ordering

  Exp a
x <  Exp a
y = if Exp a -> Exp a -> Exp Ordering
forall a. Ord a => Exp a -> Exp a -> Exp Ordering
compare Exp a
x Exp a
y Exp Ordering -> Exp Ordering -> Exp Bool
forall a. Eq a => Exp a -> Exp a -> Exp Bool
A.== Ordering -> Exp Ordering
forall e. (HasCallStack, Elt e) => e -> Exp e
constant Ordering
LT then Bool -> Exp Bool
forall e. (HasCallStack, Elt e) => e -> Exp e
constant Bool
True  else Bool -> Exp Bool
forall e. (HasCallStack, Elt e) => e -> Exp e
constant Bool
False
  Exp a
x <= Exp a
y = if Exp a -> Exp a -> Exp Ordering
forall a. Ord a => Exp a -> Exp a -> Exp Ordering
compare Exp a
x Exp a
y Exp Ordering -> Exp Ordering -> Exp Bool
forall a. Eq a => Exp a -> Exp a -> Exp Bool
A.== Ordering -> Exp Ordering
forall e. (HasCallStack, Elt e) => e -> Exp e
constant Ordering
GT then Bool -> Exp Bool
forall e. (HasCallStack, Elt e) => e -> Exp e
constant Bool
False else Bool -> Exp Bool
forall e. (HasCallStack, Elt e) => e -> Exp e
constant Bool
True
  Exp a
x >  Exp a
y = if Exp a -> Exp a -> Exp Ordering
forall a. Ord a => Exp a -> Exp a -> Exp Ordering
compare Exp a
x Exp a
y Exp Ordering -> Exp Ordering -> Exp Bool
forall a. Eq a => Exp a -> Exp a -> Exp Bool
A.== Ordering -> Exp Ordering
forall e. (HasCallStack, Elt e) => e -> Exp e
constant Ordering
GT then Bool -> Exp Bool
forall e. (HasCallStack, Elt e) => e -> Exp e
constant Bool
True  else Bool -> Exp Bool
forall e. (HasCallStack, Elt e) => e -> Exp e
constant Bool
False
  Exp a
x >= Exp a
y = if Exp a -> Exp a -> Exp Ordering
forall a. Ord a => Exp a -> Exp a -> Exp Ordering
compare Exp a
x Exp a
y Exp Ordering -> Exp Ordering -> Exp Bool
forall a. Eq a => Exp a -> Exp a -> Exp Bool
A.== Ordering -> Exp Ordering
forall e. (HasCallStack, Elt e) => e -> Exp e
constant Ordering
LT then Bool -> Exp Bool
forall e. (HasCallStack, Elt e) => e -> Exp e
constant Bool
False else Bool -> Exp Bool
forall e. (HasCallStack, Elt e) => e -> Exp e
constant Bool
True

  min Exp a
x Exp a
y = if Exp a
x Exp a -> Exp a -> Exp Bool
forall a. Ord a => Exp a -> Exp a -> Exp Bool
<= Exp a
y then Exp a
x else Exp a
y
  max Exp a
x Exp a
y = if Exp a
x Exp a -> Exp a -> Exp Bool
forall a. Ord a => Exp a -> Exp a -> Exp Bool
<= Exp a
y then Exp a
y else Exp a
x

  compare Exp a
x Exp a
y =
    if Exp a
x Exp a -> Exp a -> Exp Bool
forall a. Eq a => Exp a -> Exp a -> Exp Bool
A.== Exp a
y then Ordering -> Exp Ordering
forall e. (HasCallStack, Elt e) => e -> Exp e
constant Ordering
EQ else
    if Exp a
x   Exp a -> Exp a -> Exp Bool
forall a. Ord a => Exp a -> Exp a -> Exp Bool
<= Exp a
y then Ordering -> Exp Ordering
forall e. (HasCallStack, Elt e) => e -> Exp e
constant Ordering
LT
                else Ordering -> Exp Ordering
forall e. (HasCallStack, Elt e) => e -> Exp e
constant Ordering
GT

-- Local redefinition for use with RebindableSyntax (pulled forward from Prelude.hs)
--
ifThenElse :: Elt a => Exp Bool -> Exp a -> Exp a -> Exp a
ifThenElse :: forall a. Elt a => Exp Bool -> Exp a -> Exp a -> Exp a
ifThenElse (Exp SmartExp (EltR Bool)
c) (Exp SmartExp (EltR a)
x) (Exp SmartExp (EltR a)
y) = SmartExp (EltR a) -> Exp a
forall t. SmartExp (EltR t) -> Exp t
Exp (SmartExp (EltR a) -> Exp a) -> SmartExp (EltR a) -> Exp a
forall a b. (a -> b) -> a -> b
$ PreSmartExp SmartAcc SmartExp (EltR a) -> SmartExp (EltR a)
forall t. PreSmartExp SmartAcc SmartExp t -> SmartExp t
SmartExp (PreSmartExp SmartAcc SmartExp (EltR a) -> SmartExp (EltR a))
-> PreSmartExp SmartAcc SmartExp (EltR a) -> SmartExp (EltR a)
forall a b. (a -> b) -> a -> b
$ SmartExp TAG
-> SmartExp (EltR a)
-> SmartExp (EltR a)
-> PreSmartExp SmartAcc SmartExp (EltR a)
forall (exp :: * -> *) t (acc :: * -> *).
exp TAG -> exp t -> exp t -> PreSmartExp acc exp t
Cond (SmartExp (TAG, ()) -> SmartExp TAG
forall a b. Coerce a b => SmartExp a -> SmartExp b
mkCoerce' SmartExp (TAG, ())
SmartExp (EltR Bool)
c) SmartExp (EltR a)
x SmartExp (EltR a)
y

instance Ord () where
  < :: Exp () -> Exp () -> Exp Bool
(<)     Exp ()
_ Exp ()
_ = Bool -> Exp Bool
forall e. (HasCallStack, Elt e) => e -> Exp e
constant Bool
False
  > :: Exp () -> Exp () -> Exp Bool
(>)     Exp ()
_ Exp ()
_ = Bool -> Exp Bool
forall e. (HasCallStack, Elt e) => e -> Exp e
constant Bool
False
  >= :: Exp () -> Exp () -> Exp Bool
(>=)    Exp ()
_ Exp ()
_ = Bool -> Exp Bool
forall e. (HasCallStack, Elt e) => e -> Exp e
constant Bool
True
  <= :: Exp () -> Exp () -> Exp Bool
(<=)    Exp ()
_ Exp ()
_ = Bool -> Exp Bool
forall e. (HasCallStack, Elt e) => e -> Exp e
constant Bool
True
  min :: Exp () -> Exp () -> Exp ()
min     Exp ()
_ Exp ()
_ = () -> Exp ()
forall e. (HasCallStack, Elt e) => e -> Exp e
constant ()
  max :: Exp () -> Exp () -> Exp ()
max     Exp ()
_ Exp ()
_ = () -> Exp ()
forall e. (HasCallStack, Elt e) => e -> Exp e
constant ()
  compare :: Exp () -> Exp () -> Exp Ordering
compare Exp ()
_ Exp ()
_ = Ordering -> Exp Ordering
forall e. (HasCallStack, Elt e) => e -> Exp e
constant Ordering
EQ

instance Ord Z where
  < :: Exp Z -> Exp Z -> Exp Bool
(<)  Exp Z
_ Exp Z
_ = Bool -> Exp Bool
forall e. (HasCallStack, Elt e) => e -> Exp e
constant Bool
False
  > :: Exp Z -> Exp Z -> Exp Bool
(>)  Exp Z
_ Exp Z
_ = Bool -> Exp Bool
forall e. (HasCallStack, Elt e) => e -> Exp e
constant Bool
False
  <= :: Exp Z -> Exp Z -> Exp Bool
(<=) Exp Z
_ Exp Z
_ = Bool -> Exp Bool
forall e. (HasCallStack, Elt e) => e -> Exp e
constant Bool
True
  >= :: Exp Z -> Exp Z -> Exp Bool
(>=) Exp Z
_ Exp Z
_ = Bool -> Exp Bool
forall e. (HasCallStack, Elt e) => e -> Exp e
constant Bool
True
  min :: Exp Z -> Exp Z -> Exp Z
min  Exp Z
_ Exp Z
_ = Z -> Exp Z
forall e. (HasCallStack, Elt e) => e -> Exp e
constant Z
Z
  max :: Exp Z -> Exp Z -> Exp Z
max  Exp Z
_ Exp Z
_ = Z -> Exp Z
forall e. (HasCallStack, Elt e) => e -> Exp e
constant Z
Z


-- Instances of 'Prelude.Ord' (mostly) don't make sense with the standard
-- signatures as the return type is fixed to 'Bool'. This instance is provided
-- to provide a useful error message.
--
-- Note that 'min' and 'max' are implementable, so we do hook those into the
-- accelerate instances defined here. This allows us to use operations such as
-- 'Prelude.minimum' and 'Prelude.maximum'.
--
instance Ord a => P.Ord (Exp a) where
  < :: Exp a -> Exp a -> Bool
(<)     = String -> String -> Exp a -> Exp a -> Bool
forall a. String -> String -> a
preludeError String
"Ord.(<)"  String
"(<)"
  <= :: Exp a -> Exp a -> Bool
(<=)    = String -> String -> Exp a -> Exp a -> Bool
forall a. String -> String -> a
preludeError String
"Ord.(<=)" String
"(<=)"
  > :: Exp a -> Exp a -> Bool
(>)     = String -> String -> Exp a -> Exp a -> Bool
forall a. String -> String -> a
preludeError String
"Ord.(>)"  String
"(>)"
  >= :: Exp a -> Exp a -> Bool
(>=)    = String -> String -> Exp a -> Exp a -> Bool
forall a. String -> String -> a
preludeError String
"Ord.(>=)" String
"(>=)"
  min :: Exp a -> Exp a -> Exp a
min     = Exp a -> Exp a -> Exp a
forall a. Ord a => Exp a -> Exp a -> Exp a
min
  max :: Exp a -> Exp a -> Exp a
max     = Exp a -> Exp a -> Exp a
forall a. Ord a => Exp a -> Exp a -> Exp a
max

preludeError :: String -> String -> a
preludeError :: forall a. String -> String -> a
preludeError String
x String
y
  = String -> a
forall a. HasCallStack => String -> a
error
  (String -> a) -> String -> a
forall a b. (a -> b) -> a -> b
$ [String] -> String
unlines [ String -> String -> String -> String
forall r. PrintfType r => String -> r
printf String
"Prelude.%s applied to EDSL types: use Data.Array.Accelerate.%s instead" String
x String
y
            , String
""
            , String
"These Prelude.Ord instances are present only to fulfil superclass"
            , String
"constraints for subsequent classes in the standard Haskell numeric"
            , String
"hierarchy."
            ]

runQ $ do
  let
      integralTypes :: [Name]
      integralTypes =
        [ ''Int
        , ''Int8
        , ''Int16
        , ''Int32
        , ''Int64
        , ''Word
        , ''Word8
        , ''Word16
        , ''Word32
        , ''Word64
        ]

      floatingTypes :: [Name]
      floatingTypes =
        [ ''Half
        , ''Float
        , ''Double
        ]

      nonNumTypes :: [Name]
      nonNumTypes =
        [ ''Char
        ]

      cTypes :: [Name]
      cTypes =
        [ ''CInt
        , ''CUInt
        , ''CLong
        , ''CULong
        , ''CLLong
        , ''CULLong
        , ''CShort
        , ''CUShort
        , ''CChar
        , ''CUChar
        , ''CSChar
        , ''CFloat
        , ''CDouble
        ]

      mkPrim :: Name -> Q [Dec]
      mkPrim t =
        [d| instance Ord $(conT t) where
              (<)  = mkLt
              (>)  = mkGt
              (<=) = mkLtEq
              (>=) = mkGtEq
              min  = mkMin
              max  = mkMax
          |]

      mkLt' :: [ExpQ] -> [ExpQ] -> ExpQ
      mkLt' [x] [y]       = [| $x < $y |]
      mkLt' (x:xs) (y:ys) = [| $x < $y || ( $x A.== $y && $(mkLt' xs ys) ) |]
      mkLt' _      _      = error "mkLt'"

      mkGt' :: [ExpQ] -> [ExpQ] -> ExpQ
      mkGt' [x]    [y]    = [| $x > $y |]
      mkGt' (x:xs) (y:ys) = [| $x > $y || ( $x A.== $y && $(mkGt' xs ys) ) |]
      mkGt' _      _      = error "mkGt'"

      mkLtEq' :: [ExpQ] -> [ExpQ] -> ExpQ
      mkLtEq' [x] [y]       = [| $x < $y |]
      mkLtEq' (x:xs) (y:ys) = [| $x < $y || ( $x A.== $y && $(mkLtEq' xs ys) ) |]
      mkLtEq' _      _      = error "mkLtEq'"

      mkGtEq' :: [ExpQ] -> [ExpQ] -> ExpQ
      mkGtEq' [x]    [y]    = [| $x > $y |]
      mkGtEq' (x:xs) (y:ys) = [| $x > $y || ( $x A.== $y && $(mkGtEq' xs ys) ) |]
      mkGtEq' _      _      = error "mkGtEq'"

      mkTup :: Int -> Q [Dec]
      mkTup n =
        let
            xs      = [ mkName ('x':show i) | i <- [0 .. n-1] ]
            ys      = [ mkName ('y':show i) | i <- [0 .. n-1] ]
            cst     = tupT (map (\x -> [t| Ord $(varT x) |]) xs)
            res     = tupT (map varT xs)
            pat vs  = conP (mkName ('T':show n)) (map varP vs)
        in
        [d| instance $cst => Ord $res where
              $(pat xs) <  $(pat ys) = $( mkLt' (map varE xs) (map varE ys) )
              $(pat xs) >  $(pat ys) = $( mkGt' (map varE xs) (map varE ys) )
              $(pat xs) >= $(pat ys) = $( mkGtEq' (map varE xs) (map varE ys) )
              $(pat xs) <= $(pat ys) = $( mkLtEq' (map varE xs) (map varE ys) )
          |]

  is <- mapM mkPrim integralTypes
  fs <- mapM mkPrim floatingTypes
  ns <- mapM mkPrim nonNumTypes
  cs <- mapM mkPrim cTypes
  ts <- mapM mkTup [2..16]
  return $ concat (concat [is,fs,ns,cs,ts])

instance Ord sh => Ord (sh :. Int) where
  Exp (sh :. Int)
x <= :: Exp (sh :. Int) -> Exp (sh :. Int) -> Exp Bool
<= Exp (sh :. Int)
y = Exp (sh :. Int) -> Exp Int
forall sh a. (Elt sh, Elt a) => Exp (sh :. a) -> Exp a
indexHead Exp (sh :. Int)
x Exp Int -> Exp Int -> Exp Bool
forall a. Ord a => Exp a -> Exp a -> Exp Bool
<= Exp (sh :. Int) -> Exp Int
forall sh a. (Elt sh, Elt a) => Exp (sh :. a) -> Exp a
indexHead Exp (sh :. Int)
y Exp Bool -> Exp Bool -> Exp Bool
&& Exp (sh :. Int) -> Exp sh
forall sh a. (Elt sh, Elt a) => Exp (sh :. a) -> Exp sh
indexTail Exp (sh :. Int)
x Exp sh -> Exp sh -> Exp Bool
forall a. Ord a => Exp a -> Exp a -> Exp Bool
<= Exp (sh :. Int) -> Exp sh
forall sh a. (Elt sh, Elt a) => Exp (sh :. a) -> Exp sh
indexTail Exp (sh :. Int)
y
  Exp (sh :. Int)
x >= :: Exp (sh :. Int) -> Exp (sh :. Int) -> Exp Bool
>= Exp (sh :. Int)
y = Exp (sh :. Int) -> Exp Int
forall sh a. (Elt sh, Elt a) => Exp (sh :. a) -> Exp a
indexHead Exp (sh :. Int)
x Exp Int -> Exp Int -> Exp Bool
forall a. Ord a => Exp a -> Exp a -> Exp Bool
>= Exp (sh :. Int) -> Exp Int
forall sh a. (Elt sh, Elt a) => Exp (sh :. a) -> Exp a
indexHead Exp (sh :. Int)
y Exp Bool -> Exp Bool -> Exp Bool
&& Exp (sh :. Int) -> Exp sh
forall sh a. (Elt sh, Elt a) => Exp (sh :. a) -> Exp sh
indexTail Exp (sh :. Int)
x Exp sh -> Exp sh -> Exp Bool
forall a. Ord a => Exp a -> Exp a -> Exp Bool
>= Exp (sh :. Int) -> Exp sh
forall sh a. (Elt sh, Elt a) => Exp (sh :. a) -> Exp sh
indexTail Exp (sh :. Int)
y
  Exp (sh :. Int)
x < :: Exp (sh :. Int) -> Exp (sh :. Int) -> Exp Bool
< Exp (sh :. Int)
y  = Exp (sh :. Int) -> Exp Int
forall sh a. (Elt sh, Elt a) => Exp (sh :. a) -> Exp a
indexHead Exp (sh :. Int)
x Exp Int -> Exp Int -> Exp Bool
forall a. Ord a => Exp a -> Exp a -> Exp Bool
< Exp (sh :. Int) -> Exp Int
forall sh a. (Elt sh, Elt a) => Exp (sh :. a) -> Exp a
indexHead Exp (sh :. Int)
y
        Exp Bool -> Exp Bool -> Exp Bool
&& case TypeR (EltR sh) -> TypeR () -> Maybe (EltR sh :~: ())
forall s t. TypeR s -> TypeR t -> Maybe (s :~: t)
matchTypeR (forall a. Elt a => TypeR (EltR a)
eltR @sh) (forall a. Elt a => TypeR (EltR a)
eltR @Z) of
             Just EltR sh :~: ()
Refl -> Bool -> Exp Bool
forall e. (HasCallStack, Elt e) => e -> Exp e
constant Bool
True
             Maybe (EltR sh :~: ())
Nothing   -> Exp (sh :. Int) -> Exp sh
forall sh a. (Elt sh, Elt a) => Exp (sh :. a) -> Exp sh
indexTail Exp (sh :. Int)
x Exp sh -> Exp sh -> Exp Bool
forall a. Ord a => Exp a -> Exp a -> Exp Bool
< Exp (sh :. Int) -> Exp sh
forall sh a. (Elt sh, Elt a) => Exp (sh :. a) -> Exp sh
indexTail Exp (sh :. Int)
y
  Exp (sh :. Int)
x > :: Exp (sh :. Int) -> Exp (sh :. Int) -> Exp Bool
> Exp (sh :. Int)
y  = Exp (sh :. Int) -> Exp Int
forall sh a. (Elt sh, Elt a) => Exp (sh :. a) -> Exp a
indexHead Exp (sh :. Int)
x Exp Int -> Exp Int -> Exp Bool
forall a. Ord a => Exp a -> Exp a -> Exp Bool
> Exp (sh :. Int) -> Exp Int
forall sh a. (Elt sh, Elt a) => Exp (sh :. a) -> Exp a
indexHead Exp (sh :. Int)
y
        Exp Bool -> Exp Bool -> Exp Bool
&& case TypeR (EltR sh) -> TypeR () -> Maybe (EltR sh :~: ())
forall s t. TypeR s -> TypeR t -> Maybe (s :~: t)
matchTypeR (forall a. Elt a => TypeR (EltR a)
eltR @sh) (forall a. Elt a => TypeR (EltR a)
eltR @Z) of
             Just EltR sh :~: ()
Refl -> Bool -> Exp Bool
forall e. (HasCallStack, Elt e) => e -> Exp e
constant Bool
True
             Maybe (EltR sh :~: ())
Nothing   -> Exp (sh :. Int) -> Exp sh
forall sh a. (Elt sh, Elt a) => Exp (sh :. a) -> Exp sh
indexTail Exp (sh :. Int)
x Exp sh -> Exp sh -> Exp Bool
forall a. Ord a => Exp a -> Exp a -> Exp Bool
> Exp (sh :. Int) -> Exp sh
forall sh a. (Elt sh, Elt a) => Exp (sh :. a) -> Exp sh
indexTail Exp (sh :. Int)
y

instance Ord Ordering where
  Exp Ordering
x < :: Exp Ordering -> Exp Ordering -> Exp Bool
< Exp Ordering
y   = Exp Ordering -> Exp TAG
forall a b. Coerce (EltR a) (EltR b) => Exp a -> Exp b
mkCoerce Exp Ordering
x Exp TAG -> Exp TAG -> Exp Bool
forall a. Ord a => Exp a -> Exp a -> Exp Bool
< (Exp Ordering -> Exp TAG
forall a b. Coerce (EltR a) (EltR b) => Exp a -> Exp b
mkCoerce Exp Ordering
y :: Exp TAG)
  Exp Ordering
x > :: Exp Ordering -> Exp Ordering -> Exp Bool
> Exp Ordering
y   = Exp Ordering -> Exp TAG
forall a b. Coerce (EltR a) (EltR b) => Exp a -> Exp b
mkCoerce Exp Ordering
x Exp TAG -> Exp TAG -> Exp Bool
forall a. Ord a => Exp a -> Exp a -> Exp Bool
> (Exp Ordering -> Exp TAG
forall a b. Coerce (EltR a) (EltR b) => Exp a -> Exp b
mkCoerce Exp Ordering
y :: Exp TAG)
  Exp Ordering
x <= :: Exp Ordering -> Exp Ordering -> Exp Bool
<= Exp Ordering
y  = Exp Ordering -> Exp TAG
forall a b. Coerce (EltR a) (EltR b) => Exp a -> Exp b
mkCoerce Exp Ordering
x Exp TAG -> Exp TAG -> Exp Bool
forall a. Ord a => Exp a -> Exp a -> Exp Bool
<= (Exp Ordering -> Exp TAG
forall a b. Coerce (EltR a) (EltR b) => Exp a -> Exp b
mkCoerce Exp Ordering
y :: Exp TAG)
  Exp Ordering
x >= :: Exp Ordering -> Exp Ordering -> Exp Bool
>= Exp Ordering
y  = Exp Ordering -> Exp TAG
forall a b. Coerce (EltR a) (EltR b) => Exp a -> Exp b
mkCoerce Exp Ordering
x Exp TAG -> Exp TAG -> Exp Bool
forall a. Ord a => Exp a -> Exp a -> Exp Bool
>= (Exp Ordering -> Exp TAG
forall a b. Coerce (EltR a) (EltR b) => Exp a -> Exp b
mkCoerce Exp Ordering
y :: Exp TAG)
  min :: Exp Ordering -> Exp Ordering -> Exp Ordering
min Exp Ordering
x Exp Ordering
y = Exp TAG -> Exp Ordering
forall a b. Coerce (EltR a) (EltR b) => Exp a -> Exp b
mkCoerce (Exp TAG -> Exp Ordering) -> Exp TAG -> Exp Ordering
forall a b. (a -> b) -> a -> b
$ Exp TAG -> Exp TAG -> Exp TAG
forall a. Ord a => Exp a -> Exp a -> Exp a
min (Exp Ordering -> Exp TAG
forall a b. Coerce (EltR a) (EltR b) => Exp a -> Exp b
mkCoerce Exp Ordering
x) (Exp Ordering -> Exp TAG
forall a b. Coerce (EltR a) (EltR b) => Exp a -> Exp b
mkCoerce Exp Ordering
y :: Exp TAG)
  max :: Exp Ordering -> Exp Ordering -> Exp Ordering
max Exp Ordering
x Exp Ordering
y = Exp TAG -> Exp Ordering
forall a b. Coerce (EltR a) (EltR b) => Exp a -> Exp b
mkCoerce (Exp TAG -> Exp Ordering) -> Exp TAG -> Exp Ordering
forall a b. (a -> b) -> a -> b
$ Exp TAG -> Exp TAG -> Exp TAG
forall a. Ord a => Exp a -> Exp a -> Exp a
max (Exp Ordering -> Exp TAG
forall a b. Coerce (EltR a) (EltR b) => Exp a -> Exp b
mkCoerce Exp Ordering
x) (Exp Ordering -> Exp TAG
forall a b. Coerce (EltR a) (EltR b) => Exp a -> Exp b
mkCoerce Exp Ordering
y :: Exp TAG)