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