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 Control.Monad
   7 import Data.Ord (Ord)
   8 import Data.Proxy (Proxy(..))
   9 import Data.Type.Equality ((:~:)(Refl))
  10 import Prelude hiding (Ord(..))
  11 import qualified Data.Kind as Kind
  12 import qualified Data.Ord as Ord
  13 import qualified Data.Text as Text
  14
  15 import Language.Symantic.Parsing
  16 import Language.Symantic.Typing
  17 import Language.Symantic.Compiling
  18 import Language.Symantic.Interpreting
  19 import Language.Symantic.Transforming
  20 import Language.Symantic.Lib.Lambda
  21 import Language.Symantic.Lib.Eq (Sym_Eq)
  22 import Language.Symantic.Lib.MonoFunctor (TyFam_MonoElement)
  23
  24 -- * Class 'Sym_Ord'
  25 class Sym_Eq term => Sym_Ord term where
  26         compare  :: Ord a => term a -> term a -> term Ordering
  27         (<)      :: Ord a => term a -> term a -> term Bool; infix 4 <
  28         (<=)     :: Ord a => term a -> term a -> term Bool; infix 4 <=
  29         (>)      :: Ord a => term a -> term a -> term Bool; infix 4 >
  30         (>=)     :: Ord a => term a -> term a -> term Bool; infix 4 >=
  31         max      :: Ord a => term a -> term a -> term a
  32         min      :: Ord a => term a -> term a -> term a
  33
  34         default compare  :: (Trans t term, Ord a) => t term a -> t term a -> t term Ordering
  35         default (<)      :: (Trans t term, Ord a) => t term a -> t term a -> t term Bool
  36         default (<=)     :: (Trans t term, Ord a) => t term a -> t term a -> t term Bool
  37         default (>)      :: (Trans t term, Ord a) => t term a -> t term a -> t term Bool
  38         default (>=)     :: (Trans t term, Ord a) => t term a -> t term a -> t term Bool
  39         default max      :: (Trans t term, Ord a) => t term a -> t term a -> t term a
  40         default min      :: (Trans t term, Ord a) => t term a -> t term a -> t term a
  41
  42         compare  = trans_map2 compare
  43         (<)      = trans_map2 (<)
  44         (<=)     = trans_map2 (<=)
  45         (>)      = trans_map2 (>)
  46         (>=)     = trans_map2 (>=)
  47         min      = trans_map2 min
  48         max      = trans_map2 max
  49
  50 -- * Class 'Sym_Ordering'
  51 class Sym_Eq term => Sym_Ordering term where
  52         ordering :: Ordering -> term Ordering
  53         default ordering :: Trans t term => Ordering -> t term Ordering
  54         ordering = trans_lift . ordering
  55
  56 type instance Sym_of_Iface (Proxy Ord) = Sym_Ord
  57 type instance Sym_of_Iface (Proxy Ordering) = Sym_Ordering
  58 type instance TyConsts_of_Iface (Proxy Ord) = Proxy Ord ': TyConsts_imported_by (Proxy Ord)
  59 type instance TyConsts_of_Iface (Proxy Ordering) = Proxy Ordering ': TyConsts_imported_by (Proxy Ordering)
  60 type instance TyConsts_imported_by (Proxy Ord) =
  61  [ Proxy Bool
  62  , Proxy Ordering
  63  ]
  64 type instance TyConsts_imported_by (Proxy Ordering) =
  65  [ Proxy Bounded
  66  , Proxy Enum
  67  , Proxy Eq
  68  , Proxy Ord
  69  , Proxy Show
  70  ]
  71
  72 instance Sym_Ord HostI where
  73         compare  = liftM2 Ord.compare
  74         (<)      = liftM2 (Ord.<)
  75         (<=)     = liftM2 (Ord.<=)
  76         (>)      = liftM2 (Ord.>)
  77         (>=)     = liftM2 (Ord.>=)
  78         min      = liftM2 Ord.min
  79         max      = liftM2 Ord.max
  80 instance Sym_Ordering HostI where
  81         ordering = HostI
  82 instance Sym_Ord TextI where
  83         compare  = textI2 "compare"
  84         (<)      = textI_infix "<"  (infixN 4)
  85         (<=)     = textI_infix "<=" (infixN 4)
  86         (>)      = textI_infix ">"  (infixN 4)
  87         (>=)     = textI_infix ">=" (infixN 4)
  88         min      = textI2 "min"
  89         max      = textI2 "max"
  90 instance Sym_Ordering TextI where
  91         ordering o = TextI $ \_p _v ->
  92                 Text.pack (show o)
  93 instance (Sym_Ord r1, Sym_Ord r2) => Sym_Ord (DupI r1 r2) where
  94         compare    = dupI2 @Sym_Ord compare
  95         (<)        = dupI2 @Sym_Ord (<)
  96         (<=)       = dupI2 @Sym_Ord (<=)
  97         (>)        = dupI2 @Sym_Ord (>)
  98         (>=)       = dupI2 @Sym_Ord (>=)
  99         min        = dupI2 @Sym_Ord min
 100         max        = dupI2 @Sym_Ord max
 101 instance (Sym_Ordering r1, Sym_Ordering r2) => Sym_Ordering (DupI r1 r2) where
 102         ordering o = ordering o `DupI` ordering o
 103
 104 instance
 105  ( Read_TyNameR TyName cs rs
 106  , Inj_TyConst cs Ord
 107  ) => Read_TyNameR TyName cs (Proxy Ord ': rs) where
 108         read_TyNameR _cs (TyName "Ord") k = k (ty @Ord)
 109         read_TyNameR _rs raw k = read_TyNameR (Proxy @rs) raw k
 110 instance
 111  ( Read_TyNameR TyName cs rs
 112  , Inj_TyConst cs Ordering
 113  ) => Read_TyNameR TyName cs (Proxy Ordering ': rs) where
 114         read_TyNameR _cs (TyName "Ordering") k = k (ty @Ordering)
 115         read_TyNameR _rs raw k = read_TyNameR (Proxy @rs) raw k
 116 instance Show_TyConst cs => Show_TyConst (Proxy Ord ': cs) where
 117         show_TyConst TyConstZ{} = "Ord"
 118         show_TyConst (TyConstS c) = show_TyConst c
 119 instance Show_TyConst cs => Show_TyConst (Proxy Ordering ': cs) where
 120         show_TyConst TyConstZ{} = "Ordering"
 121         show_TyConst (TyConstS c) = show_TyConst c
 122
 123 instance Proj_TyFamC cs TyFam_MonoElement Ordering
 124
 125 instance Proj_TyConC cs (Proxy Ord)
 126 instance -- Proj_TyConC
 127  ( Proj_TyConst cs Ordering
 128  , Proj_TyConsts cs (TyConsts_imported_by (Proxy Ordering))
 129  ) => Proj_TyConC cs (Proxy Ordering) where
 130         proj_TyConC _ (TyConst q :$ TyConst c)
 131          | Just Refl <- eq_SKind (kind_of_TyConst c) SKiType
 132          , Just Refl <- proj_TyConst c (Proxy @Ordering)
 133          = case () of
 134                  _ | Just Refl <- proj_TyConst q (Proxy @Bounded) -> Just TyCon
 135                    | Just Refl <- proj_TyConst q (Proxy @Enum)    -> Just TyCon
 136                    | Just Refl <- proj_TyConst q (Proxy @Eq)      -> Just TyCon
 137                    | Just Refl <- proj_TyConst q (Proxy @Ord)     -> Just TyCon
 138                    | Just Refl <- proj_TyConst q (Proxy @Show)    -> Just TyCon
 139                  _ -> Nothing
 140         proj_TyConC _c _q = Nothing
 141 data instance TokenT meta (ts::[*]) (Proxy Ord)
 142  = Token_Term_Ord_compare (EToken meta ts)
 143  | Token_Term_Ord_le      (EToken meta ts)
 144  | Token_Term_Ord_lt      (EToken meta ts)
 145  | Token_Term_Ord_ge      (EToken meta ts)
 146  | Token_Term_Ord_gt      (EToken meta ts)
 147  | Token_Term_Ord_min     (EToken meta ts)
 148  | Token_Term_Ord_max     (EToken meta ts)
 149 data instance TokenT meta (ts::[*]) (Proxy Ordering)
 150  = Token_Term_Ordering Ordering
 151 deriving instance Eq_Token meta ts => Eq (TokenT meta ts (Proxy Ord))
 152 deriving instance Eq_Token meta ts => Eq (TokenT meta ts (Proxy Ordering))
 153 deriving instance Show_Token meta ts => Show (TokenT meta ts (Proxy Ord))
 154 deriving instance Show_Token meta ts => Show (TokenT meta ts (Proxy Ordering))
 155
 156 instance -- CompileI
 157  ( Inj_TyConst cs Bool
 158  , Inj_TyConst cs (->)
 159  , Inj_TyConst cs Ord
 160  , Inj_TyConst cs Ordering
 161  , Proj_TyCon  cs
 162  , Compile cs is
 163  ) => CompileI cs is (Proxy Ord) where
 164         compileI
 165          :: forall meta ctx ret ls rs.
 166          TokenT meta is (Proxy Ord)
 167          -> Compiler meta ctx ret cs is ls (Proxy Ord ': rs)
 168         compileI tok ctx k =
 169                 case tok of
 170                  Token_Term_Ord_compare tok_a -> compare_from tok_a (ty @Ordering) compare
 171                  Token_Term_Ord_le      tok_a -> compare_from tok_a (ty @Bool) (<=)
 172                  Token_Term_Ord_lt      tok_a -> compare_from tok_a (ty @Bool) (<)
 173                  Token_Term_Ord_ge      tok_a -> compare_from tok_a (ty @Bool) (>=)
 174                  Token_Term_Ord_gt      tok_a -> compare_from tok_a (ty @Bool) (>)
 175                  Token_Term_Ord_min     tok_a -> op2_from tok_a min
 176                  Token_Term_Ord_max     tok_a -> op2_from tok_a max
 177                 where
 178                 compare_from
 179                  :: EToken meta is
 180                  -> Type cs (res::Kind.Type)
 181                  -> (forall term a. (Sym_Ord term, Ord a) => term a -> term a -> term res)
 182                  -> Either (Error_Term meta cs is) ret
 183                 compare_from tok_a ty_res op =
 184                  -- compare :: Ord a => a -> a -> Ordering
 185                  -- (<=)    :: Ord a => a -> a -> Bool
 186                  -- (<)     :: Ord a => a -> a -> Bool
 187                  -- (>=)    :: Ord a => a -> a -> Bool
 188                  -- (>)     :: Ord a => a -> a -> Bool
 189                         compile tok_a ctx $ \ty_a (Term x) ->
 190                         check_TyCon (At (Just tok_a) (ty @Ord :$ ty_a)) $ \TyCon ->
 191                         k (ty_a ~> ty_res) $ Term $
 192                          \c -> lam $ op (x c)
 193                 op2_from tok_a
 194                  (op::forall term a. (Sym_Ord term, Ord a)
 195                          => term a -> term a -> term a) =
 196                  -- min :: Ord a => a -> a -> a
 197                  -- max :: Ord a => a -> a -> a
 198                         compile tok_a ctx $ \ty_a (Term x) ->
 199                         check_TyCon (At (Just tok_a) (ty @Ord :$ ty_a)) $ \TyCon ->
 200                         k (ty_a ~> ty_a) $ Term $
 201                          \c -> lam $ \y -> op (x c) y
 202 instance -- CompileI
 203  ( Inj_TyConst cs Ordering
 204  ) => CompileI cs is (Proxy Ordering) where
 205         compileI tok _ctx k =
 206                 case tok of
 207                  Token_Term_Ordering o -> k (ty @Ordering) $ Term $ \_c -> ordering o
 208 instance -- TokenizeT
 209  Inj_Token meta ts Ord =>
 210  TokenizeT meta ts (Proxy Ord) where
 211         tokenizeT _t = mempty
 212          { tokenizers_infix = tokenizeTMod []
 213                  [ tokenize1 "compare" infixN5 Token_Term_Ord_compare
 214                  , tokenize1 "<"  (infixN 4) Token_Term_Ord_lt
 215                  , tokenize1 "<=" (infixN 4) Token_Term_Ord_le
 216                  , tokenize1 ">"  (infixN 4) Token_Term_Ord_gt
 217                  , tokenize1 ">=" (infixN 4) Token_Term_Ord_ge
 218                  ]
 219          }
 220 instance -- TokenizeT
 221  Inj_Token meta ts Ordering =>
 222  TokenizeT meta ts (Proxy Ordering) where
 223         tokenizeT _t = mempty
 224          { tokenizers_infix = tokenizeTMod []
 225                  [ tokenize0 "LT" infixN5 $ Token_Term_Ordering LT
 226                  , tokenize0 "EQ" infixN5 $ Token_Term_Ordering EQ
 227                  , tokenize0 "GT" infixN5 $ Token_Term_Ordering GT
 228                  ]
 229          }
 230 instance Gram_Term_AtomsT meta ts (Proxy Ordering) g
 231 instance Gram_Term_AtomsT meta ts (Proxy Ord) g