{-# LANGUAGE DefaultSignatures #-} {-# LANGUAGE FlexibleContexts #-} {-# LANGUAGE FlexibleInstances #-} {-# LANGUAGE MultiParamTypeClasses #-} {-# LANGUAGE OverloadedStrings #-} {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE TypeFamilies #-} {-# OPTIONS_GHC -fno-warn-orphans #-} -- | Expression for 'Either'. module Language.Symantic.Expr.Either where import Control.Monad import Data.Proxy (Proxy(..)) import Prelude hiding (maybe) import Language.Symantic.Type import Language.Symantic.Repr import Language.Symantic.Trans.Common import Language.Symantic.Expr.Root import Language.Symantic.Expr.Error import Language.Symantic.Expr.From -- * Class 'Sym_Tuple_Lam' -- | Symantic. class Sym_Either repr where left :: repr l -> repr (Either l r) right :: repr r -> repr (Either l r) default left :: Trans t repr => t repr l -> t repr (Either l r) default right :: Trans t repr => t repr r -> t repr (Either l r) left = trans_map1 left right = trans_map1 right instance Sym_Either Repr_Host where right = liftM Right left = liftM Left instance Sym_Either Repr_Text where right = repr_text_app1 "right" left = repr_text_app1 "left" instance ( Sym_Either r1 , Sym_Either r2 ) => Sym_Either (Dup r1 r2) where left (l1 `Dup` l2) = left l1 `Dup` left l2 right (r1 `Dup` r2) = right r1 `Dup` right r2 -- * Type 'Expr_Either' -- | Expression. data Expr_Either (root:: *) type instance Root_of_Expr (Expr_Either root) = root type instance Type_of_Expr (Expr_Either root) = Type_Either type instance Sym_of_Expr (Expr_Either root) repr = (Sym_Either repr) type instance Error_of_Expr ast (Expr_Either root) = No_Error_Expr -- | Parsing utility to check that the given type is a 'Type_Either' -- or raise 'Error_Expr_Type_mismatch'. check_type_either :: forall ast ex root ty h ret. ( root ~ Root_of_Expr ex , ty ~ Type_Root_of_Expr ex , Type0_Lift Type_Either (Type_of_Expr root) , Type0_Unlift Type_Either (Type_of_Expr root) , Error_Expr_Lift (Error_Expr (Error_of_Type ast ty) ty ast) (Error_of_Expr ast root) ) => Proxy ex -> ast -> ty h -> (Type_Either ty h -> Either (Error_of_Expr ast root) ret) -> Either (Error_of_Expr ast root) ret check_type_either ex ast ty k = case type0_unlift $ unType_Root ty of Just ty_e -> k ty_e Nothing -> Left $ error_expr ex $ Error_Expr_Type_mismatch ast (Exists_Type0 (type_either (type_var0 SZero) (type_var0 $ SSucc SZero) :: ty (Either Var0 Var0))) (Exists_Type0 ty) -- | Parse 'left'. left_from :: forall root ty ast hs ret. ( ty ~ Type_Root_of_Expr (Expr_Either root) , Type0_From ast ty , Type0_Eq ty , Expr_From ast root , Type0_Lift Type_Either (Type_of_Expr root) , Type0_Unlift Type_Either (Type_of_Expr root) , Error_Expr_Lift (Error_Expr (Error_of_Type ast ty) ty ast) (Error_of_Expr ast root) , Root_of_Expr root ~ root ) => ast -> ast -> ExprFrom ast (Expr_Either root) hs ret left_from ast_ty_r ast_l ex ast ctx k = either (\err -> Left $ error_expr ex $ Error_Expr_Type err ast) id $ type0_from (Proxy::Proxy ty) ast_ty_r $ \ty_r -> Right $ expr_from (Proxy::Proxy root) ast_l ctx $ \(ty_l::ty h_l) (Forall_Repr_with_Context l) -> k (type_either ty_l ty_r) $ Forall_Repr_with_Context $ \c -> left (l c) -- | Parse 'right'. right_from :: forall root ty ast hs ret. ( ty ~ Type_Root_of_Expr (Expr_Either root) , Type0_From ast ty , Type0_Eq ty , Expr_From ast root , Type0_Lift Type_Either (Type_of_Expr root) , Type0_Unlift Type_Either (Type_of_Expr root) , Error_Expr_Lift (Error_Expr (Error_of_Type ast ty) ty ast) (Error_of_Expr ast root) , Root_of_Expr root ~ root ) => ast -> ast -> ExprFrom ast (Expr_Either root) hs ret right_from ast_ty_l ast_r ex ast ctx k = either (\err -> Left $ error_expr ex $ Error_Expr_Type err ast) id $ type0_from (Proxy::Proxy ty) ast_ty_l $ \ty_l -> Right $ expr_from (Proxy::Proxy root) ast_r ctx $ \(ty_r::ty h_r) (Forall_Repr_with_Context r) -> k (type_either ty_l ty_r) $ Forall_Repr_with_Context $ \c -> right (r c)