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

import Prelude (Num)
import Prelude hiding (Num(..))
import qualified Prelude

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

-- * Class 'Sym_Num'
type instance Sym Num = Sym_Num
class Sym_Num term where
        abs         :: Num n => term n -> term n
        negate      :: Num n => term n -> term n
        signum      :: Num n => term n -> term n
        (+)         :: Num n => term n -> term n -> term n; infixl 6 +
        (-)         :: Num n => term n -> term n -> term n; infixl 6 -
        (*)         :: Num n => term n -> term n -> term n; infixl 7 *
        fromInteger :: Num n => term Integer -> term n

        default abs         :: Sym_Num (UnT term) => Trans term => Num n => term n -> term n
        default negate      :: Sym_Num (UnT term) => Trans term => Num n => term n -> term n
        default signum      :: Sym_Num (UnT term) => Trans term => Num n => term n -> term n
        default (+)         :: Sym_Num (UnT term) => Trans term => Num n => term n -> term n -> term n
        default (-)         :: Sym_Num (UnT term) => Trans term => Num n => term n -> term n -> term n
        default (*)         :: Sym_Num (UnT term) => Trans term => Num n => term n -> term n -> term n
        default fromInteger :: Sym_Num (UnT term) => Trans term => Num n => term Integer -> term n

        abs         = trans1 abs
        negate      = trans1 negate
        signum      = trans1 signum
        (+)         = trans2 (+)
        (-)         = trans2 (-)
        (*)         = trans2 (*)
        fromInteger = trans1 fromInteger

-- Interpreting
instance Sym_Num Eval where
        abs         = eval1 Prelude.abs
        negate      = eval1 Prelude.negate
        signum      = eval1 Prelude.signum
        (+)         = eval2 (Prelude.+)
        (-)         = eval2 (Prelude.-)
        (*)         = eval2 (Prelude.*)
        fromInteger = eval1 Prelude.fromInteger
instance Sym_Num View where
        abs         = view1 "abs"
        negate      = view1 "negate"
        signum      = view1 "signum"
        (+)         = viewInfix "+" (infixB SideL 6)
        (-)         = viewInfix "-" (infixL 6)
        (*)         = viewInfix "*" (infixB SideL 7)
        fromInteger = view1 "fromInteger"
instance (Sym_Num r1, Sym_Num r2) => Sym_Num (Dup r1 r2) where
        abs         = dup1 @Sym_Num abs
        negate      = dup1 @Sym_Num negate
        signum      = dup1 @Sym_Num signum
        (+)         = dup2 @Sym_Num (+)
        (-)         = dup2 @Sym_Num (-)
        (*)         = dup2 @Sym_Num (*)
        fromInteger = dup1 @Sym_Num fromInteger

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

-- Typing
instance NameTyOf Num where
        nameTyOf _c = ["Num"] `Mod` "Num"
instance FixityOf Num
instance ClassInstancesFor Num
instance TypeInstancesFor Num

-- Compiling
instance Gram_Term_AtomsFor src ss g Num
instance (Source src, SymInj ss Num) => ModuleFor src ss Num where
        moduleFor = ["Num"] `moduleWhere`
         [ "abs"    := teNum_abs
         , "negate" := teNum_negate
         , "signum" := teNum_signum
         , "+" `withInfixB` (SideL, 6) := teNum_add
         , "-" `withInfixL` 6          := teNum_sub
         , "-" `withPrefix` 10         := teNum_negate
         , "*" `withInfixB` (SideL, 7) := teNum_mul
         , "fromInteger" := teNum_fromInteger
         ]

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

-- ** 'Term's
teNum_fromInteger :: TermDef Num '[Proxy a] (Num a #> (Integer -> a))
teNum_fromInteger = Term (tyNum a0) (tyInteger ~> a0) $ teSym @Num $ lam1 fromInteger

teNum_abs, teNum_negate, teNum_signum :: TermDef Num '[Proxy a] (Num a #> (a -> a))
teNum_abs = Term (tyNum a0) (a0 ~> a0) $ teSym @Num $ lam1 abs
teNum_negate = Term (tyNum a0) (a0 ~> a0) $ teSym @Num $ lam1 negate
teNum_signum = Term (tyNum a0) (a0 ~> a0) $ teSym @Num $ lam1 signum

teNum_add, teNum_sub, teNum_mul :: TermDef Num '[Proxy a] (Num a #> (a -> a -> a))
teNum_add = Term (tyNum a0) (a0 ~> a0 ~> a0) $ teSym @Num $ lam2 (+)
teNum_sub = Term (tyNum a0) (a0 ~> a0 ~> a0) $ teSym @Num $ lam2 (-)
teNum_mul = Term (tyNum a0) (a0 ~> a0 ~> a0) $ teSym @Num $ lam2 (*)