1use crate::utils::ArgumentIterator;
2use ahash::HashMap;
3use std::iter::empty;
4use thiserror::Error;
5
6use super::{
7 ActorOrEvent, BinOp, Constant, Expr, ExprPool, ExprRef, LambdaParseError, LanguageExpression,
8 MonOp, Variable,
9};
10use crate::{
11 lambda::{
12 LambdaExpr, LambdaExprRef, LambdaLanguageOfThought, LambdaPool, ReductionError,
13 RootedLambdaPool, types::LambdaType,
14 },
15 language::parser::parse_lot,
16};
17
18impl From<ExprRef> for LambdaExprRef {
19 fn from(value: ExprRef) -> Self {
20 LambdaExprRef(value.0)
21 }
22}
23
24impl From<LambdaExprRef> for ExprRef {
25 fn from(value: LambdaExprRef) -> Self {
26 ExprRef(value.0)
27 }
28}
29
30#[derive(Debug, Clone, Error, PartialEq, Eq)]
31pub enum LambdaConversionError {
32 #[error("There are still lambda terms in this pool")]
33 StillHasLambdaTerms,
34 #[error("Reducing lambda exprs in quantifiers is leading to a bug ({0})")]
35 ReductionError(#[from] ReductionError),
36}
37
38impl<'a> LambdaLanguageOfThought for Expr<'a> {
39 type Pool = LanguageExpression<'a>;
40 type ConversionError = LambdaConversionError;
41
42 fn n_children(&self) -> usize {
43 match self {
44 Expr::Quantifier { .. } => 2,
45 Expr::Variable(_) => 0,
46 Expr::Actor(_) => 0,
47 Expr::Event(_) => 0,
48 Expr::Constant(_) => 0,
49 Expr::Binary(..) => 2,
50 Expr::Unary(..) => 1,
51 }
52 }
53
54 fn inc_depth(&self) -> bool {
55 matches!(
56 self,
57 Expr::Quantifier { .. } | Expr::Unary(MonOp::Iota(_), _)
58 )
59 }
60
61 fn var_type(&self) -> Option<&LambdaType> {
62 match self {
63 Expr::Quantifier { var_type, .. } | Expr::Unary(MonOp::Iota(var_type), _) => {
64 match var_type {
65 ActorOrEvent::Actor => Some(LambdaType::a()),
66 ActorOrEvent::Event => Some(LambdaType::e()),
67 }
68 }
69 _ => None,
70 }
71 }
72
73 fn get_children(&self) -> impl Iterator<Item = LambdaExprRef> {
74 match self {
75 Expr::Quantifier {
76 restrictor,
77 subformula,
78 ..
79 } => vec![restrictor, subformula],
80 Expr::Binary(_, x, y) => vec![x, y],
81 Expr::Unary(_, x) => vec![x],
82 Expr::Constant(_) | Expr::Actor(_) | Expr::Event(_) | Expr::Variable(_) => vec![],
83 }
84 .into_iter()
85 .map(|x| LambdaExprRef(x.0))
86 }
87
88 fn change_children(&mut self, mut new_children: impl Iterator<Item = LambdaExprRef>) {
89 match self {
90 Expr::Quantifier {
91 restrictor,
92 subformula,
93 ..
94 } => {
95 *restrictor = ExprRef(new_children.next().unwrap().0);
96 *subformula = ExprRef(new_children.next().unwrap().0);
97 }
98 Expr::Binary(_, x, y) => {
99 *x = ExprRef(new_children.next().unwrap().0);
100 *y = ExprRef(new_children.next().unwrap().0);
101 }
102 Expr::Unary(_, x) => {
103 *x = ExprRef(new_children.next().unwrap().0);
104 }
105 Expr::Variable(_) | Expr::Actor(_) | Expr::Event(_) | Expr::Constant(_) => (),
106 }
107 }
108
109 fn remap_refs(&mut self, remap: &[usize]) {
110 match self {
111 Expr::Quantifier {
112 restrictor,
113 subformula,
114 ..
115 } => {
116 *restrictor = ExprRef(remap[restrictor.0 as usize] as u32);
117 *subformula = ExprRef(remap[subformula.0 as usize] as u32);
118 }
119 Expr::Binary(_, x, y) => {
120 *x = ExprRef(remap[x.0 as usize] as u32);
121 *y = ExprRef(remap[y.0 as usize] as u32);
122 }
123 Expr::Unary(_, x) => {
124 *x = ExprRef(remap[x.0 as usize] as u32);
125 }
126 Expr::Variable(_) | Expr::Actor(_) | Expr::Event(_) | Expr::Constant(_) => (),
127 }
128 }
129
130 fn get_type(&self) -> &LambdaType {
131 match self {
132 Expr::Quantifier { .. } => LambdaType::t(),
133 Expr::Variable(Variable::Event(_)) => LambdaType::e(),
134 Expr::Variable(Variable::Actor(_)) => LambdaType::a(),
135 Expr::Actor(_) => LambdaType::a(),
136 Expr::Event(_) => LambdaType::e(),
137 Expr::Binary(bin, ..) => match bin {
138 BinOp::AgentOf | BinOp::PatientOf | BinOp::And | BinOp::Or => LambdaType::t(),
139 },
140 Expr::Unary(mon_op, _) => match mon_op {
141 MonOp::Property(_, _) | MonOp::Not => LambdaType::t(),
142 MonOp::Iota(ActorOrEvent::Actor) => LambdaType::a(),
143 MonOp::Iota(ActorOrEvent::Event) => LambdaType::e(),
144 },
145 Expr::Constant(constant) => match constant {
146 Constant::Everyone | Constant::Property(_, ActorOrEvent::Actor) => LambdaType::at(),
147 Constant::EveryEvent | Constant::Property(_, ActorOrEvent::Event) => {
148 LambdaType::et()
149 }
150 Constant::Contradiction | Constant::Tautology => LambdaType::t(),
151 },
152 }
153 }
154
155 fn to_pool(pool: RootedLambdaPool<Self>) -> Result<Self::Pool, Self::ConversionError> {
156 let processed_pool = pool
157 .pool
158 .0
159 .into_iter()
160 .map(|x| match x {
161 LambdaExpr::LanguageOfThoughtExpr(x) => Ok(x),
162 LambdaExpr::BoundVariable(x, LambdaType::A) => {
163 Ok(Expr::Variable(Variable::Actor(x as u32)))
164 }
165 LambdaExpr::BoundVariable(x, LambdaType::E) => {
166 Ok(Expr::Variable(Variable::Event(x as u32)))
167 }
168 _ => Err(LambdaConversionError::StillHasLambdaTerms),
169 })
170 .collect::<Result<Vec<_>, LambdaConversionError>>()?;
171
172 Ok(LanguageExpression {
173 pool: ExprPool(processed_pool),
174 start: ExprRef(pool.root.0),
175 })
176 }
177
178 fn get_arguments(&self) -> impl Iterator<Item = LambdaType> {
179 match self {
180 Expr::Quantifier {
181 var_type: ActorOrEvent::Actor,
182 ..
183 } => {
184 ArgumentIterator::A([LambdaType::t().clone(), LambdaType::t().clone()].into_iter())
185 }
186 Expr::Quantifier {
187 var_type: ActorOrEvent::Event,
188 ..
189 } => {
190 ArgumentIterator::A([LambdaType::t().clone(), LambdaType::t().clone()].into_iter())
191 }
192 Expr::Binary(b, _, _) => {
193 ArgumentIterator::B(b.get_argument_type().into_iter().cloned())
194 }
195 Expr::Unary(mon_op, _) => {
196 ArgumentIterator::C([mon_op.get_argument_type().clone()].into_iter())
197 }
198 Expr::Variable(Variable::Event(_))
199 | Expr::Variable(Variable::Actor(_))
200 | Expr::Actor(_)
201 | Expr::Event(_)
202 | Expr::Constant(_) => ArgumentIterator::D(empty()),
203 }
204 }
205}
206
207impl<'a> std::fmt::Display for RootedLambdaPool<'a, Expr<'a>> {
208 fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
209 let (string, _) = self.string(self.root(), VarContext::default(), false);
210 write!(f, "{string}")
211 }
212}
213
214static VARIABLENAMES: [&str; 26] = [
215 "x", "y", "z", "a", "b", "c", "d", "e", "f", "g", "h", "i", "j", "k", "l", "m", "n", "o", "p",
216 "q", "r", "s", "t", "u", "v", "w",
217];
218
219static TRUTHS: [&str; 2] = ["phi", "psi"];
220
221static PREDICATENAMES: [&str; 3] = ["P", "Q", "R"];
222
223static OTHERFUNCTIONS: [&str; 4] = ["M", "N", "G", "K"];
224
225pub fn to_var(x: usize, t: Option<&LambdaType>) -> String {
226 let var_names = match t {
227 Some(t) if t == LambdaType::t() => TRUTHS.as_slice(),
228 Some(t) if t.is_one_place_function() => PREDICATENAMES.as_slice(),
229 Some(t) if t.is_function() => OTHERFUNCTIONS.as_slice(),
230 _ => VARIABLENAMES.as_slice(),
231 };
232
233 if x < var_names.len() {
234 var_names[x].to_string()
235 } else {
236 format!("{}{}", var_names[x % var_names.len()], x / var_names.len())
237 }
238}
239
240#[derive(Debug, Clone, Eq, PartialEq, Default)]
241pub(super) struct VarContext {
242 vars: HashMap<usize, usize>,
243 predicates: HashMap<usize, usize>,
244 other_functions: HashMap<usize, usize>,
245 truths: HashMap<usize, usize>,
246 depth: usize,
247}
248
249impl VarContext {
250 fn get_map(&self, t: Option<&LambdaType>) -> &HashMap<usize, usize> {
251 match t {
252 Some(t) if t == LambdaType::t() => &self.truths,
253 Some(t) if t.is_one_place_function() => &self.predicates,
254 Some(t) if t.is_function() => &self.other_functions,
255 _ => &self.vars,
256 }
257 }
258 fn get_map_mut(&mut self, t: Option<&LambdaType>) -> &mut HashMap<usize, usize> {
259 match t {
260 Some(t) if t == LambdaType::t() => &mut self.truths,
261 Some(t) if t.is_one_place_function() => &mut self.predicates,
262 Some(t) if t.is_function() => &mut self.other_functions,
263 _ => &mut self.vars,
264 }
265 }
266
267 pub(super) fn inc_depth_q(self, t: ActorOrEvent) -> (Self, String) {
268 let t: LambdaType = t.into();
269 self.inc_depth(&t)
270 }
271
272 pub(super) fn inc_depth(mut self, t: &LambdaType) -> (Self, String) {
273 let d = self.depth;
274 let map = self.get_map_mut(Some(t));
275 let n_var = map.len();
276 map.insert(d, n_var);
277 self.depth += 1;
278 (self, to_var(n_var, Some(t)))
279 }
280
281 pub(super) fn lambda_var(&self, bvar: usize, t: &LambdaType) -> String {
282 to_var(
283 *self.get_map(Some(t)).get(&(self.depth - bvar - 1)).unwrap(),
284 Some(t),
285 )
286 }
287}
288
289impl<'a> From<LanguageExpression<'a>> for RootedLambdaPool<'a, Expr<'a>> {
290 fn from(value: LanguageExpression<'a>) -> Self {
291 RootedLambdaPool {
292 pool: LambdaPool::from(
293 value
294 .pool
295 .0
296 .iter()
297 .map(|x| LambdaExpr::LanguageOfThoughtExpr(*x))
298 .collect(),
299 ),
300 root: crate::lambda::LambdaExprRef(value.start.0),
301 }
302 }
303}
304
305#[derive(Debug, Copy, Clone, PartialEq, Eq)]
306pub(super) enum AssociativityData {
307 Lambda,
308 App,
309 Binom(BinOp),
310 Monop,
311}
312
313#[derive(Debug, Clone, Error, PartialEq, Eq)]
315pub enum ConjoiningError {
316 #[error("Can't conjoin {0} and {1}")]
318 MismatchingTypes(LambdaType, LambdaType),
319
320 #[error("Lambda type, {0} doesn't return a truth value")]
322 DoesntReturnT(LambdaType),
323
324 #[error("One of the operands causes problems in reduction: {0})")]
326 ReductionError(#[from] ReductionError),
327}
328
329fn who_raises_who<'a>(
330 a: RootedLambdaPool<'a, Expr<'a>>,
331 b: RootedLambdaPool<'a, Expr<'a>>,
332) -> Result<
333 (
334 RootedLambdaPool<'a, Expr<'a>>,
335 RootedLambdaPool<'a, Expr<'a>>,
336 ),
337 ConjoiningError,
338> {
339 let a_type = a.get_type().unwrap();
340 let b_type = b.get_type().unwrap();
341
342 let Ok(a_rhs) = a_type.rhs() else {
343 return Err(ConjoiningError::DoesntReturnT(a_type));
344 };
345 let Ok(b_rhs) = b_type.rhs() else {
346 return Err(ConjoiningError::DoesntReturnT(b_type));
347 };
348 if b_rhs != &LambdaType::T && a_rhs != &LambdaType::T {
349 return Err(ConjoiningError::DoesntReturnT(a_type));
350 }
351
352 if a_rhs != &b_type && b_rhs != &a_type {
353 Err(ConjoiningError::MismatchingTypes(a_type, b_type))
354 } else if a_rhs == &b_type {
355 Ok((a, b))
356 } else {
357 Ok((b, a))
358 }
359}
360
361impl<'a> RootedLambdaPool<'a, Expr<'a>> {
362 pub fn conjoin(self, other: Self) -> Result<Self, ConjoiningError> {
365 let self_type = self.get_type().unwrap();
366 let other_type = other.get_type().unwrap();
367 if self_type != other_type {
368 return Err(ConjoiningError::MismatchingTypes(self_type, other_type));
369 }
370
371 let Ok((lhs, rhs)) = self_type.split() else {
372 return Err(ConjoiningError::DoesntReturnT(self_type));
373 };
374
375 if rhs != &LambdaType::T {
376 return Err(ConjoiningError::DoesntReturnT(self_type));
377 }
378 let lhs = lhs.clone();
379
380 let combinator = RootedLambdaPool {
381 pool: LambdaPool(vec![
382 LambdaExpr::Lambda(LambdaExprRef(1), self_type.clone()),
383 LambdaExpr::Lambda(LambdaExprRef(2), other_type.clone()),
384 LambdaExpr::Lambda(LambdaExprRef(3), lhs.clone()),
385 LambdaExpr::LanguageOfThoughtExpr(Expr::Binary(BinOp::And, ExprRef(4), ExprRef(7))),
386 LambdaExpr::Application {
387 subformula: LambdaExprRef(5),
388 argument: LambdaExprRef(6),
389 },
390 LambdaExpr::BoundVariable(2, self_type),
391 LambdaExpr::BoundVariable(0, lhs.clone()),
392 LambdaExpr::Application {
393 subformula: LambdaExprRef(8),
394 argument: LambdaExprRef(9),
395 },
396 LambdaExpr::BoundVariable(1, other_type),
397 LambdaExpr::BoundVariable(0, lhs),
398 ]),
399 root: LambdaExprRef(0),
400 };
401
402 let mut conjoined = combinator.merge(self).unwrap().merge(other).unwrap();
403 conjoined.reduce()?;
404 Ok(conjoined)
405 }
406
407 pub fn raised_conjoin(self, other: Self) -> Result<Self, ConjoiningError> {
414 let (a, b) = who_raises_who(self, other)?;
415 let a_type = a.get_type().unwrap();
416 let b_type = b.get_type().unwrap();
417
418 let Ok(event) = a_type.lhs() else {
419 return Err(ConjoiningError::DoesntReturnT(a_type));
420 };
421
422 let Ok(e) = b_type.lhs() else {
423 return Err(ConjoiningError::DoesntReturnT(b_type));
424 };
425 let e = e.clone();
426 let event = event.clone();
427
428 let combinator = RootedLambdaPool {
429 pool: LambdaPool(vec![
430 LambdaExpr::Lambda(LambdaExprRef(1), a_type.clone()),
431 LambdaExpr::Lambda(LambdaExprRef(2), b_type.clone()),
432 LambdaExpr::Lambda(LambdaExprRef(3), event.clone()),
433 LambdaExpr::Lambda(LambdaExprRef(4), e.clone()),
434 LambdaExpr::LanguageOfThoughtExpr(Expr::Binary(
435 BinOp::And,
436 ExprRef(5),
437 ExprRef(10),
438 )),
439 LambdaExpr::Application {
440 subformula: LambdaExprRef(6),
441 argument: LambdaExprRef(9),
442 },
443 LambdaExpr::Application {
444 subformula: LambdaExprRef(7),
445 argument: LambdaExprRef(8),
446 },
447 LambdaExpr::BoundVariable(3, a_type),
448 LambdaExpr::BoundVariable(1, event),
449 LambdaExpr::BoundVariable(0, e.clone()),
450 LambdaExpr::Application {
451 subformula: LambdaExprRef(11),
452 argument: LambdaExprRef(12),
453 },
454 LambdaExpr::BoundVariable(2, b_type),
455 LambdaExpr::BoundVariable(0, e),
456 ]),
457 root: LambdaExprRef(0),
458 };
459
460 let mut conjoined = combinator.merge(a).unwrap().merge(b).unwrap();
461 conjoined.reduce()?;
462 Ok(conjoined)
463 }
464
465 pub fn parse(s: &'a str) -> Result<Self, LambdaParseError> {
467 parse_lot(s)
468 }
469
470 fn string(
471 &self,
472 expr: LambdaExprRef,
473 c: VarContext,
474 parent_is_app: bool,
475 ) -> (String, AssociativityData) {
476 match self.get(expr) {
477 LambdaExpr::Lambda(child, lambda_type) => {
478 let (c, var) = c.inc_depth(lambda_type);
479 (
480 format!(
481 "lambda {} {} {}",
482 lambda_type,
483 var,
484 self.string(*child, c, false).0
485 ),
486 AssociativityData::Lambda,
487 )
488 }
489 LambdaExpr::Application {
490 subformula,
491 argument,
492 } => {
493 let (sub, associative) = self.string(*subformula, c.clone(), true);
494 let (arg, _) = self.string(*argument, c, false); let mut s = match associative {
498 AssociativityData::Lambda | AssociativityData::Binom(_) => {
499 format!("({sub})({arg}")
500 }
501 AssociativityData::Monop => format!("{sub}({arg}"),
502 AssociativityData::App => format!("{sub}{arg}"),
503 };
504
505 if parent_is_app {
506 s.push_str(", ");
507 } else {
508 s.push(')');
509 }
510
511 (s, AssociativityData::App)
512 }
513 LambdaExpr::BoundVariable(bvar, lambda_type) => {
514 (c.lambda_var(*bvar, lambda_type), AssociativityData::Monop)
515 }
516 LambdaExpr::FreeVariable(fvar, t) => (format!("{fvar}#{t}"), AssociativityData::Monop),
517 LambdaExpr::LanguageOfThoughtExpr(x) => match x {
518 Expr::Variable(variable) => (
519 c.lambda_var(variable.id() as usize, variable.as_lambda_type()),
520 AssociativityData::Monop,
521 ),
522 Expr::Quantifier {
523 quantifier,
524 var_type,
525 restrictor,
526 subformula,
527 } => {
528 let (c, var_string) = c.inc_depth_q(*var_type);
529 let (restrictor, _) =
530 self.string(LambdaExprRef(restrictor.0), c.clone(), false);
531 let (subformula, _) = self.string(LambdaExprRef(subformula.0), c, false);
532 (
533 format!(
534 "{}{}({}, {restrictor}, {subformula})",
535 quantifier,
536 match var_type {
537 ActorOrEvent::Actor => "",
538 ActorOrEvent::Event => "_e",
539 },
540 var_string,
541 ),
542 AssociativityData::Monop,
543 )
544 }
545 Expr::Unary(MonOp::Iota(var_type), arg) => {
546 let (c, var_string) = c.inc_depth_q(*var_type);
547 let (arg, _) = self.string(LambdaExprRef(arg.0), c, false);
548 (
549 format!(
550 "iota{}({}, {arg})",
551 match var_type {
552 ActorOrEvent::Actor => "",
553 ActorOrEvent::Event => "_e",
554 },
555 var_string,
556 ),
557 AssociativityData::Monop,
558 )
559 }
560 Expr::Actor(a) => (format!("a_{a}"), AssociativityData::Monop),
561 Expr::Event(e) => (format!("e_{e}"), AssociativityData::Monop),
562 Expr::Binary(bin_op, x, y) => {
563 let (x, x_a) = self.string(LambdaExprRef(x.0), c.clone(), false);
564 let (y, y_a) = self.string(LambdaExprRef(y.0), c, false);
565 match bin_op {
566 BinOp::AgentOf | BinOp::PatientOf => {
567 (format!("{bin_op}({x}, {y})",), AssociativityData::Monop)
568 }
569
570 BinOp::And | BinOp::Or => (
571 {
572 let mut s = String::default();
573 if add_parenthesis_for_bin_op(*bin_op, x_a) {
574 s.push_str(&format!("({x})"))
575 } else {
576 s.push_str(&x)
577 };
578 s.push_str(&format!(" {bin_op} "));
579 if add_parenthesis_for_bin_op(*bin_op, y_a) {
580 s.push_str(&format!("({y})"))
581 } else {
582 s.push_str(&y)
583 };
584 s
585 },
586 AssociativityData::Binom(*bin_op),
587 ),
588 }
589 }
590 Expr::Unary(mon_op, arg) => {
591 let (arg, arg_binom) = self.string(LambdaExprRef(arg.0), c, false);
592 (
593 match mon_op {
594 MonOp::Not => match arg_binom {
595 AssociativityData::Binom(BinOp::And)
596 | AssociativityData::Binom(BinOp::Or) => format!("{mon_op}({arg})"),
597 AssociativityData::Binom(_)
598 | AssociativityData::Lambda
599 | AssociativityData::App
600 | AssociativityData::Monop => {
601 format!("{mon_op}{arg}")
602 }
603 },
604 _ => format!("{mon_op}({arg})"),
605 },
606 AssociativityData::Monop,
607 )
608 }
609 Expr::Constant(constant) => (format!("{constant}"), AssociativityData::Monop),
610 },
611 }
612 }
613}
614
615pub(super) fn add_parenthesis_for_bin_op(x: BinOp, data: AssociativityData) -> bool {
616 match data {
617 AssociativityData::Binom(b) => match b {
618 BinOp::AgentOf | BinOp::PatientOf => false,
619 BinOp::And | BinOp::Or if b == x => false,
620 BinOp::And | BinOp::Or => true,
621 },
622 AssociativityData::Lambda => true,
623 AssociativityData::App | AssociativityData::Monop => false,
624 }
625}
626
627#[cfg(test)]
628mod test {
629 use super::to_var;
630
631 use crate::lambda::{FreeVar, types::LambdaType};
632 use crate::{Entity, Scenario, ThetaRoles, lambda::RootedLambdaPool, parse_executable};
633
634 #[test]
635 fn fancy_printing() -> anyhow::Result<()> {
636 for statement in [
637 "~AgentOf(a_John, e_0)",
638 "pa_Red(a_John) & ~pa_Red(a_Mary)",
639 "every(x, all_a, pa_Blue(x))",
640 "every(x, pa_Blue, pa_Blue(x))",
641 "every(x, pa_5, pa_10(a_59))",
642 "every_e(x, all_e, PatientOf(a_Mary, x))",
643 ] {
644 println!("{statement}");
645 let expression = parse_executable(statement)?;
646 assert_eq!(expression.to_string(), statement);
647 }
648 for s in [
649 "cool#<a,t>(a_John)",
650 "bad#<a,t>(man#a)",
651 "woah#<<e,t>,t>(lambda e x pe_wow(x))",
652 "lambda <a,t> P lambda a x P(x)",
653 "lambda <a,t> P P(a_man) & ~P(a_woman)",
654 "loves#<a,<a,t>>(a_john, a_mary)",
655 "gives#<a,<a,<a,t>>>(a_john, a_mary, a_present)",
656 "lambda e x lambda a y loves#<e,<a,t>>(x, y)",
657 ] {
658 println!("{s}");
659 let p = RootedLambdaPool::parse(s)?;
660 assert_eq!(p.to_string(), s);
661 }
662
663 Ok(())
664 }
665
666 #[test]
667 fn type_checking() -> anyhow::Result<()> {
668 let john = RootedLambdaPool::parse("a_John")?;
669 let likes = RootedLambdaPool::parse(
670 "lambda a x ((lambda a y (some_e(e, all_e, AgentOf(x, e) & PatientOf(y, e) & pe_likes(e)))))",
671 )?;
672
673 let mary = RootedLambdaPool::parse("a_Mary")?;
674 let phi = mary.clone().merge(likes.clone()).unwrap();
675 let mut phi = phi.merge(john.clone()).unwrap();
676 phi.reduce()?;
677 let pool = phi.into_pool()?;
678 assert_eq!(
679 "some_e(x, all_e, AgentOf(a_Mary, x) & PatientOf(a_John, x) & pe_likes(x))",
680 pool.to_string()
681 );
682 let phi = likes.merge(mary).unwrap();
683 let mut phi = john.merge(phi).unwrap();
684 phi.reduce()?;
685 let pool = phi.into_pool()?;
686 assert_eq!(
687 "some_e(x, all_e, AgentOf(a_Mary, x) & PatientOf(a_John, x) & pe_likes(x))",
688 pool.to_string()
689 );
690 Ok(())
691 }
692
693 #[test]
694 fn var_name_assigner() {
695 assert_eq!(to_var(0, None), "x");
696 assert_eq!(to_var(1, None), "y");
697 assert_eq!(to_var(2, None), "z");
698 assert_eq!(to_var(26, None), "x1");
699 assert_eq!(to_var(27, None), "y1");
700 assert_eq!(to_var(28, None), "z1");
701 assert_eq!(to_var(26 * 300, None), "x300");
702 }
703
704 #[test]
705 fn printing() -> anyhow::Result<()> {
706 let pool = RootedLambdaPool::parse(
707 "some_e(x0, all_e, AgentOf(a_1, x0) & PatientOf(a_0, x0) & pe_0(x0))",
708 )?;
709 assert_eq!(
710 pool.to_string(),
711 "some_e(x, all_e, AgentOf(a_1, x) & PatientOf(a_0, x) & pe_0(x))"
712 );
713 let likes = RootedLambdaPool::parse(
714 "lambda e x lambda e y (some(e, all_a, AgentOf(e, x) & PatientOf(e, y) & pe_likes(y)))",
715 )?;
716
717 let s =
718 "lambda e x lambda e y some(z, all_a, AgentOf(z, x) & PatientOf(z, y) & pe_likes(y))";
719 assert_eq!(likes.to_string(), s,);
720 let likes2 = RootedLambdaPool::parse(s)?;
721 assert_eq!(likes, likes2);
722
723 Ok(())
724 }
725
726 #[test]
727 fn fancy_quantification_reduction() -> anyhow::Result<()> {
728 let pool = RootedLambdaPool::parse("every_e(x0,pe_0(x0) & pe_1(x0), pe_2(x0))")?;
729 let scenario = Scenario::new(
730 vec![],
731 vec![ThetaRoles::default(); 5],
732 [
733 ("0", vec![Entity::Event(1), Entity::Event(2)]),
734 ("1", vec![Entity::Event(0), Entity::Event(1)]),
735 ("2", vec![Entity::Event(1)]),
736 ]
737 .into_iter()
738 .collect(),
739 );
740
741 dbg!(&pool);
742 assert!(pool.into_pool()?.run(&scenario, None)?.try_into()?);
743
744 let pool = RootedLambdaPool::parse("every_e(x0, pe_0(x0) & pe_1(x0), pe_2(x0))")?;
745
746 let scenario = Scenario::new(
747 vec![],
748 vec![ThetaRoles::default(); 5],
749 [
750 ("0", vec![Entity::Event(1), Entity::Event(2)]),
751 ("1", vec![Entity::Event(0), Entity::Event(1)]),
752 ("2", vec![Entity::Event(1)]),
753 ]
754 .into_iter()
755 .collect(),
756 );
757
758 dbg!(&pool);
759 assert!(pool.into_pool()?.run(&scenario, None)?.try_into()?);
760
761 let pool =
762 RootedLambdaPool::parse("every_e(x, pe_laughs, every(y, pe_sleeps(x), pa_woman(y)))")?;
763 println!("{}", pool.into_pool()?);
764 Ok(())
765 }
766
767 #[test]
768 fn conjoining_check() -> anyhow::Result<()> {
769 let tall = RootedLambdaPool::parse("lambda a x pa_tall(x)")?;
770 let man = RootedLambdaPool::parse("lambda a x pa_man(x)")?;
771
772 let mut tall_man = tall.conjoin(man)?;
773 tall_man.reduce()?;
774 let weird = RootedLambdaPool::parse("weird#<a,t>")?;
775 let man = RootedLambdaPool::parse("lambda a x pa_man(x)")?;
776 let weird_man = weird.conjoin(man)?;
777 assert_eq!(format!("{tall_man}"), "lambda a x pa_tall(x) & pa_man(x)");
778 assert_eq!(
779 format!("{weird_man}"),
780 "lambda a x weird#<a,t>(x) & pa_man(x)"
781 );
782
783 let voice = RootedLambdaPool::parse("lambda a x lambda e y AgentOf(x, y)")?;
784 let run = RootedLambdaPool::parse("lambda e x pe_run(x)")?;
785
786 let mut agent_run = voice.raised_conjoin(run)?;
787 agent_run.reduce()?;
788 assert_eq!(
789 format!("{agent_run}"),
790 "lambda a x lambda e y AgentOf(x, y) & pe_run(y)"
791 );
792 let voice = RootedLambdaPool::parse("lambda a x lambda e y AgentOf(x, y)")?;
793 let run = RootedLambdaPool::parse("lambda e x pe_run(x)")?;
794
795 let mut agent_run = run.raised_conjoin(voice)?;
796 agent_run.reduce()?;
797 assert_eq!(
798 format!("{agent_run}"),
799 "lambda a x lambda e y AgentOf(x, y) & pe_run(y)"
800 );
801 Ok(())
802 }
803
804 #[test]
805 fn alpha_check() -> anyhow::Result<()> {
806 let everyone = RootedLambdaPool::parse("lambda <a,t> P (every(x, all_a, P(x)))")?;
807 let someone = RootedLambdaPool::parse("lambda <a,t> P (some(x, all_a, P(x)))")?;
808 let mut likes = RootedLambdaPool::parse(
809 "lambda a x (lambda a y (some_e(e, all_e, AgentOf(y, e)&pe_likes(e)&PatientOf(x, e))))",
810 )?;
811
812 likes.apply_new_free_variable(FreeVar::Anonymous(0))?;
813 let mut sentence = likes.merge(someone).unwrap();
814 sentence.lambda_abstract_free_variable(FreeVar::Anonymous(0), LambdaType::A, true)?;
815 let mut sentence = sentence.merge(everyone).unwrap();
816 sentence.reduce()?;
817 assert_eq!(
818 sentence.to_string(),
819 "every(x, all_a, some(y, all_a, some_e(z, all_e, AgentOf(y, z) & pe_likes(z) & PatientOf(x, z))))"
820 );
821
822 let everyone = RootedLambdaPool::parse("lambda <a,t> P (every(x, all_a, P(x)))")?;
823 let someone = RootedLambdaPool::parse("lambda <a,t> P (some(x, all_a, P(x)))")?;
824 let mut likes = RootedLambdaPool::parse(
825 "lambda a x (lambda a y ( some_e(e, all_e, AgentOf(y, e)&pe_likes(e)&PatientOf(x, e)) | some(w, all_a, every_e(e, all_e, AgentOf(y, e)&pe_likes(e)&PatientOf(x, e)))))",
826 )?;
827
828 likes.apply_new_free_variable(FreeVar::Anonymous(0))?;
829 let mut sentence = likes.merge(someone).unwrap();
830 sentence.lambda_abstract_free_variable(FreeVar::Anonymous(0), LambdaType::A, true)?;
831 let mut sentence = sentence.merge(everyone).unwrap();
832 sentence.reduce()?;
833 assert_eq!(
834 sentence.to_string(),
835 "every(x, all_a, some(y, all_a, some_e(z, all_e, AgentOf(y, z) & pe_likes(z) & PatientOf(x, z)) | some(z, all_a, every_e(a, all_e, AgentOf(y, a) & pe_likes(a) & PatientOf(x, a)))))"
836 );
837 Ok(())
838 }
839}