]> Git — Sourcephile - haskell/symantic.git/blob - Language/Symantic/Expr/List.hs
factorizing Type1_From ast Type0
[haskell/symantic.git] / Language / Symantic / Expr / List.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 'List'.
11 module Language.Symantic.Expr.List where
12
13 import Control.Monad
14 import qualified Data.Function as Fun
15 import qualified Data.List as List
16 import Data.Monoid
17 import Data.Proxy (Proxy(..))
18 import qualified Data.Text as Text
19 import Data.Type.Equality ((:~:)(Refl))
20
21 import Language.Symantic.Type
22 import Language.Symantic.Repr
23 import Language.Symantic.Expr.Root
24 import Language.Symantic.Expr.Error
25 import Language.Symantic.Expr.From
26 import Language.Symantic.Expr.Lambda
27 import Language.Symantic.Trans.Common
28
29 -- * Class 'Sym_List_Lam'
30 -- | Symantic.
31 class Sym_List repr where
32 list_empty :: repr [a]
33 list_cons :: repr a -> repr [a] -> repr [a]
34 list :: [repr a] -> repr [a]
35 list_filter :: repr (a -> Bool) -> repr [a] -> repr [a]
36 list_zipWith :: repr (a -> b -> c) -> repr [a] -> repr [b] -> repr [c]
37 list_reverse :: repr [a] -> repr [a]
38
39 default list_empty :: Trans t repr => t repr [a]
40 default list_cons :: Trans t repr => t repr a -> t repr [a] -> t repr [a]
41 default list :: Trans t repr => [t repr a] -> t repr [a]
42 default list_filter :: Trans t repr => t repr (a -> Bool) -> t repr [a] -> t repr [a]
43 default list_zipWith :: Trans t repr => t repr (a -> b -> c) -> t repr [a] -> t repr [b] -> t repr [c]
44 default list_reverse :: Trans t repr => t repr [a] -> t repr [a]
45
46 list_empty = trans_lift list_empty
47 list_cons = trans_map2 list_cons
48 list l = trans_lift (list (trans_apply Prelude.<$> l))
49 list_filter = trans_map2 list_filter
50 list_zipWith = trans_map3 list_zipWith
51 list_reverse = trans_map1 list_reverse
52 instance Sym_List Repr_Host where
53 list_empty = return []
54 list_cons = liftM2 (:)
55 list = sequence
56 list_filter = liftM2 List.filter
57 list_zipWith = liftM3 List.zipWith
58 list_reverse = liftM List.reverse
59 instance Sym_List Repr_Text where
60 list_empty = Repr_Text $ \_p _v -> "[]"
61 list_cons (Repr_Text x) (Repr_Text xs) =
62 Repr_Text $ \p v ->
63 let p' = Precedence 5 in
64 paren p p' $ x p' v <> ":" <> xs p' v
65 list l = Repr_Text $ \_p v ->
66 let p' = precedence_Toplevel in
67 "[" <> Text.intercalate ", " ((\(Repr_Text a) -> a p' v) Prelude.<$> l) <> "]"
68 list_filter = repr_text_app2 "list_filter"
69 list_zipWith = repr_text_app3 "list_zipWith"
70 list_reverse = repr_text_app1 "list_reverse"
71 instance (Sym_List r1, Sym_List r2) => Sym_List (Repr_Dup r1 r2) where
72 list_empty = repr_dup0 sym_List list_empty
73 list_cons = repr_dup2 sym_List list_cons
74 list l =
75 let (l1, l2) =
76 foldr (\(x1 `Repr_Dup` x2) (xs1, xs2) ->
77 (x1:xs1, x2:xs2)) ([], []) l in
78 list l1 `Repr_Dup` list l2
79 list_filter = repr_dup2 sym_List list_filter
80 list_zipWith = repr_dup3 sym_List list_zipWith
81 list_reverse = repr_dup1 sym_List list_reverse
82
83 sym_List :: Proxy Sym_List
84 sym_List = Proxy
85
86 -- * Type 'Expr_List'
87 -- | Expression.
88 data Expr_List (root:: *)
89 type instance Root_of_Expr (Expr_List root) = root
90 type instance Type_of_Expr (Expr_List root) = Type_List
91 type instance Sym_of_Expr (Expr_List root) repr = Sym_List repr
92 type instance Error_of_Expr ast (Expr_List root) = No_Error_Expr
93
94 -- | Parsing utility to check that the given type is a 'Type_List'
95 -- or raise 'Error_Expr_Type_mismatch'.
96 check_type_list
97 :: forall ast ex root ty h ret.
98 ( root ~ Root_of_Expr ex
99 , ty ~ Type_Root_of_Expr ex
100 , Type0_Lift Type_List (Type_of_Expr root)
101 , Type0_Unlift Type_List (Type_of_Expr root)
102 , Error_Expr_Lift (Error_Expr (Error_of_Type ast ty) ty ast)
103 (Error_of_Expr ast root)
104 )
105 => Proxy ex -> ast -> ty h
106 -> (Type_List ty h -> Either (Error_of_Expr ast root) ret)
107 -> Either (Error_of_Expr ast root) ret
108 check_type_list ex ast ty k =
109 case type0_unlift $ unType_Root ty of
110 Just ty_l -> k ty_l
111 Nothing -> Left $ error_expr ex $
112 Error_Expr_Type_mismatch ast
113 (Exists_Type0 (type_list $ type_var0 SZero :: ty [Var0]))
114 (Exists_Type0 ty)
115
116 -- | Parse 'list_empty'.
117 list_empty_from
118 :: forall root ty ast hs ret.
119 ( ty ~ Type_Root_of_Expr (Expr_List root)
120 , Type0_From ast ty
121 , Type0_Lift Type_List (Type_of_Expr root)
122 , Error_Expr_Lift (Error_Expr (Error_of_Type ast ty) ty ast)
123 (Error_of_Expr ast root)
124 , Root_of_Expr root ~ root
125 ) => ast
126 -> ExprFrom ast (Expr_List root) hs ret
127 list_empty_from ast_ty_a ex ast _ctx k =
128 either (\err -> Left $ error_expr ex $ Error_Expr_Type err ast) Fun.id $
129 type0_from (Proxy::Proxy ty) ast_ty_a $ \ty_a -> Right $
130 k (type_list ty_a) $ Forall_Repr_with_Context $
131 Fun.const list_empty
132
133 -- | Parse 'list_cons'.
134 list_cons_from
135 :: forall root ty ast hs ret.
136 ( ty ~ Type_Root_of_Expr (Expr_List root)
137 , Expr_From ast root
138 , Type0_Eq ty
139 , Type0_Lift Type_List (Type_of_Expr root)
140 , Type0_Unlift Type_List (Type_of_Expr root)
141 , Error_Expr_Lift (Error_Expr (Error_of_Type ast ty) ty ast)
142 (Error_of_Expr ast root)
143 , Root_of_Expr root ~ root
144 ) => ast -> ast
145 -> ExprFrom ast (Expr_List root) hs ret
146 list_cons_from ast_a ast_l ex ast ctx k =
147 expr_from (Proxy::Proxy root) ast_a ctx $
148 \(ty_a::ty h_a) (Forall_Repr_with_Context a) ->
149 expr_from (Proxy::Proxy root) ast_l ctx $
150 \(ty_l::ty h_l) (Forall_Repr_with_Context l) ->
151 check_type_list ex ast ty_l $ \(Type1 _ ty_l_a) ->
152 check_type0_eq ex ast ty_a ty_l_a $ \Refl ->
153 k (type_list ty_a) $ Forall_Repr_with_Context $
154 \c -> list_cons (a c) (l c)
155
156 -- | Parse 'list'.
157 list_from
158 :: forall root ex ty ast hs ret.
159 ( ty ~ Type_Root_of_Expr (Expr_List root)
160 , ex ~ Expr_List root
161 , Expr_From ast root
162 , Type0_Eq ty
163 , Type0_From ast ty
164 , Type0_Lift Type_List (Type_of_Expr root)
165 , Type0_Unlift Type_List (Type_of_Expr root)
166 , Error_Expr_Lift (Error_Expr (Error_of_Type ast ty) ty ast)
167 (Error_of_Expr ast root)
168 , Root_of_Expr root ~ root
169 ) => ast -> [ast]
170 -> ExprFrom ast ex hs ret
171 list_from ast_ty_a ast_as =
172 case type0_from (Proxy::Proxy ty)
173 ast_ty_a (Right . Exists_Type0) of
174 Left err -> \ex ast _ctx _k -> Left $ error_expr ex $ Error_Expr_Type err ast
175 Right (Exists_Type0 ty_a) -> go ty_a [] ast_as
176 where
177 go :: ty ty_a
178 -> [Forall_Repr_with_Context root hs ty_a]
179 -> [ast]
180 -> ExprFrom ast (Expr_List root) hs ret
181 go ty_a as [] _ex _ast _ctx k =
182 k (type_list ty_a) $ Forall_Repr_with_Context $
183 \c -> list ((\(Forall_Repr_with_Context a) -> a c) Prelude.<$> reverse as)
184 go ty_a as (ast_x:ast_xs) ex ast ctx k =
185 expr_from (Proxy::Proxy root) ast_x ctx $
186 \(ty_x::ty h_x) x ->
187 check_type0_eq ex ast ty_a ty_x $ \Refl ->
188 go ty_a (x:as) ast_xs ex ast ctx k
189
190 -- | Parse 'list_filter'.
191 list_filter_from
192 :: forall root ty ast hs ret.
193 ( ty ~ Type_Root_of_Expr (Expr_List root)
194 , Expr_From ast root
195 , Type0_Eq ty
196 , Type0_Lift Type_Bool (Type_of_Expr root)
197 , Type0_Lift Type_Fun (Type_of_Expr root)
198 , Type0_Unlift Type_Fun (Type_of_Expr root)
199 , Type0_Lift Type_List (Type_of_Expr root)
200 , Type0_Unlift Type_List (Type_of_Expr root)
201 , Error_Expr_Lift (Error_Expr (Error_of_Type ast ty) ty ast)
202 (Error_of_Expr ast root)
203 , Root_of_Expr root ~ root
204 ) => ast -> ast
205 -> ExprFrom ast (Expr_List root) hs ret
206 list_filter_from ast_f ast_l ex ast ctx k =
207 expr_from (Proxy::Proxy root) ast_f ctx $
208 \(ty_f::ty h_f) (Forall_Repr_with_Context f) ->
209 expr_from (Proxy::Proxy root) ast_l ctx $
210 \(ty_l::ty h_l) (Forall_Repr_with_Context l) ->
211 check_type_fun ex ast ty_f $ \(Type2 Proxy ty_f_a ty_f_b) ->
212 check_type0_eq ex ast type_bool ty_f_b $ \Refl ->
213 check_type_list ex ast ty_l $ \(Type1 _ ty_l_a) ->
214 check_type0_eq ex ast ty_f_a ty_l_a $ \Refl ->
215 k ty_l $ Forall_Repr_with_Context $
216 \c -> list_filter (f c) (l c)
217
218 -- | Parse 'list_zipWith'.
219 list_zipWith_from
220 :: forall root ty ast hs ret.
221 ( ty ~ Type_Root_of_Expr (Expr_List root)
222 , Expr_From ast root
223 , Type0_Eq ty
224 , Type0_Lift Type_Fun (Type_of_Expr root)
225 , Type0_Unlift Type_Fun (Type_of_Expr root)
226 , Type0_Lift Type_List (Type_of_Expr root)
227 , Type0_Unlift Type_List (Type_of_Expr root)
228 , Error_Expr_Lift (Error_Expr (Error_of_Type ast ty) ty ast)
229 (Error_of_Expr ast root)
230 , Root_of_Expr root ~ root
231 ) => ast -> ast -> ast
232 -> ExprFrom ast (Expr_List root) hs ret
233 list_zipWith_from ast_f ast_la ast_lb ex ast ctx k =
234 -- zipWith :: (a -> b -> c) -> [a] -> [b] -> [c]
235 expr_from (Proxy::Proxy root) ast_f ctx $
236 \(ty_f::ty h_f) (Forall_Repr_with_Context f) ->
237 expr_from (Proxy::Proxy root) ast_la ctx $
238 \(ty_la::ty h_la) (Forall_Repr_with_Context la) ->
239 expr_from (Proxy::Proxy root) ast_lb ctx $
240 \(ty_lb::ty h_lb) (Forall_Repr_with_Context lb) ->
241 check_type_fun ex ast ty_f $ \(Type2 Proxy ty_f_a ty_f_b2c) ->
242 check_type_fun ex ast ty_f_b2c $ \(Type2 Proxy ty_f_b ty_f_c) ->
243 check_type_list ex ast ty_la $ \(Type1 _ ty_l_a) ->
244 check_type_list ex ast ty_lb $ \(Type1 _ ty_l_b) ->
245 check_type0_eq ex ast ty_f_a ty_l_a $ \Refl ->
246 check_type0_eq ex ast ty_f_b ty_l_b $ \Refl ->
247 check_type0_eq ex ast ty_f_a ty_l_a $ \Refl ->
248 k (type_list ty_f_c) $ Forall_Repr_with_Context $
249 \c -> list_zipWith (f c) (la c) (lb c)
250
251 -- | Parse 'list_reverse'.
252 list_reverse_from
253 :: forall root ty ast hs ret.
254 ( ty ~ Type_Root_of_Expr (Expr_List root)
255 , Expr_From ast root
256 , Type0_Eq ty
257 , Type0_Lift Type_List (Type_of_Expr root)
258 , Type0_Unlift Type_List (Type_of_Expr root)
259 , Error_Expr_Lift (Error_Expr (Error_of_Type ast ty) ty ast)
260 (Error_of_Expr ast root)
261 , Root_of_Expr root ~ root
262 ) => ast
263 -> ExprFrom ast (Expr_List root) hs ret
264 list_reverse_from ast_l ex ast ctx k =
265 expr_from (Proxy::Proxy root) ast_l ctx $
266 \(ty_l::ty h_l) (Forall_Repr_with_Context l) ->
267 check_type_list ex ast ty_l $ \(Type1 _ _ty_l_a) ->
268 k ty_l $ Forall_Repr_with_Context $
269 \c -> list_reverse (l c)