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 type instance TyConsts_imported_by (Proxy Ordering) =
  62  [ Proxy Bounded
  63  , Proxy Enum
  64  , Proxy Eq
  65  , Proxy Ord
  66  , Proxy Show
  67  ]
  68
  69 instance Sym_Ord HostI where
  70         compare  = liftM2 Ord.compare
  71         (<)      = liftM2 (Ord.<)
  72         (<=)     = liftM2 (Ord.<=)
  73         (>)      = liftM2 (Ord.>)
  74         (>=)     = liftM2 (Ord.>=)
  75         min      = liftM2 Ord.min
  76         max      = liftM2 Ord.max
  77 instance Sym_Ordering HostI where
  78         ordering = HostI
  79 instance Sym_Ord TextI where
  80         compare  = textI2 "compare"
  81         (<)      = textI_infix "<"  (infixN 4)
  82         (<=)     = textI_infix "<=" (infixN 4)
  83         (>)      = textI_infix ">"  (infixN 4)
  84         (>=)     = textI_infix ">=" (infixN 4)
  85         min      = textI2 "min"
  86         max      = textI2 "max"
  87 instance Sym_Ordering TextI where
  88         ordering o = TextI $ \_p _v ->
  89                 Text.pack (show o)
  90 instance (Sym_Ord r1, Sym_Ord r2) => Sym_Ord (DupI r1 r2) where
  91         compare    = dupI2 @Sym_Ord compare
  92         (<)        = dupI2 @Sym_Ord (<)
  93         (<=)       = dupI2 @Sym_Ord (<=)
  94         (>)        = dupI2 @Sym_Ord (>)
  95         (>=)       = dupI2 @Sym_Ord (>=)
  96         min        = dupI2 @Sym_Ord min
  97         max        = dupI2 @Sym_Ord max
  98 instance (Sym_Ordering r1, Sym_Ordering r2) => Sym_Ordering (DupI r1 r2) where
  99         ordering o = ordering o `DupI` ordering o
 100
 101 instance
 102  ( Read_TyNameR TyName cs rs
 103  , Inj_TyConst cs Ord
 104  ) => Read_TyNameR TyName cs (Proxy Ord ': rs) where
 105         read_TyNameR _cs (TyName "Ord") k = k (ty @Ord)
 106         read_TyNameR _rs raw k = read_TyNameR (Proxy @rs) raw k
 107 instance
 108  ( Read_TyNameR TyName cs rs
 109  , Inj_TyConst cs Ordering
 110  ) => Read_TyNameR TyName cs (Proxy Ordering ': rs) where
 111         read_TyNameR _cs (TyName "Ordering") k = k (ty @Ordering)
 112         read_TyNameR _rs raw k = read_TyNameR (Proxy @rs) raw k
 113 instance Show_TyConst cs => Show_TyConst (Proxy Ord ': cs) where
 114         show_TyConst TyConstZ{} = "Ord"
 115         show_TyConst (TyConstS c) = show_TyConst c
 116 instance Show_TyConst cs => Show_TyConst (Proxy Ordering ': cs) where
 117         show_TyConst TyConstZ{} = "Ordering"
 118         show_TyConst (TyConstS c) = show_TyConst c
 119
 120 instance Proj_TyFamC cs TyFam_MonoElement Ordering
 121
 122 instance Proj_TyConC cs (Proxy Ord)
 123 instance -- Proj_TyConC
 124  ( Proj_TyConst cs Ordering
 125  , Proj_TyConsts cs (TyConsts_imported_by (Proxy Ordering))
 126  ) => Proj_TyConC cs (Proxy Ordering) where
 127         proj_TyConC _ (TyConst q :$ TyConst c)
 128          | Just Refl <- eq_skind (kind_of_TyConst c) SKiType
 129          , Just Refl <- proj_TyConst c (Proxy @Ordering)
 130          = case () of
 131                  _ | Just Refl <- proj_TyConst q (Proxy @Bounded) -> Just TyCon
 132                    | Just Refl <- proj_TyConst q (Proxy @Enum)    -> Just TyCon
 133                    | Just Refl <- proj_TyConst q (Proxy @Eq)      -> Just TyCon
 134                    | Just Refl <- proj_TyConst q (Proxy @Ord)     -> Just TyCon
 135                    | Just Refl <- proj_TyConst q (Proxy @Show)    -> Just TyCon
 136                  _ -> Nothing
 137         proj_TyConC _c _q = Nothing
 138 data instance TokenT meta (ts::[*]) (Proxy Ord)
 139  = Token_Term_Ord_compare (EToken meta ts)
 140  | Token_Term_Ord_le      (EToken meta ts)
 141  | Token_Term_Ord_lt      (EToken meta ts)
 142  | Token_Term_Ord_ge      (EToken meta ts)
 143  | Token_Term_Ord_gt      (EToken meta ts)
 144  | Token_Term_Ord_min     (EToken meta ts)
 145  | Token_Term_Ord_max     (EToken meta ts)
 146 data instance TokenT meta (ts::[*]) (Proxy Ordering)
 147  = Token_Term_Ordering Ordering
 148 deriving instance Eq_Token meta ts => Eq (TokenT meta ts (Proxy Ord))
 149 deriving instance Eq_Token meta ts => Eq (TokenT meta ts (Proxy Ordering))
 150 deriving instance Show_Token meta ts => Show (TokenT meta ts (Proxy Ord))
 151 deriving instance Show_Token meta ts => Show (TokenT meta ts (Proxy Ordering))
 152
 153 instance -- CompileI
 154  ( Inj_TyConst cs Bool
 155  , Inj_TyConst cs (->)
 156  , Inj_TyConst cs Ord
 157  , Inj_TyConst cs Ordering
 158  , Proj_TyCon  cs
 159  , Compile cs is
 160  ) => CompileI cs is (Proxy Ord) where
 161         compileI
 162          :: forall meta ctx ret ls rs.
 163          TokenT meta is (Proxy Ord)
 164          -> Compiler meta ctx ret cs is ls (Proxy Ord ': rs)
 165         compileI tok ctx k =
 166                 case tok of
 167                  Token_Term_Ord_compare tok_a -> compare_from tok_a (ty @Ordering) compare
 168                  Token_Term_Ord_le      tok_a -> compare_from tok_a (ty @Bool) (<=)
 169                  Token_Term_Ord_lt      tok_a -> compare_from tok_a (ty @Bool) (<)
 170                  Token_Term_Ord_ge      tok_a -> compare_from tok_a (ty @Bool) (>=)
 171                  Token_Term_Ord_gt      tok_a -> compare_from tok_a (ty @Bool) (>)
 172                  Token_Term_Ord_min     tok_a -> op2_from tok_a min
 173                  Token_Term_Ord_max     tok_a -> op2_from tok_a max
 174                 where
 175                 compare_from
 176                  :: EToken meta is
 177                  -> Type cs (res::Kind.Type)
 178                  -> (forall term a. (Sym_Ord term, Ord a) => term a -> term a -> term res)
 179                  -> Either (Error_Term meta cs is) ret
 180                 compare_from tok_a ty_res op =
 181                  -- compare :: Ord a => a -> a -> Ordering
 182                  -- (<=)    :: Ord a => a -> a -> Bool
 183                  -- (<)     :: Ord a => a -> a -> Bool
 184                  -- (>=)    :: Ord a => a -> a -> Bool
 185                  -- (>)     :: Ord a => a -> a -> Bool
 186                         compile tok_a ctx $ \ty_a (Term x) ->
 187                         check_TyCon (At (Just tok_a) (ty @Ord :$ ty_a)) $ \TyCon ->
 188                         k (ty_a ~> ty_res) $ Term $
 189                          \c -> lam $ op (x c)
 190                 op2_from tok_a
 191                  (op::forall term a. (Sym_Ord term, Ord a)
 192                          => term a -> term a -> term a) =
 193                  -- min :: Ord a => a -> a -> a
 194                  -- max :: Ord a => a -> a -> a
 195                         compile tok_a ctx $ \ty_a (Term x) ->
 196                         check_TyCon (At (Just tok_a) (ty @Ord :$ ty_a)) $ \TyCon ->
 197                         k (ty_a ~> ty_a) $ Term $
 198                          \c -> lam $ \y -> op (x c) y
 199 instance -- CompileI
 200  ( Inj_TyConst cs Ordering
 201  ) => CompileI cs is (Proxy Ordering) where
 202         compileI tok _ctx k =
 203                 case tok of
 204                  Token_Term_Ordering o -> k (ty @Ordering) $ Term $ \_c -> ordering o
 205 instance -- TokenizeT
 206  Inj_Token meta ts Ord =>
 207  TokenizeT meta ts (Proxy Ord) where
 208         tokenizeT _t = mempty
 209          { tokenizers_infix = tokenizeTMod []
 210                  [ tokenize1 "compare" infixN5 Token_Term_Ord_compare
 211                  , tokenize1 "<"  (infixN 4) Token_Term_Ord_lt
 212                  , tokenize1 "<=" (infixN 4) Token_Term_Ord_le
 213                  , tokenize1 ">"  (infixN 4) Token_Term_Ord_gt
 214                  , tokenize1 ">=" (infixN 4) Token_Term_Ord_ge
 215                  ]
 216          }
 217 instance -- TokenizeT
 218  Inj_Token meta ts Ordering =>
 219  TokenizeT meta ts (Proxy Ordering) where
 220         tokenizeT _t = mempty
 221          { tokenizers_infix = tokenizeTMod []
 222                  [ tokenize0 "LT" infixN5 $ Token_Term_Ordering LT
 223                  , tokenize0 "EQ" infixN5 $ Token_Term_Ordering EQ
 224                  , tokenize0 "GT" infixN5 $ Token_Term_Ordering GT
 225                  ]
 226          }
 227 instance Gram_Term_AtomsT meta ts (Proxy Ordering) g
 228 instance Gram_Term_AtomsT meta ts (Proxy Ord) g