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