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
  39  ( Sym_Either r1
  40  , Sym_Either r2
  41  ) => Sym_Either (Dup r1 r2) where
  42         left  (l1 `Dup` l2) = left  l1 `Dup` left  l2
  43         right (r1 `Dup` r2) = right r1 `Dup` right r2
  44
  45 -- * Type 'Expr_Either'
  46 -- | Expression.
  47 data Expr_Either (root:: *)
  48 type instance Root_of_Expr      (Expr_Either root)      = root
  49 type instance Type_of_Expr      (Expr_Either root)      = Type_Either
  50 type instance Sym_of_Expr       (Expr_Either root) repr = (Sym_Either repr)
  51 type instance Error_of_Expr ast (Expr_Either root)      = No_Error_Expr
  52
  53 -- | Parsing utility to check that the given type is a 'Type_Either'
  54 -- or raise 'Error_Expr_Type_mismatch'.
  55 check_type_either
  56  :: forall ast ex root ty h ret.
  57  ( root ~ Root_of_Expr ex
  58  , ty ~ Type_Root_of_Expr ex
  59  , Type0_Lift   Type_Either (Type_of_Expr root)
  60  , Type0_Unlift Type_Either (Type_of_Expr root)
  61  , Error_Expr_Lift (Error_Expr (Error_of_Type ast ty) ty ast)
  62                    (Error_of_Expr ast root)
  63  )
  64  => Proxy ex -> ast -> ty h
  65  -> (Type_Either ty h -> Either (Error_of_Expr ast root) ret)
  66  -> Either (Error_of_Expr ast root) ret
  67 check_type_either ex ast ty k =
  68         case type0_unlift $ unType_Root ty of
  69          Just ty_e -> k ty_e
  70          Nothing -> Left $
  71                 error_expr ex $
  72                 Error_Expr_Type_mismatch ast
  73                  (Exists_Type0 (type_either (type_var0 SZero) (type_var0 $ SSucc SZero)
  74                  :: ty (Either Var0 Var0)))
  75                  (Exists_Type0 ty)
  76
  77 -- | Parse 'left'.
  78 left_from
  79  :: forall root ty ast hs ret.
  80  ( ty ~ Type_Root_of_Expr (Expr_Either root)
  81  , Type0_From ast ty
  82  , Type0_Eq ty
  83  , Expr_From ast root
  84  , Type0_Lift   Type_Either (Type_of_Expr root)
  85  , Type0_Unlift Type_Either (Type_of_Expr root)
  86  , Error_Expr_Lift (Error_Expr (Error_of_Type ast ty) ty ast)
  87                    (Error_of_Expr ast root)
  88  , Root_of_Expr root ~ root
  89  ) => ast -> ast
  90  -> ExprFrom ast (Expr_Either root) hs ret
  91 left_from ast_ty_r ast_l ex ast ctx k =
  92         either (\err -> Left $ error_expr ex $ Error_Expr_Type err ast) id $
  93         type0_from (Proxy::Proxy ty) ast_ty_r $ \ty_r -> Right $
  94         expr_from (Proxy::Proxy root) ast_l ctx $
  95          \(ty_l::ty h_l) (Forall_Repr_with_Context l) ->
  96         k (type_either ty_l ty_r) $ Forall_Repr_with_Context $
  97                 \c -> left (l c)
  98
  99 -- | Parse 'right'.
 100 right_from
 101  :: forall root ty ast hs ret.
 102  ( ty ~ Type_Root_of_Expr (Expr_Either root)
 103  , Type0_From ast ty
 104  , Type0_Eq ty
 105  , Expr_From ast root
 106  , Type0_Lift   Type_Either (Type_of_Expr root)
 107  , Type0_Unlift Type_Either (Type_of_Expr root)
 108  , Error_Expr_Lift (Error_Expr (Error_of_Type ast ty) ty ast)
 109                    (Error_of_Expr ast root)
 110  , Root_of_Expr root ~ root
 111  ) => ast -> ast
 112  -> ExprFrom ast (Expr_Either root) hs ret
 113 right_from ast_ty_l ast_r ex ast ctx k =
 114         either (\err -> Left $ error_expr ex $ Error_Expr_Type err ast) id $
 115         type0_from (Proxy::Proxy ty) ast_ty_l $ \ty_l -> Right $
 116         expr_from (Proxy::Proxy root) ast_r ctx $
 117          \(ty_r::ty h_r) (Forall_Repr_with_Context r) ->
 118         k (type_either ty_l ty_r) $ Forall_Repr_with_Context $
 119                 \c -> right (r c)