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 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
  17 import Language.Symantic.Interpreting
  18 import Language.Symantic.Transforming
  19 import Language.Symantic.Lib.Lambda
  20 import Language.Symantic.Lib.Eq (Sym_Eq)
  21
  22 -- * Class 'Sym_Ord'
  23 class Sym_Eq term => Sym_Ord term where
  24         ordering :: Ordering -> term Ordering
  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 ordering :: Trans t term => Ordering -> t term Ordering
  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         ordering = trans_lift . ordering
  43         compare  = trans_map2 compare
  44         (<)      = trans_map2 (<)
  45         (<=)     = trans_map2 (<=)
  46         (>)      = trans_map2 (>)
  47         (>=)     = trans_map2 (>=)
  48         min      = trans_map2 min
  49         max      = trans_map2 max
  50
  51 infix 4 <
  52 infix 4 <=
  53 infix 4 >
  54 infix 4 >=
  55
  56 type instance Sym_of_Iface (Proxy Ord) = Sym_Ord
  57 type instance Consts_of_Iface (Proxy Ord) = Proxy Ord ': Consts_imported_by Ord
  58 type instance Consts_imported_by Ord = '[]
  59
  60 instance Sym_Ord HostI where
  61         ordering = HostI
  62         compare  = liftM2 Ord.compare
  63         (<)      = liftM2 (Ord.<)
  64         (<=)     = liftM2 (Ord.<=)
  65         (>)      = liftM2 (Ord.>)
  66         (>=)     = liftM2 (Ord.>=)
  67         min      = liftM2 Ord.min
  68         max      = liftM2 Ord.max
  69 instance Sym_Ord TextI where
  70         ordering o = TextI $ \_p _v ->
  71                 Text.pack (show o)
  72         compare  = textI2  "compare"
  73         (<)      = textI_infix "<"  (infixN 4)
  74         (<=)     = textI_infix "<=" (infixN 4)
  75         (>)      = textI_infix ">"  (infixN 4)
  76         (>=)     = textI_infix ">=" (infixN 4)
  77         min      = textI2  "min"
  78         max      = textI2  "max"
  79 instance (Sym_Ord r1, Sym_Ord r2) => Sym_Ord (DupI r1 r2) where
  80         ordering o = ordering o `DupI` ordering o
  81         compare    = dupI2 (Proxy @Sym_Ord) compare
  82         (<)        = dupI2 (Proxy @Sym_Ord) (<)
  83         (<=)       = dupI2 (Proxy @Sym_Ord) (<=)
  84         (>)        = dupI2 (Proxy @Sym_Ord) (>)
  85         (>=)       = dupI2 (Proxy @Sym_Ord) (>=)
  86         min        = dupI2 (Proxy @Sym_Ord) min
  87         max        = dupI2 (Proxy @Sym_Ord) max
  88
  89 instance
  90  ( Read_TypeNameR Type_Name cs rs
  91  , Inj_Const cs Ord
  92  ) => Read_TypeNameR Type_Name cs (Proxy Ord ': rs) where
  93         read_typenameR _cs (Type_Name "Ord") k = k (ty @Ord)
  94         read_typenameR _rs raw k = read_typenameR (Proxy @rs) raw k
  95 instance Show_Const cs => Show_Const (Proxy Ord ': cs) where
  96         show_const ConstZ{} = "Ord"
  97         show_const (ConstS c) = show_const c
  98
  99 instance Proj_ConC cs (Proxy Ord)
 100 data instance TokenT meta (ts::[*]) (Proxy Ord)
 101  = Token_Term_Ordering    Ordering
 102  | Token_Term_Ord_compare (EToken meta ts)
 103  | Token_Term_Ord_le      (EToken meta ts)
 104  | Token_Term_Ord_lt      (EToken meta ts)
 105  | Token_Term_Ord_ge      (EToken meta ts)
 106  | Token_Term_Ord_gt      (EToken meta ts)
 107  | Token_Term_Ord_min     (EToken meta ts)
 108  | Token_Term_Ord_max     (EToken meta ts)
 109 deriving instance Eq_Token meta ts => Eq (TokenT meta ts (Proxy Ord))
 110 deriving instance Show_Token meta ts => Show (TokenT meta ts (Proxy Ord))
 111 instance -- CompileI
 112  ( Inj_Const (Consts_of_Ifaces is) Bool
 113  , Inj_Const (Consts_of_Ifaces is) (->)
 114  , Inj_Const (Consts_of_Ifaces is) Ord
 115  , Inj_Const (Consts_of_Ifaces is) Ordering
 116  , Proj_Con (Consts_of_Ifaces is)
 117  , Compile is
 118  ) => CompileI is (Proxy Ord) where
 119         compileI
 120          :: forall meta ctx ret ls rs.
 121          TokenT meta is (Proxy Ord)
 122          -> CompileT meta ctx ret is ls (Proxy Ord ': rs)
 123         compileI tok ctx k =
 124                 case tok of
 125                  Token_Term_Ordering o -> k (ty @Ordering) $ TermO $ \_c -> ordering o
 126                  Token_Term_Ord_compare tok_a -> compare_from tok_a (ty @Ordering) compare
 127                  Token_Term_Ord_le      tok_a -> compare_from tok_a (ty @Bool) (<=)
 128                  Token_Term_Ord_lt      tok_a -> compare_from tok_a (ty @Bool) (<)
 129                  Token_Term_Ord_ge      tok_a -> compare_from tok_a (ty @Bool) (>=)
 130                  Token_Term_Ord_gt      tok_a -> compare_from tok_a (ty @Bool) (>)
 131                  Token_Term_Ord_min     tok_a -> op2_from tok_a min
 132                  Token_Term_Ord_max     tok_a -> op2_from tok_a max
 133                 where
 134                 compare_from
 135                  :: EToken meta is
 136                  -> Type (Consts_of_Ifaces is) (res::Kind.Type)
 137                  -> (forall term a. (Sym_Ord term, Ord a) => term a -> term a -> term res)
 138                  -> Either (Error_Term meta is) ret
 139                 compare_from tok_a ty_res op =
 140                  -- compare :: Ord a => a -> a -> Ordering
 141                  -- (<=)    :: Ord a => a -> a -> Bool
 142                  -- (<)     :: Ord a => a -> a -> Bool
 143                  -- (>=)    :: Ord a => a -> a -> Bool
 144                  -- (>)     :: Ord a => a -> a -> Bool
 145                         compileO tok_a ctx $ \ty_a (TermO x) ->
 146                         check_con (At (Just tok_a) (ty @Ord :$ ty_a)) $ \Con ->
 147                         k (ty_a ~> ty_res) $ TermO $
 148                          \c -> lam $ op (x c)
 149                 op2_from tok_a
 150                  (op::forall term a. (Sym_Ord term, Ord a)
 151                          => term a -> term a -> term a) =
 152                  -- min :: Ord a => a -> a -> a
 153                  -- max :: Ord a => a -> a -> a
 154                         compileO tok_a ctx $ \ty_a (TermO x) ->
 155                         check_con (At (Just tok_a) (ty @Ord :$ ty_a)) $ \Con ->
 156                         k (ty_a ~> ty_a) $ TermO $
 157                          \c -> lam $ \y -> op (x c) y
 158 instance -- TokenizeT
 159  Inj_Token meta ts Ord =>
 160  TokenizeT meta ts (Proxy Ord) where
 161         tokenizeT _t = mempty
 162          { tokenizers_infix = tokenizeTMod []
 163                  [ tokenize0 "LT" infixN5 $ Token_Term_Ordering LT
 164                  , tokenize0 "EQ" infixN5 $ Token_Term_Ordering EQ
 165                  , tokenize0 "GT" infixN5 $ Token_Term_Ordering GT
 166                  , tokenize1 "compare" infixN5 Token_Term_Ord_compare
 167                  , tokenize1 "<"  (infixN 4) Token_Term_Ord_lt
 168                  , tokenize1 "<=" (infixN 4) Token_Term_Ord_le
 169                  , tokenize1 ">"  (infixN 4) Token_Term_Ord_gt
 170                  , tokenize1 ">=" (infixN 4) Token_Term_Ord_ge
 171                  ]
 172          }
 173 instance Gram_Term_AtomsT meta ts (Proxy Ord) g