{-# LANGUAGE UndecidableInstances #-}
{-# OPTIONS_GHC -fno-warn-orphans #-}
module Language.Symantic.Lib.Ord where
import Data.Ord (Ord)
import Prelude hiding (Ord(..))
import qualified Data.Ord as Ord
import qualified Data.Text as Text
import Language.Symantic
import Language.Symantic.Lib.Bool (tyBool)
import Language.Symantic.Lib.Function (a0)
import Language.Symantic.Lib.Eq (Sym_Eq)
type instance Sym Ordering = Sym_Ordering
class Sym_Eq term => Sym_Ordering term where
ordering :: Ordering -> term Ordering
default ordering :: Sym_Ordering (UnT term) => Trans term => Ordering -> term Ordering
ordering = trans . ordering
instance Sym_Ordering Eval where
ordering = Eval
instance Sym_Ordering View where
ordering o = View $ \_p _v ->
Text.pack (show o)
instance (Sym_Ordering r1, Sym_Ordering r2) => Sym_Ordering (Dup r1 r2) where
ordering o = ordering o `Dup` ordering o
instance (Sym_Ordering term, Sym_Lambda term) => Sym_Ordering (BetaT term)
instance NameTyOf Ordering where
nameTyOf _c = ["Ord"] `Mod` "Ordering"
instance ClassInstancesFor Ordering
instance TypeInstancesFor Ordering
instance Gram_Term_AtomsFor src ss g Ordering
instance (Source src, SymInj ss Ordering) => ModuleFor src ss Ordering where
moduleFor = [] `moduleWhere`
[ "LT" := teOrdering LT
, "EQ" := teOrdering EQ
, "GT" := teOrdering GT
]
tyOrdering :: Source src => LenInj vs => Type src vs Ordering
tyOrdering = tyConst @(K Ordering) @Ordering
teOrdering :: Source src => SymInj ss Ordering => Ordering -> Term src ss ts '[] (() #> Ordering)
teOrdering o = Term noConstraint tyOrdering $ teSym @Ordering $ ordering o
type instance Sym Ord = Sym_Ord
class Sym_Eq term => Sym_Ord term where
compare :: Ord a => term a -> term a -> term Ordering
(<) :: Ord a => term a -> term a -> term Bool; infix 4 <
(<=) :: Ord a => term a -> term a -> term Bool; infix 4 <=
(>) :: Ord a => term a -> term a -> term Bool; infix 4 >
(>=) :: Ord a => term a -> term a -> term Bool; infix 4 >=
max :: Ord a => term a -> term a -> term a
min :: Ord a => term a -> term a -> term a
default compare :: Sym_Ord (UnT term) => Trans term => Ord a => term a -> term a -> term Ordering
default (<) :: Sym_Ord (UnT term) => Trans term => Ord a => term a -> term a -> term Bool
default (<=) :: Sym_Ord (UnT term) => Trans term => Ord a => term a -> term a -> term Bool
default (>) :: Sym_Ord (UnT term) => Trans term => Ord a => term a -> term a -> term Bool
default (>=) :: Sym_Ord (UnT term) => Trans term => Ord a => term a -> term a -> term Bool
default max :: Sym_Ord (UnT term) => Trans term => Ord a => term a -> term a -> term a
default min :: Sym_Ord (UnT term) => Trans term => Ord a => term a -> term a -> term a
compare = trans2 compare
(<) = trans2 (<)
(<=) = trans2 (<=)
(>) = trans2 (>)
(>=) = trans2 (>=)
min = trans2 min
max = trans2 max
instance Sym_Ord Eval where
compare = eval2 Ord.compare
(<) = eval2 (Ord.<)
(<=) = eval2 (Ord.<=)
(>) = eval2 (Ord.>)
(>=) = eval2 (Ord.>=)
min = eval2 Ord.min
max = eval2 Ord.max
instance Sym_Ord View where
compare = view2 "compare"
(<) = viewInfix "<" (infixN 4)
(<=) = viewInfix "<=" (infixN 4)
(>) = viewInfix ">" (infixN 4)
(>=) = viewInfix ">=" (infixN 4)
min = view2 "min"
max = view2 "max"
instance (Sym_Ord r1, Sym_Ord r2) => Sym_Ord (Dup r1 r2) where
compare = dup2 @Sym_Ord compare
(<) = dup2 @Sym_Ord (<)
(<=) = dup2 @Sym_Ord (<=)
(>) = dup2 @Sym_Ord (>)
(>=) = dup2 @Sym_Ord (>=)
min = dup2 @Sym_Ord min
max = dup2 @Sym_Ord max
instance (Sym_Ord term, Sym_Lambda term) => Sym_Ord (BetaT term)
instance NameTyOf Ord where
nameTyOf _c = ["Ord"] `Mod` "Ord"
instance FixityOf Ord
instance ClassInstancesFor Ord where
proveConstraintFor _ (TyConst _ _ q :$ z)
| Just HRefl <- proj_ConstKiTy @_ @Ordering z
= case () of
_ | Just Refl <- proj_Const @Bounded q -> Just Dict
| Just Refl <- proj_Const @Enum q -> Just Dict
| Just Refl <- proj_Const @Eq q -> Just Dict
| Just Refl <- proj_Const @Ord q -> Just Dict
| Just Refl <- proj_Const @Show q -> Just Dict
_ -> Nothing
proveConstraintFor _c _q = Nothing
instance TypeInstancesFor Ord
instance Gram_Term_AtomsFor src ss g Ord
instance (Source src, SymInj ss Ord) => ModuleFor src ss Ord where
moduleFor = ["Ord"] `moduleWhere`
[ "compare" := teOrd_compare
, "<" `withInfixN` 4 := teOrd_lt
, "<=" `withInfixN` 4 := teOrd_le
, ">" `withInfixN` 4 := teOrd_gt
, ">=" `withInfixN` 4 := teOrd_ge
]
tyOrd :: Source src => Type src vs a -> Type src vs (Ord a)
tyOrd a = tyConstLen @(K Ord) @Ord (lenVars a) `tyApp` a
teOrd_compare :: TermDef Ord '[Proxy a] (Ord a #> (a -> a -> Ordering))
teOrd_compare = Term (tyOrd a0) (a0 ~> a0 ~> tyOrdering) $ teSym @Ord $ lam2 compare
teOrd_le, teOrd_lt, teOrd_ge, teOrd_gt :: TermDef Ord '[Proxy a] (Ord a #> (a -> a -> Bool))
teOrd_le = Term (tyOrd a0) (a0 ~> a0 ~> tyBool) $ teSym @Ord $ lam2 (<=)
teOrd_lt = Term (tyOrd a0) (a0 ~> a0 ~> tyBool) $ teSym @Ord $ lam2 (<)
teOrd_ge = Term (tyOrd a0) (a0 ~> a0 ~> tyBool) $ teSym @Ord $ lam2 (>=)
teOrd_gt = Term (tyOrd a0) (a0 ~> a0 ~> tyBool) $ teSym @Ord $ lam2 (>)
teOrd_min, teOrd_max :: TermDef Ord '[Proxy a] (Ord a #> (a -> a -> a))
teOrd_min = Term (tyOrd a0) (a0 ~> a0 ~> a0) $ teSym @Ord $ lam2 min
teOrd_max = Term (tyOrd a0) (a0 ~> a0 ~> a0) $ teSym @Ord $ lam2 max