Language/Symantic/Expr/Either.hs

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