{-# 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 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
			from_ast1 ast $ \ast_a as ->
			term_from ast_a ctx $ \ty_a (TermLC x) ->
			check_constraint (At (Just ast_a) (tyIntegral :$ ty_a)) $ \Con ->
			k as (ty_a ~> ty_a) $ TermLC $
			 \c -> lam $ \y -> op (x c) y
		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)
			from_ast1 ast $ \ast_a as ->
			term_from ast_a ctx $ \ty_a (TermLC x) ->
			check_constraint (At (Just ast_a) (tyIntegral :$ ty_a)) $ \Con ->
			k as (ty_a ~> (tyTuple2 :$ ty_a) :$ ty_a) $ TermLC $
			 \c -> lam $ \y -> op (x c) y

-- | 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"