{-# 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 (Dup r1 r2) where
	tuple2 (a1 `Dup` a2) (b1 `Dup` b2) =
		tuple2 a1 b1 `Dup` tuple2 a2 b2
	fst (t1 `Dup` t2) = fst t1 `Dup` fst t2
	snd (t1 `Dup` t2) = snd t1 `Dup` snd t2

-- * 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
 , Lift_Type   Type_Tuple2 (Type_of_Expr root)
 , Unlift_Type Type_Tuple2 (Type_of_Expr root)
 , Lift_Error_Expr (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 unlift_type $ unType_Root ty of
	 Just ty_t -> k ty_t
	 Nothing -> Left $
		error_expr ex $
		Error_Expr_Type_mismatch ast
		 (Exists_Type (type_tuple2 (type_var0 SZero) (type_var0 $ SSucc SZero)
		 :: ty (Var0, Var0)))
		 (Exists_Type ty)

-- | Parse 'tuple2'.
tuple2_from
 :: forall root ty ast hs ret.
 ( ty ~ Type_Root_of_Expr (Expr_Tuple2 root)
 , Eq_Type ty
 , Expr_from ast root
 , Lift_Type   Type_Tuple2 (Type_of_Expr root)
 , Unlift_Type Type_Tuple2 (Type_of_Expr root)
 , Lift_Error_Expr (Error_Expr (Error_of_Type ast ty) ty ast)
                   (Error_of_Expr ast root)
 , Root_of_Expr root ~ root
 ) => ast -> ast
 -> Expr_From 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)
 , Eq_Type ty
 , Expr_from ast root
 , Lift_Type   Type_Tuple2 (Type_of_Expr root)
 , Unlift_Type Type_Tuple2 (Type_of_Expr root)
 , Lift_Error_Expr (Error_Expr (Error_of_Type ast ty) ty ast)
                   (Error_of_Expr ast root)
 , Root_of_Expr root ~ root
 ) => ast
 -> Expr_From 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 $ \(Type_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)
 , Eq_Type ty
 , Expr_from ast root
 , Lift_Type   Type_Tuple2 (Type_of_Expr root)
 , Unlift_Type Type_Tuple2 (Type_of_Expr root)
 , Lift_Error_Expr (Error_Expr (Error_of_Type ast ty) ty ast)
                   (Error_of_Expr ast root)
 , Root_of_Expr root ~ root
 ) => ast
 -> Expr_From 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 $ \(Type_Type2 _ _ty_a ty_b) ->
	k ty_b $ Forall_Repr_with_Context $
	 \c -> snd (t c)