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   = textI2 "quotRem"
  71         divMod    = textI2 "divMod"
  72         toInteger = textI1 "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
  83  ( Read_TypeNameR Text cs rs
  84  , Inj_Const cs Integral
  85  ) => Read_TypeNameR Text cs (Proxy Integral ': rs) where
  86         read_typenameR _cs "Integral" k = k (ty @Integral)
  87         read_typenameR _rs raw k = read_typenameR (Proxy @rs) raw k
  88 instance Show_Const cs => Show_Const (Proxy Integral ': cs) where
  89         show_const ConstZ{} = "Integral"
  90         show_const (ConstS c) = show_const c
  91
  92 instance Proj_ConC cs (Proxy Integral)
  93 data instance TokenT meta (ts::[*]) (Proxy Integral)
  94  = Token_Term_Integral_quot    (EToken meta ts)
  95  | Token_Term_Integral_rem     (EToken meta ts)
  96  | Token_Term_Integral_div     (EToken meta ts)
  97  | Token_Term_Integral_mod     (EToken meta ts)
  98  | Token_Term_Integral_quotRem (EToken meta ts)
  99  | Token_Term_Integral_divMod  (EToken meta ts)
 100 deriving instance Eq_Token meta ts => Eq (TokenT meta ts (Proxy Integral))
 101 deriving instance Show_Token meta ts => Show (TokenT meta ts (Proxy Integral))
 102 instance -- CompileI
 103  ( Inj_Const (Consts_of_Ifaces is) Integral
 104  , Inj_Const (Consts_of_Ifaces is) (->)
 105  , Inj_Const (Consts_of_Ifaces is) (,)
 106  , Proj_Con  (Consts_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                 where
 118                 op2_from tok_a
 119                  (op::forall term a. (Sym_Integral term, Integral a)
 120                          => term a -> term a -> term a) =
 121                  -- quot :: Integral i => i -> i -> i
 122                  -- rem  :: Integral i => i -> i -> i
 123                  -- div  :: Integral i => i -> i -> i
 124                  -- mod  :: Integral i => i -> i -> i
 125                         compileO tok_a ctx $ \ty_a (TermO x) ->
 126                         check_con (At (Just tok_a) (ty @Integral :$ ty_a)) $ \Con ->
 127                         k (ty_a ~> ty_a) $ TermO $
 128                          \c -> lam $ \y -> op (x c) y
 129                 op2t2_from tok_a
 130                  (op::forall term a. (Sym_Integral term, Integral a)
 131                          => term a -> term a -> term (a, a)) =
 132                  -- quotRem :: Integral i => i -> i -> (i, i)
 133                  -- divMod  :: Integral i => i -> i -> (i, i)
 134                         compileO tok_a ctx $ \ty_a (TermO x) ->
 135                         check_con (At (Just tok_a) (ty @Integral :$ ty_a)) $ \Con ->
 136                         k (ty_a ~> (ty @(,) :$ ty_a) :$ ty_a) $ TermO $
 137                          \c -> lam $ \y -> op (x c) y