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

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

import Language.Symantic.Parsing
import Language.Symantic.Typing
import Language.Symantic.Compiling.Term
import Language.Symantic.Interpreting
import Language.Symantic.Transforming.Trans

-- * 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
	(-)         :: Num n => term n -> term n -> term n
	(*)         :: Num n => term n -> term n -> term n
	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

infixl 6 +
infixl 6 -
infixl 7 *

type instance Sym_of_Iface (Proxy Num) = Sym_Num
type instance Consts_of_Iface (Proxy Num) = Proxy Num ': Consts_imported_by Num
type instance Consts_imported_by 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         = textI_app1 "abs"
	negate      = textI_app1 "negate"
	signum      = textI_app1 "signum"
	(+)         = textI_infix "+" (Precedence 6)
	(-)         = textI_infix "-" (Precedence 6)
	(*)         = textI_infix "-" (Precedence 7)
	fromInteger = textI_app1 "fromInteger"
instance (Sym_Num r1, Sym_Num r2) => Sym_Num (DupI r1 r2) where
	abs         = dupI1 (Proxy @Sym_Num) abs
	negate      = dupI1 (Proxy @Sym_Num) negate
	signum      = dupI1 (Proxy @Sym_Num) signum
	(+)         = dupI2 (Proxy @Sym_Num) (+)
	(-)         = dupI2 (Proxy @Sym_Num) (-)
	(*)         = dupI2 (Proxy @Sym_Num) (*)
	fromInteger = dupI1 (Proxy @Sym_Num) fromInteger

instance Const_from Text cs => Const_from Text (Proxy Num ': cs) where
	const_from "Num" k = k (ConstZ kind)
	const_from s k = const_from s $ k . ConstS
instance Show_Const cs => Show_Const (Proxy Num ': cs) where
	show_const ConstZ{} = "Num"
	show_const (ConstS c) = show_const c

instance Proj_ConC 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 -- Term_fromI
 ( Const_from Name_LamVar (Consts_of_Ifaces is)
 , Inj_Const (Consts_of_Ifaces is) Num
 , Inj_Const (Consts_of_Ifaces is) (->)
 , Inj_Const (Consts_of_Ifaces is) Integer
 , Proj_Con  (Consts_of_Ifaces is)
 , Term_from is
 ) => Term_fromI is (Proxy Num) where
	term_fromI 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
			type_from tok_ty_a $ \(ty_a::Type (Consts_of_Ifaces is) a) ->
			check_kind
			 (At Nothing SKiType)
			 (At (Just tok_ty_a) $ kind_of ty_a) $ \Refl ->
			check_con (At (Just tok_ty_a) (ty @Num :$ ty_a)) $ \Con ->
			k (ty @Integer ~> ty_a) $ TermLC $
				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
			term_from tok_a ctx $ \ty_a (TermLC x) ->
			check_con (At (Just tok_a) (ty @Num :$ ty_a)) $ \Con ->
			k ty_a $ TermLC $
			 \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
			term_from tok_a ctx $ \ty_a (TermLC x) ->
			check_con (At (Just tok_a) (ty @Num :$ ty_a)) $ \Con ->
			k (ty_a ~> ty_a) $ TermLC $
			 \c -> lam $ \y -> op (x c) y