]> Git — Sourcephile - haskell/symantic.git/blob - symantic-lib/Language/Symantic/Lib/MonoFoldable.hs
Fix Mono{Foldable,Functor} and {Semi,Is}Sequence constraints.
[haskell/symantic.git] / symantic-lib / Language / Symantic / Lib / MonoFoldable.hs
1 {-# LANGUAGE UndecidableInstances #-}
2 {-# OPTIONS_GHC -fno-warn-orphans #-}
3 {-# OPTIONS_GHC -fconstraint-solver-iterations=9 #-}
4 -- | Symantic for 'MonoFoldable'.
5 module Language.Symantic.Lib.MonoFoldable where
6
7 import Control.Monad (liftM, liftM2, liftM3)
8 import Data.MonoTraversable (MonoFoldable)
9 import Data.Proxy
10 import Data.Type.Equality ((:~:)(Refl))
11 import qualified Data.MonoTraversable as MT
12
13 import Language.Symantic.Parsing
14 import Language.Symantic.Typing
15 import Language.Symantic.Compiling
16 import Language.Symantic.Interpreting
17 import Language.Symantic.Transforming
18 import Language.Symantic.Lib.MonoFunctor
19
20 -- * Class 'Sym_MonoFoldable'
21 class Sym_MonoFunctor term => Sym_MonoFoldable term where
22 ofoldMap :: (MonoFoldable o, Monoid m) => term (MT.Element o -> m) -> term o -> term m
23 ofoldr :: MonoFoldable o => term (MT.Element o -> b -> b) -> term b -> term o -> term b
24 ofoldl' :: MonoFoldable o => term (b -> MT.Element o -> b) -> term b -> term o -> term b
25 olength :: MonoFoldable o => term o -> term Int
26 onull :: MonoFoldable o => term o -> term Bool
27 oall :: MonoFoldable o => term (MT.Element o -> Bool) -> term o -> term Bool
28 oany :: MonoFoldable o => term (MT.Element o -> Bool) -> term o -> term Bool
29 otoList :: MonoFoldable o => term o -> term [MT.Element o]
30 default ofoldMap :: (Trans t term, MonoFoldable o, Monoid m)
31 => t term (MT.Element o -> m) -> t term o -> t term m
32 default ofoldr :: (Trans t term, MonoFoldable o)
33 => t term (MT.Element o -> b -> b) -> t term b -> t term o -> t term b
34 default ofoldl' :: (Trans t term, MonoFoldable o)
35 => t term (b -> MT.Element o -> b) -> t term b -> t term o -> t term b
36 default olength :: (Trans t term, MonoFoldable o) => t term o -> t term Int
37 default onull :: (Trans t term, MonoFoldable o) => t term o -> t term Bool
38 default oall :: (Trans t term, MonoFoldable o) => t term (MT.Element o -> Bool) -> t term o -> t term Bool
39 default oany :: (Trans t term, MonoFoldable o) => t term (MT.Element o -> Bool) -> t term o -> t term Bool
40 default otoList :: (Trans t term, MonoFoldable o) => t term o -> t term [MT.Element o]
41 ofoldMap = trans_map2 ofoldMap
42 ofoldr = trans_map3 ofoldr
43 ofoldl' = trans_map3 ofoldl'
44 olength = trans_map1 olength
45 onull = trans_map1 onull
46 oall = trans_map2 oall
47 oany = trans_map2 oany
48 otoList = trans_map1 otoList
49
50 type instance Sym_of_Iface (Proxy MonoFoldable) = Sym_MonoFoldable
51 type instance TyConsts_of_Iface (Proxy MonoFoldable) = Proxy MonoFoldable ': TyConsts_imported_by (Proxy MonoFoldable)
52 type instance TyConsts_imported_by (Proxy MonoFoldable) =
53 [ Proxy (->)
54 , Proxy Bool
55 , Proxy Int
56 , Proxy Monoid
57 ]
58
59 instance Sym_MonoFoldable HostI where
60 ofoldMap = liftM2 MT.ofoldMap
61 ofoldr = liftM3 MT.ofoldr
62 ofoldl' = liftM3 MT.ofoldl'
63 olength = liftM MT.olength
64 onull = liftM MT.onull
65 oall = liftM2 MT.oall
66 oany = liftM2 MT.oany
67 otoList = liftM MT.otoList
68 instance Sym_MonoFoldable TextI where
69 ofoldMap = textI2 "ofoldMap"
70 ofoldr = textI3 "ofoldr"
71 ofoldl' = textI3 "ofoldl'"
72 olength = textI1 "olength"
73 onull = textI1 "onull"
74 oall = textI2 "oall"
75 oany = textI2 "oany"
76 otoList = textI1 "otoList"
77 instance (Sym_MonoFoldable r1, Sym_MonoFoldable r2) => Sym_MonoFoldable (DupI r1 r2) where
78 ofoldMap = dupI2 @Sym_MonoFoldable ofoldMap
79 ofoldr = dupI3 @Sym_MonoFoldable ofoldr
80 ofoldl' = dupI3 @Sym_MonoFoldable ofoldl'
81 olength = dupI1 @Sym_MonoFoldable olength
82 onull = dupI1 @Sym_MonoFoldable onull
83 oall = dupI2 @Sym_MonoFoldable oall
84 oany = dupI2 @Sym_MonoFoldable oany
85 otoList = dupI1 @Sym_MonoFoldable otoList
86
87 instance
88 ( Read_TyNameR TyName cs rs
89 , Inj_TyConst cs MonoFoldable
90 ) => Read_TyNameR TyName cs (Proxy MonoFoldable ': rs) where
91 read_TyNameR _cs (TyName "MonoFoldable") k = k (ty @MonoFoldable)
92 read_TyNameR _rs raw k = read_TyNameR (Proxy @rs) raw k
93 instance Show_TyConst cs => Show_TyConst (Proxy MonoFoldable ': cs) where
94 show_TyConst TyConstZ{} = "MonoFoldable"
95 show_TyConst (TyConstS c) = show_TyConst c
96
97 instance Proj_TyConC cs (Proxy MonoFoldable)
98
99 data instance TokenT meta (ts::[*]) (Proxy MonoFoldable)
100 = Token_Term_MonoFoldable_ofoldMap (EToken meta ts) (EToken meta ts)
101 | Token_Term_MonoFoldable_ofoldr (EToken meta ts) (EToken meta ts) (EToken meta ts)
102 | Token_Term_MonoFoldable_ofoldl' (EToken meta ts) (EToken meta ts) (EToken meta ts)
103 | Token_Term_MonoFoldable_olength (EToken meta ts)
104 | Token_Term_MonoFoldable_onull (EToken meta ts)
105 | Token_Term_MonoFoldable_oall (EToken meta ts) (EToken meta ts)
106 | Token_Term_MonoFoldable_oany (EToken meta ts) (EToken meta ts)
107 | Token_Term_MonoFoldable_otoList (EToken meta ts)
108 deriving instance Eq_Token meta ts => Eq (TokenT meta ts (Proxy MonoFoldable))
109 deriving instance Show_Token meta ts => Show (TokenT meta ts (Proxy MonoFoldable))
110 instance -- CompileI
111 ( Inj_TyConst cs MonoFoldable
112 , Inj_TyConst cs (->)
113 , Inj_TyConst cs []
114 , Inj_TyConst cs Monoid
115 , Inj_TyConst cs Bool
116 , Inj_TyConst cs Int
117 , Proj_TyCon cs
118 , Proj_TyFam cs TyFam_MonoElement
119 , Compile cs is
120 ) => CompileI cs is (Proxy MonoFoldable) where
121 compileI
122 :: forall meta ctx ret ls rs.
123 TokenT meta is (Proxy MonoFoldable)
124 -> CompileT meta ctx ret cs is ls (Proxy MonoFoldable ': rs)
125 compileI tok ctx k =
126 case tok of
127 Token_Term_MonoFoldable_ofoldMap tok_f tok_o ->
128 -- ofoldMap :: Monoid m => (Element o -> m) -> o -> m
129 compileO tok_f ctx $ \ty_f (TermO f) ->
130 compileO tok_o ctx $ \ty_o (TermO o) ->
131 check_TyEq2 (ty @(->)) (At (Just tok_f) ty_f) $ \Refl ty_f_a ty_m ->
132 check_TyCon (At (Just tok_f) (ty @MonoFoldable :$ ty_o)) $ \TyCon ->
133 check_TyCon (At (Just tok_f) (ty @Monoid :$ ty_m)) $ \TyCon ->
134 check_TyFam (At (Just tok_o) TyFam_MonoElement) (ty_o `TypesS` TypesZ) $ \ty_o_e ->
135 check_TyEq
136 (At Nothing ty_o_e)
137 (At (Just tok_f) ty_f_a) $ \Refl ->
138 k ty_m $ TermO $
139 \c -> ofoldMap (f c) (o c)
140 Token_Term_MonoFoldable_ofoldr tok_e2b2b tok_b tok_o ->
141 ofoldr_from tok_e2b2b tok_b tok_o ofoldr
142 Token_Term_MonoFoldable_ofoldl' tok_b2e2b tok_b tok_o ->
143 ofoldl_from tok_b2e2b tok_b tok_o ofoldl'
144 Token_Term_MonoFoldable_olength tok_o -> o2ty_from tok_o olength
145 Token_Term_MonoFoldable_onull tok_o -> o2ty_from tok_o onull
146 Token_Term_MonoFoldable_oall tok_e2Bool tok_o -> oalloany_from tok_e2Bool tok_o oall
147 Token_Term_MonoFoldable_oany tok_e2Bool tok_o -> oalloany_from tok_e2Bool tok_o oany
148 Token_Term_MonoFoldable_otoList tok_o ->
149 -- otoList :: MonoFoldable o => o -> [MT.Element o]
150 compileO tok_o ctx $ \ty_o (TermO o) ->
151 check_TyCon (At (Just tok_o) (ty @MonoFoldable :$ ty_o)) $ \TyCon ->
152 check_TyFam (At (Just tok_o) TyFam_MonoElement) (ty_o `TypesS` TypesZ) $ \ty_o_e ->
153 k (ty @[] :$ ty_o_e) $ TermO $
154 \c -> otoList (o c)
155 where
156 ofoldr_from tok_e2b2b tok_b tok_o
157 (fold::forall term o b.
158 (Sym_MonoFoldable term, MonoFoldable o)
159 => term (MT.Element o -> b -> b) -> term b -> term o -> term b) =
160 -- ofoldr :: MonoFoldable o => (MT.Element o -> b -> b) -> b -> o -> b
161 compileO tok_e2b2b ctx $ \ty_e2b2b (TermO e2b2b) ->
162 compileO tok_b ctx $ \ty_b (TermO b) ->
163 compileO tok_o ctx $ \ty_o (TermO o) ->
164 check_TyEq2 (ty @(->)) (At (Just tok_e2b2b) ty_e2b2b) $ \Refl ty_e2b2b_e ty_e2b2b_b2b ->
165 check_TyEq2 (ty @(->)) (At (Just tok_e2b2b) ty_e2b2b_b2b) $ \Refl ty_e2b2b_b2b_b0 ty_e2b2b_b2b_b1 ->
166 check_TyEq
167 (At (Just tok_e2b2b) ty_e2b2b_b2b_b0)
168 (At (Just tok_e2b2b) ty_e2b2b_b2b_b1) $ \Refl ->
169 check_TyEq
170 (At (Just tok_e2b2b) ty_e2b2b_b2b_b0)
171 (At (Just tok_b) ty_b) $ \Refl ->
172 check_TyCon (At (Just tok_o) (ty @MonoFoldable :$ ty_o)) $ \TyCon ->
173 check_TyFam (At (Just tok_o) TyFam_MonoElement) (ty_o `TypesS` TypesZ) $ \ty_o_e ->
174 check_TyEq
175 (At (Just tok_e2b2b) ty_e2b2b_e)
176 (At (Just tok_o) ty_o_e) $ \Refl ->
177 k ty_b $ TermO $
178 \c -> fold (e2b2b c) (b c) (o c)
179 ofoldl_from tok_b2e2b tok_b tok_o
180 (fold::forall term o b.
181 (Sym_MonoFoldable term, MonoFoldable o)
182 => term (b -> MT.Element o -> b) -> term b -> term o -> term b) =
183 -- ofoldl' :: MonoFoldable o => (b -> MT.Element o -> b) -> b -> o -> b
184 compileO tok_b2e2b ctx $ \ty_b2e2b (TermO b2e2b) ->
185 compileO tok_b ctx $ \ty_b (TermO b) ->
186 compileO tok_o ctx $ \ty_o (TermO o) ->
187 check_TyEq2 (ty @(->)) (At (Just tok_b2e2b) ty_b2e2b) $ \Refl ty_b2e2b_b ty_b2e2b_a2b ->
188 check_TyEq2 (ty @(->)) (At (Just tok_b2e2b) ty_b2e2b_a2b) $ \Refl ty_b2e2b_a2b_e ty_b2e2b_a2b_b ->
189 check_TyEq
190 (At (Just tok_b2e2b) ty_b2e2b_b)
191 (At (Just tok_b2e2b) ty_b2e2b_a2b_b) $ \Refl ->
192 check_TyEq
193 (At (Just tok_b2e2b) ty_b2e2b_b)
194 (At (Just tok_b) ty_b) $ \Refl ->
195 check_TyCon (At (Just tok_o) (ty @MonoFoldable :$ ty_o)) $ \TyCon ->
196 check_TyFam (At (Just tok_o) TyFam_MonoElement) (ty_o `TypesS` TypesZ) $ \ty_o_e ->
197 check_TyEq
198 (At (Just tok_b2e2b) ty_b2e2b_a2b_e)
199 (At (Just tok_o) ty_o_e) $ \Refl ->
200 k ty_b $ TermO $
201 \c -> fold (b2e2b c) (b c) (o c)
202 o2ty_from
203 :: forall typ. Inj_TyConst cs typ
204 => EToken meta is
205 -> (forall term o. (Sym_MonoFoldable term, MonoFoldable o) => term o -> term typ)
206 -> Either (Error_Term meta cs is) ret
207 o2ty_from tok_o f =
208 -- olength :: MonoFoldable o => o -> Int
209 -- onull :: MonoFoldable o => o -> Bool
210 compileO tok_o ctx $ \ty_o (TermO o) ->
211 check_TyCon (At (Just tok_o) (ty @MonoFoldable :$ ty_o)) $ \TyCon ->
212 k (TyConst inj_TyConst::Type cs typ) $ TermO $
213 \c -> f (o c)
214 oalloany_from
215 tok_e2Bool tok_o
216 (g::forall term o.
217 (Sym_MonoFoldable term, MonoFoldable o)
218 => term (MT.Element o -> Bool) -> term o -> term Bool) =
219 -- all :: MonoFoldable o => (MT.Element o -> Bool) -> o -> Bool
220 -- any :: MonoFoldable o => (MT.Element o -> Bool) -> o -> Bool
221 compileO tok_e2Bool ctx $ \ty_e2Bool (TermO e2Bool) ->
222 compileO tok_o ctx $ \ty_o (TermO o) ->
223 check_TyEq2 (ty @(->)) (At (Just tok_e2Bool) ty_e2Bool) $ \Refl ty_e2Bool_e ty_e2Bool_Bool ->
224 check_TyCon (At (Just tok_o) (ty @MonoFoldable :$ ty_o)) $ \TyCon ->
225 check_TyFam (At (Just tok_o) TyFam_MonoElement) (ty_o `TypesS` TypesZ) $ \ty_o_e ->
226 check_TyEq
227 (At (Just tok_e2Bool) ty_e2Bool_e)
228 (At (Just tok_o) ty_o_e) $ \Refl ->
229 check_TyEq
230 (At Nothing (ty @Bool))
231 (At (Just tok_e2Bool) ty_e2Bool_Bool) $ \Refl ->
232 k (ty @Bool) $ TermO $
233 \c -> g (e2Bool c) (o c)
234 instance -- TokenizeT
235 Inj_Token meta ts MonoFoldable =>
236 TokenizeT meta ts (Proxy MonoFoldable) where
237 tokenizeT _t = mempty
238 { tokenizers_infix = tokenizeTMod []
239 [ tokenize2 "ofoldMap" infixN5 Token_Term_MonoFoldable_ofoldMap
240 , tokenize3 "ofoldr" infixN5 Token_Term_MonoFoldable_ofoldr
241 , tokenize3 "ofoldl'" infixN5 Token_Term_MonoFoldable_ofoldl'
242 , tokenize1 "olength" infixN5 Token_Term_MonoFoldable_olength
243 , tokenize1 "onull" infixN5 Token_Term_MonoFoldable_onull
244 , tokenize2 "oall" infixN5 Token_Term_MonoFoldable_oall
245 , tokenize2 "oany" infixN5 Token_Term_MonoFoldable_oany
246 , tokenize1 "otoList" infixN5 Token_Term_MonoFoldable_otoList
247 ]
248 }
249 instance Gram_Term_AtomsT meta ts (Proxy MonoFoldable) g