Either.hs

{-# 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 _ (TyApp _ (TyConst _ _ q) (TyApp _ c _l))
	 | Just HRefl <- proj_ConstKiTy @_ @Either c
	 = 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 _ (TyApp _ tq@(TyConst _ _ q) (TyApp _ (TyApp _ c l) r))
	 | Just HRefl <- proj_ConstKiTy @_ @Either c
	 = 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 (TyApp _ (TyApp _ c _ty_l) r `TypesS` TypesZ)
	 | Just HRefl <- proj_ConstKi @_ @Element f
	 , Just HRefl <- proj_ConstKiTy @_ @Either c
	 = 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