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