{-# LANGUAGE DefaultSignatures #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
-- | Expression for 'Num'.
module Language.Symantic.Expr.Num where

import Control.Monad
import Prelude hiding (Num(..))
import Prelude (Num)
import qualified Prelude
import Data.Proxy (Proxy(..))
import Data.Type.Equality ((:~:)(Refl))

import Language.Symantic.Type
import Language.Symantic.Repr
import Language.Symantic.Expr.Root
import Language.Symantic.Expr.Error
import Language.Symantic.Expr.From
import Language.Symantic.Trans.Common

-- * Class 'Sym_Num'
-- | Symantic.
class Sym_Num repr where
	abs         :: Num n => repr n -> repr n
	negate      :: Num n => repr n -> repr n
	signum      :: Num n => repr n -> repr n
	(+)         :: Num n => repr n -> repr n -> repr n
	(-)         :: Num n => repr n -> repr n -> repr n
	(*)         :: Num n => repr n -> repr n -> repr n
	fromInteger :: Num n => repr Integer -> repr n
	
	default abs         :: (Trans t repr, Num n) => t repr n -> t repr n
	default negate      :: (Trans t repr, Num n) => t repr n -> t repr n
	default signum      :: (Trans t repr, Num n) => t repr n -> t repr n
	default (+)         :: (Trans t repr, Num n) => t repr n -> t repr n -> t repr n
	default (-)         :: (Trans t repr, Num n) => t repr n -> t repr n -> t repr n
	default (*)         :: (Trans t repr, Num n) => t repr n -> t repr n -> t repr n
	default fromInteger :: (Trans t repr, Num n) => t repr Integer -> t repr 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 *

instance Sym_Num Repr_Host 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 Repr_Text where
	abs         = repr_text_app1 "abs"
	negate      = repr_text_app1 "negate"
	signum      = repr_text_app1 "signum"
	(+)         = repr_text_infix "+" (Precedence 6)
	(-)         = repr_text_infix "-" (Precedence 6)
	(*)         = repr_text_infix "-" (Precedence 7)
	fromInteger = repr_text_app1 "fromInteger"
instance (Sym_Num r1, Sym_Num r2) => Sym_Num (Repr_Dup r1 r2) where
	abs         = repr_dup1 sym_Num abs
	negate      = repr_dup1 sym_Num negate
	signum      = repr_dup1 sym_Num signum
	(+)         = repr_dup2 sym_Num (+)
	(-)         = repr_dup2 sym_Num (-)
	(*)         = repr_dup2 sym_Num (*)
	fromInteger = repr_dup1 sym_Num fromInteger

sym_Num :: Proxy Sym_Num
sym_Num = Proxy

-- * Type 'Expr_Num'
-- | Expression.
data Expr_Num (root:: *)
type instance Root_of_Expr      (Expr_Num root)      = root
type instance Type_of_Expr      (Expr_Num root)      = No_Type
type instance Sym_of_Expr       (Expr_Num root) repr = Sym_Num repr
type instance Error_of_Expr ast (Expr_Num root)      = No_Error_Expr

-- | Parse 'fst'.
fromInteger_from
 :: forall root ty ast hs ret.
 ( ty ~ Type_Root_of_Expr (Expr_Num root)
 , Type0_Eq ty
 , Expr_From ast root
 , Type0_Lift   Type_Integer (Type_of_Expr root)
 , Type0_Unlift Type_Integer (Type_of_Expr root)
 , Type0_Constraint Num ty
 , Error_Expr_Lift (Error_Expr (Error_of_Type ast ty) ty ast)
                   (Error_of_Expr ast root)
 , Root_of_Expr root ~ root
 ) => ast
 -> ExprFrom ast (Expr_Num root) hs ret
fromInteger_from ast_i ex ast ctx k =
 -- fromInteger :: Num a => Integer -> a
	expr_from (Proxy::Proxy root) ast_i ctx $
	 \(ty_i::ty h_i) (Forall_Repr_with_Context i) ->
	check_type0_eq ex ast type_integer ty_i $ \Refl ->
	k ty_i $ Forall_Repr_with_Context $
	 \c -> fromInteger (i c)