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

import Control.Monad (liftM, liftM2)
import Data.Proxy
import Data.Type.Equality ((:~:)(Refl))
import Prelude (Num)
import Prelude hiding (Num(..))
import qualified Data.Function as Fun
import qualified Prelude

import Language.Symantic.Parsing
import Language.Symantic.Typing
import Language.Symantic.Compiling
import Language.Symantic.Interpreting
import Language.Symantic.Transforming
import Language.Symantic.Lib.Lambda

-- * Class '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         :: (Trans t term, Num n) => t term n -> t term n
	default negate      :: (Trans t term, Num n) => t term n -> t term n
	default signum      :: (Trans t term, Num n) => t term n -> t term n
	default (+)         :: (Trans t term, Num n) => t term n -> t term n -> t term n
	default (-)         :: (Trans t term, Num n) => t term n -> t term n -> t term n
	default (*)         :: (Trans t term, Num n) => t term n -> t term n -> t term n
	default fromInteger :: (Trans t term, Num n) => t term Integer -> t term n
	
	abs         = trans_map1 abs
	negate      = trans_map1 negate
	signum      = trans_map1 signum
	(+)         = trans_map2 (+)
	(-)         = trans_map2 (-)
	(*)         = trans_map2 (*)
	fromInteger = trans_map1 fromInteger

type instance Sym_of_Iface (Proxy Num) = Sym_Num
type instance TyConsts_of_Iface (Proxy Num) = Proxy Num ': TyConsts_imported_by (Proxy Num)
type instance TyConsts_imported_by (Proxy Num) =
 '[ Proxy Integer
 ]

instance Sym_Num HostI where
	abs         = liftM Prelude.abs
	negate      = liftM Prelude.negate
	signum      = liftM Prelude.signum
	(+)         = liftM2 (Prelude.+)
	(-)         = liftM2 (Prelude.-)
	(*)         = liftM2 (Prelude.*)
	fromInteger = liftM Prelude.fromInteger
instance Sym_Num TextI where
	abs         = textI1 "abs"
	negate      = textI1 "negate"
	signum      = textI1 "signum"
	(+)         = textI_infix "+" (infixB L 6)
	(-)         = textI_infix "-" (infixL 6)
	(*)         = textI_infix "*" (infixB L 7)
	fromInteger = textI1 "fromInteger"
instance (Sym_Num r1, Sym_Num r2) => Sym_Num (DupI r1 r2) where
	abs         = dupI1 @Sym_Num abs
	negate      = dupI1 @Sym_Num negate
	signum      = dupI1 @Sym_Num signum
	(+)         = dupI2 @Sym_Num (+)
	(-)         = dupI2 @Sym_Num (-)
	(*)         = dupI2 @Sym_Num (*)
	fromInteger = dupI1 @Sym_Num fromInteger

instance
 ( Read_TyNameR TyName cs rs
 , Inj_TyConst cs Num
 ) => Read_TyNameR TyName cs (Proxy Num ': rs) where
	read_TyNameR _cs (TyName "Num") k = k (ty @Num)
	read_TyNameR _rs raw k = read_TyNameR (Proxy @rs) raw k
instance Show_TyConst cs => Show_TyConst (Proxy Num ': cs) where
	show_TyConst TyConstZ{} = "Num"
	show_TyConst (TyConstS c) = show_TyConst c

instance Proj_TyConC cs (Proxy Num)
data instance TokenT meta (ts::[*]) (Proxy Num)
 = Token_Term_Num_abs         (EToken meta ts)
 | Token_Term_Num_negate      (EToken meta ts)
 | Token_Term_Num_signum      (EToken meta ts)
 | Token_Term_Num_add         (EToken meta ts)
 | Token_Term_Num_sub         (EToken meta ts)
 | Token_Term_Num_mul         (EToken meta ts)
 | Token_Term_Num_fromInteger (EToken meta '[Proxy Token_Type])
deriving instance (Eq meta, Eq_Token meta ts) => Eq (TokenT meta ts (Proxy Num))
deriving instance (Show meta, Show_Token meta ts) => Show (TokenT meta ts (Proxy Num))

instance -- CompileI
 ( Read_TyName TyName cs
 , Inj_TyConst        cs Num
 , Inj_TyConst        cs (->)
 , Inj_TyConst        cs Integer
 , Proj_TyCon         cs
 , Compile cs is
 ) => CompileI cs is (Proxy Num) where
	compileI tok ctx k =
		case tok of
		 Token_Term_Num_abs    tok_a -> op1_from tok_a abs
		 Token_Term_Num_negate tok_a -> op1_from tok_a negate
		 Token_Term_Num_signum tok_a -> op1_from tok_a signum
		 Token_Term_Num_add    tok_a -> op2_from tok_a (+)
		 Token_Term_Num_sub    tok_a -> op2_from tok_a (-)
		 Token_Term_Num_mul    tok_a -> op2_from tok_a (*)
		 Token_Term_Num_fromInteger tok_ty_a ->
			-- fromInteger :: Num a => Integer -> a
			compile_Type tok_ty_a $ \(ty_a::Type cs a) ->
			check_Kind
			 (At Nothing SKiType)
			 (At (Just tok_ty_a) $ kind_of ty_a) $ \Refl ->
			check_TyCon (At (Just tok_ty_a) (ty @Num :$ ty_a)) $ \TyCon ->
			k (ty @Integer ~> ty_a) $ Term $
				Fun.const $ lam fromInteger
		where
		op1_from tok_a
		 (op::forall term a. (Sym_Num term, Num a)
			 => term a -> term a) =
		 -- abs    :: Num a => a -> a
		 -- negate :: Num a => a -> a
		 -- signum :: Num a => a -> a
			compile tok_a ctx $ \ty_a (Term x) ->
			check_TyCon (At (Just tok_a) (ty @Num :$ ty_a)) $ \TyCon ->
			k ty_a $ Term $
			 \c -> op (x c)
		op2_from tok_a
		 (op::forall term a. (Sym_Num term, Num a)
			 => term a -> term a -> term a) =
		 -- (+) :: Num a => a -> a -> a
		 -- (-) :: Num a => a -> a -> a
		 -- (*) :: Num a => a -> a -> a
			compile tok_a ctx $ \ty_a (Term x) ->
			check_TyCon (At (Just tok_a) (ty @Num :$ ty_a)) $ \TyCon ->
			k (ty_a ~> ty_a) $ Term $
			 \c -> lam $ \y -> op (x c) y
instance -- TokenizeT
 Inj_Token meta ts Num =>
 TokenizeT meta ts (Proxy Num) where
	tokenizeT _t = mempty
	 { tokenizers_infix = tokenizeTMod []
		 [ tokenize1 "abs"    infixN5 Token_Term_Num_abs
		 , tokenize1 "negate" infixN5 Token_Term_Num_negate
		 , tokenize1 "signum" infixN5 Token_Term_Num_signum
		 , tokenize1 "+" (infixB L 6) Token_Term_Num_add
		 , tokenize1 "-" (infixL 6) Token_Term_Num_sub
		 , tokenize1 "*" (infixB L 7) Token_Term_Num_mul
		 , (TeName "fromInteger",) ProTok_Term
			 { protok_term = \meta -> ProTokPi $ \a ->
				ProTokTe $ inj_EToken meta $ Token_Term_Num_fromInteger a
			 , protok_fixity = infixN5
			 }
		 ]
	 , tokenizers_prefix = tokenizeTMod []
		 [ tokenize1 "-"   (Prefix 10) Token_Term_Num_negate
		 ]
	 }
instance Gram_Term_AtomsT meta ts (Proxy Num) g