{-# LANGUAGE UndecidableInstances #-}
{-# OPTIONS_GHC -fno-warn-orphans #-}
{-# OPTIONS_GHC -fconstraint-solver-iterations=6 #-}
-- | Symantic for 'Integral'.
module Language.Symantic.Lib.Integral where

import Control.Monad (liftM, liftM2)
import Data.Proxy
import qualified Prelude
import Prelude (Integral)
import Prelude hiding (Integral(..))

import Language.Symantic.Parsing
import Language.Symantic.Typing
import Language.Symantic.Compiling
import Language.Symantic.Interpreting
import Language.Symantic.Transforming
import Language.Symantic.Lib.Lambda

-- * Class 'Sym_Integral'
class Sym_Integral term where
	quot      :: Integral i => term i -> term i -> term i; infixl 7 `quot`
	rem       :: Integral i => term i -> term i -> term i; infixl 7 `rem`
	div       :: Integral i => term i -> term i -> term i; infixl 7 `div`
	mod       :: Integral i => term i -> term i -> term i; infixl 7 `mod`
	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

type instance Sym_of_Iface (Proxy Integral) = Sym_Integral
type instance TyConsts_of_Iface (Proxy Integral) = Proxy Integral ': TyConsts_imported_by Integral
type instance TyConsts_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`" (infixL 7)
	div       = textI_infix "`div`"  (infixL 7)
	rem       = textI_infix "`rem`"  (infixL 7)
	mod       = textI_infix "`mod`"  (infixL 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 @Sym_Integral quot
	rem       = dupI2 @Sym_Integral rem
	div       = dupI2 @Sym_Integral div
	mod       = dupI2 @Sym_Integral mod
	quotRem   = dupI2 @Sym_Integral quotRem
	divMod    = dupI2 @Sym_Integral divMod
	toInteger = dupI1 @Sym_Integral toInteger

instance
 ( Read_TyNameR TyName cs rs
 , Inj_TyConst cs Integral
 ) => Read_TyNameR TyName cs (Proxy Integral ': rs) where
	read_TyNameR _cs (TyName "Integral") k = k (ty @Integral)
	read_TyNameR _rs raw k = read_TyNameR (Proxy @rs) raw k
instance Show_TyConst cs => Show_TyConst (Proxy Integral ': cs) where
	show_TyConst TyConstZ{} = "Integral"
	show_TyConst (TyConstS c) = show_TyConst c

instance Proj_TyConC 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)
 | Token_Term_Integral_toInteger (EToken meta ts)
deriving instance (Eq meta, Eq_Token meta ts) => Eq (TokenT meta ts (Proxy Integral))
deriving instance (Show meta, Show_Token meta ts) => Show (TokenT meta ts (Proxy Integral))
instance -- CompileI
 ( Read_TyName TyName cs
 , Inj_TyConst        cs Integral
 , Inj_TyConst        cs (->)
 , Inj_TyConst        cs (,)
 , Inj_TyConst        cs Integer
 , Proj_TyCon         cs
 , Compile cs is
 ) => CompileI cs 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
		 Token_Term_Integral_toInteger tok_a ->
			-- toInteger :: Integral a => a -> Integer
			compileO tok_a ctx $ \ty_a (TermO a) ->
			check_TyCon (At (Just tok_a) (ty @Integral :$ ty_a)) $ \TyCon ->
			k (ty @Integer) $ TermO $
				\c -> toInteger (a c)
		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_TyCon (At (Just tok_a) (ty @Integral :$ ty_a)) $ \TyCon ->
			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_TyCon (At (Just tok_a) (ty @Integral :$ ty_a)) $ \TyCon ->
			k (ty_a ~> (ty @(,) :$ ty_a) :$ ty_a) $ TermO $
			 \c -> lam $ \y -> op (x c) y
instance -- TokenizeT
 Inj_Token meta ts Integral =>
 TokenizeT meta ts (Proxy Integral) where
	tokenizeT _t = mempty
	 { tokenizers_infix = tokenizeTMod []
		 [ tokenize1 "quot"      (infixL 7) Token_Term_Integral_quot
		 , tokenize1 "rem"       (infixL 7) Token_Term_Integral_rem
		 , tokenize1 "div"       (infixL 7) Token_Term_Integral_div
		 , tokenize1 "mod"       (infixL 7) Token_Term_Integral_mod
		 , tokenize1 "quotRem"   infixN5    Token_Term_Integral_quotRem
		 , tokenize1 "divMod"    infixN5    Token_Term_Integral_divMod
		 , tokenize1 "toInteger" infixN5    Token_Term_Integral_toInteger
		 ]
	 }
instance Gram_Term_AtomsT meta ts (Proxy Integral) g