Language/Symantic/Compiling/Ord.hs

   1 {-# LANGUAGE UndecidableInstances #-}
   2 {-# OPTIONS_GHC -fno-warn-orphans #-}
   3 -- | Symantic for 'Ord'.
   4 module Language.Symantic.Compiling.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 Data.Text (Text)
  11 import qualified Data.Kind as Kind
  12 import Prelude hiding (Ord(..))
  13
  14 import Language.Symantic.Parsing
  15 import Language.Symantic.Typing
  16 import Language.Symantic.Compiling.Term
  17 import Language.Symantic.Compiling.Eq (Sym_Eq)
  18 import Language.Symantic.Interpreting
  19 import Language.Symantic.Transforming.Trans
  20
  21 -- * Class 'Sym_Ord'
  22 class Sym_Eq term => Sym_Ord term where
  23         compare :: Ord a => term a -> term a -> term Ordering
  24         (<)     :: Ord a => term a -> term a -> term Bool
  25         (<=)    :: Ord a => term a -> term a -> term Bool
  26         (>)     :: Ord a => term a -> term a -> term Bool
  27         (>=)    :: Ord a => term a -> term a -> term Bool
  28         max     :: Ord a => term a -> term a -> term a
  29         min     :: Ord a => term a -> term a -> term a
  30
  31         default compare :: (Trans t term, Ord a) => t term a -> t term a -> t term Ordering
  32         default (<)     :: (Trans t term, Ord a) => t term a -> t term a -> t term Bool
  33         default (<=)    :: (Trans t term, Ord a) => t term a -> t term a -> t term Bool
  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 max     :: (Trans t term, Ord a) => t term a -> t term a -> t term a
  37         default min     :: (Trans t term, Ord a) => t term a -> t term a -> t term a
  38
  39         compare  = trans_map2 compare
  40         (<)      = trans_map2 (<)
  41         (<=)     = trans_map2 (<=)
  42         (>)      = trans_map2 (>)
  43         (>=)     = trans_map2 (>=)
  44         min      = trans_map2 min
  45         max      = trans_map2 max
  46
  47 infix 4 <
  48 infix 4 <=
  49 infix 4 >
  50 infix 4 >=
  51
  52 type instance Sym_of_Iface (Proxy Ord) = Sym_Ord
  53 type instance Consts_of_Iface (Proxy Ord) = Proxy Ord ': Consts_imported_by Ord
  54 type instance Consts_imported_by Ord = '[]
  55
  56 instance Sym_Ord HostI where
  57         compare = liftM2 Ord.compare
  58         (<)     = liftM2 (Ord.<)
  59         (<=)    = liftM2 (Ord.<=)
  60         (>)     = liftM2 (Ord.>)
  61         (>=)    = liftM2 (Ord.>=)
  62         min     = liftM2 Ord.min
  63         max     = liftM2 Ord.max
  64 instance Sym_Ord TextI where
  65         compare = textI_app2  "compare"
  66         (<)     = textI_infix "<"  (Precedence 4)
  67         (<=)    = textI_infix "<=" (Precedence 4)
  68         (>)     = textI_infix ">"  (Precedence 4)
  69         (>=)    = textI_infix ">=" (Precedence 4)
  70         min     = textI_app2  "min"
  71         max     = textI_app2  "max"
  72 instance (Sym_Ord r1, Sym_Ord r2) => Sym_Ord (DupI r1 r2) where
  73         compare = dupI2 (Proxy @Sym_Ord) compare
  74         (<)     = dupI2 (Proxy @Sym_Ord) (<)
  75         (<=)    = dupI2 (Proxy @Sym_Ord) (<=)
  76         (>)     = dupI2 (Proxy @Sym_Ord) (>)
  77         (>=)    = dupI2 (Proxy @Sym_Ord) (>=)
  78         min     = dupI2 (Proxy @Sym_Ord) min
  79         max     = dupI2 (Proxy @Sym_Ord) max
  80
  81 instance Const_from Text cs => Const_from Text (Proxy Ord ': cs) where
  82         const_from "Ord" k = k (ConstZ kind)
  83         const_from s k = const_from s $ k . ConstS
  84 instance Show_Const cs => Show_Const (Proxy Ord ': cs) where
  85         show_const ConstZ{} = "Ord"
  86         show_const (ConstS c) = show_const c
  87
  88 instance Proj_ConC cs (Proxy Ord)
  89 data instance TokenT meta (ts::[*]) (Proxy Ord)
  90  = Token_Term_Ord_compare (EToken meta ts)
  91  | Token_Term_Ord_le      (EToken meta ts)
  92  | Token_Term_Ord_lt      (EToken meta ts)
  93  | Token_Term_Ord_ge      (EToken meta ts)
  94  | Token_Term_Ord_gt      (EToken meta ts)
  95  | Token_Term_Ord_min     (EToken meta ts)
  96  | Token_Term_Ord_max     (EToken meta ts)
  97 deriving instance Eq_Token meta ts => Eq (TokenT meta ts (Proxy Ord))
  98 deriving instance Show_Token meta ts => Show (TokenT meta ts (Proxy Ord))
  99 instance -- Term_fromI
 100  ( Inj_Const (Consts_of_Ifaces is) Bool
 101  , Inj_Const (Consts_of_Ifaces is) (->)
 102  , Inj_Const (Consts_of_Ifaces is) Ord
 103  , Inj_Const (Consts_of_Ifaces is) Ordering
 104  , Proj_Con (Consts_of_Ifaces is)
 105  , Term_from is
 106  ) => Term_fromI is (Proxy Ord) where
 107         term_fromI
 108          :: forall meta ctx ret ls rs.
 109          TokenT meta is (Proxy Ord)
 110          -> Term_fromT meta ctx ret is ls (Proxy Ord ': rs)
 111         term_fromI tok ctx k =
 112                 case tok of
 113                  Token_Term_Ord_compare tok_a -> compare_from tok_a (ty @Ordering) compare
 114                  Token_Term_Ord_le      tok_a -> compare_from tok_a (ty @Bool) (<=)
 115                  Token_Term_Ord_lt      tok_a -> compare_from tok_a (ty @Bool) (<)
 116                  Token_Term_Ord_ge      tok_a -> compare_from tok_a (ty @Bool) (>=)
 117                  Token_Term_Ord_gt      tok_a -> compare_from tok_a (ty @Bool) (>)
 118                  Token_Term_Ord_min     tok_a -> op2_from tok_a min
 119                  Token_Term_Ord_max     tok_a -> op2_from tok_a max
 120                 where
 121                 compare_from
 122                  :: EToken meta is
 123                  -> Type (Consts_of_Ifaces is) (res::Kind.Type)
 124                  -> (forall term a. (Sym_Ord term, Ord a) => term a -> term a -> term res)
 125                  -> Either (Error_Term meta is) ret
 126                 compare_from tok_a ty_res op =
 127                  -- compare :: Ord a => a -> a -> Ordering
 128                  -- (<=)    :: Ord a => a -> a -> Bool
 129                  -- (<)     :: Ord a => a -> a -> Bool
 130                  -- (>=)    :: Ord a => a -> a -> Bool
 131                  -- (>)     :: Ord a => a -> a -> Bool
 132                         term_from tok_a ctx $ \ty_a (TermLC x) ->
 133                         check_con (At (Just tok_a) (ty @Ord :$ ty_a)) $ \Con ->
 134                         k (ty_a ~> ty_res) $ TermLC $
 135                          \c -> lam $ op (x c)
 136                 op2_from tok_a
 137                  (op::forall term a. (Sym_Ord term, Ord a)
 138                          => term a -> term a -> term a) =
 139                  -- min :: Ord a => a -> a -> a
 140                  -- max :: Ord a => a -> a -> a
 141                         term_from tok_a ctx $ \ty_a (TermLC x) ->
 142                         check_con (At (Just tok_a) (ty @Ord :$ ty_a)) $ \Con ->
 143                         k (ty_a ~> ty_a) $ TermLC $
 144                          \c -> lam $ \y -> op (x c) y