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