{-# LANGUAGE UndecidableInstances #-}
{-# OPTIONS_GHC -fno-warn-orphans #-}
{-# OPTIONS_GHC -fconstraint-solver-iterations=11 #-}
-- | Symantic for @(,)@.
module Language.Symantic.Compiling.Tuple2 where

import Control.Monad (liftM, liftM2)
import Data.Monoid ((<>))
import Data.Proxy
import Data.Text (Text)
import qualified Data.Tuple as Tuple
import Data.Type.Equality ((:~:)(Refl))
import Prelude hiding (fst, snd)

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

-- * Class 'Sym_Tuple2'
class Sym_Tuple2 term where
	tuple2 :: term a -> term b -> term (a, b)
	fst :: term (a, b) -> term a
	snd :: term (a, b) -> term b
	
	default tuple2 :: Trans t term => t term a -> t term b -> t term (a, b)
	default fst :: Trans t term => t term (a, b) -> t term a
	default snd :: Trans t term => t term (a, b) -> t term b
	
	tuple2 = trans_map2 tuple2
	fst    = trans_map1 fst
	snd    = trans_map1 snd

type instance Sym_of_Iface (Proxy (,)) = Sym_Tuple2
type instance Consts_of_Iface (Proxy (,)) = Proxy (,) ': Consts_imported_by (,)
type instance Consts_imported_by (,) =
 [ Proxy Applicative
 , Proxy Bounded
 , Proxy Eq
 , Proxy Foldable
 , Proxy Functor
 , Proxy Monad
 , Proxy Monoid
 , Proxy Ord
 , Proxy Traversable
 ]

instance Sym_Tuple2 HostI where
	tuple2 = liftM2 (,)
	fst    = liftM  Tuple.fst
	snd    = liftM  Tuple.snd
instance Sym_Tuple2 TextI where
	tuple2 (TextI a) (TextI b) =
		TextI $ \_p v ->
			let p' = precedence_Toplevel in
			"(" <> a p' v <> ", " <> b p' v <> ")"
	fst = textI_app1 "fst"
	snd = textI_app1 "snd"
instance (Sym_Tuple2 r1, Sym_Tuple2 r2) => Sym_Tuple2 (DupI r1 r2) where
	tuple2 = dupI2 (Proxy @Sym_Tuple2) tuple2
	fst    = dupI1 (Proxy @Sym_Tuple2) fst
	snd    = dupI1 (Proxy @Sym_Tuple2) snd

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

instance -- Proj_ConC
 ( Proj_Const cs (,)
 , Proj_Consts cs (Consts_imported_by (,))
 , Proj_Con cs
 , Inj_Const cs Monoid
 ) => Proj_ConC cs (Proxy (,)) where
	proj_conC _ (TyConst q :$ (TyConst c :$ a))
	 | Just Refl <- eq_skind (kind_of_const c) (SKiType `SKiArrow` SKiType `SKiArrow` SKiType)
	 , Just Refl <- proj_const c (Proxy::Proxy (,))
	 = case () of
		 _ | Just Refl <- proj_const q (Proxy::Proxy Applicative)
		   , Just Con  <- proj_con (ty @Monoid :$ a) -> Just Con
		   | Just Refl <- proj_const q (Proxy::Proxy Functor)     -> Just Con
		   | Just Refl <- proj_const q (Proxy::Proxy Foldable)    -> Just Con
		   | Just Refl <- proj_const q (Proxy::Proxy Monad)
		   , Just Con  <- proj_con (ty @Monoid :$ a) -> Just Con
		   | Just Refl <- proj_const q (Proxy::Proxy Traversable) -> Just Con
		 _ -> Nothing
	proj_conC _ (t@(TyConst q) :$ (TyConst c :$ a :$ b))
	 | Just Refl <- eq_skind (kind_of_const c) (SKiType `SKiArrow` SKiType `SKiArrow` SKiType)
	 , Just Refl <- proj_const c (Proxy::Proxy (,))
	 = case () of
		 _ | Just Refl <- proj_const q (Proxy::Proxy Bounded)
		   , Just Con  <- proj_con (t :$ a)
		   , Just Con  <- proj_con (t :$ b) -> Just Con
		   | Just Refl <- proj_const q (Proxy::Proxy Eq)
		   , Just Con  <- proj_con (t :$ a)
		   , Just Con  <- proj_con (t :$ b) -> Just Con
		   | Just Refl <- proj_const q (Proxy::Proxy Monoid)
		   , Just Con  <- proj_con (t :$ a)
		   , Just Con  <- proj_con (t :$ b) -> Just Con
		   | Just Refl <- proj_const q (Proxy::Proxy Ord)
		   , Just Con  <- proj_con (t :$ a)
		   , Just Con  <- proj_con (t :$ b) -> Just Con
		 _ -> Nothing
	proj_conC _c _q = Nothing
data instance TokenT meta (ts::[*]) (Proxy (,))
 = Token_Term_Tuple2     (EToken meta ts) (EToken meta ts)
 | Token_Term_Tuple2_fst (EToken meta ts)
 | Token_Term_Tuple2_snd (EToken meta ts)
deriving instance Eq_Token meta ts => Eq (TokenT meta ts (Proxy (,)))
deriving instance Show_Token meta ts => Show (TokenT meta ts (Proxy (,)))
instance -- Term_fromI
 ( Inj_Const (Consts_of_Ifaces is) (,)
 , Term_from is
 ) => Term_fromI is (Proxy (,)) where
	term_fromI tok ctx k =
		case tok of
		 Token_Term_Tuple2 tok_a tok_b ->
			-- (,) :: a -> b -> (a, b)
			term_from tok_a ctx $ \ty_a (TermLC a) ->
			term_from tok_b ctx $ \ty_b (TermLC b) ->
			k (ty @(,) :$ ty_a :$ ty_b) $ TermLC $
			 \c -> tuple2 (a c) (b c)
		 Token_Term_Tuple2_fst tok_ab ->
			-- fst :: (a, b) -> a
			term_from tok_ab ctx $ \ty_ab (TermLC ab) ->
			check_type2 (ty @(,)) (At (Just tok_ab) ty_ab) $ \Refl ty_a _ty_b ->
			k ty_a $ TermLC $
			 \c -> fst (ab c)
		 Token_Term_Tuple2_snd tok_ab ->
			-- snd :: (a, b) -> b
			term_from tok_ab ctx $ \ty_ab (TermLC ab) ->
			check_type2 (ty @(,)) (At (Just tok_ab) ty_ab) $ \Refl _ty_a ty_b ->
			k ty_b $ TermLC $
			 \c -> snd (ab c)