{-# 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 #-}
{-# OPTIONS_GHC -fconstraint-solver-iterations=6 #-}
-- | Symantic for 'Integral'.
module Language.Symantic.Compiling.Integral where

import Control.Monad (liftM, liftM2)
import Data.Proxy
import Data.String (IsString)
import Data.Text (Text)
import Data.Type.Equality ((:~:)(Refl))
import qualified Prelude
import Prelude hiding (Integral(..))
import Prelude (Integral)

import Language.Symantic.Typing
import Language.Symantic.Compiling.Term
import Language.Symantic.Compiling.Tuple2 (tyTuple2)
import Language.Symantic.Interpreting
import Language.Symantic.Transforming.Trans

-- * Class 'Sym_Integral'
class Sym_Integral term where
	quot      :: Integral i => term i -> term i -> term i
	rem       :: Integral i => term i -> term i -> term i
	div       :: Integral i => term i -> term i -> term i
	mod       :: Integral i => term i -> term i -> term i
	quotRem   :: Integral i => term i -> term i -> term (i, i)
	divMod    :: Integral i => term i -> term i -> term (i, i)
	toInteger :: Integral i => term i -> term Integer
	
	default quot      :: (Trans t term, Integral i) => t term i -> t term i -> t term i
	default rem       :: (Trans t term, Integral i) => t term i -> t term i -> t term i
	default div       :: (Trans t term, Integral i) => t term i -> t term i -> t term i
	default mod       :: (Trans t term, Integral i) => t term i -> t term i -> t term i
	default quotRem   :: (Trans t term, Integral i) => t term i -> t term i -> t term (i, i)
	default divMod    :: (Trans t term, Integral i) => t term i -> t term i -> t term (i, i)
	default toInteger :: (Trans t term, Integral i) => t term i -> t term Integer
	
	quot      = trans_map2 quot
	rem       = trans_map2 rem
	div       = trans_map2 div
	mod       = trans_map2 mod
	quotRem   = trans_map2 quotRem
	divMod    = trans_map2 divMod
	toInteger = trans_map1 toInteger

infixl 7 `quot`
infixl 7 `rem`
infixl 7 `div`
infixl 7 `mod`

type instance Sym_of_Iface (Proxy Integral) = Sym_Integral
type instance Consts_of_Iface (Proxy Integral) = Proxy Integral ': Consts_imported_by Integral
type instance Consts_imported_by Integral =
 '[ Proxy (,)
 ]

instance Sym_Integral HostI where
	quot      = liftM2 Prelude.quot
	rem       = liftM2 Prelude.rem
	div       = liftM2 Prelude.div
	mod       = liftM2 Prelude.mod
	quotRem   = liftM2 Prelude.quotRem
	divMod    = liftM2 Prelude.divMod
	toInteger = liftM  Prelude.toInteger
instance Sym_Integral TextI where
	quot      = textI_infix "`quot`" (Precedence 7)
	div       = textI_infix "`div`"  (Precedence 7)
	rem       = textI_infix "`rem`"  (Precedence 7)
	mod       = textI_infix "`mod`"  (Precedence 7)
	quotRem   = textI_app2 "quotRem"
	divMod    = textI_app2 "divMod"
	toInteger = textI_app1 "toInteger"
instance (Sym_Integral r1, Sym_Integral r2) => Sym_Integral (DupI r1 r2) where
	quot      = dupI2 sym_Integral quot
	rem       = dupI2 sym_Integral rem
	div       = dupI2 sym_Integral div
	mod       = dupI2 sym_Integral mod
	quotRem   = dupI2 sym_Integral quotRem
	divMod    = dupI2 sym_Integral divMod
	toInteger = dupI1 sym_Integral toInteger

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

instance -- Proj_ConC
 Proj_ConC cs (Proxy Integral)
instance -- Term_fromI
 ( AST ast
 , Lexem ast ~ LamVarName
 , Inj_Const (Consts_of_Ifaces is) Integral
 , Inj_Const (Consts_of_Ifaces is) (->)
 , Inj_Const (Consts_of_Ifaces is) (,)
 , Proj_Con  (Consts_of_Ifaces is)
 , Term_from is ast
 ) => Term_fromI is (Proxy Integral) ast where
	term_fromI ast ctx k =
		case ast_lexem ast of
		 "quot"    -> integral_op2_from quot
		 "rem"     -> integral_op2_from rem
		 "div"     -> integral_op2_from div
		 "mod"     -> integral_op2_from mod
		 "quotRem" -> integral_op2t2_from quotRem
		 "divMod"  -> integral_op2t2_from divMod
		 _ -> Left $ Error_Term_unsupported
		where
		integral_op2_from
		 (op::forall term a. (Sym_Integral term, Integral a)
			 => term a -> term a -> term a) =
		 -- quot :: Integral i => i -> i -> i
		 -- rem  :: Integral i => i -> i -> i
		 -- div  :: Integral i => i -> i -> i
		 -- mod  :: Integral i => i -> i -> i
			case ast_nodes ast of
			 [] -> Left $ Error_Term_Syntax $
				Error_Syntax_more_arguments_needed $ At (Just ast) 1
			 [ast_a] ->
				term_from ast_a ctx $ \ty_a (TermLC x) ->
				check_constraint (At (Just ast_a) (tyIntegral :$ ty_a)) $ \Con ->
				k (ty_a ~> ty_a) $ TermLC $
				 \c -> lam $ \y -> op (x c) y
			 [ast_a, ast_y] ->
				term_from ast_a ctx $ \ty_a (TermLC x) ->
				term_from ast_y ctx $ \ty_y (TermLC y) ->
				check_type (At (Just ast_a) ty_a) (At (Just ast_y) ty_y) $ \Refl ->
				check_constraint (At (Just ast_a) (tyIntegral :$ ty_a)) $ \Con ->
				k ty_a $ TermLC $
				 \c -> op (x c) (y c)
			 _ -> Left $ Error_Term_Syntax $
				Error_Syntax_too_many_arguments $ At (Just ast) 2
		integral_op2t2_from
		 (op::forall term a. (Sym_Integral term, Integral a)
			 => term a -> term a -> term (a, a)) =
		 -- quotRem :: Integral i => i -> i -> (i, i)
		 -- divMod  :: Integral i => i -> i -> (i, i)
			case ast_nodes ast of
			 [] -> Left $ Error_Term_Syntax $
				Error_Syntax_more_arguments_needed $ At (Just ast) 1
			 [ast_a] ->
				term_from ast_a ctx $ \ty_a (TermLC x) ->
				check_constraint (At (Just ast_a) (tyIntegral :$ ty_a)) $ \Con ->
				k (ty_a ~> (tyTuple2 :$ ty_a) :$ ty_a) $ TermLC $
				 \c -> lam $ \y -> op (x c) y
			 [ast_a, ast_y] ->
				term_from ast_a ctx $ \ty_a (TermLC x) ->
				term_from ast_y ctx $ \ty_y (TermLC y) ->
				check_type (At (Just ast_a) ty_a) (At (Just ast_y) ty_y) $ \Refl ->
				check_constraint (At (Just ast_a) (tyIntegral :$ ty_a)) $ \Con ->
				k ((tyTuple2 :$ ty_a) :$ ty_a) $ TermLC $
				 \c -> op (x c) (y c)
			 _ -> Left $ Error_Term_Syntax $
				Error_Syntax_too_many_arguments $ At (Just ast) 2

-- | The 'Integral' 'Type'
tyIntegral :: Inj_Const cs Integral => Type cs Integral
tyIntegral = TyConst inj_const

sym_Integral :: Proxy Sym_Integral
sym_Integral = Proxy

syIntegral :: IsString a => [Syntax a] -> Syntax a
syIntegral = Syntax "Integral"