]> Git — Sourcephile - haskell/symantic.git/blob - Language/Symantic/Expr/Either.hs
factorizing Type1_From ast Type0
[haskell/symantic.git] / 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 = repr_dup1 sym_Either left
40 right = repr_dup1 sym_Either right
41
42 sym_Either :: Proxy Sym_Either
43 sym_Either = Proxy
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)