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