]> Git — Sourcephile - haskell/symantic.git/blob - Language/Symantic/Compiling/Sequences.hs
Fix comment typo.
[haskell/symantic.git] / Language / Symantic / Compiling / Sequences.hs
1 {-# LANGUAGE UndecidableInstances #-}
2 {-# OPTIONS_GHC -fno-warn-orphans #-}
3 -- | Symantic for 'Sequences'.
4 module Language.Symantic.Compiling.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.Term
18 import Language.Symantic.Compiling.MonoFunctor (Fam_MonoElement(..))
19 import Language.Symantic.Interpreting
20 import Language.Symantic.Transforming.Trans
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 Consts_of_Iface (Proxy SemiSequence) = Proxy SemiSequence ': Consts_imported_by SemiSequence
39 type instance Consts_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 (Proxy @Sym_SemiSequence) intersperse
57 cons = dupI2 (Proxy @Sym_SemiSequence) cons
58 snoc = dupI2 (Proxy @Sym_SemiSequence) snoc
59 reverse = dupI1 (Proxy @Sym_SemiSequence) reverse
60
61 instance Const_from Text cs => Const_from Text (Proxy SemiSequence ': cs) where
62 const_from "SemiSequence" k = k (ConstZ kind)
63 const_from s k = const_from s $ k . ConstS
64 instance Show_Const cs => Show_Const (Proxy SemiSequence ': cs) where
65 show_const ConstZ{} = "SemiSequence"
66 show_const (ConstS c) = show_const c
67
68 instance -- Proj_ConC
69 ( Proj_Const cs SemiSequence
70 , Proj_Consts cs (Consts_imported_by SemiSequence)
71 ) => Proj_ConC cs (Proxy SemiSequence) where
72 proj_conC _ (TyConst q :$ s)
73 | Just Refl <- eq_skind (kind_of_const q) (SKiType `SKiArrow` SKiConstraint)
74 , Just Refl <- proj_const q (Proxy::Proxy SemiSequence)
75 = case s of
76 TyConst c
77 | Just Refl <- eq_skind (kind_of_const c) SKiType ->
78 case () of
79 _ | Just Refl <- proj_const c (Proxy::Proxy Text) -> Just Con
80 _ -> Nothing
81 TyConst c :$ _o
82 | Just Refl <- eq_skind (kind_of_const c) (SKiType `SKiArrow` SKiType) ->
83 case () of
84 _ | Just Refl <- proj_const c (Proxy::Proxy []) -> Just Con
85 _ -> Nothing
86 _ -> Nothing
87 proj_conC _c _q = Nothing
88 data instance TokenT meta (ts::[*]) (Proxy SemiSequence)
89 = Token_Term_SemiSequence_intersperse (EToken meta ts) (EToken meta ts)
90 | Token_Term_SemiSequence_cons (EToken meta ts) (EToken meta ts)
91 | Token_Term_SemiSequence_snoc (EToken meta ts) (EToken meta ts)
92 | Token_Term_SemiSequence_reverse (EToken meta ts)
93 deriving instance Eq_Token meta ts => Eq (TokenT meta ts (Proxy SemiSequence))
94 deriving instance Show_Token meta ts => Show (TokenT meta ts (Proxy SemiSequence))
95 instance -- CompileI
96 ( Inj_Const (Consts_of_Ifaces is) SemiSequence
97 , Proj_Con (Consts_of_Ifaces is)
98 , Proj_Fam (Consts_of_Ifaces is) Fam_MonoElement
99 , Compile is
100 ) => CompileI is (Proxy SemiSequence) where
101 compileI
102 :: forall meta ctx ret ls rs.
103 TokenT meta is (Proxy SemiSequence)
104 -> CompileT meta ctx ret is ls (Proxy SemiSequence ': rs)
105 compileI tok ctx k =
106 case tok of
107 Token_Term_SemiSequence_intersperse tok_e tok_s ->
108 e2s2s_from tok_e tok_s intersperse
109 Token_Term_SemiSequence_cons tok_e tok_s ->
110 e2s2s_from tok_e tok_s cons
111 Token_Term_SemiSequence_snoc tok_s tok_e ->
112 e2s2s_from tok_s tok_e (Prelude.flip snoc)
113 Token_Term_SemiSequence_reverse tok_s ->
114 -- reverse :: SemiSequence s => s -> s
115 compileO tok_s ctx $ \ty_s (TermO s) ->
116 check_con (At (Just tok_s) (ty @SemiSequence :$ ty_s)) $ \Con ->
117 k ty_s $ TermO $
118 \c -> reverse (s c)
119 where
120 e2s2s_from tok_e tok_s
121 (f::forall term s.
122 (Sym_SemiSequence term, SemiSequence s)
123 => term (MT.Element s) -> term s -> term s) =
124 -- intersperse :: SemiSequence s => MT.Element s -> s -> s
125 -- cons :: SemiSequence s => MT.Element s -> s -> s
126 -- snoc :: SemiSequence s => s -> MT.Element s -> s
127 compileO tok_e ctx $ \ty_e (TermO e) ->
128 compileO tok_s ctx $ \ty_s (TermO s) ->
129 check_con (At (Just tok_s) (ty @SemiSequence :$ ty_s)) $ \Con ->
130 check_fam (At (Just tok_s) Fam_MonoElement) (ty_s `TypesS` TypesZ) $ \ty_s_e ->
131 check_type (At Nothing ty_s_e) (At (Just tok_e) ty_e) $ \Refl ->
132 k ty_s $ TermO $
133 \c -> f (e c) (s c)
134
135 -- * Class 'Sym_IsSequence'
136 class Sym_IsSequence term where
137 filter :: IsSequence s => term (MT.Element s -> Bool) -> term s -> term s
138 default filter :: (Trans t term, IsSequence s) => t term (MT.Element s -> Bool) -> t term s -> t term s
139 filter = trans_map2 filter
140
141 type instance Sym_of_Iface (Proxy IsSequence) = Sym_IsSequence
142 type instance Consts_of_Iface (Proxy IsSequence) = Proxy IsSequence ': Consts_imported_by IsSequence
143 type instance Consts_imported_by IsSequence =
144 [ Proxy IsSequence
145 , Proxy (->)
146 , Proxy []
147 , Proxy Text
148 , Proxy Bool
149 ]
150
151 instance Sym_IsSequence HostI where
152 filter = liftM2 Seqs.filter
153 instance Sym_IsSequence TextI where
154 filter = textI2 "filter"
155 instance (Sym_IsSequence r1, Sym_IsSequence r2) => Sym_IsSequence (DupI r1 r2) where
156 filter = dupI2 (Proxy @Sym_IsSequence) filter
157
158 instance Const_from Text cs => Const_from Text (Proxy IsSequence ': cs) where
159 const_from "IsSequence" k = k (ConstZ kind)
160 const_from s k = const_from s $ k . ConstS
161 instance Show_Const cs => Show_Const (Proxy IsSequence ': cs) where
162 show_const ConstZ{} = "IsSequence"
163 show_const (ConstS c) = show_const c
164
165 instance -- Proj_ConC
166 ( Proj_Const cs IsSequence
167 , Proj_Consts cs (Consts_imported_by IsSequence)
168 ) => Proj_ConC cs (Proxy IsSequence) where
169 proj_conC _ (TyConst q :$ s)
170 | Just Refl <- eq_skind (kind_of_const q) (SKiType `SKiArrow` SKiConstraint)
171 , Just Refl <- proj_const q (Proxy::Proxy IsSequence)
172 = case s of
173 TyConst c
174 | Just Refl <- eq_skind (kind_of_const c) SKiType ->
175 case () of
176 _ | Just Refl <- proj_const c (Proxy::Proxy Text) -> Just Con
177 _ -> Nothing
178 TyConst c :$ _o
179 | Just Refl <- eq_skind (kind_of_const c) (SKiType `SKiArrow` SKiType) ->
180 case () of
181 _ | Just Refl <- proj_const c (Proxy::Proxy []) -> Just Con
182 _ -> Nothing
183 _ -> Nothing
184 proj_conC _c _q = Nothing
185 data instance TokenT meta (ts::[*]) (Proxy IsSequence)
186 = Token_Term_IsSequence_filter (EToken meta ts) (EToken meta ts)
187 deriving instance Eq_Token meta ts => Eq (TokenT meta ts (Proxy IsSequence))
188 deriving instance Show_Token meta ts => Show (TokenT meta ts (Proxy IsSequence))
189 instance -- CompileI
190 ( Inj_Const (Consts_of_Ifaces is) IsSequence
191 , Inj_Const (Consts_of_Ifaces is) (->)
192 , Inj_Const (Consts_of_Ifaces is) Bool
193 , Proj_Con (Consts_of_Ifaces is)
194 , Proj_Fam (Consts_of_Ifaces is) Fam_MonoElement
195 , Compile is
196 ) => CompileI is (Proxy IsSequence) where
197 compileI
198 :: forall meta ctx ret ls rs.
199 TokenT meta is (Proxy IsSequence)
200 -> CompileT meta ctx ret is ls (Proxy IsSequence ': rs)
201 compileI tok ctx k =
202 case tok of
203 Token_Term_IsSequence_filter tok_e2Bool tok_s ->
204 -- filter :: IsSequence s => (MT.Element s -> Bool) -> s -> s
205 compileO tok_e2Bool ctx $ \ty_e2Bool (TermO e2Bool) ->
206 compileO tok_s ctx $ \ty_s (TermO s) ->
207 check_type2 (ty @(->)) (At (Just tok_e2Bool) ty_e2Bool) $ \Refl ty_e2Bool_e ty_e2Bool_Bool ->
208 check_type
209 (At Nothing (ty @Bool))
210 (At (Just tok_e2Bool) ty_e2Bool_Bool) $ \Refl ->
211 check_con (At (Just tok_s) (ty @IsSequence :$ ty_s)) $ \Con ->
212 check_fam (At (Just tok_s) Fam_MonoElement) (ty_s `TypesS` TypesZ) $ \ty_s_e ->
213 check_type
214 (At Nothing ty_s_e)
215 (At (Just tok_e2Bool) ty_e2Bool_e) $ \Refl ->
216 k ty_s $ TermO $
217 \c -> filter (e2Bool c) (s c)