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 Prelude (Integral)
  10 import Prelude hiding (Integral(..))
  11 import qualified Prelude
  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 (Proxy Integral)
  48 type instance TyConsts_imported_by (Proxy 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
  99 instance -- CompileI
 100  ( Read_TyName TyName cs
 101  , Inj_TyConst        cs Integral
 102  , Inj_TyConst        cs (->)
 103  , Inj_TyConst        cs (,)
 104  , Inj_TyConst        cs Integer
 105  , Proj_TyCon         cs
 106  , Compile cs is
 107  ) => CompileI cs is (Proxy Integral) where
 108         compileI tok ctx k =
 109                 case tok of
 110                  Token_Term_Integral_quot      tok_a -> op2_from tok_a quot
 111                  Token_Term_Integral_rem       tok_a -> op2_from tok_a rem
 112                  Token_Term_Integral_div       tok_a -> op2_from tok_a div
 113                  Token_Term_Integral_mod       tok_a -> op2_from tok_a mod
 114                  Token_Term_Integral_quotRem   tok_a -> op2t2_from tok_a quotRem
 115                  Token_Term_Integral_divMod    tok_a -> op2t2_from tok_a divMod
 116                  Token_Term_Integral_toInteger tok_a ->
 117                         -- toInteger :: Integral a => a -> Integer
 118                         compile tok_a ctx $ \ty_a (Term a) ->
 119                         check_TyCon (At (Just tok_a) (ty @Integral :$ ty_a)) $ \TyCon ->
 120                         k (ty @Integer) $ Term $
 121                                 \c -> toInteger (a c)
 122                 where
 123                 op2_from tok_a
 124                  (op::forall term a. (Sym_Integral term, Integral a)
 125                          => term a -> term a -> term a) =
 126                  -- quot :: Integral i => i -> i -> i
 127                  -- rem  :: Integral i => i -> i -> i
 128                  -- div  :: Integral i => i -> i -> i
 129                  -- mod  :: Integral i => i -> i -> i
 130                         compile tok_a ctx $ \ty_a (Term x) ->
 131                         check_TyCon (At (Just tok_a) (ty @Integral :$ ty_a)) $ \TyCon ->
 132                         k (ty_a ~> ty_a) $ Term $
 133                          \c -> lam $ \y -> op (x c) y
 134                 op2t2_from tok_a
 135                  (op::forall term a. (Sym_Integral term, Integral a)
 136                          => term a -> term a -> term (a, a)) =
 137                  -- quotRem :: Integral i => i -> i -> (i, i)
 138                  -- divMod  :: Integral i => i -> i -> (i, i)
 139                         compile tok_a ctx $ \ty_a (Term x) ->
 140                         check_TyCon (At (Just tok_a) (ty @Integral :$ ty_a)) $ \TyCon ->
 141                         k (ty_a ~> (ty @(,) :$ ty_a) :$ ty_a) $ Term $
 142                          \c -> lam $ \y -> op (x c) y
 143 instance -- TokenizeT
 144  Inj_Token meta ts Integral =>
 145  TokenizeT meta ts (Proxy Integral) where
 146         tokenizeT _t = mempty
 147          { tokenizers_infix = tokenizeTMod []
 148                  [ tokenize1 "quot"      (infixL 7) Token_Term_Integral_quot
 149                  , tokenize1 "rem"       (infixL 7) Token_Term_Integral_rem
 150                  , tokenize1 "div"       (infixL 7) Token_Term_Integral_div
 151                  , tokenize1 "mod"       (infixL 7) Token_Term_Integral_mod
 152                  , tokenize1 "quotRem"   infixN5    Token_Term_Integral_quotRem
 153                  , tokenize1 "divMod"    infixN5    Token_Term_Integral_divMod
 154                  , tokenize1 "toInteger" infixN5    Token_Term_Integral_toInteger
 155                  ]
 156          }
 157 instance Gram_Term_AtomsT meta ts (Proxy Integral) g