symantic-lib/Language/Symantic/Lib/Ord.hs

   1 {-# LANGUAGE UndecidableInstances #-}
   2 {-# OPTIONS_GHC -fno-warn-orphans #-}
   3 -- | Symantic for 'Ord'.
   4 module Language.Symantic.Lib.Ord where
   5
   6 import Data.Ord (Ord)
   7 import Prelude hiding (Ord(..))
   8 import qualified Data.Ord as Ord
   9 import qualified Data.Text as Text
  10
  11 import Language.Symantic
  12 import Language.Symantic.Lib.Bool (tyBool)
  13 import Language.Symantic.Lib.Function (a0)
  14 import Language.Symantic.Lib.Eq (Sym_Eq)
  15
  16 -- * Class 'Sym_Ordering'
  17 type instance Sym Ordering = Sym_Ordering
  18 class Sym_Eq term => Sym_Ordering term where
  19         ordering :: Ordering -> term Ordering
  20         default ordering :: Sym_Ordering (UnT term) => Trans term => Ordering -> term Ordering
  21         ordering = trans . ordering
  22
  23 -- Interpreting
  24 instance Sym_Ordering Eval where
  25         ordering = Eval
  26 instance Sym_Ordering View where
  27         ordering o = View $ \_p _v ->
  28                 Text.pack (show o)
  29 instance (Sym_Ordering r1, Sym_Ordering r2) => Sym_Ordering (Dup r1 r2) where
  30         ordering o = ordering o `Dup` ordering o
  31
  32 -- Transforming
  33 instance (Sym_Ordering term, Sym_Lambda term) => Sym_Ordering (BetaT term)
  34
  35 -- Typing
  36 instance NameTyOf Ordering where
  37         nameTyOf _c = ["Ord"] `Mod` "Ordering"
  38 instance ClassInstancesFor Ordering
  39 instance TypeInstancesFor Ordering
  40
  41 -- Compiling
  42 instance Gram_Term_AtomsFor src ss g Ordering
  43 instance (Source src, SymInj ss Ordering) => ModuleFor src ss Ordering where
  44         moduleFor = [] `moduleWhere`
  45          [ "LT" := teOrdering LT
  46          , "EQ" := teOrdering EQ
  47          , "GT" := teOrdering GT
  48          ]
  49
  50 -- ** 'Type's
  51 tyOrdering :: Source src => LenInj vs => Type src vs Ordering
  52 tyOrdering = tyConst @(K Ordering) @Ordering
  53
  54 -- ** 'Term's
  55 teOrdering :: Source src => SymInj ss Ordering => Ordering -> Term src ss ts '[] (() #> Ordering)
  56 teOrdering o = Term noConstraint tyOrdering $ teSym @Ordering $ ordering o
  57
  58 -- * Class 'Sym_Ord'
  59 type instance Sym Ord = Sym_Ord
  60 class Sym_Eq term => Sym_Ord term where
  61         compare  :: Ord a => term a -> term a -> term Ordering
  62         (<)      :: Ord a => term a -> term a -> term Bool; infix 4 <
  63         (<=)     :: Ord a => term a -> term a -> term Bool; infix 4 <=
  64         (>)      :: Ord a => term a -> term a -> term Bool; infix 4 >
  65         (>=)     :: Ord a => term a -> term a -> term Bool; infix 4 >=
  66         max      :: Ord a => term a -> term a -> term a
  67         min      :: Ord a => term a -> term a -> term a
  68
  69         default compare  :: Sym_Ord (UnT term) => Trans term => Ord a => term a -> term a -> term Ordering
  70         default (<)      :: Sym_Ord (UnT term) => Trans term => Ord a => term a -> term a -> term Bool
  71         default (<=)     :: Sym_Ord (UnT term) => Trans term => Ord a => term a -> term a -> term Bool
  72         default (>)      :: Sym_Ord (UnT term) => Trans term => Ord a => term a -> term a -> term Bool
  73         default (>=)     :: Sym_Ord (UnT term) => Trans term => Ord a => term a -> term a -> term Bool
  74         default max      :: Sym_Ord (UnT term) => Trans term => Ord a => term a -> term a -> term a
  75         default min      :: Sym_Ord (UnT term) => Trans term => Ord a => term a -> term a -> term a
  76
  77         compare  = trans2 compare
  78         (<)      = trans2 (<)
  79         (<=)     = trans2 (<=)
  80         (>)      = trans2 (>)
  81         (>=)     = trans2 (>=)
  82         min      = trans2 min
  83         max      = trans2 max
  84
  85 -- Interpreting
  86 instance Sym_Ord Eval where
  87         compare  = eval2 Ord.compare
  88         (<)      = eval2 (Ord.<)
  89         (<=)     = eval2 (Ord.<=)
  90         (>)      = eval2 (Ord.>)
  91         (>=)     = eval2 (Ord.>=)
  92         min      = eval2 Ord.min
  93         max      = eval2 Ord.max
  94 instance Sym_Ord View where
  95         compare  = view2 "compare"
  96         (<)      = viewInfix "<"  (infixN 4)
  97         (<=)     = viewInfix "<=" (infixN 4)
  98         (>)      = viewInfix ">"  (infixN 4)
  99         (>=)     = viewInfix ">=" (infixN 4)
 100         min      = view2 "min"
 101         max      = view2 "max"
 102 instance (Sym_Ord r1, Sym_Ord r2) => Sym_Ord (Dup r1 r2) where
 103         compare    = dup2 @Sym_Ord compare
 104         (<)        = dup2 @Sym_Ord (<)
 105         (<=)       = dup2 @Sym_Ord (<=)
 106         (>)        = dup2 @Sym_Ord (>)
 107         (>=)       = dup2 @Sym_Ord (>=)
 108         min        = dup2 @Sym_Ord min
 109         max        = dup2 @Sym_Ord max
 110
 111 -- Transforming
 112 instance (Sym_Ord term, Sym_Lambda term) => Sym_Ord (BetaT term)
 113
 114 -- Typing
 115 instance NameTyOf Ord where
 116         nameTyOf _c = ["Ord"] `Mod` "Ord"
 117 instance FixityOf Ord
 118 instance ClassInstancesFor Ord where
 119         proveConstraintFor _ (TyConst _ _ q :$ z)
 120          | Just HRefl <- proj_ConstKiTy @_ @Ordering z
 121          = case () of
 122                  _ | Just Refl <- proj_Const @Bounded q -> Just Dict
 123                    | Just Refl <- proj_Const @Enum    q -> Just Dict
 124                    | Just Refl <- proj_Const @Eq      q -> Just Dict
 125                    | Just Refl <- proj_Const @Ord     q -> Just Dict
 126                    | Just Refl <- proj_Const @Show    q -> Just Dict
 127                  _ -> Nothing
 128         proveConstraintFor _c _q = Nothing
 129 instance TypeInstancesFor Ord
 130
 131 -- Compiling
 132 instance Gram_Term_AtomsFor src ss g Ord
 133 instance (Source src, SymInj ss Ord) => ModuleFor src ss Ord where
 134         moduleFor = ["Ord"] `moduleWhere`
 135          [ "compare" := teOrd_compare
 136          , "<"  `withInfixN` 4 := teOrd_lt
 137          , "<=" `withInfixN` 4 := teOrd_le
 138          , ">"  `withInfixN` 4 := teOrd_gt
 139          , ">=" `withInfixN` 4 := teOrd_ge
 140          ]
 141
 142 -- ** 'Type's
 143 tyOrd :: Source src => Type src vs a -> Type src vs (Ord a)
 144 tyOrd a = tyConstLen @(K Ord) @Ord (lenVars a) `tyApp` a
 145
 146 -- ** 'Term's
 147 teOrd_compare :: TermDef Ord '[Proxy a] (Ord a #> (a -> a -> Ordering))
 148 teOrd_compare = Term (tyOrd a0) (a0 ~> a0 ~> tyOrdering) $ teSym @Ord $ lam2 compare
 149
 150 teOrd_le, teOrd_lt, teOrd_ge, teOrd_gt :: TermDef Ord '[Proxy a] (Ord a #> (a -> a -> Bool))
 151 teOrd_le = Term (tyOrd a0) (a0 ~> a0 ~> tyBool) $ teSym @Ord $ lam2 (<=)
 152 teOrd_lt = Term (tyOrd a0) (a0 ~> a0 ~> tyBool) $ teSym @Ord $ lam2 (<)
 153 teOrd_ge = Term (tyOrd a0) (a0 ~> a0 ~> tyBool) $ teSym @Ord $ lam2 (>=)
 154 teOrd_gt = Term (tyOrd a0) (a0 ~> a0 ~> tyBool) $ teSym @Ord $ lam2 (>)
 155
 156 teOrd_min, teOrd_max :: TermDef Ord '[Proxy a] (Ord a #> (a -> a -> a))
 157 teOrd_min = Term (tyOrd a0) (a0 ~> a0 ~> a0) $ teSym @Ord $ lam2 min
 158 teOrd_max = Term (tyOrd a0) (a0 ~> a0 ~> a0) $ teSym @Ord $ lam2 max