symantic-lib/Language/Symantic/Lib/Integral.hs

   1 {-# LANGUAGE UndecidableInstances #-}
   2 {-# OPTIONS_GHC -fno-warn-orphans #-}
   3 {-# OPTIONS_GHC -fconstraint-solver-iterations=6 #-}
   4 -- | Symantic for 'Integral'.
   5 module Language.Symantic.Lib.Integral where
   6
   7 import Control.Monad (liftM, liftM2)
   8 import Data.Proxy
   9 import qualified Prelude
  10 import Prelude (Integral)
  11 import Prelude hiding (Integral(..))
  12
  13 import Language.Symantic.Parsing
  14 import Language.Symantic.Typing
  15 import Language.Symantic.Compiling
  16 import Language.Symantic.Interpreting
  17 import Language.Symantic.Transforming
  18 import Language.Symantic.Lib.Lambda
  19
  20 -- * Class 'Sym_Integral'
  21 class Sym_Integral term where
  22         quot      :: Integral i => term i -> term i -> term i; infixl 7 `quot`
  23         rem       :: Integral i => term i -> term i -> term i; infixl 7 `rem`
  24         div       :: Integral i => term i -> term i -> term i; infixl 7 `div`
  25         mod       :: Integral i => term i -> term i -> term i; infixl 7 `mod`
  26         quotRem   :: Integral i => term i -> term i -> term (i, i)
  27         divMod    :: Integral i => term i -> term i -> term (i, i)
  28         toInteger :: Integral i => term i -> term Integer
  29
  30         default quot      :: (Trans t term, Integral i) => t term i -> t term i -> t term i
  31         default rem       :: (Trans t term, Integral i) => t term i -> t term i -> t term i
  32         default div       :: (Trans t term, Integral i) => t term i -> t term i -> t term i
  33         default mod       :: (Trans t term, Integral i) => t term i -> t term i -> t term i
  34         default quotRem   :: (Trans t term, Integral i) => t term i -> t term i -> t term (i, i)
  35         default divMod    :: (Trans t term, Integral i) => t term i -> t term i -> t term (i, i)
  36         default toInteger :: (Trans t term, Integral i) => t term i -> t term Integer
  37
  38         quot      = trans_map2 quot
  39         rem       = trans_map2 rem
  40         div       = trans_map2 div
  41         mod       = trans_map2 mod
  42         quotRem   = trans_map2 quotRem
  43         divMod    = trans_map2 divMod
  44         toInteger = trans_map1 toInteger
  45
  46 type instance Sym_of_Iface (Proxy Integral) = Sym_Integral
  47 type instance TyConsts_of_Iface (Proxy Integral) = Proxy Integral ': TyConsts_imported_by Integral
  48 type instance TyConsts_imported_by Integral =
  49  '[ Proxy (,)
  50  ]
  51
  52 instance Sym_Integral HostI where
  53         quot      = liftM2 Prelude.quot
  54         rem       = liftM2 Prelude.rem
  55         div       = liftM2 Prelude.div
  56         mod       = liftM2 Prelude.mod
  57         quotRem   = liftM2 Prelude.quotRem
  58         divMod    = liftM2 Prelude.divMod
  59         toInteger = liftM  Prelude.toInteger
  60 instance Sym_Integral TextI where
  61         quot      = textI_infix "`quot`" (infixL 7)
  62         div       = textI_infix "`div`"  (infixL 7)
  63         rem       = textI_infix "`rem`"  (infixL 7)
  64         mod       = textI_infix "`mod`"  (infixL 7)
  65         quotRem   = textI2 "quotRem"
  66         divMod    = textI2 "divMod"
  67         toInteger = textI1 "toInteger"
  68 instance (Sym_Integral r1, Sym_Integral r2) => Sym_Integral (DupI r1 r2) where
  69         quot      = dupI2 @Sym_Integral quot
  70         rem       = dupI2 @Sym_Integral rem
  71         div       = dupI2 @Sym_Integral div
  72         mod       = dupI2 @Sym_Integral mod
  73         quotRem   = dupI2 @Sym_Integral quotRem
  74         divMod    = dupI2 @Sym_Integral divMod
  75         toInteger = dupI1 @Sym_Integral toInteger
  76
  77 instance
  78  ( Read_TyNameR TyName cs rs
  79  , Inj_TyConst cs Integral
  80  ) => Read_TyNameR TyName cs (Proxy Integral ': rs) where
  81         read_TyNameR _cs (TyName "Integral") k = k (ty @Integral)
  82         read_TyNameR _rs raw k = read_TyNameR (Proxy @rs) raw k
  83 instance Show_TyConst cs => Show_TyConst (Proxy Integral ': cs) where
  84         show_TyConst TyConstZ{} = "Integral"
  85         show_TyConst (TyConstS c) = show_TyConst c
  86
  87 instance Proj_TyConC cs (Proxy Integral)
  88 data instance TokenT meta (ts::[*]) (Proxy Integral)
  89  = Token_Term_Integral_quot      (EToken meta ts)
  90  | Token_Term_Integral_rem       (EToken meta ts)
  91  | Token_Term_Integral_div       (EToken meta ts)
  92  | Token_Term_Integral_mod       (EToken meta ts)
  93  | Token_Term_Integral_quotRem   (EToken meta ts)
  94  | Token_Term_Integral_divMod    (EToken meta ts)
  95  | Token_Term_Integral_toInteger (EToken meta ts)
  96 deriving instance (Eq meta, Eq_Token meta ts) => Eq (TokenT meta ts (Proxy Integral))
  97 deriving instance (Show meta, Show_Token meta ts) => Show (TokenT meta ts (Proxy Integral))
  98 instance -- CompileI
  99  ( Read_TyName TyName cs
 100  , Inj_TyConst        cs Integral
 101  , Inj_TyConst        cs (->)
 102  , Inj_TyConst        cs (,)
 103  , Inj_TyConst        cs Integer
 104  , Proj_TyCon         cs
 105  , Compile cs is
 106  ) => CompileI cs is (Proxy Integral) where
 107         compileI tok ctx k =
 108                 case tok of
 109                  Token_Term_Integral_quot      tok_a -> op2_from tok_a quot
 110                  Token_Term_Integral_rem       tok_a -> op2_from tok_a rem
 111                  Token_Term_Integral_div       tok_a -> op2_from tok_a div
 112                  Token_Term_Integral_mod       tok_a -> op2_from tok_a mod
 113                  Token_Term_Integral_quotRem   tok_a -> op2t2_from tok_a quotRem
 114                  Token_Term_Integral_divMod    tok_a -> op2t2_from tok_a divMod
 115                  Token_Term_Integral_toInteger tok_a ->
 116                         -- toInteger :: Integral a => a -> Integer
 117                         compileO tok_a ctx $ \ty_a (TermO a) ->
 118                         check_TyCon (At (Just tok_a) (ty @Integral :$ ty_a)) $ \TyCon ->
 119                         k (ty @Integer) $ TermO $
 120                                 \c -> toInteger (a c)
 121                 where
 122                 op2_from tok_a
 123                  (op::forall term a. (Sym_Integral term, Integral a)
 124                          => term a -> term a -> term a) =
 125                  -- quot :: Integral i => i -> i -> i
 126                  -- rem  :: Integral i => i -> i -> i
 127                  -- div  :: Integral i => i -> i -> i
 128                  -- mod  :: Integral i => i -> i -> i
 129                         compileO tok_a ctx $ \ty_a (TermO x) ->
 130                         check_TyCon (At (Just tok_a) (ty @Integral :$ ty_a)) $ \TyCon ->
 131                         k (ty_a ~> ty_a) $ TermO $
 132                          \c -> lam $ \y -> op (x c) y
 133                 op2t2_from tok_a
 134                  (op::forall term a. (Sym_Integral term, Integral a)
 135                          => term a -> term a -> term (a, a)) =
 136                  -- quotRem :: Integral i => i -> i -> (i, i)
 137                  -- divMod  :: Integral i => i -> i -> (i, i)
 138                         compileO tok_a ctx $ \ty_a (TermO x) ->
 139                         check_TyCon (At (Just tok_a) (ty @Integral :$ ty_a)) $ \TyCon ->
 140                         k (ty_a ~> (ty @(,) :$ ty_a) :$ ty_a) $ TermO $
 141                          \c -> lam $ \y -> op (x c) y
 142 instance -- TokenizeT
 143  Inj_Token meta ts Integral =>
 144  TokenizeT meta ts (Proxy Integral) where
 145         tokenizeT _t = mempty
 146          { tokenizers_infix = tokenizeTMod []
 147                  [ tokenize1 "quot"      (infixL 7) Token_Term_Integral_quot
 148                  , tokenize1 "rem"       (infixL 7) Token_Term_Integral_rem
 149                  , tokenize1 "div"       (infixL 7) Token_Term_Integral_div
 150                  , tokenize1 "mod"       (infixL 7) Token_Term_Integral_mod
 151                  , tokenize1 "quotRem"   infixN5    Token_Term_Integral_quotRem
 152                  , tokenize1 "divMod"    infixN5    Token_Term_Integral_divMod
 153                  , tokenize1 "toInteger" infixN5    Token_Term_Integral_toInteger
 154                  ]
 155          }
 156 instance Gram_Term_AtomsT meta ts (Proxy Integral) g