1use super::{
2 structs::*,
3 traits::*,
4 utils::*,
5};
6use crate::internal::functional::{
7 base::*,
8 nat::*,
9 type_app::*,
10};
11
12impl<Row, F> serde::Serialize for AppSum<'static, Row, F>
13where
14 F: TyCon,
15 Row: SumApp<'static, F>,
16 Row::Applied:
17 Send + 'static + serde::Serialize + for<'de> serde::Deserialize<'de>,
18{
19 fn serialize<S>(
20 &self,
21 serializer: S,
22 ) -> Result<S::Ok, S::Error>
23 where
24 S: serde::Serializer,
25 {
26 let row: &Row::Applied = get_sum_borrow(self);
27
28 row.serialize(serializer)
29 }
30}
31
32impl<'a, Row, F, T> serde::Deserialize<'a> for AppSum<'a, Row, F>
33where
34 F: TyCon,
35 T: Send + 'static,
36 Row: SumApp<'a, F, Applied = T>,
37 T: serde::Serialize + for<'de> serde::Deserialize<'de>,
38{
39 fn deserialize<D>(deserializer: D) -> Result<Self, D::Error>
40 where
41 D: serde::Deserializer<'a>,
42 {
43 let row = T::deserialize(deserializer)?;
44
45 Ok(AppSum::new(row))
46 }
47}
48
49impl<'a, S, Row, F> HasSumApp<'a, Row, F> for S
50where
51 F: TyCon,
52 S: Send,
53 Row: SumApp<'a, F, Applied = S>,
54{
55 fn get_sum(self: Box<Self>) -> Box<Row::Applied>
56 where
57 F: TyCon,
58 Row: SumApp<'a, F>,
59 {
60 self
61 }
62
63 fn get_sum_borrow(&self) -> &Row::Applied
64 where
65 F: TyCon,
66 Row: SumApp<'a, F>,
67 {
68 self
69 }
70}
71
72impl<A, R> RowCon for (A, R) where R: RowCon {}
73
74impl RowCon for () {}
75
76impl ToRow for ()
77{
78 type Row = ();
79}
80
81impl<A, R> ToRow for (A, R)
82where
83 A: Send + 'static,
84 R: RowCon,
85{
86 type Row = (A, R);
87}
88
89impl<'a, F: 'a, A: 'a, R: 'a> SumApp<'a, F> for (A, R)
90where
91 F: TyCon,
92 R: RowCon,
93{
94 type Applied = Sum<App<'a, F, A>, AppSum<'a, R, F>>;
95}
96
97impl<'a, F> SumApp<'a, F> for ()
98where
99 F: TyCon,
100{
101 type Applied = Bottom;
102}
103
104impl<'a, F: 'a, A: 'a, R: 'a> FlattenSumApp<'a, F> for (A, R)
105where
106 R: FlattenSumApp<'a, F>,
107 F: TypeApp<'a, A>,
108{
109 type FlattenApplied = Sum<F::Applied, R::FlattenApplied>;
110
111 fn unflatten_sum(row1: Self::FlattenApplied) -> Self::Applied
112 {
113 match row1 {
114 Sum::Inl(field) => Sum::Inl(App::new(field)),
115 Sum::Inr(row2) => {
116 let row3 = R::unflatten_sum(row2);
117
118 Sum::Inr(AppSum::new(row3))
119 }
120 }
121 }
122
123 fn flatten_sum(row1: AppSum<'a, Self, F>) -> Self::FlattenApplied
124 {
125 match row1.get_sum() {
126 Sum::Inl(field1) => {
127 let field2 = field1.get_applied();
128
129 Sum::Inl(field2)
130 }
131 Sum::Inr(row2) => {
132 let row3 = R::flatten_sum(row2);
133
134 Sum::Inr(row3)
135 }
136 }
137 }
138}
139
140impl<'a, F> FlattenSumApp<'a, F> for ()
141where
142 F: TyCon,
143{
144 type FlattenApplied = Bottom;
145
146 fn unflatten_sum(row: Self::FlattenApplied) -> Self::Applied
147 {
148 row
149 }
150
151 fn flatten_sum(row: AppSum<Self, F>) -> Self::FlattenApplied
152 {
153 row.get_sum()
154 }
155}
156
157impl SumFunctor for ()
158{
159 fn lift_sum<'a, T: 'a, F1: 'a, F2: 'a>(
160 _lift: T,
161 row1: AppSum<'a, Self, F1>,
162 ) -> AppSum<'a, Self, F2>
163 where
164 F1: TyCon,
165 F2: TyCon,
166 T: NaturalTransformation<'a, F1, F2>,
167 {
168 absurd(row1)
169 }
170}
171
172impl<A, R> SumFunctor for (A, R)
173where
174 A: Send + 'static,
175 R: SumFunctor,
176{
177 fn lift_sum<'a, T: 'a, F1: 'a, F2: 'a>(
178 lift: T,
179 row1: AppSum<'a, Self, F1>,
180 ) -> AppSum<'a, Self, F2>
181 where
182 F1: TyCon,
183 F2: TyCon,
184 T: NaturalTransformation<'a, F1, F2>,
185 Self: 'a,
186 {
187 let row2 = row1.get_sum();
188
189 match row2 {
190 Sum::Inl(fa1) => {
191 let fa2 = lift.lift(fa1);
192
193 AppSum::new(Sum::Inl(fa2))
194 }
195 Sum::Inr(b) => AppSum::new(Sum::Inr(R::lift_sum::<T, F1, F2>(lift, b))),
196 }
197 }
198}
199
200impl<A, R> Prism<(A, R)> for ChoiceSelector<Z>
201where
202 A: Send,
203 R: RowCon,
204{
205 type Elem = A;
206
207 fn inject_elem<'a, F: 'a + Send>(
208 t: App<'a, F, Self::Elem>
209 ) -> AppSum<'a, (A, R), F>
210 where
211 F: TyCon,
212 (A, R): 'a,
213 {
214 AppSum::new(Sum::Inl(t))
215 }
216
217 fn extract_elem<'a, F: 'a + Send>(
218 row: AppSum<'a, (A, R), F>
219 ) -> Option<App<'a, F, Self::Elem>>
220 where
221 F: TyCon,
222 (A, R): 'a,
223 {
224 match row.get_sum() {
225 Sum::Inl(e) => Some(e),
226 Sum::Inr(_) => None,
227 }
228 }
229}
230
231impl<N, A, R> Prism<(A, R)> for ChoiceSelector<S<N>>
232where
233 R: RowCon,
234 A: Send + 'static,
235 ChoiceSelector<N>: Prism<R>,
236{
237 type Elem = <ChoiceSelector<N> as Prism<R>>::Elem;
238
239 fn inject_elem<'a, F: 'a + Send>(
240 elem: App<'a, F, Self::Elem>
241 ) -> AppSum<'a, (A, R), F>
242 where
243 F: TyCon,
244 (A, R): 'a,
245 {
246 AppSum::new(Sum::Inr(<ChoiceSelector<N> as Prism<R>>::inject_elem(elem)))
247 }
248
249 fn extract_elem<'a, F: 'a + Send>(
250 row: AppSum<'a, (A, R), F>
251 ) -> Option<App<'a, F, Self::Elem>>
252 where
253 F: TyCon,
254 (A, R): 'a,
255 {
256 match row.get_sum() {
257 Sum::Inl(_) => None,
258 Sum::Inr(rest) => <ChoiceSelector<N> as Prism<R>>::extract_elem(rest),
259 }
260 }
261}