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

import Data.Proxy (Proxy(..))
import Prelude hiding (maybe, fst, snd)

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

-- * 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

-- * 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)