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

import Prelude (Integral)
import Prelude hiding (Integral(..))
import qualified Prelude

import Language.Symantic
import Language.Symantic.Lib.Function (a0)
import Language.Symantic.Lib.Integer (tyInteger)
import Language.Symantic.Lib.Tuple2 (tyTuple2)

-- * Class 'Sym_Integral'
type instance Sym Integral = 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      :: Sym_Integral (UnT term) => Trans term => Integral i => term i -> term i -> term i
	default rem       :: Sym_Integral (UnT term) => Trans term => Integral i => term i -> term i -> term i
	default div       :: Sym_Integral (UnT term) => Trans term => Integral i => term i -> term i -> term i
	default mod       :: Sym_Integral (UnT term) => Trans term => Integral i => term i -> term i -> term i
	default quotRem   :: Sym_Integral (UnT term) => Trans term => Integral i => term i -> term i -> term (i, i)
	default divMod    :: Sym_Integral (UnT term) => Trans term => Integral i => term i -> term i -> term (i, i)
	default toInteger :: Sym_Integral (UnT term) => Trans term => Integral i => term i -> term Integer
	
	quot      = trans2 quot
	rem       = trans2 rem
	div       = trans2 div
	mod       = trans2 mod
	quotRem   = trans2 quotRem
	divMod    = trans2 divMod
	toInteger = trans1 toInteger

-- Interpreting
instance Sym_Integral Eval where
	quot      = eval2 Prelude.quot
	rem       = eval2 Prelude.rem
	div       = eval2 Prelude.div
	mod       = eval2 Prelude.mod
	quotRem   = eval2 Prelude.quotRem
	divMod    = eval2 Prelude.divMod
	toInteger = eval1 Prelude.toInteger
instance Sym_Integral View where
	quot      = viewInfix "`quot`" (infixL 7)
	div       = viewInfix "`div`"  (infixL 7)
	rem       = viewInfix "`rem`"  (infixL 7)
	mod       = viewInfix "`mod`"  (infixL 7)
	quotRem   = view2 "quotRem"
	divMod    = view2 "divMod"
	toInteger = view1 "toInteger"
instance (Sym_Integral r1, Sym_Integral r2) => Sym_Integral (Dup r1 r2) where
	quot      = dup2 @Sym_Integral quot
	rem       = dup2 @Sym_Integral rem
	div       = dup2 @Sym_Integral div
	mod       = dup2 @Sym_Integral mod
	quotRem   = dup2 @Sym_Integral quotRem
	divMod    = dup2 @Sym_Integral divMod
	toInteger = dup1 @Sym_Integral toInteger

-- Transforming
instance (Sym_Integral term, Sym_Lambda term) => Sym_Integral (BetaT term)

-- Typing
instance FixityOf Integral
instance ClassInstancesFor Integral
instance TypeInstancesFor Integral

-- Compiling
instance Gram_Term_AtomsFor src ss g Integral
instance (Source src, Inj_Sym ss Integral) => ModuleFor src ss Integral where
	moduleFor = ["Integral"] `moduleWhere`
	 [ "quot" `withInfixL` 7 := teIntegral_quot
	 , "rem"  `withInfixL` 7 := teIntegral_rem
	 , "div"  `withInfixL` 7 := teIntegral_div
	 , "mod"  `withInfixL` 7 := teIntegral_mod
	 , "quotRem"   := teIntegral_quotRem
	 , "divMod"    := teIntegral_divMod
	 , "toInteger" := teIntegral_toInteger
	 ]

-- ** 'Type's
tyIntegral :: Source src => Type src vs a -> Type src vs (Integral a)
tyIntegral a = tyConstLen @(K Integral) @Integral (lenVars a) `tyApp` a

-- ** 'Term's
teIntegral_quot, teIntegral_rem, teIntegral_div, teIntegral_mod :: TermDef Integral '[Proxy a] (Integral a #> (a -> a -> a))
teIntegral_quot = Term (tyIntegral a0) (a0 ~> a0 ~> a0) $ teSym @Integral $ lam2 quot
teIntegral_rem  = Term (tyIntegral a0) (a0 ~> a0 ~> a0) $ teSym @Integral $ lam2 rem
teIntegral_div  = Term (tyIntegral a0) (a0 ~> a0 ~> a0) $ teSym @Integral $ lam2 div
teIntegral_mod  = Term (tyIntegral a0) (a0 ~> a0 ~> a0) $ teSym @Integral $ lam2 mod

teIntegral_quotRem, teIntegral_divMod :: TermDef Integral '[Proxy a] (Integral a #> (a -> a -> (a, a)))
teIntegral_quotRem = Term (tyIntegral a0) (a0 ~> a0 ~> tyTuple2 a0 a0) $ teSym @Integral $ lam2 quotRem
teIntegral_divMod  = Term (tyIntegral a0) (a0 ~> a0 ~> tyTuple2 a0 a0) $ teSym @Integral $ lam2 divMod

teIntegral_toInteger :: TermDef Integral '[Proxy a] (Integral a #> (a -> Integer))
teIntegral_toInteger = Term (tyIntegral a0) (a0 ~> tyInteger) $ teSym @Integral $ lam1 toInteger