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