Language/Symantic/Compiling/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.Compiling.Integral where
   6
   7 import Control.Monad (liftM, liftM2)
   8 import Data.Proxy
   9 import Data.Text (Text)
  10 import qualified Prelude
  11 import Prelude hiding (Integral(..))
  12 import Prelude (Integral)
  13
  14 import Language.Symantic.Parsing
  15 import Language.Symantic.Typing
  16 import Language.Symantic.Compiling.Term
  17 import Language.Symantic.Interpreting
  18 import Language.Symantic.Transforming.Trans
  19
  20 -- * Class 'Sym_Integral'
  21 class Sym_Integral term where
  22         quot      :: Integral i => term i -> term i -> term i
  23         rem       :: Integral i => term i -> term i -> term i
  24         div       :: Integral i => term i -> term i -> term i
  25         mod       :: Integral i => term i -> term i -> term i
  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 infixl 7 `quot`
  47 infixl 7 `rem`
  48 infixl 7 `div`
  49 infixl 7 `mod`
  50
  51 type instance Sym_of_Iface (Proxy Integral) = Sym_Integral
  52 type instance Consts_of_Iface (Proxy Integral) = Proxy Integral ': Consts_imported_by Integral
  53 type instance Consts_imported_by Integral =
  54  '[ Proxy (,)
  55  ]
  56
  57 instance Sym_Integral HostI where
  58         quot      = liftM2 Prelude.quot
  59         rem       = liftM2 Prelude.rem
  60         div       = liftM2 Prelude.div
  61         mod       = liftM2 Prelude.mod
  62         quotRem   = liftM2 Prelude.quotRem
  63         divMod    = liftM2 Prelude.divMod
  64         toInteger = liftM  Prelude.toInteger
  65 instance Sym_Integral TextI where
  66         quot      = textI_infix "`quot`" (Precedence 7)
  67         div       = textI_infix "`div`"  (Precedence 7)
  68         rem       = textI_infix "`rem`"  (Precedence 7)
  69         mod       = textI_infix "`mod`"  (Precedence 7)
  70         quotRem   = textI_app2 "quotRem"
  71         divMod    = textI_app2 "divMod"
  72         toInteger = textI_app1 "toInteger"
  73 instance (Sym_Integral r1, Sym_Integral r2) => Sym_Integral (DupI r1 r2) where
  74         quot      = dupI2 (Proxy @Sym_Integral) quot
  75         rem       = dupI2 (Proxy @Sym_Integral) rem
  76         div       = dupI2 (Proxy @Sym_Integral) div
  77         mod       = dupI2 (Proxy @Sym_Integral) mod
  78         quotRem   = dupI2 (Proxy @Sym_Integral) quotRem
  79         divMod    = dupI2 (Proxy @Sym_Integral) divMod
  80         toInteger = dupI1 (Proxy @Sym_Integral) toInteger
  81
  82 instance Const_from Text cs => Const_from Text (Proxy Integral ': cs) where
  83         const_from "Integral" k = k (ConstZ kind)
  84         const_from s k = const_from s $ k . ConstS
  85 instance Show_Const cs => Show_Const (Proxy Integral ': cs) where
  86         show_const ConstZ{} = "Integral"
  87         show_const (ConstS c) = show_const c
  88
  89 instance Proj_ConC 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 deriving instance Eq_Token meta ts => Eq (TokenT meta ts (Proxy Integral))
  98 deriving instance Show_Token meta ts => Show (TokenT meta ts (Proxy Integral))
  99 instance -- Term_fromI
 100  ( Inj_Const (Consts_of_Ifaces is) Integral
 101  , Inj_Const (Consts_of_Ifaces is) (->)
 102  , Inj_Const (Consts_of_Ifaces is) (,)
 103  , Proj_Con  (Consts_of_Ifaces is)
 104  , Term_from is
 105  ) => Term_fromI is (Proxy Integral) where
 106         term_fromI tok ctx k =
 107                 case tok of
 108                  Token_Term_Integral_quot    tok_a -> op2_from tok_a quot
 109                  Token_Term_Integral_rem     tok_a -> op2_from tok_a rem
 110                  Token_Term_Integral_div     tok_a -> op2_from tok_a div
 111                  Token_Term_Integral_mod     tok_a -> op2_from tok_a mod
 112                  Token_Term_Integral_quotRem tok_a -> op2t2_from tok_a quotRem
 113                  Token_Term_Integral_divMod  tok_a -> op2t2_from tok_a divMod
 114                 where
 115                 op2_from tok_a
 116                  (op::forall term a. (Sym_Integral term, Integral a)
 117                          => term a -> term a -> term a) =
 118                  -- quot :: Integral i => i -> i -> i
 119                  -- rem  :: Integral i => i -> i -> i
 120                  -- div  :: Integral i => i -> i -> i
 121                  -- mod  :: Integral i => i -> i -> i
 122                         term_from tok_a ctx $ \ty_a (TermLC x) ->
 123                         check_con (At (Just tok_a) (ty @Integral :$ ty_a)) $ \Con ->
 124                         k (ty_a ~> ty_a) $ TermLC $
 125                          \c -> lam $ \y -> op (x c) y
 126                 op2t2_from tok_a
 127                  (op::forall term a. (Sym_Integral term, Integral a)
 128                          => term a -> term a -> term (a, a)) =
 129                  -- quotRem :: Integral i => i -> i -> (i, i)
 130                  -- divMod  :: Integral i => i -> i -> (i, i)
 131                         term_from tok_a ctx $ \ty_a (TermLC x) ->
 132                         check_con (At (Just tok_a) (ty @Integral :$ ty_a)) $ \Con ->
 133                         k (ty_a ~> (ty @(,) :$ ty_a) :$ ty_a) $ TermLC $
 134                          \c -> lam $ \y -> op (x c) y