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