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

import Data.Semigroup ((<>))
import Prelude hiding (fst, snd)
import qualified Data.Tuple as Tuple
import qualified Data.MonoTraversable as MT

import Language.Symantic
import Language.Symantic.Grammar
import Language.Symantic.Lib.Function (a0, b1)
import Language.Symantic.Lib.MonoFunctor (Element)
import Language.Symantic.Lib.Monoid (tyMonoid)

-- * Class 'Sym_Tuple2'
type instance Sym (,) = 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 :: Sym_Tuple2 (UnT term) => Trans term => term a -> term b -> term (a, b)
	default fst    :: Sym_Tuple2 (UnT term) => Trans term => term (a, b) -> term a
	default snd    :: Sym_Tuple2 (UnT term) => Trans term => term (a, b) -> term b
	
	tuple2 = trans2 tuple2
	fst    = trans1 fst
	snd    = trans1 snd

-- Interpreting
instance Sym_Tuple2 Eval where
	tuple2 = eval2 (,)
	fst    = eval1 Tuple.fst
	snd    = eval1 Tuple.snd
instance Sym_Tuple2 View where
	tuple2 (View a) (View b) =
		View $ \_po v ->
			"(" <> a (op, SideL) v <> ", " <> b (op, SideR) v <> ")"
			where op = infixN 0
	fst = view1 "fst"
	snd = view1 "snd"
instance (Sym_Tuple2 r1, Sym_Tuple2 r2) => Sym_Tuple2 (Dup r1 r2) where
	tuple2 = dup2 @Sym_Tuple2 tuple2
	fst    = dup1 @Sym_Tuple2 fst
	snd    = dup1 @Sym_Tuple2 snd

-- Transforming
instance (Sym_Tuple2 term, Sym_Lambda term) => Sym_Tuple2 (BetaT term)

-- Typing
instance FixityOf (,) where
	fixityOf _c = Just $ Fixity2 $ infixN (-1)
instance ClassInstancesFor (,) where
	proveConstraintFor _ (TyApp _ (TyConst _ _ q) (TyApp _ c a))
	 | Just HRefl <- proj_ConstKiTy @_ @(,) c
	 = case () of
		 _ | Just Refl <- proj_Const @Applicative q
		   , Just Dict <- proveConstraint (tyMonoid a) -> Just Dict
		   | Just Refl <- proj_Const @Functor q  -> Just Dict
		   | Just Refl <- proj_Const @Foldable q -> Just Dict
		   | Just Refl <- proj_Const @Monad q
		   , Just Dict <- proveConstraint (tyMonoid a) -> Just Dict
		   | Just Refl <- proj_Const @Traversable q -> Just Dict
		 _ -> Nothing
	proveConstraintFor _ (TyApp _ tq@(TyConst _ _ q) (TyApp _ (TyApp _ c a) b))
	 | Just HRefl <- proj_ConstKiTy @_ @(,) c
	 = case () of
		 _ | Just Refl <- proj_Const @Bounded q
		   , Just Dict <- proveConstraint (tq `tyApp` a)
		   , Just Dict <- proveConstraint (tq `tyApp` b) -> Just Dict
		   | Just Refl <- proj_Const @Eq q
		   , Just Dict <- proveConstraint (tq `tyApp` a)
		   , Just Dict <- proveConstraint (tq `tyApp` b) -> Just Dict
		   | Just Refl <- proj_Const @Monoid q
		   , Just Dict <- proveConstraint (tq `tyApp` a)
		   , Just Dict <- proveConstraint (tq `tyApp` b) -> Just Dict
		   | Just Refl <- proj_Const @Ord q
		   , Just Dict <- proveConstraint (tq `tyApp` a)
		   , Just Dict <- proveConstraint (tq `tyApp` b) -> Just Dict
		   | Just Refl <- proj_Const @Show q
		   , Just Dict <- proveConstraint (tq `tyApp` a)
		   , Just Dict <- proveConstraint (tq `tyApp` b) -> Just Dict
		   | Just Refl <- proj_Const @MT.MonoFoldable q -> Just Dict
		   | Just Refl <- proj_Const @MT.MonoFunctor q  -> Just Dict
		 _ -> Nothing
	proveConstraintFor _c _q = Nothing
instance TypeInstancesFor (,) where
	expandFamFor _c _len f (TyApp _ (TyApp _ c _a) b `TypesS` TypesZ)
	 | Just HRefl <- proj_ConstKi @_ @Element f
	 , Just HRefl <- proj_ConstKiTy @_ @(,) c
	 = Just b
	expandFamFor _c _len _fam _as = Nothing

-- Compiling
instance
 ( Gram_Source src g
 , Gram_Alt g
 , Gram_Rule g
 , Gram_Comment g
 , Gram_Term src ss g
 , SymInj ss (,)
 ) => Gram_Term_AtomsFor src ss g (,) where
	g_term_atomsFor =
	 -- TODO: proper TupleSections
	 [ rule "teTuple2_2" $
		source $ parens $
		(\a b src ->
			BinTree2 (BinTree2 (BinTree0 $ Token_Term $ TermAVT $ (`setSource` src) $ teTuple2) a) b)
		 <$> g_term
		 <*  symbol ","
		 <*> g_term
	 , rule "teTuple2" $
		source $
		(\src -> BinTree0 $ Token_Term $ TermAVT $ (`setSource` src) $ teTuple2)
		 <$ symbol "(,)"
	 ]
instance (Source src, SymInj ss (,)) => ModuleFor src ss (,) where
	moduleFor = ["Tuple2"] `moduleWhere`
	 [ "fst" := teTuple2_fst
	 , "snd" := teTuple2_snd
	 ]

-- ** 'Term's
tyTuple2 :: Source src => LenInj vs => Type src vs a -> Type src vs b -> Type src vs (a, b)
tyTuple2 a b = tyConst @(K (,)) @(,) `tyApp` a `tyApp` b

teTuple2 :: TermDef (,) '[Proxy a, Proxy b] (() #> (a -> b -> (a, b)))
teTuple2 = Term noConstraint (a0 ~> b1 ~> tyTuple2 a0 b1) $ teSym @(,) $ lam2 tuple2
teTuple2_fst :: TermDef (,) '[Proxy a, Proxy b] (() #> ((a, b) -> a))
teTuple2_fst = Term noConstraint (tyTuple2 a0 b1 ~> a0) $ teSym @(,) $ lam1 fst
teTuple2_snd :: TermDef (,) '[Proxy a, Proxy b] (() #> ((a, b) -> b))
teTuple2_snd = Term noConstraint (tyTuple2 a0 b1 ~> b1) $ teSym @(,) $ lam1 snd