]> Git — Sourcephile - haskell/symantic.git/blob - Language/Symantic/Expr/List.hs
explore parsing of partially applied functions
[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 = list_empty `Repr_Dup` list_empty
73 list_cons (a1 `Repr_Dup` a2) (l1 `Repr_Dup` l2) = list_cons a1 l1 `Repr_Dup` list_cons a2 l2
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 (f1 `Repr_Dup` f2) (l1 `Repr_Dup` l2) =
80 list_filter f1 l1 `Repr_Dup` list_filter f2 l2
81 list_zipWith (f1 `Repr_Dup` f2) (la1 `Repr_Dup` la2) (lb1 `Repr_Dup` lb2) =
82 list_zipWith f1 la1 lb1 `Repr_Dup` list_zipWith f2 la2 lb2
83 list_reverse (l1 `Repr_Dup` l2) =
84 list_reverse l1 `Repr_Dup` list_reverse l2
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 $
112 error_expr ex $
113 Error_Expr_Type_mismatch ast
114 (Exists_Type0 (type_list $ type_var0 SZero
115 :: ty [Var0]))
116 (Exists_Type0 ty)
117
118 -- | Parse 'list_empty'.
119 list_empty_from
120 :: forall root ty ast hs ret.
121 ( ty ~ Type_Root_of_Expr (Expr_List root)
122 , Type0_From ast ty
123 , Type0_Lift Type_List (Type_of_Expr root)
124 , Error_Expr_Lift (Error_Expr (Error_of_Type ast ty) ty ast)
125 (Error_of_Expr ast root)
126 , Root_of_Expr root ~ root
127 ) => ast
128 -> ExprFrom ast (Expr_List root) hs ret
129 list_empty_from ast_ty_a ex ast _ctx k =
130 either (\err -> Left $ error_expr ex $ Error_Expr_Type err ast) Fun.id $
131 type0_from (Proxy::Proxy ty) ast_ty_a $ \ty_a -> Right $
132 k (type_list ty_a) $ Forall_Repr_with_Context $
133 Fun.const list_empty
134
135 -- | Parse 'list_cons'.
136 list_cons_from
137 :: forall root ty ast hs ret.
138 ( ty ~ Type_Root_of_Expr (Expr_List root)
139 , Expr_From ast root
140 , Type0_Eq ty
141 , Type0_Lift Type_List (Type_of_Expr root)
142 , Type0_Unlift Type_List (Type_of_Expr root)
143 , Error_Expr_Lift (Error_Expr (Error_of_Type ast ty) ty ast)
144 (Error_of_Expr ast root)
145 , Root_of_Expr root ~ root
146 ) => ast -> ast
147 -> ExprFrom ast (Expr_List root) hs ret
148 list_cons_from ast_a ast_l ex ast ctx k =
149 expr_from (Proxy::Proxy root) ast_a ctx $
150 \(ty_a::ty h_a) (Forall_Repr_with_Context a) ->
151 expr_from (Proxy::Proxy root) ast_l ctx $
152 \(ty_l::ty h_l) (Forall_Repr_with_Context l) ->
153 check_type_list ex ast ty_l $ \(Type1 _ ty_l_a) ->
154 check_type0_eq ex ast ty_a ty_l_a $ \Refl ->
155 k (type_list ty_a) $ Forall_Repr_with_Context $
156 \c -> list_cons (a c) (l c)
157
158 -- | Parse 'list'.
159 list_from
160 :: forall root ex ty ast hs ret.
161 ( ty ~ Type_Root_of_Expr (Expr_List root)
162 , ex ~ Expr_List root
163 , Expr_From ast root
164 , Type0_Eq ty
165 , Type0_From ast ty
166 , Type0_Lift Type_List (Type_of_Expr root)
167 , Type0_Unlift Type_List (Type_of_Expr root)
168 , Error_Expr_Lift (Error_Expr (Error_of_Type ast ty) ty ast)
169 (Error_of_Expr ast root)
170 , Root_of_Expr root ~ root
171 ) => ast -> [ast]
172 -> ExprFrom ast ex hs ret
173 list_from ast_ty_a ast_as =
174 case type0_from (Proxy::Proxy ty)
175 ast_ty_a (Right . Exists_Type0) of
176 Left err -> \ex ast _ctx _k -> Left $ error_expr ex $ Error_Expr_Type err ast
177 Right (Exists_Type0 ty_a) -> go ty_a [] ast_as
178 where
179 go :: ty ty_a
180 -> [Forall_Repr_with_Context root hs ty_a]
181 -> [ast]
182 -> ExprFrom ast (Expr_List root) hs ret
183 go ty_a as [] _ex _ast _ctx k =
184 k (type_list ty_a) $ Forall_Repr_with_Context $
185 \c -> list ((\(Forall_Repr_with_Context a) -> a c) Prelude.<$> reverse as)
186 go ty_a as (ast_x:ast_xs) ex ast ctx k =
187 expr_from (Proxy::Proxy root) ast_x ctx $
188 \(ty_x::ty h_x) x ->
189 check_type0_eq ex ast ty_a ty_x $ \Refl ->
190 go ty_a (x:as) ast_xs ex ast ctx k
191
192 -- | Parse 'list_filter'.
193 list_filter_from
194 :: forall root ty ast hs ret.
195 ( ty ~ Type_Root_of_Expr (Expr_List root)
196 , Expr_From ast root
197 , Type0_Eq ty
198 , Type0_Lift Type_Bool (Type_of_Expr root)
199 , Type0_Lift Type_Fun (Type_of_Expr root)
200 , Type0_Unlift Type_Fun (Type_of_Expr root)
201 , Type0_Lift Type_List (Type_of_Expr root)
202 , Type0_Unlift Type_List (Type_of_Expr root)
203 , Error_Expr_Lift (Error_Expr (Error_of_Type ast ty) ty ast)
204 (Error_of_Expr ast root)
205 , Root_of_Expr root ~ root
206 ) => ast -> ast
207 -> ExprFrom ast (Expr_List root) hs ret
208 list_filter_from ast_f ast_l ex ast ctx k =
209 expr_from (Proxy::Proxy root) ast_f ctx $
210 \(ty_f::ty h_f) (Forall_Repr_with_Context f) ->
211 expr_from (Proxy::Proxy root) ast_l ctx $
212 \(ty_l::ty h_l) (Forall_Repr_with_Context l) ->
213 check_type_fun ex ast ty_f $ \(Type2 Proxy ty_f_a ty_f_b) ->
214 check_type0_eq ex ast type_bool ty_f_b $ \Refl ->
215 check_type_list ex ast ty_l $ \(Type1 _ ty_l_a) ->
216 check_type0_eq ex ast ty_f_a ty_l_a $ \Refl ->
217 k ty_l $ Forall_Repr_with_Context $
218 \c -> list_filter (f c) (l c)
219
220 -- | Parse 'list_zipWith'.
221 list_zipWith_from
222 :: forall root ty ast hs ret.
223 ( ty ~ Type_Root_of_Expr (Expr_List root)
224 , Expr_From ast root
225 , Type0_Eq ty
226 , Type0_Lift Type_Fun (Type_of_Expr root)
227 , Type0_Unlift Type_Fun (Type_of_Expr root)
228 , Type0_Lift Type_List (Type_of_Expr root)
229 , Type0_Unlift Type_List (Type_of_Expr root)
230 , Error_Expr_Lift (Error_Expr (Error_of_Type ast ty) ty ast)
231 (Error_of_Expr ast root)
232 , Root_of_Expr root ~ root
233 ) => ast -> ast -> ast
234 -> ExprFrom ast (Expr_List root) hs ret
235 list_zipWith_from ast_f ast_la ast_lb ex ast ctx k =
236 -- zipWith :: (a -> b -> c) -> [a] -> [b] -> [c]
237 expr_from (Proxy::Proxy root) ast_f ctx $
238 \(ty_f::ty h_f) (Forall_Repr_with_Context f) ->
239 expr_from (Proxy::Proxy root) ast_la ctx $
240 \(ty_la::ty h_la) (Forall_Repr_with_Context la) ->
241 expr_from (Proxy::Proxy root) ast_lb ctx $
242 \(ty_lb::ty h_lb) (Forall_Repr_with_Context lb) ->
243 check_type_fun ex ast ty_f $ \(Type2 Proxy ty_f_a ty_f_b2c) ->
244 check_type_fun ex ast ty_f_b2c $ \(Type2 Proxy ty_f_b ty_f_c) ->
245 check_type_list ex ast ty_la $ \(Type1 _ ty_l_a) ->
246 check_type_list ex ast ty_lb $ \(Type1 _ ty_l_b) ->
247 check_type0_eq ex ast ty_f_a ty_l_a $ \Refl ->
248 check_type0_eq ex ast ty_f_b ty_l_b $ \Refl ->
249 check_type0_eq ex ast ty_f_a ty_l_a $ \Refl ->
250 k (type_list ty_f_c) $ Forall_Repr_with_Context $
251 \c -> list_zipWith (f c) (la c) (lb c)
252
253 -- | Parse 'list_reverse'.
254 list_reverse_from
255 :: forall root ty ast hs ret.
256 ( ty ~ Type_Root_of_Expr (Expr_List root)
257 , Expr_From ast root
258 , Type0_Eq ty
259 , Type0_Lift Type_List (Type_of_Expr root)
260 , Type0_Unlift Type_List (Type_of_Expr root)
261 , Error_Expr_Lift (Error_Expr (Error_of_Type ast ty) ty ast)
262 (Error_of_Expr ast root)
263 , Root_of_Expr root ~ root
264 ) => ast
265 -> ExprFrom ast (Expr_List root) hs ret
266 list_reverse_from ast_l ex ast ctx k =
267 expr_from (Proxy::Proxy root) ast_l ctx $
268 \(ty_l::ty h_l) (Forall_Repr_with_Context l) ->
269 check_type_list ex ast ty_l $ \(Type1 _ _ty_l_a) ->
270 k ty_l $ Forall_Repr_with_Context $
271 \c -> list_reverse (l c)