{-# 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=7 #-}
-- | Symantic for 'Either'.
module Language.Symantic.Compiling.Either where

import Control.Monad (liftM, liftM3)
import qualified Data.Either as Either
import qualified Data.Function as Fun
import Data.Proxy
import Data.String (IsString)
import Data.Text (Text)
import Data.Type.Equality ((:~:)(Refl))
import Prelude hiding (either)

import Language.Symantic.Typing
import Language.Symantic.Compiling.Term
import Language.Symantic.Interpreting
import Language.Symantic.Transforming.Trans

-- * Class 'Sym_Tuple'
class Sym_Either term where
	_Left  :: term l -> term (Either l r)
	_Right :: term r -> term (Either l r)
	either :: term (l -> a) -> term (r -> a) -> term (Either l r) -> term a
	default _Left  :: Trans t term => t term l -> t term (Either l r)
	default _Right :: Trans t term => t term r -> t term (Either l r)
	default either :: Trans t term => t term (l -> a) -> t term (r -> a) -> t term (Either l r) -> t term a
	_Left  = trans_map1 _Left
	_Right = trans_map1 _Right
	either = trans_map3 either

type instance Sym_of_Iface (Proxy Either) = Sym_Either
type instance Consts_of_Iface (Proxy Either) = Proxy Either ': Consts_imported_by Either
type instance Consts_imported_by Either =
 [ Proxy (->)
 , Proxy Applicative
 , Proxy Eq
 , Proxy Foldable
 , Proxy Functor
 , Proxy Monad
 , Proxy Ord
 , Proxy Traversable
 ]

instance Sym_Either HostI where
	_Right = liftM Right
	_Left  = liftM Left
	either = liftM3 Either.either
instance Sym_Either TextI where
	_Right = textI_app1 "Right"
	_Left  = textI_app1 "Left"
	either = textI_app3 "either"
instance (Sym_Either r1, Sym_Either r2) => Sym_Either (DupI r1 r2) where
	_Left  = dupI1 sym_Either _Left
	_Right = dupI1 sym_Either _Right
	either = dupI3 sym_Either either

instance Const_from Text cs => Const_from Text (Proxy Either ': cs) where
	const_from "Either" k = k (ConstZ kind)
	const_from s k = const_from s $ k . ConstS
instance Show_Const cs => Show_Const (Proxy Either ': cs) where
	show_const ConstZ{} = "Either"
	show_const (ConstS c) = show_const c
instance -- Proj_ConC
 ( Proj_Const cs Either
 , Proj_Consts cs (Consts_imported_by Either)
 , Proj_Con cs
 ) => Proj_ConC cs (Proxy Either) where
	proj_conC _ (TyConst q :$ (TyConst c :$ _l))
	 | Just Refl <- eq_skind (kind_of_const c) (SKiType `SKiArrow` SKiType `SKiArrow` SKiType)
	 , Just Refl <- proj_const c (Proxy::Proxy Either)
	 = Just $ case () of
		 _ | Just Refl <- proj_const q (Proxy::Proxy Functor)     -> Just Con
		   | Just Refl <- proj_const q (Proxy::Proxy Applicative) -> Just Con
		   | Just Refl <- proj_const q (Proxy::Proxy Monad)       -> Just Con
		   | Just Refl <- proj_const q (Proxy::Proxy Foldable)    -> Just Con
		   | Just Refl <- proj_const q (Proxy::Proxy Traversable) -> Just Con
		 _ -> Nothing
	proj_conC _ (t@(TyConst q) :$ (TyConst c :$ l :$ r))
	 | Just Refl <- eq_skind (kind_of_const c) (SKiType `SKiArrow` SKiType `SKiArrow` SKiType)
	 , Just Refl <- proj_const c (Proxy::Proxy Either)
	 = Just $ case () of
		 _ | Just Refl <- proj_const q (Proxy::Proxy Eq)
		   , Just Con  <- proj_con (t :$ l)
		   , Just Con  <- proj_con (t :$ r) -> Just Con
		   | Just Refl <- proj_const q (Proxy::Proxy Ord)
		   , Just Con  <- proj_con (t :$ l)
		   , Just Con  <- proj_con (t :$ r) -> Just Con
		 _ -> Nothing
	proj_conC _c _q = Nothing
instance -- Term_fromI
 ( AST ast
 , Lexem ast ~ LamVarName
 , Const_from (Lexem ast) (Consts_of_Ifaces is)
 , Inj_Const (Consts_of_Ifaces is) Either
 , Inj_Const (Consts_of_Ifaces is) (->)
 , Term_from is ast
 ) => Term_fromI is (Proxy Either) ast where
	term_fromI ast ctx k =
		case ast_lexem ast of
		 "Left"   -> left_from
		 "Right"  -> right_from
		 "either" -> either_from
		 _ -> Left $ Error_Term_unsupported
		where
		left_from =
		 -- Left :: l -> Either l r
			from_ast2 ast $ \ast_ty_r ast_l ->
			Either.either (Left . Error_Term_Typing . At (Just ast)) Fun.id $
			type_from ast_ty_r $ \ty_r -> Right $
			check_kind ast SKiType (At (Just ast_ty_r) ty_r) $ \Refl ->
			term_from ast_l ctx $ \ty_l (TermLC l) ->
			k ((tyEither :$ ty_l) :$ ty_r) $ TermLC $
			 \c -> _Left (l c)
		right_from =
		 -- Right :: r -> Either l r
			from_ast2 ast $ \ast_ty_l ast_r ->
			Either.either (Left . Error_Term_Typing . At (Just ast)) Fun.id $
			type_from ast_ty_l $ \ty_l -> Right $
			check_kind ast SKiType (At (Just ast_ty_l) ty_l) $ \Refl ->
			term_from ast_r ctx $ \ty_r (TermLC r) ->
			k ((tyEither :$ ty_l) :$ ty_r) $ TermLC $
			 \c -> _Right (r c)
		either_from =
		 -- either :: (l -> a) -> (r -> a) -> Either l r -> a
			case ast_nodes ast of
			 [] -> Left $ Error_Term_Syntax $
				Error_Syntax_more_arguments_needed $ At (Just ast) 2
			 [ast_l2a, ast_r2a] ->
				term_from ast_l2a ctx $ \ty_l2a (TermLC l2a) ->
				term_from ast_r2a ctx $ \ty_r2a (TermLC r2a) ->
				check_type2 tyFun ast_l2a ty_l2a $ \Refl ty_l2a_l ty_l2a_a ->
				check_type2 tyFun ast_r2a ty_r2a $ \Refl ty_r2a_r ty_r2a_a ->
				check_type (At (Just ast_l2a) ty_l2a_a) (At (Just ast_r2a) ty_r2a_a) $ \Refl ->
				k ((tyEither :$ ty_l2a_l) :$ ty_r2a_r ~> ty_l2a_a) $ TermLC $
				 \c -> lam $ either (l2a c) (r2a c)
			 [ast_l2a, ast_r2a, ast_e] ->
				term_from ast_l2a ctx $ \ty_l2a (TermLC l2a) ->
				term_from ast_r2a ctx $ \ty_r2a (TermLC r2a) ->
				term_from ast_e   ctx $ \ty_e   (TermLC e) ->
				check_type2 tyFun ast_l2a ty_l2a $ \Refl ty_l2a_l ty_l2a_a ->
				check_type2 tyFun ast_r2a ty_r2a $ \Refl ty_r2a_r ty_r2a_a ->
				check_type (At (Just ast_l2a) ty_l2a_a) (At (Just ast_r2a) ty_r2a_a) $ \Refl ->
				check_type2 tyEither ast_e ty_e $ \Refl ty_e_l ty_e_r ->
				check_type (At (Just ast_l2a) ty_l2a_l) (At (Just ast_e) ty_e_l) $ \Refl ->
				check_type (At (Just ast_r2a) ty_r2a_r) (At (Just ast_e) ty_e_r) $ \Refl ->
				k ty_l2a_a $ TermLC $
				 \c -> either (l2a c) (r2a c) (e c)
			 _ -> Left $ Error_Term_Syntax $
				Error_Syntax_too_many_arguments $ At (Just ast) 3

-- | The 'Either' 'Type'
tyEither :: Inj_Const cs Either => Type cs Either
tyEither = TyConst inj_const

sym_Either :: Proxy Sym_Either
sym_Either = Proxy

syEither :: IsString a => [Syntax a] -> Syntax a
syEither = Syntax "Either"