{-# LANGUAGE UndecidableInstances #-} {-# OPTIONS_GHC -fno-warn-orphans #-} {-# OPTIONS_GHC -fconstraint-solver-iterations=8 #-} -- | Symantic for 'Either'. module Language.Symantic.Compiling.Either where import Control.Monad (liftM, liftM3) import qualified Data.Either as Either import Data.Proxy import Data.Text (Text) import Data.Type.Equality ((:~:)(Refl)) import Prelude hiding (either) import Language.Symantic.Parsing 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 Show , 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 (Proxy @Sym_Either) _Left _Right = dupI1 (Proxy @Sym_Either) _Right either = dupI3 (Proxy @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) = 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) = 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 | Just Refl <- proj_const q (Proxy::Proxy Show) , Just Con <- proj_con (t :$ l) , Just Con <- proj_con (t :$ r) -> Just Con _ -> Nothing proj_conC _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 ( Const_from Name_LamVar (Consts_of_Ifaces is) , Inj_Const (Consts_of_Ifaces is) Either , Inj_Const (Consts_of_Ifaces is) (->) -- , Proj_Token is Token_Type , Compile is ) => CompileI 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 (Consts_of_Ifaces is) 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 (Consts_of_Ifaces is) 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_type2 (ty @(->)) (At (Just tok_l2a) ty_l2a) $ \Refl ty_l2a_l ty_l2a_a -> check_type2 (ty @(->)) (At (Just tok_r2a) ty_r2a) $ \Refl ty_r2a_r ty_r2a_a -> check_type (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)