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