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