]> Git — Sourcephile - haskell/symantic.git/blob - Language/Symantic/Expr/Foldable.hs
explore parsing of partially applied functions
[haskell/symantic.git] / Language / Symantic / Expr / Foldable.hs
1 {-# LANGUAGE DefaultSignatures #-}
2 {-# LANGUAGE GADTs #-}
3 {-# LANGUAGE FlexibleContexts #-}
4 {-# LANGUAGE FlexibleInstances #-}
5 {-# LANGUAGE MultiParamTypeClasses #-}
6 {-# LANGUAGE OverloadedStrings #-}
7 {-# LANGUAGE Rank2Types #-}
8 {-# LANGUAGE ScopedTypeVariables #-}
9 {-# LANGUAGE TypeFamilies #-}
10 {-# LANGUAGE TypeOperators #-}
11 {-# OPTIONS_GHC -fno-warn-orphans #-}
12 -- | Expression for 'Foldable'.
13 module Language.Symantic.Expr.Foldable where
14
15 import Control.Monad
16 import Data.Monoid
17 import Data.Foldable (Foldable)
18 import qualified Data.Foldable as Foldable
19 import Data.Proxy (Proxy(..))
20 import Data.Type.Equality ((:~:)(Refl))
21 import Prelude hiding ((<$>), Foldable(..))
22
23 import Language.Symantic.Type
24 import Language.Symantic.Repr
25 import Language.Symantic.Expr.Root
26 import Language.Symantic.Expr.Error
27 import Language.Symantic.Expr.From
28 import Language.Symantic.Expr.Lambda
29 import Language.Symantic.Trans.Common
30
31 -- * Class 'Sym_Foldable'
32 -- | Symantic.
33 class Sym_Foldable repr where
34 foldMap :: (Foldable t, Monoid m) => repr (a -> m) -> repr (t a) -> repr m
35 length :: Foldable t => repr (t a) -> repr Int
36 null :: Foldable t => repr (t a) -> repr Bool
37 minimum :: (Foldable t, Ord a) => repr (t a) -> repr a
38 maximum :: (Foldable t, Ord a) => repr (t a) -> repr a
39 elem :: (Foldable t, Eq a) => repr a -> repr (t a) -> repr Bool
40 default foldMap :: (Trans tr repr, Foldable t, Monoid m)
41 => tr repr (a -> m) -> tr repr (t a) -> tr repr m
42 default length :: (Trans tr repr, Foldable t) => tr repr (t a) -> tr repr Int
43 default null :: (Trans tr repr, Foldable t) => tr repr (t a) -> tr repr Bool
44 default minimum :: (Trans tr repr, Foldable t, Ord a) => tr repr (t a) -> tr repr a
45 default maximum :: (Trans tr repr, Foldable t, Ord a) => tr repr (t a) -> tr repr a
46 default elem :: (Trans tr repr, Foldable t, Eq a) => tr repr a -> tr repr (t a) -> tr repr Bool
47 foldMap = trans_map2 foldMap
48 length = trans_map1 length
49 null = trans_map1 null
50 minimum = trans_map1 minimum
51 maximum = trans_map1 maximum
52 elem = trans_map2 elem
53 instance Sym_Foldable Repr_Host where
54 foldMap = liftM2 Foldable.foldMap
55 null = liftM Foldable.null
56 length = liftM Foldable.length
57 minimum = liftM Foldable.minimum
58 maximum = liftM Foldable.maximum
59 elem = liftM2 Foldable.elem
60 instance Sym_Foldable Repr_Text where
61 foldMap = repr_text_app2 "foldMap"
62 null = repr_text_app1 "null"
63 length = repr_text_app1 "length"
64 minimum = repr_text_app1 "minimum"
65 maximum = repr_text_app1 "maximum"
66 elem = repr_text_app2 "elem"
67 instance
68 ( Sym_Foldable r1
69 , Sym_Foldable r2
70 ) => Sym_Foldable (Repr_Dup r1 r2) where
71 foldMap (f1 `Repr_Dup` f2) (m1 `Repr_Dup` m2) =
72 foldMap f1 m1 `Repr_Dup` foldMap f2 m2
73 length (f1 `Repr_Dup` f2) = length f1 `Repr_Dup` length f2
74 null (f1 `Repr_Dup` f2) = null f1 `Repr_Dup` null f2
75 minimum (f1 `Repr_Dup` f2) = minimum f1 `Repr_Dup` minimum f2
76 maximum (f1 `Repr_Dup` f2) = maximum f1 `Repr_Dup` maximum f2
77 elem (a1 `Repr_Dup` a2) (f1 `Repr_Dup` f2) = elem a1 f1 `Repr_Dup` elem a2 f2
78
79 -- * Type 'Expr_Foldable'
80 -- | Expression.
81 data Expr_Foldable (root:: *)
82 type instance Root_of_Expr (Expr_Foldable root) = root
83 type instance Type_of_Expr (Expr_Foldable root) = No_Type
84 type instance Sym_of_Expr (Expr_Foldable root) repr = (Sym_Foldable repr)
85 type instance Error_of_Expr ast (Expr_Foldable root) = No_Error_Expr
86
87 -- | Parse 'foldMap'.
88 foldMap_from
89 :: forall root ty ast hs ret.
90 ( ty ~ Type_Root_of_Expr (Expr_Foldable root)
91 , Expr_From ast root
92 , Type0_Eq ty
93 , Type0_Lift Type_Fun (Type_of_Expr root)
94 , Type0_Unlift Type_Fun (Type_of_Expr root)
95 , Type0_Constraint Monoid ty
96 , Type1_Constraint Foldable ty
97 , Type1_Unlift (Type_of_Expr root)
98 , Error_Expr_Lift (Error_Expr (Error_of_Type ast ty) ty ast)
99 (Error_of_Expr ast root)
100 , Root_of_Expr root ~ root
101 ) => ast -> ast
102 -> ExprFrom ast (Expr_Foldable root) hs ret
103 foldMap_from ast_f ast_ta ex ast ctx k =
104 -- foldMap :: (Foldable t, Monoid m) => (a -> m) -> t a -> m
105 expr_from (Proxy::Proxy root) ast_f ctx $
106 \(ty_f::ty h_f) (Forall_Repr_with_Context f) ->
107 expr_from (Proxy::Proxy root) ast_ta ctx $
108 \(ty_ta::ty h_ta) (Forall_Repr_with_Context ta) ->
109 check_type_fun ex ast ty_f $ \(Type2 Proxy ty_f_a ty_f_m) ->
110 check_type1 ex ast ty_ta $ \(Type1 _t (ty_t_a::ty h_t_a), Type1_Lift _ty_t) ->
111 check_type0_eq ex ast ty_f_a ty_t_a $ \Refl ->
112 check_type1_constraint ex (Proxy::Proxy Foldable) ast ty_ta $ \Dict ->
113 check_type0_constraint ex (Proxy::Proxy Monoid) ast ty_f_m $ \Dict ->
114 k ty_f_m $ Forall_Repr_with_Context $
115 \c -> foldMap (f c) (ta c)
116
117 -- | Parse 'length'.
118 length_from
119 :: forall root ty ast hs ret.
120 ( ty ~ Type_Root_of_Expr (Expr_Foldable root)
121 , Expr_From ast root
122 , Type0_Eq ty
123 , Type0_Lift Type_Int (Type_of_Expr root)
124 , Type1_Constraint Foldable ty
125 , Type1_Unlift (Type_of_Expr root)
126 , Error_Expr_Lift (Error_Expr (Error_of_Type ast ty) ty ast)
127 (Error_of_Expr ast root)
128 , Root_of_Expr root ~ root
129 ) => ast
130 -> ExprFrom ast (Expr_Foldable root) hs ret
131 length_from ast_ta ex ast ctx k =
132 -- length :: Foldable t => t a -> Int
133 expr_from (Proxy::Proxy root) ast_ta ctx $
134 \(ty_ta::ty h_ta) (Forall_Repr_with_Context ta) ->
135 check_type1 ex ast ty_ta $ \(Type1{}, _) ->
136 check_type1_constraint ex (Proxy::Proxy Foldable) ast ty_ta $ \Dict ->
137 k type_int $ Forall_Repr_with_Context $
138 \c -> length (ta c)
139
140 -- | Parse 'null'.
141 null_from
142 :: forall root ty ast hs ret.
143 ( ty ~ Type_Root_of_Expr (Expr_Foldable root)
144 , Expr_From ast root
145 , Type0_Eq ty
146 , Type0_Lift Type_Bool (Type_of_Expr root)
147 , Type1_Constraint Foldable ty
148 , Type1_Unlift (Type_of_Expr root)
149 , Error_Expr_Lift (Error_Expr (Error_of_Type ast ty) ty ast)
150 (Error_of_Expr ast root)
151 , Root_of_Expr root ~ root
152 ) => ast
153 -> ExprFrom ast (Expr_Foldable root) hs ret
154 null_from ast_ta ex ast ctx k =
155 -- null :: Foldable t => t a -> Bool
156 expr_from (Proxy::Proxy root) ast_ta ctx $
157 \(ty_ta::ty h_ta) (Forall_Repr_with_Context ta) ->
158 check_type1 ex ast ty_ta $ \(Type1{}, _) ->
159 check_type1_constraint ex (Proxy::Proxy Foldable) ast ty_ta $ \Dict ->
160 k type_bool $ Forall_Repr_with_Context $
161 \c -> null (ta c)
162
163 -- | Parse 'minimum'.
164 minimum_from
165 :: forall root ty ast hs ret.
166 ( ty ~ Type_Root_of_Expr (Expr_Foldable root)
167 , Expr_From ast root
168 , Type0_Eq ty
169 , Type0_Constraint Ord ty
170 , Type1_Constraint Foldable ty
171 , Type1_Unlift (Type_of_Expr root)
172 , Error_Expr_Lift (Error_Expr (Error_of_Type ast ty) ty ast)
173 (Error_of_Expr ast root)
174 , Root_of_Expr root ~ root
175 ) => ast
176 -> ExprFrom ast (Expr_Foldable root) hs ret
177 minimum_from ast_ta ex ast ctx k =
178 -- minimum :: (Foldable t, Ord a) => t a -> a
179 expr_from (Proxy::Proxy root) ast_ta ctx $
180 \(ty_ta::ty h_ta) (Forall_Repr_with_Context ta) ->
181 check_type1 ex ast ty_ta $ \(Type1 _ ty_t_a, _) ->
182 check_type1_constraint ex (Proxy::Proxy Foldable) ast ty_ta $ \Dict ->
183 check_type0_constraint ex (Proxy::Proxy Ord) ast ty_t_a $ \Dict ->
184 k ty_t_a $ Forall_Repr_with_Context $
185 \c -> minimum (ta c)
186
187 -- | Parse 'maximum'.
188 maximum_from
189 :: forall root ty ast hs ret.
190 ( ty ~ Type_Root_of_Expr (Expr_Foldable root)
191 , Expr_From ast root
192 , Type0_Eq ty
193 , Type0_Constraint Ord ty
194 , Type1_Constraint Foldable ty
195 , Type1_Unlift (Type_of_Expr root)
196 , Error_Expr_Lift (Error_Expr (Error_of_Type ast ty) ty ast)
197 (Error_of_Expr ast root)
198 , Root_of_Expr root ~ root
199 ) => ast
200 -> ExprFrom ast (Expr_Foldable root) hs ret
201 maximum_from ast_ta ex ast ctx k =
202 -- maximum :: (Foldable t, Ord a) => t a -> a
203 expr_from (Proxy::Proxy root) ast_ta ctx $
204 \(ty_ta::ty h_ta) (Forall_Repr_with_Context ta) ->
205 check_type1 ex ast ty_ta $ \(Type1 _ ty_t_a, _) ->
206 check_type1_constraint ex (Proxy::Proxy Foldable) ast ty_ta $ \Dict ->
207 check_type0_constraint ex (Proxy::Proxy Ord) ast ty_t_a $ \Dict ->
208 k ty_t_a $ Forall_Repr_with_Context $
209 \c -> maximum (ta c)
210
211 -- | Parse 'elem'.
212 elem_from
213 :: forall root ty ast hs ret.
214 ( ty ~ Type_Root_of_Expr (Expr_Foldable root)
215 , Expr_From ast root
216 , Type0_Eq ty
217 , Type0_Constraint Eq ty
218 , Type0_Lift Type_Bool (Type_of_Expr root)
219 , Type1_Constraint Foldable ty
220 , Type1_Unlift (Type_of_Expr root)
221 , Error_Expr_Lift (Error_Expr (Error_of_Type ast ty) ty ast)
222 (Error_of_Expr ast root)
223 , Root_of_Expr root ~ root
224 ) => ast -> ast
225 -> ExprFrom ast (Expr_Foldable root) hs ret
226 elem_from ast_a ast_ta ex ast ctx k =
227 -- elem :: (Foldable t, Eq a) => a -> t a -> Bool
228 expr_from (Proxy::Proxy root) ast_a ctx $
229 \(ty_a::ty h_a) (Forall_Repr_with_Context a) ->
230 expr_from (Proxy::Proxy root) ast_ta ctx $
231 \(ty_ta::ty h_ta) (Forall_Repr_with_Context ta) ->
232 check_type1 ex ast ty_ta $ \(Type1 _ ty_t_a, _) ->
233 check_type0_eq ex ast ty_a ty_t_a $ \Refl ->
234 check_type1_constraint ex (Proxy::Proxy Foldable) ast ty_ta $ \Dict ->
235 check_type0_constraint ex (Proxy::Proxy Eq) ast ty_a $ \Dict ->
236 k type_bool $ Forall_Repr_with_Context $
237 \c -> a c `elem` ta c