]> Git — Sourcephile - haskell/symantic.git/blob - Language/Symantic/Lib/Sequences.hs
Fix Lib.Text.
[haskell/symantic.git] / Language / Symantic / Lib / Sequences.hs
1 {-# LANGUAGE UndecidableInstances #-}
2 {-# OPTIONS_GHC -fno-warn-orphans #-}
3 -- | Symantic for 'Sequences'.
4 module Language.Symantic.Lib.Sequences where
5
6 import Control.Monad (liftM, liftM2)
7 import qualified Data.MonoTraversable as MT
8 import Data.Proxy
9 import Data.Sequences (SemiSequence, IsSequence)
10 import qualified Data.Sequences as Seqs
11 import Data.Text (Text)
12 import Data.Type.Equality ((:~:)(Refl))
13 import Prelude hiding (filter, reverse)
14
15 import Language.Symantic.Parsing
16 import Language.Symantic.Parsing.Grammar
17 import Language.Symantic.Typing
18 import Language.Symantic.Compiling
19 import Language.Symantic.Interpreting
20 import Language.Symantic.Transforming.Trans
21 import Language.Symantic.Lib.MonoFunctor (Fam_MonoElement(..))
22
23 -- * Class 'Sym_SemiSequence'
24 class Sym_SemiSequence term where
25 intersperse :: SemiSequence s => term (MT.Element s) -> term s -> term s
26 cons :: SemiSequence s => term (MT.Element s) -> term s -> term s
27 snoc :: SemiSequence s => term s -> term (MT.Element s) -> term s
28 reverse :: SemiSequence s => term s -> term s
29 default intersperse :: (Trans t term, SemiSequence s) => t term (MT.Element s) -> t term s -> t term s
30 default cons :: (Trans t term, SemiSequence s) => t term (MT.Element s) -> t term s -> t term s
31 default snoc :: (Trans t term, SemiSequence s) => t term s -> t term (MT.Element s) -> t term s
32 default reverse :: (Trans t term, SemiSequence s) => t term s -> t term s
33 intersperse = trans_map2 cons
34 cons = trans_map2 cons
35 snoc = trans_map2 snoc
36 reverse = trans_map1 reverse
37
38 type instance Sym_of_Iface (Proxy SemiSequence) = Sym_SemiSequence
39 type instance Consts_of_Iface (Proxy SemiSequence) = Proxy SemiSequence ': Consts_imported_by SemiSequence
40 type instance Consts_imported_by SemiSequence =
41 [ Proxy SemiSequence
42 , Proxy []
43 , Proxy Text
44 ]
45
46 instance Sym_SemiSequence HostI where
47 intersperse = liftM2 Seqs.intersperse
48 cons = liftM2 Seqs.cons
49 snoc = liftM2 Seqs.snoc
50 reverse = liftM Seqs.reverse
51 instance Sym_SemiSequence TextI where
52 intersperse = textI2 "intersperse"
53 cons = textI2 "cons"
54 snoc = textI2 "snoc"
55 reverse = textI1 "reverse"
56 instance (Sym_SemiSequence r1, Sym_SemiSequence r2) => Sym_SemiSequence (DupI r1 r2) where
57 intersperse = dupI2 (Proxy @Sym_SemiSequence) intersperse
58 cons = dupI2 (Proxy @Sym_SemiSequence) cons
59 snoc = dupI2 (Proxy @Sym_SemiSequence) snoc
60 reverse = dupI1 (Proxy @Sym_SemiSequence) reverse
61
62 instance
63 ( Read_TypeNameR Type_Name cs rs
64 , Inj_Const cs SemiSequence
65 ) => Read_TypeNameR Type_Name cs (Proxy SemiSequence ': rs) where
66 read_typenameR _cs (Type_Name "SemiSequence") k = k (ty @SemiSequence)
67 read_typenameR _rs raw k = read_typenameR (Proxy @rs) raw k
68 instance Show_Const cs => Show_Const (Proxy SemiSequence ': cs) where
69 show_const ConstZ{} = "SemiSequence"
70 show_const (ConstS c) = show_const c
71
72 instance -- Proj_ConC
73 ( Proj_Const cs SemiSequence
74 , Proj_Consts cs (Consts_imported_by SemiSequence)
75 ) => Proj_ConC cs (Proxy SemiSequence) where
76 proj_conC _ (TyConst q :$ s)
77 | Just Refl <- eq_skind (kind_of_const q) (SKiType `SKiArrow` SKiConstraint)
78 , Just Refl <- proj_const q (Proxy @SemiSequence)
79 = case s of
80 TyConst c
81 | Just Refl <- eq_skind (kind_of_const c) SKiType ->
82 case () of
83 _ | Just Refl <- proj_const c (Proxy @Text) -> Just Con
84 _ -> Nothing
85 TyConst c :$ _o
86 | Just Refl <- eq_skind (kind_of_const c) (SKiType `SKiArrow` SKiType) ->
87 case () of
88 _ | Just Refl <- proj_const c (Proxy @[]) -> Just Con
89 _ -> Nothing
90 _ -> Nothing
91 proj_conC _c _q = Nothing
92 data instance TokenT meta (ts::[*]) (Proxy SemiSequence)
93 = Token_Term_SemiSequence_intersperse (EToken meta ts) (EToken meta ts)
94 | Token_Term_SemiSequence_cons (EToken meta ts) (EToken meta ts)
95 | Token_Term_SemiSequence_snoc (EToken meta ts) (EToken meta ts)
96 | Token_Term_SemiSequence_reverse (EToken meta ts)
97 deriving instance Eq_Token meta ts => Eq (TokenT meta ts (Proxy SemiSequence))
98 deriving instance Show_Token meta ts => Show (TokenT meta ts (Proxy SemiSequence))
99 instance -- CompileI
100 ( Inj_Const (Consts_of_Ifaces is) SemiSequence
101 , Proj_Con (Consts_of_Ifaces is)
102 , Proj_Fam (Consts_of_Ifaces is) Fam_MonoElement
103 , Compile is
104 ) => CompileI is (Proxy SemiSequence) where
105 compileI
106 :: forall meta ctx ret ls rs.
107 TokenT meta is (Proxy SemiSequence)
108 -> CompileT meta ctx ret is ls (Proxy SemiSequence ': rs)
109 compileI tok ctx k =
110 case tok of
111 Token_Term_SemiSequence_intersperse tok_e tok_s ->
112 e2s2s_from tok_e tok_s intersperse
113 Token_Term_SemiSequence_cons tok_e tok_s ->
114 e2s2s_from tok_e tok_s cons
115 Token_Term_SemiSequence_snoc tok_s tok_e ->
116 e2s2s_from tok_s tok_e (Prelude.flip snoc)
117 Token_Term_SemiSequence_reverse tok_s ->
118 -- reverse :: SemiSequence s => s -> s
119 compileO tok_s ctx $ \ty_s (TermO s) ->
120 check_con (At (Just tok_s) (ty @SemiSequence :$ ty_s)) $ \Con ->
121 k ty_s $ TermO $
122 \c -> reverse (s c)
123 where
124 e2s2s_from tok_e tok_s
125 (f::forall term s.
126 (Sym_SemiSequence term, SemiSequence s)
127 => term (MT.Element s) -> term s -> term s) =
128 -- intersperse :: SemiSequence s => MT.Element s -> s -> s
129 -- cons :: SemiSequence s => MT.Element s -> s -> s
130 -- snoc :: SemiSequence s => s -> MT.Element s -> s
131 compileO tok_e ctx $ \ty_e (TermO e) ->
132 compileO tok_s ctx $ \ty_s (TermO s) ->
133 check_con (At (Just tok_s) (ty @SemiSequence :$ ty_s)) $ \Con ->
134 check_fam (At (Just tok_s) Fam_MonoElement) (ty_s `TypesS` TypesZ) $ \ty_s_e ->
135 check_type (At Nothing ty_s_e) (At (Just tok_e) ty_e) $ \Refl ->
136 k ty_s $ TermO $
137 \c -> f (e c) (s c)
138 instance -- TokenizeT
139 Inj_Token meta ts SemiSequence =>
140 TokenizeT meta ts (Proxy SemiSequence) where
141 tokenizeT _t = mempty
142 { tokenizers_infix = tokenizeTMod []
143 [ tokenize2 "intersperse" infixN5 Token_Term_SemiSequence_intersperse
144 , tokenize2 "cons" infixN5 Token_Term_SemiSequence_cons
145 , tokenize2 "snoc" infixN5 Token_Term_SemiSequence_snoc
146 , tokenize1 "reverse" infixN5 Token_Term_SemiSequence_reverse
147 ]
148 }
149 instance Gram_Term_AtomsT meta ts (Proxy SemiSequence) g
150
151 -- * Class 'Sym_IsSequence'
152 class Sym_IsSequence term where
153 filter :: IsSequence s => term (MT.Element s -> Bool) -> term s -> term s
154 default filter :: (Trans t term, IsSequence s) => t term (MT.Element s -> Bool) -> t term s -> t term s
155 filter = trans_map2 filter
156
157 type instance Sym_of_Iface (Proxy IsSequence) = Sym_IsSequence
158 type instance Consts_of_Iface (Proxy IsSequence) = Proxy IsSequence ': Consts_imported_by IsSequence
159 type instance Consts_imported_by IsSequence =
160 [ Proxy IsSequence
161 , Proxy (->)
162 , Proxy []
163 , Proxy Text
164 , Proxy Bool
165 ]
166
167 instance Sym_IsSequence HostI where
168 filter = liftM2 Seqs.filter
169 instance Sym_IsSequence TextI where
170 filter = textI2 "filter"
171 instance (Sym_IsSequence r1, Sym_IsSequence r2) => Sym_IsSequence (DupI r1 r2) where
172 filter = dupI2 (Proxy @Sym_IsSequence) filter
173
174 instance
175 ( Read_TypeNameR Type_Name cs rs
176 , Inj_Const cs IsSequence
177 ) => Read_TypeNameR Type_Name cs (Proxy IsSequence ': rs) where
178 read_typenameR _cs (Type_Name "IsSequence") k = k (ty @IsSequence)
179 read_typenameR _rs raw k = read_typenameR (Proxy @rs) raw k
180 instance Show_Const cs => Show_Const (Proxy IsSequence ': cs) where
181 show_const ConstZ{} = "IsSequence"
182 show_const (ConstS c) = show_const c
183
184 instance -- Proj_ConC
185 ( Proj_Const cs IsSequence
186 , Proj_Consts cs (Consts_imported_by IsSequence)
187 ) => Proj_ConC cs (Proxy IsSequence) where
188 proj_conC _ (TyConst q :$ s)
189 | Just Refl <- eq_skind (kind_of_const q) (SKiType `SKiArrow` SKiConstraint)
190 , Just Refl <- proj_const q (Proxy @IsSequence)
191 = case s of
192 TyConst c
193 | Just Refl <- eq_skind (kind_of_const c) SKiType ->
194 case () of
195 _ | Just Refl <- proj_const c (Proxy @Text) -> Just Con
196 _ -> Nothing
197 TyConst c :$ _o
198 | Just Refl <- eq_skind (kind_of_const c) (SKiType `SKiArrow` SKiType) ->
199 case () of
200 _ | Just Refl <- proj_const c (Proxy @[]) -> Just Con
201 _ -> Nothing
202 _ -> Nothing
203 proj_conC _c _q = Nothing
204 data instance TokenT meta (ts::[*]) (Proxy IsSequence)
205 = Token_Term_IsSequence_filter (EToken meta ts) (EToken meta ts)
206 deriving instance Eq_Token meta ts => Eq (TokenT meta ts (Proxy IsSequence))
207 deriving instance Show_Token meta ts => Show (TokenT meta ts (Proxy IsSequence))
208 instance -- CompileI
209 ( Inj_Const (Consts_of_Ifaces is) IsSequence
210 , Inj_Const (Consts_of_Ifaces is) (->)
211 , Inj_Const (Consts_of_Ifaces is) Bool
212 , Proj_Con (Consts_of_Ifaces is)
213 , Proj_Fam (Consts_of_Ifaces is) Fam_MonoElement
214 , Compile is
215 ) => CompileI is (Proxy IsSequence) where
216 compileI
217 :: forall meta ctx ret ls rs.
218 TokenT meta is (Proxy IsSequence)
219 -> CompileT meta ctx ret is ls (Proxy IsSequence ': rs)
220 compileI tok ctx k =
221 case tok of
222 Token_Term_IsSequence_filter tok_e2Bool tok_s ->
223 -- filter :: IsSequence s => (MT.Element s -> Bool) -> s -> s
224 compileO tok_e2Bool ctx $ \ty_e2Bool (TermO e2Bool) ->
225 compileO tok_s ctx $ \ty_s (TermO s) ->
226 check_type2 (ty @(->)) (At (Just tok_e2Bool) ty_e2Bool) $ \Refl ty_e2Bool_e ty_e2Bool_Bool ->
227 check_type
228 (At Nothing (ty @Bool))
229 (At (Just tok_e2Bool) ty_e2Bool_Bool) $ \Refl ->
230 check_con (At (Just tok_s) (ty @IsSequence :$ ty_s)) $ \Con ->
231 check_fam (At (Just tok_s) Fam_MonoElement) (ty_s `TypesS` TypesZ) $ \ty_s_e ->
232 check_type
233 (At Nothing ty_s_e)
234 (At (Just tok_e2Bool) ty_e2Bool_e) $ \Refl ->
235 k ty_s $ TermO $
236 \c -> filter (e2Bool c) (s c)
237 instance -- TokenizeT
238 Inj_Token meta ts IsSequence =>
239 TokenizeT meta ts (Proxy IsSequence) where
240 tokenizeT _t = mempty
241 { tokenizers_infix = tokenizeTMod []
242 [ tokenize2 "filter" infixN5 Token_Term_IsSequence_filter
243 ]
244 }
245 instance Gram_Term_AtomsT meta ts (Proxy IsSequence) g