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

import Control.Monad (liftM, liftM2)
import Data.Monoid ((<>))
import Data.Proxy
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
import Language.Symantic.Interpreting
import Language.Symantic.Transforming

-- * 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 TyConsts_of_Iface (Proxy (,)) = Proxy (,) ': TyConsts_imported_by (,)
type instance TyConsts_imported_by (,) =
 [ Proxy Applicative
 , Proxy Bounded
 , Proxy Eq
 , Proxy Foldable
 , Proxy Functor
 , Proxy Monad
 , Proxy Monoid
 , Proxy Ord
 , Proxy Show
 , 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 $ \_po v ->
			"(" <> a (op, L) v <> ", " <> b (op, R) v <> ")"
			where op = infixN 0
	fst = textI1 "fst"
	snd = textI1 "snd"
instance (Sym_Tuple2 r1, Sym_Tuple2 r2) => Sym_Tuple2 (DupI r1 r2) where
	tuple2 = dupI2 @Sym_Tuple2 tuple2
	fst    = dupI1 @Sym_Tuple2 fst
	snd    = dupI1 @Sym_Tuple2 snd

instance
 ( Read_TyNameR TyName cs rs
 , Inj_TyConst cs (,)
 ) => Read_TyNameR TyName cs (Proxy (,) ': rs) where
	read_TyNameR _cs (TyName "(,)") k = k (ty @(,))
	read_TyNameR _rs raw k = read_TyNameR (Proxy @rs) raw k
instance Show_TyConst cs => Show_TyConst (Proxy (,) ': cs) where
	show_TyConst TyConstZ{} = "(,)"
	show_TyConst (TyConstS c) = show_TyConst c

instance -- Proj_TyConC
 ( Proj_TyConst cs (,)
 , Proj_TyConsts cs (TyConsts_imported_by (,))
 , Proj_TyCon cs
 , Inj_TyConst cs Monoid
 ) => Proj_TyConC cs (Proxy (,)) where
	proj_TyConC _ (TyConst q :$ (TyConst c :$ a))
	 | Just Refl <- eq_skind (kind_of_TyConst c) (SKiType `SKiArrow` SKiType `SKiArrow` SKiType)
	 , Just Refl <- proj_TyConst c (Proxy @(,))
	 = case () of
		 _ | Just Refl <- proj_TyConst q (Proxy @Applicative)
		   , Just TyCon  <- proj_TyCon (ty @Monoid :$ a)     -> Just TyCon
		   | Just Refl <- proj_TyConst q (Proxy @Functor)  -> Just TyCon
		   | Just Refl <- proj_TyConst q (Proxy @Foldable) -> Just TyCon
		   | Just Refl <- proj_TyConst q (Proxy @Monad)
		   , Just TyCon  <- proj_TyCon (ty @Monoid :$ a) -> Just TyCon
		   | Just Refl <- proj_TyConst q (Proxy @Traversable) -> Just TyCon
		 _ -> Nothing
	proj_TyConC _ (t@(TyConst q) :$ (TyConst c :$ a :$ b))
	 | Just Refl <- eq_skind (kind_of_TyConst c) (SKiType `SKiArrow` SKiType `SKiArrow` SKiType)
	 , Just Refl <- proj_TyConst c (Proxy @(,))
	 = case () of
		 _ | Just Refl <- proj_TyConst q (Proxy @Bounded)
		   , Just TyCon  <- proj_TyCon (t :$ a)
		   , Just TyCon  <- proj_TyCon (t :$ b) -> Just TyCon
		   | Just Refl <- proj_TyConst q (Proxy @Eq)
		   , Just TyCon  <- proj_TyCon (t :$ a)
		   , Just TyCon  <- proj_TyCon (t :$ b) -> Just TyCon
		   | Just Refl <- proj_TyConst q (Proxy @Monoid)
		   , Just TyCon  <- proj_TyCon (t :$ a)
		   , Just TyCon  <- proj_TyCon (t :$ b) -> Just TyCon
		   | Just Refl <- proj_TyConst q (Proxy @Ord)
		   , Just TyCon  <- proj_TyCon (t :$ a)
		   , Just TyCon  <- proj_TyCon (t :$ b) -> Just TyCon
		   | Just Refl <- proj_TyConst q (Proxy @Show)
		   , Just TyCon  <- proj_TyCon (t :$ a)
		   , Just TyCon  <- proj_TyCon (t :$ b) -> Just TyCon
		 _ -> Nothing
	proj_TyConC _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 -- CompileI
 ( Inj_TyConst (TyConsts_of_Ifaces is) (,)
 , Compile is
 ) => CompileI is (Proxy (,)) where
	compileI tok ctx k =
		case tok of
		 Token_Term_Tuple2 tok_a tok_b ->
			-- (,) :: a -> b -> (a, b)
			compileO tok_a ctx $ \ty_a (TermO a) ->
			compileO tok_b ctx $ \ty_b (TermO b) ->
			k (ty @(,) :$ ty_a :$ ty_b) $ TermO $
			 \c -> tuple2 (a c) (b c)
		 Token_Term_Tuple2_fst tok_ab ->
			-- fst :: (a, b) -> a
			compileO tok_ab ctx $ \ty_ab (TermO ab) ->
			check_TyEq2 (ty @(,)) (At (Just tok_ab) ty_ab) $ \Refl ty_a _ty_b ->
			k ty_a $ TermO $
			 \c -> fst (ab c)
		 Token_Term_Tuple2_snd tok_ab ->
			-- snd :: (a, b) -> b
			compileO tok_ab ctx $ \ty_ab (TermO ab) ->
			check_TyEq2 (ty @(,)) (At (Just tok_ab) ty_ab) $ \Refl _ty_a ty_b ->
			k ty_b $ TermO $
			 \c -> snd (ab c)
instance -- TokenizeT
 Inj_Token meta ts (,) =>
 TokenizeT meta ts (Proxy (,)) where
	tokenizeT _t = mempty
	 { tokenizers_infix = tokenizeTMod []
		 [ tokenize1 "fst" infixN5 Token_Term_Tuple2_fst
		 , tokenize1 "snd" infixN5 Token_Term_Tuple2_snd
		 ]
	 }
instance -- Gram_Term_AtomsT
 ( Alt g
 , Gram_Rule g
 , Gram_Lexer g
 , Gram_Meta meta g
 , Gram_Term ts meta g
 , Inj_Token meta ts (->)
 , Inj_Token meta ts (,)
 ) => Gram_Term_AtomsT meta ts (Proxy (,)) g where
	term_atomsT _t =
	 [ rule "term_tuple2" $
		metaG $ parens $
		(\a b meta -> ProTok $ inj_EToken meta $ Token_Term_Tuple2 a b)
		 <$> termG
		 <*  symbol ","
		 <*> termG
	 , rule "term_tuple2" $
		metaG $
		(\meta -> ProTokLam $ \a -> ProTokLam $ \b -> ProTok $ inj_EToken meta $ Token_Term_Tuple2 a b)
		 <$ symbol "(,)"
	 ]