{-# 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 qualified Data.Function as Fun
import Data.Proxy
import Data.Type.Equality ((:~:)(Refl))
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 '[Proxy Token_Type])
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 (TyConsts_of_Ifaces is)
 , Inj_TyConst (TyConsts_of_Ifaces is) Integral
 , Inj_TyConst (TyConsts_of_Ifaces is) (->)
 , Inj_TyConst (TyConsts_of_Ifaces is) (,)
 , Inj_TyConst (TyConsts_of_Ifaces is) Integer
 , Proj_TyCon  (TyConsts_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
		 Token_Term_Integral_toInteger tok_ty_a ->
			-- toInteger :: Integral a => a -> Integer
			compile_Type tok_ty_a $ \(ty_a::Type (TyConsts_of_Ifaces is) a) ->
			check_Kind
			 (At Nothing SKiType)
			 (At (Just tok_ty_a) $ kind_of ty_a) $ \Refl ->
			check_TyCon (At (Just tok_ty_a) (ty @Integral :$ ty_a)) $ \TyCon ->
			k (ty_a ~> ty @Integer) $ TermO $
				Fun.const $ lam toInteger
		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
		 , (Term_Name "toInteger",) Term_ProTok
			 { term_protok = \meta -> ProTokPi $ \a ->
				ProTok $ inj_EToken meta $ Token_Term_Integral_toInteger a
			 , term_fixity = infixN5
			 }
		 ]
	 }
instance Gram_Term_AtomsT meta ts (Proxy Integral) g