{-# LANGUAGE UndecidableInstances #-}
{-# OPTIONS_GHC -fno-warn-orphans #-}
{-# OPTIONS_GHC -fconstraint-solver-iterations=8 #-}
-- | Symantic for 'Either'.
module Language.Symantic.Lib.Either where

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

import Language.Symantic.Parsing
import Language.Symantic.Typing
import Language.Symantic.Compiling
import Language.Symantic.Interpreting
import Language.Symantic.Transforming
import Language.Symantic.Lib.Lambda

-- * 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 TyConsts_of_Iface (Proxy Either) = Proxy Either ': TyConsts_imported_by Either
type instance TyConsts_imported_by Either =
 [ Proxy (->)
 , Proxy Applicative
 , Proxy Eq
 , Proxy Foldable
 , Proxy Functor
 , Proxy Monad
 , Proxy Ord
 , Proxy Show
 , Proxy Traversable
 ]

instance Sym_Either HostI where
	_Right = liftM Right
	_Left  = liftM Left
	either = liftM3 Either.either
instance Sym_Either TextI where
	_Right = textI1 "Right"
	_Left  = textI1 "Left"
	either = textI3 "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
 ( Read_TyNameR TyName cs rs
 , Inj_TyConst cs Either
 ) => Read_TyNameR TyName cs (Proxy Either ': rs) where
	read_TyNameR _cs (TyName "Either") k = k (ty @Either)
	read_TyNameR _rs raw k = read_TyNameR (Proxy @rs) raw k
instance Show_TyConst cs => Show_TyConst (Proxy Either ': cs) where
	show_TyConst TyConstZ{} = "Either"
	show_TyConst (TyConstS c) = show_TyConst c
instance -- Proj_TyConC
 ( Proj_TyConst cs Either
 , Proj_TyConsts cs (TyConsts_imported_by Either)
 , Proj_TyCon cs
 ) => Proj_TyConC cs (Proxy Either) where
	proj_TyConC _ (TyConst q :$ (TyConst c :$ _l))
	 | Just Refl <- eq_skind (kind_of_TyConst c) (SKiType `SKiArrow` SKiType `SKiArrow` SKiType)
	 , Just Refl <- proj_TyConst c (Proxy @Either)
	 = case () of
		 _ | Just Refl <- proj_TyConst q (Proxy @Functor)     -> Just TyCon
		   | Just Refl <- proj_TyConst q (Proxy @Applicative) -> Just TyCon
		   | Just Refl <- proj_TyConst q (Proxy @Monad)       -> Just TyCon
		   | Just Refl <- proj_TyConst q (Proxy @Foldable)    -> Just TyCon
		   | Just Refl <- proj_TyConst q (Proxy @Traversable) -> Just TyCon
		 _ -> Nothing
	proj_TyConC _ (t@(TyConst q) :$ (TyConst c :$ l :$ r))
	 | Just Refl <- eq_skind (kind_of_TyConst c) (SKiType `SKiArrow` SKiType `SKiArrow` SKiType)
	 , Just Refl <- proj_TyConst c (Proxy @Either)
	 = case () of
		 _ | Just Refl <- proj_TyConst q (Proxy @Eq)
		   , Just TyCon  <- proj_TyCon (t :$ l)
		   , Just TyCon  <- proj_TyCon (t :$ r) -> Just TyCon
		   | Just Refl <- proj_TyConst q (Proxy @Ord)
		   , Just TyCon  <- proj_TyCon (t :$ l)
		   , Just TyCon  <- proj_TyCon (t :$ r) -> Just TyCon
		   | Just Refl <- proj_TyConst q (Proxy @Show)
		   , Just TyCon  <- proj_TyCon (t :$ l)
		   , Just TyCon  <- proj_TyCon (t :$ r) -> Just TyCon
		 _ -> Nothing
	proj_TyConC _c _q = Nothing
data instance TokenT meta (ts::[*]) (Proxy Either)
 = Token_Term_Either_Left   (EToken meta '[Proxy Token_Type]) (EToken meta ts)
 | Token_Term_Either_Right  (EToken meta '[Proxy Token_Type]) (EToken meta ts)
 | Token_Term_Either_either (EToken meta ts) (EToken meta ts)
deriving instance (Eq meta, Eq_Token meta ts) => Eq (TokenT meta ts (Proxy Either))
deriving instance (Show meta, Show_Token meta ts) => Show (TokenT meta ts (Proxy Either))
instance -- CompileI
 ( Read_TyName TyName cs
 , Inj_TyConst        cs Either
 , Inj_TyConst        cs (->)
 -- , Proj_Token is Token_Type
 , Compile cs is
 ) => CompileI cs is (Proxy Either) where
	compileI tok ctx k =
		case tok of
		 Token_Term_Either_Left tok_ty_r tok_l ->
			-- Left :: l -> Either l r
			compile_Type tok_ty_r $ \(ty_r::Type cs r) ->
			check_Kind
			 (At Nothing SKiType)
			 (At (Just tok_ty_r) $ kind_of ty_r) $ \Refl ->
			compileO tok_l ctx $ \ty_l (TermO l) ->
			k ((ty @Either :$ ty_l) :$ ty_r) $ TermO $
			 \c -> _Left (l c)
		 Token_Term_Either_Right tok_ty_l tok_r ->
			-- Right :: r -> Either l r
			compile_Type tok_ty_l $ \(ty_l::Type cs l) ->
			check_Kind
			 (At Nothing SKiType)
			 (At (Just tok_ty_l) $ kind_of ty_l) $ \Refl ->
			compileO tok_r ctx $ \ty_r (TermO r) ->
			k ((ty @Either :$ ty_l) :$ ty_r) $ TermO $
			 \c -> _Right (r c)
		 Token_Term_Either_either tok_l2a tok_r2a ->
			-- either :: (l -> a) -> (r -> a) -> Either l r -> a
			compileO tok_l2a ctx $ \ty_l2a (TermO l2a) ->
			compileO tok_r2a ctx $ \ty_r2a (TermO r2a) ->
			check_TyEq2 (ty @(->)) (At (Just tok_l2a) ty_l2a) $ \Refl ty_l2a_l ty_l2a_a ->
			check_TyEq2 (ty @(->)) (At (Just tok_r2a) ty_r2a) $ \Refl ty_r2a_r ty_r2a_a ->
			check_TyEq (At (Just tok_l2a) ty_l2a_a) (At (Just tok_r2a) ty_r2a_a) $ \Refl ->
			k ((ty @Either :$ ty_l2a_l) :$ ty_r2a_r ~> ty_l2a_a) $ TermO $
			 \c -> lam $ either (l2a c) (r2a c)
instance -- TokenizeT
 Inj_Token meta ts Either =>
 TokenizeT meta ts (Proxy Either) where
	tokenizeT _t = mempty
	 { tokenizers_infix = tokenizeTMod []
		 [ (Term_Name "Left",) Term_ProTok
			 { term_protok = \meta -> ProTokLam $ \l -> ProTokPi $ \r ->
				ProTok $ inj_EToken meta $ Token_Term_Either_Left r l
			 , term_fixity = infixN5 }
		 , (Term_Name "Right",) Term_ProTok
			 { term_protok = \meta -> ProTokPi $ \l -> ProTokLam $ \r ->
				ProTok $ inj_EToken meta $ Token_Term_Either_Right l r
			 , term_fixity = infixN5 }
		 , tokenize2 "either" infixN5 Token_Term_Either_either
		 ]
	 }
instance Gram_Term_AtomsT meta ts (Proxy Either) g