{-# LANGUAGE DataKinds #-}
{-# LANGUAGE DefaultSignatures #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE Rank2Types #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# 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.String (IsString)
import Data.Text (Text)
import Data.Type.Equality ((:~:)(Refl))
import qualified Prelude
import Prelude hiding (Num(..))
import Prelude (Num)

import Language.Symantic.Typing
import Language.Symantic.Compiling.Term
import Language.Symantic.Compiling.Integer (tyInteger)
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 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 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
 Proj_ConC cs (Proxy Num)
instance -- Term_fromI
 ( AST ast
 , Lexem ast ~ LamVarName
 , Const_from (Lexem ast) (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 ast
 ) => Term_fromI is (Proxy Num) ast where
	term_fromI ast ctx k =
		case ast_lexem ast of
		 "abs"         -> num_op1_from abs
		 "negate"      -> num_op1_from negate
		 "signum"      -> num_op1_from signum
		 "+"           -> num_op2_from (+)
		 "-"           -> num_op2_from (-)
		 "*"           -> num_op2_from (*)
		 "fromInteger" -> fromInteger_from
		 _ -> Left $ Error_Term_unsupported
		where
		num_op1_from
		 (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
			from_ast1 ast $ \ast_a as ->
			term_from ast_a ctx $ \ty_a (TermLC x) ->
			check_constraint (At (Just ast_a) (tyNum :$ ty_a)) $ \Con ->
			k as ty_a $ TermLC $
			 \c -> op (x c)
		num_op2_from
		 (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
			from_ast1 ast $ \ast_a as ->
			term_from ast_a ctx $ \ty_a (TermLC x) ->
			check_constraint (At (Just ast_a) (tyNum :$ ty_a)) $ \Con ->
			k as (ty_a ~> ty_a) $ TermLC $
			 \c -> lam $ \y -> op (x c) y
		fromInteger_from =
		 -- fromInteger :: Num a => Integer -> a
			from_ast1 ast $ \ast_ty_a as ->
			either (Left . Error_Term_Typing . At (Just ast)) Fun.id $
			type_from ast_ty_a $ \ty_a -> Right $
			check_kind ast SKiType (At (Just ast_ty_a) ty_a) $ \Refl ->
			check_constraint (At (Just ast_ty_a) (tyNum :$ ty_a)) $ \Con ->
			k as (tyInteger ~> ty_a) $ TermLC $
			Fun.const $ lam fromInteger

-- | The 'Num' 'Type'
tyNum :: Inj_Const cs Num => Type cs Num
tyNum = TyConst inj_const

sym_Num :: Proxy Sym_Num
sym_Num = Proxy

syNum :: IsString a => [Syntax a] -> Syntax a
syNum = Syntax "Num"