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                  :: Type_Root_of_Expr ex (Either Var0 Var0)))
  69                  (Exists_Type ty)
  70
  71 -- | Parse 'left'.
  72 left_from
  73  :: forall root ty ty_root ast hs ret.
  74  ( ty ~ Type_Root_of_Expr (Expr_Either root)
  75  , ty_root ~ Type_Root_of_Expr root
  76  , Type_from ast ty_root
  77  , Eq_Type (Type_Root_of_Expr root)
  78  , Expr_from ast root
  79  , Lift_Type   Type_Either (Type_of_Expr root)
  80  , Unlift_Type Type_Either (Type_of_Expr root)
  81  , Lift_Error_Expr (Error_Expr (Error_of_Type ast ty) ty ast)
  82                    (Error_of_Expr ast root)
  83  , Root_of_Expr root ~ root
  84  ) => ast -> ast
  85  -> Expr_From ast (Expr_Either root) hs ret
  86 left_from ast_ty_r ast_l ex ast ctx k =
  87         either (\err -> Left $ error_expr ex $ Error_Expr_Type err ast) id $
  88         type_from (Proxy::Proxy ty_root) ast_ty_r $ \ty_r -> Right $
  89         expr_from (Proxy::Proxy root) ast_l ctx $
  90          \(ty_l::Type_Root_of_Expr root h_l) (Forall_Repr_with_Context l) ->
  91         k (type_either ty_l ty_r) $ Forall_Repr_with_Context $
  92                 \c -> left (l c)
  93
  94 -- | Parse 'right'.
  95 right_from
  96  :: forall root ty ty_root ast hs ret.
  97  ( ty ~ Type_Root_of_Expr (Expr_Either root)
  98  , ty_root ~ Type_Root_of_Expr root
  99  , Type_from ast ty_root
 100  , Eq_Type (Type_Root_of_Expr root)
 101  , Expr_from ast root
 102  , Lift_Type   Type_Either (Type_of_Expr root)
 103  , Unlift_Type Type_Either (Type_of_Expr root)
 104  , Lift_Error_Expr (Error_Expr (Error_of_Type ast ty) ty ast)
 105                    (Error_of_Expr ast root)
 106  , Root_of_Expr root ~ root
 107  ) => ast -> ast
 108  -> Expr_From ast (Expr_Either root) hs ret
 109 right_from ast_ty_l ast_r ex ast ctx k =
 110         either (\err -> Left $ error_expr ex $ Error_Expr_Type err ast) id $
 111         type_from (Proxy::Proxy ty_root) ast_ty_l $ \ty_l -> Right $
 112         expr_from (Proxy::Proxy root) ast_r ctx $
 113          \(ty_r::Type_Root_of_Expr root h_r) (Forall_Repr_with_Context r) ->
 114         k (type_either ty_l ty_r) $ Forall_Repr_with_Context $
 115                 \c -> right (r c)