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 (lam:: * -> *) (root:: *)
  33 type instance Root_of_Expr      (Expr_Either lam root)      = root
  34 type instance Type_of_Expr      (Expr_Either lam root)      = Type_Either
  35 type instance Sym_of_Expr       (Expr_Either lam root) repr = (Sym_Either repr)
  36 type instance Error_of_Expr ast (Expr_Either lam 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 Functor (Type_Either root) where
  41         constraint_type1 _c Type_Type2{} = Just Dict
  42 instance Constraint_Type1 Applicative (Type_Type1 (Proxy (Either l)) root)
  43
  44 -- | Parsing utility to check that the given type is a 'Type_Either'
  45 -- or raise 'Error_Expr_Type_mismatch'.
  46 check_type_either
  47  :: forall ast ex root ty h ret.
  48  ( root ~ Root_of_Expr ex
  49  , ty ~ Type_Root_of_Expr ex
  50  , Lift_Type   Type_Either (Type_of_Expr root)
  51  , Unlift_Type Type_Either (Type_of_Expr root)
  52  , Lift_Error_Expr (Error_Expr (Error_of_Type ast ty) ty ast)
  53                    (Error_of_Expr ast root)
  54  )
  55  => Proxy ex -> ast -> ty h
  56  -> (Type_Either ty h -> Either (Error_of_Expr ast root) ret)
  57  -> Either (Error_of_Expr ast root) ret
  58 check_type_either ex ast ty k =
  59         case unlift_type $ unType_Root ty of
  60          Just ty_e -> k ty_e
  61          Nothing -> Left $
  62                 error_expr ex $
  63                 Error_Expr_Type_mismatch ast
  64                  (Exists_Type (type_either (type_var0 SZero) (type_var0 $ SSucc SZero)
  65                  :: Type_Root_of_Expr ex (Either Var0 Var0)))
  66                  (Exists_Type ty)
  67
  68 -- | Parse 'left'.
  69 left_from
  70  :: forall root lam ty ty_root ast hs ret.
  71  ( ty ~ Type_Root_of_Expr (Expr_Either lam root)
  72  , ty_root ~ Type_Root_of_Expr root
  73  , Type_from ast ty_root
  74  , Eq_Type (Type_Root_of_Expr root)
  75  , Expr_from ast root
  76  , Lift_Type   Type_Either (Type_of_Expr root)
  77  , Unlift_Type Type_Either (Type_of_Expr root)
  78  , Lift_Error_Expr (Error_Expr (Error_of_Type ast ty) ty ast)
  79                    (Error_of_Expr ast root)
  80  , Root_of_Expr root ~ root
  81  ) => ast -> ast
  82  -> Expr_From ast (Expr_Either lam root) hs ret
  83 left_from ast_l ast_ty_r ex ast ctx k =
  84         expr_from (Proxy::Proxy root) ast_l ctx $
  85          \(ty_l::Type_Root_of_Expr root h_l) (Forall_Repr_with_Context l) ->
  86         either (\err -> Left $ error_expr ex $ Error_Expr_Type err ast) id $
  87         type_from (Proxy::Proxy ty_root) ast_ty_r $ \ty_r -> Right $
  88         k (type_either ty_l ty_r) $ Forall_Repr_with_Context $
  89                 \c -> left (l c)
  90
  91 -- | Parse 'right'.
  92 right_from
  93  :: forall root lam ty ty_root ast hs ret.
  94  ( ty ~ Type_Root_of_Expr (Expr_Either lam root)
  95  , ty_root ~ Type_Root_of_Expr root
  96  , Type_from ast ty_root
  97  , Eq_Type (Type_Root_of_Expr root)
  98  , Expr_from ast root
  99  , Lift_Type   Type_Either (Type_of_Expr root)
 100  , Unlift_Type Type_Either (Type_of_Expr root)
 101  , Lift_Error_Expr (Error_Expr (Error_of_Type ast ty) ty ast)
 102                    (Error_of_Expr ast root)
 103  , Root_of_Expr root ~ root
 104  ) => ast -> ast
 105  -> Expr_From ast (Expr_Either lam root) hs ret
 106 right_from ast_r ast_ty_l ex ast ctx k =
 107         expr_from (Proxy::Proxy root) ast_r ctx $
 108          \(ty_r::Type_Root_of_Expr root h_r) (Forall_Repr_with_Context r) ->
 109         either (\err -> Left $ error_expr ex $ Error_Expr_Type err ast) id $
 110         type_from (Proxy::Proxy ty_root) ast_ty_l $ \ty_l -> Right $
 111         k (type_either ty_l ty_r) $ Forall_Repr_with_Context $
 112                 \c -> right (r c)