]> Git — Sourcephile - haskell/symantic.git/blob - Language/Symantic/Expr/Maybe.hs
init
[haskell/symantic.git] / Language / Symantic / Expr / Maybe.hs
1 {-# LANGUAGE DefaultSignatures #-}
2 {-# LANGUAGE FlexibleContexts #-}
3 {-# LANGUAGE FlexibleInstances #-}
4 {-# LANGUAGE MultiParamTypeClasses #-}
5 {-# LANGUAGE ScopedTypeVariables #-}
6 {-# LANGUAGE TypeFamilies #-}
7 {-# LANGUAGE TypeOperators #-}
8 {-# OPTIONS_GHC -fno-warn-orphans #-}
9 -- | Expression for 'Maybe'.
10 module Language.Symantic.Expr.Maybe where
11
12 import Data.Proxy (Proxy(..))
13 import Data.Type.Equality ((:~:)(Refl))
14 import Prelude hiding (maybe)
15
16 import Language.Symantic.Type
17 import Language.Symantic.Trans.Common
18 import Language.Symantic.Expr.Common
19 import Language.Symantic.Expr.Lambda
20 import Language.Symantic.Expr.Functor
21 import Language.Symantic.Expr.Applicative
22
23 -- * Class 'Sym_Maybe_Lam'
24 -- | Symantic.
25 class Sym_Maybe repr where
26 nothing :: repr (Maybe a)
27 just :: repr a -> repr (Maybe a)
28
29 default nothing :: Trans t repr => t repr (Maybe a)
30 default just :: Trans t repr => t repr a -> t repr (Maybe a)
31 nothing = trans_lift nothing
32 just = trans_map1 just
33 -- | Symantic requiring a 'Lambda'.
34 class Sym_Maybe_Lam lam repr where
35 maybe
36 :: repr b
37 -> repr (Lambda lam a b)
38 -> repr (Maybe a)
39 -> repr b
40
41 default maybe
42 :: Trans t repr
43 => t repr b
44 -> t repr (Lambda lam a b)
45 -> t repr (Maybe a)
46 -> t repr b
47 maybe = trans_map3 maybe
48
49 -- * Type 'Expr_Maybe'
50 -- | Expression.
51 data Expr_Maybe (lam:: * -> *) (root:: *)
52 type instance Root_of_Expr (Expr_Maybe lam root) = root
53 type instance Type_of_Expr (Expr_Maybe lam root) = Type_Maybe
54 type instance Sym_of_Expr (Expr_Maybe lam root) repr = (Sym_Maybe repr, Sym_Maybe_Lam lam repr)
55 type instance Error_of_Expr ast (Expr_Maybe lam root) = No_Error_Expr
56
57 instance Constraint_Type1 Functor_with_Lambda (Type_Maybe root) where
58 constraint_type1 _c (Type_Type1 _ _) = Just Dict
59 instance Constraint_Type1 Applicative_with_Lambda (Type_Maybe root) where
60 constraint_type1 _c (Type_Type1 _ _) = Just Dict
61
62 -- | Parsing utility to check that the given type is a 'Type_Maybe'
63 -- or raise 'Error_Expr_Type_mismatch'.
64 check_type_maybe
65 :: forall ast ex root ty h ret.
66 ( root ~ Root_of_Expr ex
67 , ty ~ Type_Root_of_Expr ex
68 , Lift_Type Type_Maybe (Type_of_Expr root)
69 , Unlift_Type Type_Maybe (Type_of_Expr root)
70 , Lift_Error_Expr (Error_Expr (Error_of_Type ast ty) ty ast)
71 (Error_of_Expr ast root)
72 )
73 => Proxy ex -> ast -> ty h
74 -> (Type_Maybe ty h -> Either (Error_of_Expr ast root) ret)
75 -> Either (Error_of_Expr ast root) ret
76 check_type_maybe ex ast ty k =
77 case unlift_type $ unType_Root ty of
78 Just ty_l -> k ty_l
79 Nothing -> Left $
80 error_expr ex $
81 Error_Expr_Type_mismatch ast
82 (Exists_Type (type_maybe $ type_var0 SZero
83 :: Type_Root_of_Expr ex (Maybe Var0)))
84 (Exists_Type ty)
85
86 -- | Parse 'maybe'.
87 maybe_from
88 :: forall root lam ty ty_root ast hs ret.
89 ( ty ~ Type_Root_of_Expr (Expr_Maybe lam root)
90 , ty_root ~ Type_of_Expr root
91 , Eq_Type ty
92 , Expr_from ast root
93 , Lift_Type (Type_Fun lam) ty_root
94 , Unlift_Type (Type_Fun lam) ty_root
95 , Lift_Type Type_Maybe ty_root
96 , Unlift_Type Type_Maybe ty_root
97 , Lift_Error_Expr (Error_Expr (Error_of_Type ast ty) ty ast)
98 (Error_of_Expr ast root)
99 , Root_of_Expr root ~ root
100 ) => ast -> ast -> ast
101 -> Expr_From ast (Expr_Maybe lam root) hs ret
102 maybe_from ast_n ast_j ast_m ex ast ctx k =
103 expr_from (Proxy::Proxy root) ast_n ctx $
104 \(ty_n::Type_Root_of_Expr root h_n) (Forall_Repr_with_Context n) ->
105 expr_from (Proxy::Proxy root) ast_j ctx $
106 \(ty_j::Type_Root_of_Expr root h_j) (Forall_Repr_with_Context j) ->
107 expr_from (Proxy::Proxy root) ast_m ctx $
108 \(ty_m::Type_Root_of_Expr root h_m) (Forall_Repr_with_Context m) ->
109 check_type_fun ex ast ty_j $ \(Type_Type2 Proxy ty_j_a ty_j_b
110 :: Type_Fun lam (Type_Root_of_Expr root) h_j) ->
111 check_type_maybe ex ast ty_m $ \(Type_Type1 _ ty_m_a) ->
112 check_eq_type ex ast ty_n ty_j_b $ \Refl ->
113 check_eq_type ex ast ty_m_a ty_j_a $ \Refl ->
114 k ty_n $ Forall_Repr_with_Context $
115 \c -> maybe (n c) (j c) (m c)
116
117 -- | Parse 'nothing'.
118 nothing_from
119 :: forall root lam ty ty_root ast hs ret.
120 ( ty ~ Type_Root_of_Expr (Expr_Maybe lam root)
121 , ty_root ~ Type_Root_of_Expr root
122 , Type_from ast ty_root
123 , Lift_Type_Root Type_Maybe ty_root
124 , Lift_Error_Expr (Error_Expr (Error_of_Type ast ty) ty ast)
125 (Error_of_Expr ast root)
126 , Root_of_Expr root ~ root
127 ) => ast
128 -> Expr_From ast (Expr_Maybe lam root) hs ret
129 nothing_from ast_ty_a ex ast _ctx k =
130 case type_from (Proxy::Proxy ty_root)
131 ast_ty_a (Right . Exists_Type) of
132 Left err -> Left $ error_expr ex $ Error_Expr_Type err ast
133 Right (Exists_Type ty_a) ->
134 k (type_maybe ty_a) $ Forall_Repr_with_Context $
135 const nothing
136
137 -- | Parse 'just'.
138 just_from
139 :: forall root lam ty ast hs ret.
140 ( ty ~ Type_Root_of_Expr (Expr_Maybe lam root)
141 , Expr_from ast root
142 , Lift_Type_Root Type_Maybe (Type_Root_of_Expr root)
143 , Root_of_Expr root ~ root
144 ) => ast
145 -> Expr_From ast (Expr_Maybe lam root) hs ret
146 just_from ast_a _ex _ast ctx k =
147 expr_from (Proxy::Proxy root) ast_a ctx $
148 \(ty_a::Type_Root_of_Expr root h_a) (Forall_Repr_with_Context a) ->
149 k (type_maybe ty_a) $ Forall_Repr_with_Context $
150 \c -> just (a c)