{-# 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