{-# 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 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 (*)