{-# LANGUAGE DefaultSignatures #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeFamilies #-}
{-# OPTIONS_GHC -fno-warn-orphans #-}
-- | Expression for tuples.
module Language.Symantic.Expr.Tuple where

import Control.Monad
import Data.Monoid
import Data.Proxy (Proxy(..))
import qualified Data.Tuple as Tuple
import Prelude hiding (maybe, fst, snd)

import Language.Symantic.Type
import Language.Symantic.Repr
import Language.Symantic.Expr.Root
import Language.Symantic.Expr.Error
import Language.Symantic.Expr.From
import Language.Symantic.Trans.Common

-- * Class 'Sym_Tuple_Lam'
-- | Symantic.
class Sym_Tuple2 repr where
	tuple2 :: repr a -> repr b -> repr (a, b)
	fst :: repr (a, b) -> repr a
	snd :: repr (a, b) -> repr b
	
	default tuple2 :: Trans t repr => t repr a -> t repr b -> t repr (a, b)
	default fst :: Trans t repr => t repr (a, b) -> t repr a
	default snd :: Trans t repr => t repr (a, b) -> t repr b
	
	tuple2 = trans_map2 tuple2
	fst    = trans_map1 fst
	snd    = trans_map1 snd
instance Sym_Tuple2 Repr_Host where
	tuple2 = liftM2 (,)
	fst    = liftM  Tuple.fst
	snd    = liftM  Tuple.snd
instance Sym_Tuple2 Repr_Text where
	tuple2 (Repr_Text a) (Repr_Text b) =
		Repr_Text $ \_p v ->
			let p' = precedence_Toplevel in
			"(" <> a p' v <> ", " <> b p' v <> ")"
	fst = repr_text_app1 "fst"
	snd = repr_text_app1 "snd"
instance (Sym_Tuple2 r1, Sym_Tuple2 r2) => Sym_Tuple2 (Repr_Dup r1 r2) where
	tuple2 = repr_dup2 sym_Tuple2 tuple2
	fst    = repr_dup1 sym_Tuple2 fst
	snd    = repr_dup1 sym_Tuple2 snd

sym_Tuple2 :: Proxy Sym_Tuple2
sym_Tuple2 = Proxy

-- * Type 'Expr_Tuple2'
-- | Expression.
data Expr_Tuple2 (root:: *)
type instance Root_of_Expr      (Expr_Tuple2 root)      = root
type instance Type_of_Expr      (Expr_Tuple2 root)      = Type_Tuple2
type instance Sym_of_Expr       (Expr_Tuple2 root) repr = Sym_Tuple2 repr
type instance Error_of_Expr ast (Expr_Tuple2 root)      = No_Error_Expr

-- | Parsing utility to check that the given type is a 'Type_Tuple2'
-- or raise 'Error_Expr_Type_mismatch'.
check_type_tuple2
 :: forall ast ex root ty h ret.
 ( root ~ Root_of_Expr ex
 , ty ~ Type_Root_of_Expr ex
 , Type0_Lift   Type_Tuple2 (Type_of_Expr root)
 , Type0_Unlift Type_Tuple2 (Type_of_Expr root)
 , Error_Expr_Lift (Error_Expr (Error_of_Type ast ty) ty ast)
                   (Error_of_Expr ast root)
 )
 => Proxy ex -> ast -> ty h
 -> (Type_Tuple2 ty h -> Either (Error_of_Expr ast root) ret)
 -> Either (Error_of_Expr ast root) ret
check_type_tuple2 ex ast ty k =
	case type0_unlift $ unType_Root ty of
	 Just ty_t -> k ty_t
	 Nothing -> Left $
		error_expr ex $
		Error_Expr_Type_mismatch ast
		 (Exists_Type0 (type_tuple2 (type_var0 SZero) (type_var0 $ SSucc SZero)
		 :: ty (Var0, Var0)))
		 (Exists_Type0 ty)

-- | Parse 'tuple2'.
tuple2_from
 :: forall root ty ast hs ret.
 ( ty ~ Type_Root_of_Expr (Expr_Tuple2 root)
 , Type0_Eq ty
 , Expr_From ast root
 , Type0_Lift   Type_Tuple2 (Type_of_Expr root)
 , Type0_Unlift Type_Tuple2 (Type_of_Expr root)
 , Error_Expr_Lift (Error_Expr (Error_of_Type ast ty) ty ast)
                   (Error_of_Expr ast root)
 , Root_of_Expr root ~ root
 ) => ast -> ast
 -> ExprFrom ast (Expr_Tuple2 root) hs ret
tuple2_from ast_a ast_b _ex _ast ctx k =
	expr_from (Proxy::Proxy root) ast_a ctx $
	 \(ty_a::ty h_a) (Forall_Repr_with_Context a) ->
	expr_from (Proxy::Proxy root) ast_b ctx $
	 \(ty_b::ty h_b) (Forall_Repr_with_Context b) ->
	k (type_tuple2 ty_a ty_b) $ Forall_Repr_with_Context $
	 \c -> tuple2 (a c) (b c)

-- | Parse 'fst'.
fst_from
 :: forall root ty ast hs ret.
 ( ty ~ Type_Root_of_Expr (Expr_Tuple2 root)
 , Type0_Eq ty
 , Expr_From ast root
 , Type0_Lift   Type_Tuple2 (Type_of_Expr root)
 , Type0_Unlift Type_Tuple2 (Type_of_Expr root)
 , Error_Expr_Lift (Error_Expr (Error_of_Type ast ty) ty ast)
                   (Error_of_Expr ast root)
 , Root_of_Expr root ~ root
 ) => ast
 -> ExprFrom ast (Expr_Tuple2 root) hs ret
fst_from ast_t ex ast ctx k =
	expr_from (Proxy::Proxy root) ast_t ctx $
	 \(ty_t::ty h_t) (Forall_Repr_with_Context t) ->
	check_type_tuple2 ex ast ty_t $ \(Type2 _ ty_a _ty_b) ->
	k ty_a $ Forall_Repr_with_Context $
	 \c -> fst (t c)

-- | Parse 'snd'.
snd_from
 :: forall root ty ast hs ret.
 ( ty ~ Type_Root_of_Expr (Expr_Tuple2 root)
 , Type0_Eq ty
 , Expr_From ast root
 , Type0_Lift   Type_Tuple2 (Type_of_Expr root)
 , Type0_Unlift Type_Tuple2 (Type_of_Expr root)
 , Error_Expr_Lift (Error_Expr (Error_of_Type ast ty) ty ast)
                   (Error_of_Expr ast root)
 , Root_of_Expr root ~ root
 ) => ast
 -> ExprFrom ast (Expr_Tuple2 root) hs ret
snd_from ast_t ex ast ctx k =
	expr_from (Proxy::Proxy root) ast_t ctx $
	 \(ty_t::ty h_t) (Forall_Repr_with_Context t) ->
	check_type_tuple2 ex ast ty_t $ \(Type2 _ _ty_a ty_b) ->
	k ty_b $ Forall_Repr_with_Context $
	 \c -> snd (t c)