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

simple_semantics/language/
serializations.rs
