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 (Proxy 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 ClassInstancesFor Ordering
  37 instance TypeInstancesFor Ordering
  38
  39 -- Compiling
  40 instance Gram_Term_AtomsFor src ss g Ordering
  41 instance (Source src, Inj_Sym ss Ordering) => ModuleFor src ss Ordering where
  42         moduleFor = [] `moduleWhere`
  43          [ "LT" := teOrdering LT
  44          , "EQ" := teOrdering EQ
  45          , "GT" := teOrdering GT
  46          ]
  47
  48 -- ** 'Type's
  49 tyOrdering :: Source src => Inj_Len vs => Type src vs Ordering
  50 tyOrdering = tyConst @(K Ordering) @Ordering
  51
  52 -- ** 'Term's
  53 teOrdering :: Source src => Inj_Sym ss Ordering => Ordering -> Term src ss ts '[] (() #> Ordering)
  54 teOrdering o = Term noConstraint tyOrdering $ teSym @Ordering $ ordering o
  55
  56 -- * Class 'Sym_Ord'
  57 type instance Sym (Proxy Ord) = Sym_Ord
  58 class Sym_Eq term => Sym_Ord term where
  59         compare  :: Ord a => term a -> term a -> term Ordering
  60         (<)      :: Ord a => term a -> term a -> term Bool; infix 4 <
  61         (<=)     :: Ord a => term a -> term a -> term Bool; infix 4 <=
  62         (>)      :: Ord a => term a -> term a -> term Bool; infix 4 >
  63         (>=)     :: Ord a => term a -> term a -> term Bool; infix 4 >=
  64         max      :: Ord a => term a -> term a -> term a
  65         min      :: Ord a => term a -> term a -> term a
  66
  67         default compare  :: Sym_Ord (UnT term) => Trans term => Ord a => term a -> term a -> term Ordering
  68         default (<)      :: Sym_Ord (UnT term) => Trans term => Ord a => term a -> term a -> term Bool
  69         default (<=)     :: Sym_Ord (UnT term) => Trans term => Ord a => term a -> term a -> term Bool
  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 max      :: Sym_Ord (UnT term) => Trans term => Ord a => term a -> term a -> term a
  73         default min      :: Sym_Ord (UnT term) => Trans term => Ord a => term a -> term a -> term a
  74
  75         compare  = trans2 compare
  76         (<)      = trans2 (<)
  77         (<=)     = trans2 (<=)
  78         (>)      = trans2 (>)
  79         (>=)     = trans2 (>=)
  80         min      = trans2 min
  81         max      = trans2 max
  82
  83 -- Interpreting
  84 instance Sym_Ord Eval where
  85         compare  = eval2 Ord.compare
  86         (<)      = eval2 (Ord.<)
  87         (<=)     = eval2 (Ord.<=)
  88         (>)      = eval2 (Ord.>)
  89         (>=)     = eval2 (Ord.>=)
  90         min      = eval2 Ord.min
  91         max      = eval2 Ord.max
  92 instance Sym_Ord View where
  93         compare  = view2 "compare"
  94         (<)      = viewInfix "<"  (infixN 4)
  95         (<=)     = viewInfix "<=" (infixN 4)
  96         (>)      = viewInfix ">"  (infixN 4)
  97         (>=)     = viewInfix ">=" (infixN 4)
  98         min      = view2 "min"
  99         max      = view2 "max"
 100 instance (Sym_Ord r1, Sym_Ord r2) => Sym_Ord (Dup r1 r2) where
 101         compare    = dup2 @Sym_Ord compare
 102         (<)        = dup2 @Sym_Ord (<)
 103         (<=)       = dup2 @Sym_Ord (<=)
 104         (>)        = dup2 @Sym_Ord (>)
 105         (>=)       = dup2 @Sym_Ord (>=)
 106         min        = dup2 @Sym_Ord min
 107         max        = dup2 @Sym_Ord max
 108
 109 -- Transforming
 110 instance (Sym_Ord term, Sym_Lambda term) => Sym_Ord (BetaT term)
 111
 112 -- Typing
 113 instance FixityOf Ord
 114 instance ClassInstancesFor Ord where
 115         proveConstraintFor _ (TyApp _ (TyConst _ _ q) z)
 116          | Just HRefl <- proj_ConstKiTy @_ @Ordering z
 117          = case () of
 118                  _ | Just Refl <- proj_Const @Bounded q -> Just Dict
 119                    | Just Refl <- proj_Const @Enum    q -> Just Dict
 120                    | Just Refl <- proj_Const @Eq      q -> Just Dict
 121                    | Just Refl <- proj_Const @Ord     q -> Just Dict
 122                    | Just Refl <- proj_Const @Show    q -> Just Dict
 123                  _ -> Nothing
 124         proveConstraintFor _c _q = Nothing
 125 instance TypeInstancesFor Ord
 126
 127 -- Compiling
 128 instance Gram_Term_AtomsFor src ss g Ord
 129 instance (Source src, Inj_Sym ss Ord) => ModuleFor src ss Ord where
 130         moduleFor = ["Ord"] `moduleWhere`
 131          [ "compare" := teOrd_compare
 132          , "<"  `withInfixN` 4 := teOrd_lt
 133          , "<=" `withInfixN` 4 := teOrd_le
 134          , ">"  `withInfixN` 4 := teOrd_gt
 135          , ">=" `withInfixN` 4 := teOrd_ge
 136          ]
 137
 138 -- ** 'Type's
 139 tyOrd :: Source src => Type src vs a -> Type src vs (Ord a)
 140 tyOrd a = tyConstLen @(K Ord) @Ord (lenVars a) `tyApp` a
 141
 142 -- ** 'Term's
 143 teOrd_compare :: TermDef Ord '[Proxy a] (Ord a #> (a -> a -> Ordering))
 144 teOrd_compare = Term (tyOrd a0) (a0 ~> a0 ~> tyOrdering) $ teSym @Ord $ lam2 compare
 145
 146 teOrd_le, teOrd_lt, teOrd_ge, teOrd_gt :: TermDef Ord '[Proxy a] (Ord a #> (a -> a -> Bool))
 147 teOrd_le = Term (tyOrd a0) (a0 ~> a0 ~> tyBool) $ teSym @Ord $ lam2 (<=)
 148 teOrd_lt = Term (tyOrd a0) (a0 ~> a0 ~> tyBool) $ teSym @Ord $ lam2 (<)
 149 teOrd_ge = Term (tyOrd a0) (a0 ~> a0 ~> tyBool) $ teSym @Ord $ lam2 (>=)
 150 teOrd_gt = Term (tyOrd a0) (a0 ~> a0 ~> tyBool) $ teSym @Ord $ lam2 (>)
 151
 152 teOrd_min, teOrd_max :: TermDef Ord '[Proxy a] (Ord a #> (a -> a -> a))
 153 teOrd_min = Term (tyOrd a0) (a0 ~> a0 ~> a0) $ teSym @Ord $ lam2 min
 154 teOrd_max = Term (tyOrd a0) (a0 ~> a0 ~> a0) $ teSym @Ord $ lam2 max