{-# 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=11 #-}
-- | Symantic for @(,)@.
module Language.Symantic.Compiling.Tuple2 where

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

import Language.Symantic.Typing
import Language.Symantic.Compiling.Term
import Language.Symantic.Compiling.Monoid (tyMonoid)
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 sym_Tuple2 tuple2
	fst    = dupI1 sym_Tuple2 fst
	snd    = dupI1 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 (,))
	 = Just $ case () of
		 _ | Just Refl <- proj_const q (Proxy::Proxy Applicative)
		   , Just Con  <- proj_con (tyMonoid :$ 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 (tyMonoid :$ 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 (,))
	 = Just $ 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
instance -- Term_fromI
 ( AST ast
 , Lexem ast ~ LamVarName
 , Inj_Const (Consts_of_Ifaces is) (,)
 , Term_from is ast
 ) => Term_fromI is (Proxy (,)) ast where
	term_fromI ast ctx k =
		case ast_lexem ast of
		 "(,)" -> tuple2_from
		 "fst" -> fst_from
		 "snd" -> snd_from
		 _ -> Left $ Error_Term_unsupported
		where
		tuple2_from =
		 -- (,) :: a -> b -> (a, b)
			from_ast2 ast $ \ast_a ast_b as ->
			term_from ast_a ctx $ \ty_a (TermLC a) ->
			term_from ast_b ctx $ \ty_b (TermLC b) ->
			k as (tyTuple2 :$ ty_a :$ ty_b) $ TermLC $
			 \c -> tuple2 (a c) (b c)
		fst_from =
		 -- fst :: (a, b) -> a
			from_ast1 ast $ \ast_ab as ->
			term_from ast_ab ctx $ \ty_ab (TermLC ab) ->
			check_type2 tyTuple2 ast_ab ty_ab $ \Refl ty_a _ty_b ->
			k as ty_a $ TermLC $
			 \c -> fst (ab c)
		snd_from =
		 -- snd :: (a, b) -> b
			from_ast1 ast $ \ast_ab as ->
			term_from ast_ab ctx $ \ty_ab (TermLC ab) ->
			check_type2 tyTuple2 ast_ab ty_ab $ \Refl _ty_a ty_b ->
			k as ty_b $ TermLC $
			 \c -> snd (ab c)

-- | The '(,)' 'Type'
tyTuple2 :: Inj_Const cs (,) => Type cs (,)
tyTuple2 = TyConst inj_const

sym_Tuple2 :: Proxy Sym_Tuple2
sym_Tuple2 = Proxy

syTuple2 :: IsString a => [Syntax a] -> Syntax a
syTuple2 = Syntax "(,)"