simple_semantics/language/
lambda_implementation.rs

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///An error which results from a failed application of [`RootedLambdaPool::conjoin`]
314#[derive(Debug, Clone, Error, PartialEq, Eq)]
315pub enum ConjoiningError {
316    ///Both arguments have to have the same type
317    #[error("Can't conjoin {0} and {1}")]
318    MismatchingTypes(LambdaType, LambdaType),
319
320    ///The type must return a truth value
321    #[error("Lambda type, {0} doesn't return a truth value")]
322    DoesntReturnT(LambdaType),
323
324    ///One of the arguments has an internal problem leading to reduction errors
325    #[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    ///Takes two lambda expressions, phi and psi of type <x, t> where x is any type and returns phi
363    ///AND psi.
364    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    ///Takes two lambda expressions, phi <x, <y,t>> and psi of type <y, t> where x and y is any type and returns phi
408    ///AND psi.
409    ///
410    ///This is a generalized kind of Event Identification from Kratzer (1996)
411    ///
412    /// - Kratzer, A. (1996). Severing the External Argument from its Verb. In J. Rooryck & L. Zaring (Eds.), Phrase Structure and the Lexicon (pp. 109–137). Springer Netherlands. https://doi.org/10.1007/978-94-015-8617-7_5
413    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    ///Create a [`RootedLambdaPool<Expr>`] from a string.
466    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); // false
495                // since apps only collapse if they're a left chain
496
497                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}