{-# LANGUAGE UndecidableInstances #-} {-# OPTIONS_GHC -fno-warn-orphans #-} -- | Symantic for 'Ord'. 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) -- * Class 'Sym_Ordering' type instance Sym (Proxy 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 -- Interpreting 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 -- Transforming instance (Sym_Ordering term, Sym_Lambda term) => Sym_Ordering (BetaT term) -- Typing instance ClassInstancesFor Ordering instance TypeInstancesFor Ordering -- Compiling instance Gram_Term_AtomsFor src ss g Ordering instance (Source src, Inj_Sym ss Ordering) => ModuleFor src ss Ordering where moduleFor _s = [] `moduleWhere` [ "LT" := teOrdering LT , "EQ" := teOrdering EQ , "GT" := teOrdering GT ] -- ** 'Type's tyOrdering :: Source src => Inj_Len vs => Type src vs Ordering tyOrdering = tyConst @(K Ordering) @Ordering -- ** 'Term's teOrdering :: Source src => Inj_Sym ss Ordering => Ordering -> Term src ss ts '[] (() #> Ordering) teOrdering o = Term noConstraint tyOrdering $ teSym @Ordering $ ordering o -- * Class 'Sym_Ord' type instance Sym (Proxy 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 -- Interpreting 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 -- Transforming instance (Sym_Ord term, Sym_Lambda term) => Sym_Ord (BetaT term) -- Typing instance FixityOf Ord instance ClassInstancesFor Ord where proveConstraintFor _ (TyApp _ (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 -- Compiling instance Gram_Term_AtomsFor src ss g Ord instance (Source src, Inj_Sym ss Ord) => ModuleFor src ss Ord where moduleFor _s = ["Ord"] `moduleWhere` [ "compare" := teOrd_compare , "<" `withInfixN` 4 := teOrd_lt , "<=" `withInfixN` 4 := teOrd_le , ">" `withInfixN` 4 := teOrd_gt , ">=" `withInfixN` 4 := teOrd_ge ] -- ** 'Type's tyOrd :: Source src => Type src vs a -> Type src vs (Ord a) tyOrd a = tyConstLen @(K Ord) @Ord (lenVars a) `tyApp` a -- ** 'Term's 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