Language/Symantic/Expr/Either.hs

   1 {-# LANGUAGE DefaultSignatures #-}
   2 {-# LANGUAGE FlexibleContexts #-}
   3 {-# LANGUAGE FlexibleInstances #-}
   4 {-# LANGUAGE MultiParamTypeClasses #-}
   5 {-# LANGUAGE ScopedTypeVariables #-}
   6 {-# LANGUAGE TypeFamilies #-}
   7 {-# OPTIONS_GHC -fno-warn-orphans #-}
   8 -- | Expression for 'Either'.
   9 module Language.Symantic.Expr.Either where
  10
  11 import Data.Proxy (Proxy(..))
  12 import Prelude hiding (maybe)
  13
  14 import Language.Symantic.Type
  15 import Language.Symantic.Trans.Common
  16 import Language.Symantic.Expr.Root
  17 import Language.Symantic.Expr.Error
  18 import Language.Symantic.Expr.From
  19
  20 -- * Class 'Sym_Tuple_Lam'
  21 -- | Symantic.
  22 class Sym_Either repr where
  23         left  :: repr l -> repr (Either l r)
  24         right :: repr r -> repr (Either l r)
  25         default left  :: Trans t repr => t repr l -> t repr (Either l r)
  26         default right :: Trans t repr => t repr r -> t repr (Either l r)
  27         left  = trans_map1 left
  28         right = trans_map1 right
  29
  30 -- * Type 'Expr_Either'
  31 -- | Expression.
  32 data Expr_Either (root:: *)
  33 type instance Root_of_Expr      (Expr_Either root)      = root
  34 type instance Type_of_Expr      (Expr_Either root)      = Type_Either
  35 type instance Sym_of_Expr       (Expr_Either root) repr = (Sym_Either repr)
  36 type instance Error_of_Expr ast (Expr_Either root)      = No_Error_Expr
  37
  38 instance Constraint_Type1 Functor (Type_Type1 (Proxy (Either l)) root) where
  39         constraint_type1 _c Type_Type1{} = Just Dict
  40 instance Constraint_Type1 Applicative (Type_Type1 (Proxy (Either l)) root) where
  41         constraint_type1 _c Type_Type1{} = Just Dict
  42 instance Constraint_Type1 Traversable (Type_Type1 (Proxy (Either l)) root) where
  43         constraint_type1 _c Type_Type1{} = Just Dict
  44 instance Constraint_Type1 Monad (Type_Type1 (Proxy (Either l)) root) where
  45         constraint_type1 _c Type_Type1{} = Just Dict
  46
  47 -- | Parsing utility to check that the given type is a 'Type_Either'
  48 -- or raise 'Error_Expr_Type_mismatch'.
  49 check_type_either
  50  :: forall ast ex root ty h ret.
  51  ( root ~ Root_of_Expr ex
  52  , ty ~ Type_Root_of_Expr ex
  53  , Lift_Type   Type_Either (Type_of_Expr root)
  54  , Unlift_Type Type_Either (Type_of_Expr root)
  55  , Lift_Error_Expr (Error_Expr (Error_of_Type ast ty) ty ast)
  56                    (Error_of_Expr ast root)
  57  )
  58  => Proxy ex -> ast -> ty h
  59  -> (Type_Either ty h -> Either (Error_of_Expr ast root) ret)
  60  -> Either (Error_of_Expr ast root) ret
  61 check_type_either ex ast ty k =
  62         case unlift_type $ unType_Root ty of
  63          Just ty_e -> k ty_e
  64          Nothing -> Left $
  65                 error_expr ex $
  66                 Error_Expr_Type_mismatch ast
  67                  (Exists_Type (type_either (type_var0 SZero) (type_var0 $ SSucc SZero)
  68                  :: ty (Either Var0 Var0)))
  69                  (Exists_Type ty)
  70
  71 -- | Parse 'left'.
  72 left_from
  73  :: forall root ty ast hs ret.
  74  ( ty ~ Type_Root_of_Expr (Expr_Either root)
  75  , Type_from ast ty
  76  , Eq_Type ty
  77  , Expr_from ast root
  78  , Lift_Type   Type_Either (Type_of_Expr root)
  79  , Unlift_Type Type_Either (Type_of_Expr root)
  80  , Lift_Error_Expr (Error_Expr (Error_of_Type ast ty) ty ast)
  81                    (Error_of_Expr ast root)
  82  , Root_of_Expr root ~ root
  83  ) => ast -> ast
  84  -> Expr_From ast (Expr_Either root) hs ret
  85 left_from ast_ty_r ast_l ex ast ctx k =
  86         either (\err -> Left $ error_expr ex $ Error_Expr_Type err ast) id $
  87         type_from (Proxy::Proxy ty) ast_ty_r $ \ty_r -> Right $
  88         expr_from (Proxy::Proxy root) ast_l ctx $
  89          \(ty_l::ty h_l) (Forall_Repr_with_Context l) ->
  90         k (type_either ty_l ty_r) $ Forall_Repr_with_Context $
  91                 \c -> left (l c)
  92
  93 -- | Parse 'right'.
  94 right_from
  95  :: forall root ty ast hs ret.
  96  ( ty ~ Type_Root_of_Expr (Expr_Either root)
  97  , Type_from ast ty
  98  , Eq_Type ty
  99  , Expr_from ast root
 100  , Lift_Type   Type_Either (Type_of_Expr root)
 101  , Unlift_Type Type_Either (Type_of_Expr root)
 102  , Lift_Error_Expr (Error_Expr (Error_of_Type ast ty) ty ast)
 103                    (Error_of_Expr ast root)
 104  , Root_of_Expr root ~ root
 105  ) => ast -> ast
 106  -> Expr_From ast (Expr_Either root) hs ret
 107 right_from ast_ty_l ast_r ex ast ctx k =
 108         either (\err -> Left $ error_expr ex $ Error_Expr_Type err ast) id $
 109         type_from (Proxy::Proxy ty) ast_ty_l $ \ty_l -> Right $
 110         expr_from (Proxy::Proxy root) ast_r ctx $
 111          \(ty_r::ty h_r) (Forall_Repr_with_Context r) ->
 112         k (type_either ty_l ty_r) $ Forall_Repr_with_Context $
 113                 \c -> right (r c)