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