{-# LANGUAGE UndecidableInstances #-}
{-# OPTIONS_GHC -fno-warn-orphans #-}
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)
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
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
instance (Sym_Either term, Sym_Lambda term) => Sym_Either (BetaT term)
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
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
]
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
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