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

import Prelude hiding (either)
import qualified Data.Either as Either
import qualified Data.MonoTraversable as MT

import Language.Symantic
import Language.Symantic.Lib.MonoFunctor (Element)
import Language.Symantic.Lib.Function (a0, b1, c2)

-- * Class 'Sym_Either'
type instance Sym Either = Sym_Either
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  :: Sym_Either (UnT term) => Trans term => term l -> term (Either l r)
        default _Right :: Sym_Either (UnT term) => Trans term => term r -> term (Either l r)
        default either :: Sym_Either (UnT term) => Trans term => term (l -> a) -> term (r -> a) -> term (Either l r) -> term a

        _Left  = trans1 _Left
        _Right = trans1 _Right
        either = trans3 either

-- Interpreting
instance Sym_Either Eval where
        _Right = eval1 Right
        _Left  = eval1 Left
        either = eval3 Either.either
instance Sym_Either View where
        _Right = view1 "Right"
        _Left  = view1 "Left"
        either = view3 "either"
instance (Sym_Either r1, Sym_Either r2) => Sym_Either (Dup r1 r2) where
        _Left  = dup1 @Sym_Either _Left
        _Right = dup1 @Sym_Either _Right
        either = dup3 @Sym_Either either

-- Transforming
instance (Sym_Either term, Sym_Lambda term) => Sym_Either (BetaT term)

-- Typing
instance NameTyOf Either where
        nameTyOf _c = ["Either"] `Mod` "Either"
instance FixityOf Either
instance ClassInstancesFor Either where
        proveConstraintFor _ (TyConst _ _ q :$ e:@_l)
         | Just HRefl <- proj_ConstKiTy @_ @Either e
         = case () of
                 _ | Just Refl <- proj_Const @Functor     q -> Just Dict
                   | Just Refl <- proj_Const @Applicative q -> Just Dict
                   | Just Refl <- proj_Const @Monad       q -> Just Dict
                   | Just Refl <- proj_Const @Foldable    q -> Just Dict
                   | Just Refl <- proj_Const @Traversable q -> Just Dict
                 _ -> Nothing
        proveConstraintFor _ (tq@(TyConst _ _ q) :$ e:@l:@r)
         | Just HRefl <- proj_ConstKiTy @_ @Either e
         = case () of
                 _ | Just Refl <- proj_Const @Eq q
                   , Just Dict <- proveConstraint (tq`tyApp`l)
                   , Just Dict <- proveConstraint (tq`tyApp`r) -> Just Dict
                   | Just Refl <- proj_Const @Ord q
                   , Just Dict <- proveConstraint (tq`tyApp`l)
                   , Just Dict <- proveConstraint (tq`tyApp`r) -> Just Dict
                   | Just Refl <- proj_Const @Show q
                   , Just Dict <- proveConstraint (tq`tyApp`l)
                   , Just Dict <- proveConstraint (tq`tyApp`r) -> Just Dict
                   | Just Refl <- proj_Const @MT.MonoFoldable q -> Just Dict
                   | Just Refl <- proj_Const @MT.MonoFunctor  q -> Just Dict
                 _ -> Nothing
        proveConstraintFor _c _q = Nothing
instance TypeInstancesFor Either where
        expandFamFor _c _len f (e:@_ty_l:@r `TypesS` TypesZ)
         | Just HRefl <- proj_ConstKi @_ @Element f
         , Just HRefl <- proj_ConstKiTy @_ @Either e
         = Just r
        expandFamFor _c _len _fam _as = Nothing

-- Compiling
instance Gram_Term_AtomsFor src ss g Either
instance (Source src, SymInj ss Either) => ModuleFor src ss Either where
        moduleFor = ["Either"] `moduleWhere`
         [ "Left"   := teEither_Left
         , "Right"  := teEither_Right
         , "either" := teEither_either
         ]

-- ** 'Type's
tyEither :: Source src => Type src vs l -> Type src vs r -> Type src vs (Either l r)
tyEither l r = tyConstLen @(K Either) @Either (lenVars l) `tyApp` l `tyApp` r

-- ** 'Term's
teEither_Left :: TermDef Either '[Proxy a, Proxy b] (() #> (a -> Either a b))
teEither_Left = Term noConstraint (a0 ~> tyEither a0 b1) $ teSym @Either $ lam1 _Left
teEither_Right :: TermDef Either '[Proxy a, Proxy b] (() #> (b -> Either a b))
teEither_Right = Term noConstraint (b1 ~> tyEither a0 b1) $ teSym @Either $ lam1 _Right
teEither_either :: TermDef Either '[Proxy a, Proxy b, Proxy c] (() #> ((a -> c) -> (b -> c) -> Either a b -> c))
teEither_either = Term noConstraint ((a0 ~> c2) ~> (b1 ~> c2) ~> tyEither a0 b1 ~> c2) $ teSym @Either $ lam3 either