simple_semantics/language/
serializations.rs

1use serde::{Deserialize, Deserializer, Serialize};
2
3use crate::{
4    lambda::{FreeVar, LambdaExpr, LambdaExprRef, RootedLambdaPool, types::LambdaType},
5    language::{
6        ActorOrEvent, BinOp, Expr, MonOp,
7        lambda_implementation::{AssociativityData, add_parenthesis_for_bin_op},
8    },
9};
10
11use crate::language::lambda_implementation::VarContext;
12
13impl Serialize for LambdaType {
14    fn serialize<S>(&self, serializer: S) -> Result<S::Ok, S::Error>
15    where
16        S: serde::Serializer,
17    {
18        serializer.serialize_str(self.to_string().as_str())
19    }
20}
21
22impl<'de> Deserialize<'de> for LambdaType {
23    fn deserialize<D>(deserializer: D) -> Result<Self, D::Error>
24    where
25        D: Deserializer<'de>,
26    {
27        let s = String::deserialize(deserializer)?;
28        LambdaType::from_string(&s).map_err(serde::de::Error::custom)
29    }
30}
31impl<'src> Serialize for RootedLambdaPool<'src, Expr<'src>> {
32    fn serialize<S>(&self, serializer: S) -> Result<S::Ok, S::Error>
33    where
34        S: serde::Serializer,
35    {
36        serializer.serialize_str(self.to_string().as_str())
37    }
38}
39impl<'de, 'a> Deserialize<'de> for RootedLambdaPool<'a, Expr<'a>>
40where
41    'de: 'a,
42{
43    fn deserialize<D>(deserializer: D) -> Result<Self, D::Error>
44    where
45        D: Deserializer<'de>,
46    {
47        let s = <&'de str>::deserialize(deserializer)?;
48        RootedLambdaPool::parse(s).map_err(serde::de::Error::custom)
49    }
50}
51
52impl RootedLambdaPool<'_, Expr<'_>> {
53    #[allow(clippy::too_many_lines)]
54    pub(super) fn tokens<'a, 'b: 'a>(
55        &'a self,
56        expr: LambdaExprRef,
57        c: VarContext,
58        v: &mut Vec<Token<'a>>,
59        parent_is_app: bool,
60    ) -> AssociativityData {
61        match self.get(expr) {
62            LambdaExpr::Lambda(child, lambda_type) => {
63                let (c, var) = c.inc_depth(lambda_type);
64                v.push(Token::Lambda {
65                    t: lambda_type,
66                    var: TokenVar::Bound(var),
67                });
68
69                self.tokens(*child, c, v, false);
70                AssociativityData::Lambda
71            }
72            LambdaExpr::BoundVariable(bvar, lambda_type) => {
73                v.push(Token::Var(TokenVar::Bound(
74                    c.lambda_var(*bvar, lambda_type),
75                )));
76                AssociativityData::Monop
77            }
78            LambdaExpr::FreeVariable(fvar, t) => {
79                v.push(Token::Var(TokenVar::Free {
80                    label: fvar.to_string(),
81                    t,
82                    anon: match fvar {
83                        FreeVar::Named(_) => false,
84                        FreeVar::Anonymous(_) => true,
85                    },
86                }));
87                AssociativityData::Monop
88            }
89
90            LambdaExpr::Application {
91                subformula,
92                argument,
93            } => {
94                let mut new_v = vec![];
95
96                match self.tokens(*subformula, c.clone(), &mut new_v, true) {
97                    AssociativityData::Binom(_) | AssociativityData::Lambda => {
98                        v.push(Token::OpenDelim);
99                        v.extend(new_v);
100                        v.push(Token::CloseDelim);
101                        v.push(Token::OpenDelim);
102                    }
103                    AssociativityData::Monop => {
104                        v.extend(new_v);
105                        v.push(Token::OpenDelim);
106                    }
107                    AssociativityData::App => {
108                        v.extend(new_v);
109                    }
110                }
111                self.tokens(*argument, c.clone(), v, false);
112
113                if parent_is_app {
114                    v.push(Token::ArgSep);
115                } else {
116                    v.push(Token::CloseDelim);
117                }
118                AssociativityData::App
119            }
120            LambdaExpr::LanguageOfThoughtExpr(x) => match x {
121                Expr::Quantifier {
122                    quantifier,
123                    var_type,
124                    restrictor,
125                    subformula,
126                } => {
127                    let (c, var_string) = c.inc_depth_q(*var_type);
128
129                    v.push(Token::Quantifier {
130                        q: quantifier.to_string(),
131                        t: match var_type {
132                            ActorOrEvent::Actor => LambdaType::a(),
133                            ActorOrEvent::Event => LambdaType::e(),
134                        },
135                        var: TokenVar::Bound(var_string),
136                    });
137                    v.push(Token::OpenDelim);
138                    self.tokens(LambdaExprRef(restrictor.0), c.clone(), v, false);
139                    v.push(Token::ArgSep);
140                    self.tokens(LambdaExprRef(subformula.0), c, v, false);
141                    v.push(Token::CloseDelim);
142                    AssociativityData::Monop
143                }
144                Expr::Unary(MonOp::Iota(var_type), subformula) => {
145                    let (c, var_string) = c.inc_depth_q(*var_type);
146
147                    v.push(Token::Iota {
148                        t: match var_type {
149                            ActorOrEvent::Actor => LambdaType::a(),
150                            ActorOrEvent::Event => LambdaType::e(),
151                        },
152                        var: TokenVar::Bound(var_string),
153                    });
154                    v.push(Token::OpenDelim);
155                    self.tokens(LambdaExprRef(subformula.0), c, v, false);
156                    v.push(Token::CloseDelim);
157                    AssociativityData::Monop
158                }
159                Expr::Variable(variable) => {
160                    v.push(Token::Var(TokenVar::Bound(c.lambda_var(
161                        variable.id() as usize,
162                        variable.as_lambda_type(),
163                    ))));
164                    AssociativityData::Monop
165                }
166                Expr::Actor(a) => {
167                    v.push(Token::Actor(a.to_string()));
168                    AssociativityData::Monop
169                }
170                Expr::Event(e) => {
171                    v.push(Token::Event(e.to_string()));
172                    AssociativityData::Monop
173                }
174                Expr::Binary(bin_op, x, y) => match bin_op {
175                    BinOp::AgentOf | BinOp::PatientOf => {
176                        v.push(Token::Func(bin_op.to_string()));
177                        v.push(Token::OpenDelim);
178                        self.tokens(LambdaExprRef(x.0), c.clone(), v, false);
179                        v.push(Token::ArgSep);
180                        self.tokens(LambdaExprRef(y.0), c, v, false);
181                        v.push(Token::CloseDelim);
182                        AssociativityData::Monop
183                    }
184
185                    BinOp::And | BinOp::Or => {
186                        let mut x_v = vec![];
187                        let x_a = self.tokens(LambdaExprRef(x.0), c.clone(), &mut x_v, false);
188                        let mut y_v = vec![];
189                        let y_a = self.tokens(LambdaExprRef(y.0), c.clone(), &mut y_v, false);
190
191                        if add_parenthesis_for_bin_op(*bin_op, x_a) {
192                            v.push(Token::OpenDelim);
193                            v.extend(x_v);
194                            v.push(Token::CloseDelim);
195                        } else {
196                            v.extend(x_v);
197                        }
198                        v.push(Token::Func(bin_op.to_string()));
199                        if add_parenthesis_for_bin_op(*bin_op, y_a) {
200                            v.push(Token::OpenDelim);
201                            v.extend(y_v);
202                            v.push(Token::CloseDelim);
203                        } else {
204                            v.extend(y_v);
205                        }
206                        AssociativityData::Binom(*bin_op)
207                    }
208                },
209                Expr::Unary(mon_op, arg) => {
210                    let s = match mon_op {
211                        super::MonOp::Property(s, _) => s.to_string(),
212                        super::MonOp::Iota(_) | super::MonOp::Not => mon_op.to_string(),
213                    };
214                    v.push(Token::Func(s));
215
216                    let mut new_v = vec![];
217                    let child_asso = self.tokens(LambdaExprRef(arg.0), c, &mut new_v, false);
218
219                    if mon_op == &MonOp::Not {
220                        match child_asso {
221                            AssociativityData::Binom(BinOp::And | BinOp::Or) => {
222                                v.push(Token::OpenDelim);
223                                v.extend(new_v);
224                                v.push(Token::CloseDelim);
225                            }
226                            AssociativityData::Binom(_)
227                            | AssociativityData::Lambda
228                            | AssociativityData::App
229                            | AssociativityData::Monop => {
230                                v.extend(new_v);
231                            }
232                        }
233                    } else {
234                        v.push(Token::OpenDelim);
235                        v.extend(new_v);
236                        v.push(Token::CloseDelim);
237                    }
238
239                    AssociativityData::Monop
240                }
241                Expr::Constant(constant) => {
242                    let s = match constant {
243                        super::Constant::Everyone
244                        | super::Constant::EveryEvent
245                        | super::Constant::Tautology
246                        | super::Constant::Contradiction => constant.to_string(),
247                        super::Constant::Property(s, _) => s.to_string(),
248                    };
249                    v.push(Token::Const(s));
250                    AssociativityData::Monop
251                }
252            },
253        }
254    }
255}
256
257#[derive(Debug, Clone, Serialize)]
258pub(super) enum TokenVar<'a> {
259    Bound(String),
260    Free {
261        label: String,
262        t: &'a LambdaType,
263        anon: bool,
264    },
265}
266
267#[derive(Debug, Clone, Serialize)]
268pub(super) enum Token<'a> {
269    Lambda {
270        t: &'a LambdaType,
271        var: TokenVar<'a>,
272    },
273    Var(TokenVar<'a>),
274    Actor(String),
275    Event(String),
276    Func(String),
277    Const(String),
278    Iota {
279        t: &'a LambdaType,
280        var: TokenVar<'a>,
281    },
282    Quantifier {
283        q: String,
284        var: TokenVar<'a>,
285        t: &'a LambdaType,
286    },
287    OpenDelim,
288    ArgSep,
289    CloseDelim,
290}
291
292///A special kind of `RootedLambdaPool` that should be used to display in fancy math modes, e.g. with
293///Typst or (potentially) LaTeX.
294pub struct MathModeExpression<'a>(Vec<Token<'a>>);
295
296impl<'src> RootedLambdaPool<'src, Expr<'src>> {
297    ///Get a [`MathModeExpression`] to be serialized for documents.
298    #[must_use]
299    pub fn for_document(&self) -> MathModeExpression<'_> {
300        let mut v: Vec<Token> = vec![];
301        self.tokens(self.root, VarContext::default(), &mut v, false);
302        MathModeExpression(v)
303    }
304}
305
306impl Serialize for MathModeExpression<'_> {
307    fn serialize<S>(&self, serializer: S) -> Result<S::Ok, S::Error>
308    where
309        S: serde::Serializer,
310    {
311        self.0.serialize(serializer)
312    }
313}
314
315#[cfg(test)]
316mod test {
317
318    use crate::lambda::{RootedLambdaPool, types::LambdaType};
319
320    #[test]
321    fn type_serializing() -> anyhow::Result<()> {
322        for s in ["a", "<a,t>", "<<e,<e,<<a,t>,t>>>, t>"] {
323            let t = LambdaType::from_string(s)?;
324            let t_str = serde_json::to_string(&t)?;
325            let t_json: LambdaType = serde_json::from_str(t_str.as_str())?;
326            assert_eq!(t, t_json);
327        }
328
329        Ok(())
330    }
331
332    #[test]
333    fn serializing() -> anyhow::Result<()> {
334        for (statement, json) in [
335            (
336                "~(AgentOf(a_John,e_0))",
337                "[{\"Func\":\"~\"},{\"Func\":\"AgentOf\"},\"OpenDelim\",{\"Actor\":\"John\"},\"ArgSep\",{\"Event\":\"0\"},\"CloseDelim\"]",
338            ),
339            (
340                "(pa_Red(a_John) & ~(pa_Red(a_Mary)))",
341                "[{\"Func\":\"Red\"},\"OpenDelim\",{\"Actor\":\"John\"},\"CloseDelim\",{\"Func\":\"&\"},{\"Func\":\"~\"},{\"Func\":\"Red\"},\"OpenDelim\",{\"Actor\":\"Mary\"},\"CloseDelim\"]",
342            ),
343            (
344                "every(x,all_a,pa_Blue(x))",
345                "[{\"Quantifier\":{\"q\":\"every\",\"var\":{\"Bound\":\"x\"},\"t\":\"a\"}},\"OpenDelim\",{\"Const\":\"all_a\"},\"ArgSep\",{\"Func\":\"Blue\"},\"OpenDelim\",{\"Var\":{\"Bound\":\"x\"}},\"CloseDelim\",\"CloseDelim\"]",
346            ),
347            (
348                "every(x,pa_Blue,pa_Blue(x))",
349                "[{\"Quantifier\":{\"q\":\"every\",\"var\":{\"Bound\":\"x\"},\"t\":\"a\"}},\"OpenDelim\",{\"Const\":\"Blue\"},\"ArgSep\",{\"Func\":\"Blue\"},\"OpenDelim\",{\"Var\":{\"Bound\":\"x\"}},\"CloseDelim\",\"CloseDelim\"]",
350            ),
351            (
352                "every(x,pa_5,pa_10(a_59))",
353                "[{\"Quantifier\":{\"q\":\"every\",\"var\":{\"Bound\":\"x\"},\"t\":\"a\"}},\"OpenDelim\",{\"Const\":\"5\"},\"ArgSep\",{\"Func\":\"10\"},\"OpenDelim\",{\"Actor\":\"59\"},\"CloseDelim\",\"CloseDelim\"]",
354            ),
355            (
356                "every_e(x,all_e,PatientOf(a_Mary,x))",
357                "[{\"Quantifier\":{\"q\":\"every\",\"var\":{\"Bound\":\"x\"},\"t\":\"e\"}},\"OpenDelim\",{\"Const\":\"all_e\"},\"ArgSep\",{\"Func\":\"PatientOf\"},\"OpenDelim\",{\"Actor\":\"Mary\"},\"ArgSep\",{\"Var\":{\"Bound\":\"x\"}},\"CloseDelim\",\"CloseDelim\"]",
358            ),
359            (
360                "(cool#<a,t>)(a_John)",
361                "[{\"Var\":{\"Free\":{\"label\":\"cool\",\"t\":\"<a,t>\",\"anon\":false}}},\"OpenDelim\",{\"Actor\":\"John\"},\"CloseDelim\"]",
362            ),
363            (
364                "(bad#<a,t>)(man#a)",
365                "[{\"Var\":{\"Free\":{\"label\":\"bad\",\"t\":\"<a,t>\",\"anon\":false}}},\"OpenDelim\",{\"Var\":{\"Free\":{\"label\":\"man\",\"t\":\"a\",\"anon\":false}}},\"CloseDelim\"]",
366            ),
367            (
368                "((loves#<a,<a,t>>)(a_mary))(a_john)",
369                "[{\"Var\":{\"Free\":{\"label\":\"loves\",\"t\":\"<a,<a,t>>\",\"anon\":false}}},\"OpenDelim\",{\"Actor\":\"mary\"},\"ArgSep\",{\"Actor\":\"john\"},\"CloseDelim\"]",
370            ),
371            (
372                "True | (True & False)",
373                "[{\"Const\":\"True\"},{\"Func\":\"|\"},\"OpenDelim\",{\"Const\":\"True\"},{\"Func\":\"&\"},{\"Const\":\"False\"},\"CloseDelim\"]",
374            ),
375            (
376                "(True | True) & False",
377                "[\"OpenDelim\",{\"Const\":\"True\"},{\"Func\":\"|\"},{\"Const\":\"True\"},\"CloseDelim\",{\"Func\":\"&\"},{\"Const\":\"False\"}]",
378            ),
379            (
380                "lambda a x (lambda a y (likes#<a,<a,t>>(x))(y))",
381                "[{\"Lambda\":{\"t\":\"a\",\"var\":{\"Bound\":\"x\"}}},{\"Lambda\":{\"t\":\"a\",\"var\":{\"Bound\":\"y\"}}},{\"Var\":{\"Free\":{\"label\":\"likes\",\"t\":\"<a,<a,t>>\",\"anon\":false}}},\"OpenDelim\",{\"Var\":{\"Bound\":\"x\"}},\"ArgSep\",{\"Var\":{\"Bound\":\"y\"}},\"CloseDelim\"]",
382            ),
383            (
384                "lambda <a,t> P iota(x, P(x))",
385                "[{\"Lambda\":{\"t\":\"<a,t>\",\"var\":{\"Bound\":\"P\"}}},{\"Iota\":{\"t\":\"a\",\"var\":{\"Bound\":\"x\"}}},\"OpenDelim\",{\"Var\":{\"Bound\":\"P\"}},\"OpenDelim\",{\"Var\":{\"Bound\":\"x\"}},\"CloseDelim\",\"CloseDelim\"]",
386            ),
387        ] {
388            let expression = RootedLambdaPool::parse(statement)?;
389            assert_eq!(json, serde_json::to_string(&expression.for_document())?);
390        }
391
392        Ok(())
393    }
394}
simple_semantics/language/serializations.rs

simple_semantics/language/
serializations.rs
