{-# LANGUAGE UndecidableInstances #-} {-# OPTIONS_GHC -fno-warn-orphans #-} {-# OPTIONS_GHC -fconstraint-solver-iterations=6 #-} -- | Symantic for 'Integral'. module Language.Symantic.Compiling.Integral where import Control.Monad (liftM, liftM2) import Data.Proxy import Data.Text (Text) import qualified Prelude import Prelude hiding (Integral(..)) import Prelude (Integral) import Language.Symantic.Parsing import Language.Symantic.Typing import Language.Symantic.Compiling.Term import Language.Symantic.Interpreting import Language.Symantic.Transforming.Trans -- * Class 'Sym_Integral' class Sym_Integral term where quot :: Integral i => term i -> term i -> term i rem :: Integral i => term i -> term i -> term i div :: Integral i => term i -> term i -> term i mod :: Integral i => term i -> term i -> term i quotRem :: Integral i => term i -> term i -> term (i, i) divMod :: Integral i => term i -> term i -> term (i, i) toInteger :: Integral i => term i -> term Integer default quot :: (Trans t term, Integral i) => t term i -> t term i -> t term i default rem :: (Trans t term, Integral i) => t term i -> t term i -> t term i default div :: (Trans t term, Integral i) => t term i -> t term i -> t term i default mod :: (Trans t term, Integral i) => t term i -> t term i -> t term i default quotRem :: (Trans t term, Integral i) => t term i -> t term i -> t term (i, i) default divMod :: (Trans t term, Integral i) => t term i -> t term i -> t term (i, i) default toInteger :: (Trans t term, Integral i) => t term i -> t term Integer quot = trans_map2 quot rem = trans_map2 rem div = trans_map2 div mod = trans_map2 mod quotRem = trans_map2 quotRem divMod = trans_map2 divMod toInteger = trans_map1 toInteger infixl 7 `quot` infixl 7 `rem` infixl 7 `div` infixl 7 `mod` type instance Sym_of_Iface (Proxy Integral) = Sym_Integral type instance Consts_of_Iface (Proxy Integral) = Proxy Integral ': Consts_imported_by Integral type instance Consts_imported_by Integral = '[ Proxy (,) ] instance Sym_Integral HostI where quot = liftM2 Prelude.quot rem = liftM2 Prelude.rem div = liftM2 Prelude.div mod = liftM2 Prelude.mod quotRem = liftM2 Prelude.quotRem divMod = liftM2 Prelude.divMod toInteger = liftM Prelude.toInteger instance Sym_Integral TextI where quot = textI_infix "`quot`" (Precedence 7) div = textI_infix "`div`" (Precedence 7) rem = textI_infix "`rem`" (Precedence 7) mod = textI_infix "`mod`" (Precedence 7) quotRem = textI2 "quotRem" divMod = textI2 "divMod" toInteger = textI1 "toInteger" instance (Sym_Integral r1, Sym_Integral r2) => Sym_Integral (DupI r1 r2) where quot = dupI2 (Proxy @Sym_Integral) quot rem = dupI2 (Proxy @Sym_Integral) rem div = dupI2 (Proxy @Sym_Integral) div mod = dupI2 (Proxy @Sym_Integral) mod quotRem = dupI2 (Proxy @Sym_Integral) quotRem divMod = dupI2 (Proxy @Sym_Integral) divMod toInteger = dupI1 (Proxy @Sym_Integral) toInteger instance ( Read_TypeNameR Text cs rs , Inj_Const cs Integral ) => Read_TypeNameR Text cs (Proxy Integral ': rs) where read_typenameR _cs "Integral" k = k (ty @Integral) read_typenameR _rs raw k = read_typenameR (Proxy @rs) raw k instance Show_Const cs => Show_Const (Proxy Integral ': cs) where show_const ConstZ{} = "Integral" show_const (ConstS c) = show_const c instance Proj_ConC cs (Proxy Integral) data instance TokenT meta (ts::[*]) (Proxy Integral) = Token_Term_Integral_quot (EToken meta ts) | Token_Term_Integral_rem (EToken meta ts) | Token_Term_Integral_div (EToken meta ts) | Token_Term_Integral_mod (EToken meta ts) | Token_Term_Integral_quotRem (EToken meta ts) | Token_Term_Integral_divMod (EToken meta ts) deriving instance Eq_Token meta ts => Eq (TokenT meta ts (Proxy Integral)) deriving instance Show_Token meta ts => Show (TokenT meta ts (Proxy Integral)) instance -- CompileI ( Inj_Const (Consts_of_Ifaces is) Integral , Inj_Const (Consts_of_Ifaces is) (->) , Inj_Const (Consts_of_Ifaces is) (,) , Proj_Con (Consts_of_Ifaces is) , Compile is ) => CompileI is (Proxy Integral) where compileI tok ctx k = case tok of Token_Term_Integral_quot tok_a -> op2_from tok_a quot Token_Term_Integral_rem tok_a -> op2_from tok_a rem Token_Term_Integral_div tok_a -> op2_from tok_a div Token_Term_Integral_mod tok_a -> op2_from tok_a mod Token_Term_Integral_quotRem tok_a -> op2t2_from tok_a quotRem Token_Term_Integral_divMod tok_a -> op2t2_from tok_a divMod where op2_from tok_a (op::forall term a. (Sym_Integral term, Integral a) => term a -> term a -> term a) = -- quot :: Integral i => i -> i -> i -- rem :: Integral i => i -> i -> i -- div :: Integral i => i -> i -> i -- mod :: Integral i => i -> i -> i compileO tok_a ctx $ \ty_a (TermO x) -> check_con (At (Just tok_a) (ty @Integral :$ ty_a)) $ \Con -> k (ty_a ~> ty_a) $ TermO $ \c -> lam $ \y -> op (x c) y op2t2_from tok_a (op::forall term a. (Sym_Integral term, Integral a) => term a -> term a -> term (a, a)) = -- quotRem :: Integral i => i -> i -> (i, i) -- divMod :: Integral i => i -> i -> (i, i) compileO tok_a ctx $ \ty_a (TermO x) -> check_con (At (Just tok_a) (ty @Integral :$ ty_a)) $ \Con -> k (ty_a ~> (ty @(,) :$ ty_a) :$ ty_a) $ TermO $ \c -> lam $ \y -> op (x c) y