{-# 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 NameTyOf Integral where
        nameTyOf _c = ["Integral"] `Mod` "Integral"
instance FixityOf Integral
instance ClassInstancesFor Integral
instance TypeInstancesFor Integral

-- Compiling
instance Gram_Term_AtomsFor src ss g Integral
instance (Source src, SymInj 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