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

import Control.Monad
import Data.Proxy (Proxy(..))
import Prelude hiding (maybe)

import Language.Symantic.Type
import Language.Symantic.Repr
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_Either repr where
	left  :: repr l -> repr (Either l r)
	right :: repr r -> repr (Either l r)
	default left  :: Trans t repr => t repr l -> t repr (Either l r)
	default right :: Trans t repr => t repr r -> t repr (Either l r)
	left  = trans_map1 left
	right = trans_map1 right
instance Sym_Either Repr_Host where
	right = liftM Right
	left  = liftM Left
instance Sym_Either Repr_Text where
	right = repr_text_app1 "right"
	left  = repr_text_app1 "left"
instance
 ( Sym_Either r1
 , Sym_Either r2
 ) => Sym_Either (Dup r1 r2) where
	left  (l1 `Dup` l2) = left  l1 `Dup` left  l2
	right (r1 `Dup` r2) = right r1 `Dup` right r2

-- * Type 'Expr_Either'
-- | Expression.
data Expr_Either (root:: *)
type instance Root_of_Expr      (Expr_Either root)      = root
type instance Type_of_Expr      (Expr_Either root)      = Type_Either
type instance Sym_of_Expr       (Expr_Either root) repr = (Sym_Either repr)
type instance Error_of_Expr ast (Expr_Either root)      = No_Error_Expr

-- | Parsing utility to check that the given type is a 'Type_Either'
-- or raise 'Error_Expr_Type_mismatch'.
check_type_either
 :: forall ast ex root ty h ret.
 ( root ~ Root_of_Expr ex
 , ty ~ Type_Root_of_Expr ex
 , Type0_Lift   Type_Either (Type_of_Expr root)
 , Type0_Unlift Type_Either (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_Either ty h -> Either (Error_of_Expr ast root) ret)
 -> Either (Error_of_Expr ast root) ret
check_type_either ex ast ty k =
	case type0_unlift $ unType_Root ty of
	 Just ty_e -> k ty_e
	 Nothing -> Left $
		error_expr ex $
		Error_Expr_Type_mismatch ast
		 (Exists_Type0 (type_either (type_var0 SZero) (type_var0 $ SSucc SZero)
		 :: ty (Either Var0 Var0)))
		 (Exists_Type0 ty)

-- | Parse 'left'.
left_from
 :: forall root ty ast hs ret.
 ( ty ~ Type_Root_of_Expr (Expr_Either root)
 , Type0_From ast ty
 , Type0_Eq ty
 , Expr_From ast root
 , Type0_Lift   Type_Either (Type_of_Expr root)
 , Type0_Unlift Type_Either (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_Either root) hs ret
left_from ast_ty_r ast_l ex ast ctx k =
	either (\err -> Left $ error_expr ex $ Error_Expr_Type err ast) id $
	type0_from (Proxy::Proxy ty) ast_ty_r $ \ty_r -> Right $
	expr_from (Proxy::Proxy root) ast_l ctx $
	 \(ty_l::ty h_l) (Forall_Repr_with_Context l) ->
	k (type_either ty_l ty_r) $ Forall_Repr_with_Context $
		\c -> left (l c)

-- | Parse 'right'.
right_from
 :: forall root ty ast hs ret.
 ( ty ~ Type_Root_of_Expr (Expr_Either root)
 , Type0_From ast ty
 , Type0_Eq ty
 , Expr_From ast root
 , Type0_Lift   Type_Either (Type_of_Expr root)
 , Type0_Unlift Type_Either (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_Either root) hs ret
right_from ast_ty_l ast_r ex ast ctx k =
	either (\err -> Left $ error_expr ex $ Error_Expr_Type err ast) id $
	type0_from (Proxy::Proxy ty) ast_ty_l $ \ty_l -> Right $
	expr_from (Proxy::Proxy root) ast_r ctx $
	 \(ty_r::ty h_r) (Forall_Repr_with_Context r) ->
	k (type_either ty_l ty_r) $ Forall_Repr_with_Context $
		\c -> right (r c)