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