simple_semantics/
lambda.rs

1//! The module that defines the basic lambda calculus used to compose expressions in the langauge
2//! of thought.
3
4use crate::utils::ArgumentIterator;
5use serde::{Deserialize, Serialize};
6use smallvec::{SmallVec, smallvec};
7use std::{
8    cmp::Ordering,
9    collections::{HashSet, VecDeque},
10    fmt::{Debug, Display},
11    hash::Hash,
12    iter::empty,
13    marker::PhantomData,
14};
15use thiserror::Error;
16
17pub mod types;
18use types::{LambdaType, TypeError};
19
20pub(crate) type Bvar = usize;
21
22///Errors resulting from interacting with a lambda calculus expression.
23#[derive(Debug, Clone, Error, PartialEq, Eq)]
24pub enum LambdaError {
25    ///A function application which violates the type system
26    #[error("The free variable has type {free_var} while the argument is {arg}")]
27    BadFreeVariableApp {
28        ///The type of the free variable involved
29        free_var: LambdaType,
30        ///The argument applied to a free variable.
31        arg: LambdaType,
32    },
33    ///A free variable that violates the type sytem
34    #[error("The free variable has type {free_var} while its lambda takes {lambda}")]
35    BadFreeVariable {
36        ///The type of the free variable involved
37        free_var: LambdaType,
38        ///The argument applied to a free variable.
39        lambda: LambdaType,
40    },
41
42    ///An internally caused error if `DeBruijn` indices are invalid.
43    #[error(
44        "A bound variable {var:?} cannot have a DeBruijn index higher than its lambda depth ({depth})"
45    )]
46    BadBoundVariable {
47        ///The `DeBruijn` index
48        var: LambdaExprRef,
49        ///The depth of the expression
50        depth: usize,
51    },
52
53    ///Any internal type error.
54    #[error("Expression has type error ({0})")]
55    TypeError(#[from] TypeError),
56
57    ///An error caused by a failed reduction
58    #[error("Failed reduction: {0}")]
59    ReductionError(#[from] ReductionError),
60}
61
62///A conversion error used when converting to a [`RootedLambdaPool`] from a [`Vec<Option<LambdaExpr>>`]
63#[derive(Debug, Clone, Error, PartialEq, Eq)]
64pub enum LambdaTryFromError {
65    ///This error happens if the vector is not exclusively [`Some`].
66    #[error("The vec contains None")]
67    HasNone,
68}
69
70///An error from a faulty reduction
71#[derive(Debug, Clone, Error, PartialEq, Eq)]
72pub enum ReductionError {
73    ///A invalid reference to a [`LambdaExpr`] is passed.
74    #[error("{0:?} is not a valid ref!")]
75    NotValidRef(LambdaExprRef),
76    ///A reference to a [`LambdaExpr`] which is not an application is passed
77    #[error("{0:?} is not an application!")]
78    NotApplication(LambdaExprRef),
79
80    ///An application that doesn't apply a lambda expression
81    #[error("The left hand side of the application ({app:?}), {lhs:?} is not a lambda expression!")]
82    NotLambdaInApplication {
83        ///The entire application
84        app: LambdaExprRef,
85        ///The left hand side of the application, which should be but isn't a lambda expression
86        lhs: LambdaExprRef,
87    },
88
89    ///Any general malformed types.
90    #[error("Incorrect types: {0}")]
91    TypeError(#[from] TypeError),
92}
93
94///An index to a [`LambdaExpr`] in the lambda pool.
95#[derive(Debug, Clone, Copy, Eq, PartialEq, Hash, PartialOrd, Ord, Serialize, Deserialize)]
96pub struct LambdaExprRef(pub u32);
97
98impl LambdaExprRef {
99    pub(crate) fn new(x: usize) -> Self {
100        LambdaExprRef(u32::try_from(x).expect("Reference is too high!"))
101    }
102}
103
104///A trait which allows one to define a language of thought that interacts with the lambda
105///calculus. An example implementation can be found for [`crate::language::Expr`].
106pub trait LambdaLanguageOfThought {
107    ///The type of the executable syntax tree
108    type Pool;
109    ///Error for converting from [`RootedLambdaPool<T>`] to [`LambdaLanguageOfThought::Pool`]
110    type ConversionError;
111
112    ///Given an expression, get an iterator of its children
113    fn get_children(&self) -> impl Iterator<Item = LambdaExprRef>;
114
115    ///Update the references such that `LambdaExprRef(0)` is remapped to `LambdaExprRef(remap[0])`.
116    ///(Used in garbage collection).
117    fn remap_refs(&mut self, remap: &[u32]);
118
119    ///Returns true if this is somewhere that can bind variables (e.g. should we increment debruijn
120    ///indices
121    fn inc_depth(&self) -> bool;
122
123    ///Returns the type of the bound variable at an instruction
124    fn var_type(&self) -> Option<&LambdaType>;
125
126    ///Given a list of new references for all children of an expr, change its children.
127    fn change_children(&mut self, new_children: impl Iterator<Item = LambdaExprRef>);
128
129    ///Get the number of children of an expression.
130    fn n_children(&self) -> usize;
131
132    ///Get the return type of an expression.
133    fn get_type(&self) -> &LambdaType;
134
135    ///Get the type of all children in order.
136    fn get_arguments(&self) -> impl Iterator<Item = LambdaType>;
137
138    ///Checks whether an expression is commutative
139    fn commutative(&self) -> bool {
140        false
141    }
142
143    ///Checks if two expressions are the same, *ignoring* their subtrees (so different children
144    ///shouldn't matter)
145    fn same_expr(&self, other: &Self) -> bool;
146
147    ///Provides the lexicographic ordering of two expressions (ignoring children)
148    fn cmp_expr(&self, other: &Self) -> std::cmp::Ordering;
149
150    ///Convert from a [`RootedLambdaPool<T>`] to [`LambdaLanguageOfThought::Pool`]. May return an
151    ///error if there are any lambda terms left in the [`RootedLambdaPool<T>`] (e.g. not fully
152    ///reduced).
153    ///
154    ///# Errors
155    ///Returns a [`ConversionError`] if the pool cannot be converted for some reason (usually
156    ///unreduced lambda types)
157    fn to_pool(pool: RootedLambdaPool<Self>) -> Result<Self::Pool, Self::ConversionError>
158    where
159        Self: Sized;
160}
161
162impl LambdaLanguageOfThought for () {
163    type Pool = ();
164    type ConversionError = ();
165    fn get_children(&self) -> impl Iterator<Item = LambdaExprRef> {
166        std::iter::empty()
167    }
168
169    fn n_children(&self) -> usize {
170        0
171    }
172
173    fn var_type(&self) -> Option<&LambdaType> {
174        None
175    }
176
177    fn same_expr(&self, _other: &Self) -> bool {
178        true
179    }
180
181    fn remap_refs(&mut self, _: &[u32]) {}
182
183    fn change_children(&mut self, _: impl Iterator<Item = LambdaExprRef>) {}
184
185    fn get_type(&self) -> &LambdaType {
186        unimplemented!()
187    }
188
189    fn inc_depth(&self) -> bool {
190        false
191    }
192
193    fn get_arguments(&self) -> impl Iterator<Item = LambdaType> {
194        empty()
195    }
196
197    fn to_pool(_: RootedLambdaPool<Self>) -> Result<Self::Pool, ()> {
198        Ok(())
199    }
200
201    fn cmp_expr(&self, _other: &Self) -> std::cmp::Ordering {
202        Ordering::Equal
203    }
204}
205
206///A free variable which can either be named or refered to by a integer.
207#[derive(Debug, Clone, Copy, Eq, PartialEq, Hash, PartialOrd, Ord, Serialize, Deserialize)]
208pub enum FreeVar<'a> {
209    ///A labeled free variable
210    #[serde(borrow)]
211    Named(&'a str),
212    ///An anonymous free variable defined by an index.
213    Anonymous(usize),
214}
215
216impl Display for FreeVar<'_> {
217    fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
218        match self {
219            FreeVar::Named(s) => write!(f, "{s}"),
220            FreeVar::Anonymous(t) => write!(f, "{t}"),
221        }
222    }
223}
224
225impl<'a> From<&'a str> for FreeVar<'a> {
226    fn from(value: &'a str) -> Self {
227        FreeVar::Named(value)
228    }
229}
230
231impl From<usize> for FreeVar<'_> {
232    fn from(value: usize) -> Self {
233        FreeVar::Anonymous(value)
234    }
235}
236
237#[derive(Debug, Clone, Eq, PartialEq, Hash, PartialOrd, Ord, Serialize, Deserialize)]
238///The core expression type of a lambda term
239pub enum LambdaExpr<'a, T> {
240    ///A lambda of a given type.
241    Lambda(LambdaExprRef, LambdaType),
242    ///A variable bound by a lambda, labeled by its [De Bruijn index](https://en.wikipedia.org/wiki/De_Bruijn_index).
243    BoundVariable(Bvar, LambdaType),
244    ///A free variable (may be named or anonymous, see [`FreeVar`]).
245    FreeVariable(#[serde(borrow)] FreeVar<'a>, LambdaType),
246    ///The application of an argument to a function
247    Application {
248        ///The body of the function
249        subformula: LambdaExprRef,
250
251        ///The argument of the function
252        argument: LambdaExprRef,
253    },
254    ///Any expression which is not part of the lambda calculus directly (e.g. primitives). See
255    ///[`crate::Expr`] for an example.
256    LanguageOfThoughtExpr(T),
257}
258
259impl<T: LambdaLanguageOfThought> LambdaExpr<'_, T> {
260    pub(crate) fn var_type(&self) -> Option<&LambdaType> {
261        match self {
262            LambdaExpr::Lambda(_, lambda_type) => Some(lambda_type),
263            LambdaExpr::LanguageOfThoughtExpr(e) => e.var_type(),
264            LambdaExpr::BoundVariable(..)
265            | LambdaExpr::FreeVariable(..)
266            | LambdaExpr::Application { .. } => None,
267        }
268    }
269    pub(crate) fn inc_depth(&self) -> bool {
270        match self {
271            LambdaExpr::Lambda(..) => true,
272            LambdaExpr::LanguageOfThoughtExpr(e) => e.inc_depth(),
273            LambdaExpr::BoundVariable(..)
274            | LambdaExpr::FreeVariable(..)
275            | LambdaExpr::Application { .. } => false,
276        }
277    }
278
279    pub(crate) fn commutative(&self) -> bool {
280        match self {
281            LambdaExpr::LanguageOfThoughtExpr(e) => e.commutative(),
282            LambdaExpr::Lambda(..)
283            | LambdaExpr::BoundVariable(..)
284            | LambdaExpr::FreeVariable(..)
285            | LambdaExpr::Application { .. } => false,
286        }
287    }
288}
289
290#[derive(Debug, Clone)]
291///A lambda expression with its root defined.
292pub struct RootedLambdaPool<'src, T: LambdaLanguageOfThought> {
293    pub(crate) pool: LambdaPool<'src, T>,
294    pub(crate) root: LambdaExprRef,
295}
296
297impl<T: PartialEq + LambdaLanguageOfThought> PartialEq for RootedLambdaPool<'_, T> {
298    fn eq(&self, other: &Self) -> bool {
299        let mut bfs = self.pool.bfs_from(self.root).map(|(x, _)| self.pool.get(x));
300        let mut o_bfs = other
301            .pool
302            .bfs_from(other.root)
303            .map(|(x, _)| other.pool.get(x));
304        loop {
305            let x = bfs.next();
306            let y = o_bfs.next();
307            match (x, y) {
308                (None, None) => return true,
309                (None, Some(_)) | (Some(_), None) => return false,
310                (Some(a), Some(b)) => {
311                    if !a.same_expr(b) {
312                        return false;
313                    }
314                }
315            }
316        }
317    }
318}
319impl<T: PartialEq + LambdaLanguageOfThought> Eq for RootedLambdaPool<'_, T> {}
320
321impl<T: LambdaLanguageOfThought + PartialEq + Eq> PartialOrd for RootedLambdaPool<'_, T> {
322    fn partial_cmp(&self, other: &Self) -> Option<std::cmp::Ordering> {
323        Some(self.cmp(other))
324    }
325}
326
327impl<T: LambdaLanguageOfThought + PartialEq + Eq> Ord for RootedLambdaPool<'_, T> {
328    fn cmp(&self, other: &Self) -> std::cmp::Ordering {
329        self.len().cmp(&other.len()).then_with(|| {
330            let mut stack: SmallVec<[_; 2]> = smallvec![(self.root, other.root)];
331            while let Some((alpha, beta)) = stack.pop() {
332                let alpha = self.get(alpha);
333                let beta = other.get(beta);
334                match alpha.cmp_expr(beta) {
335                    Ordering::Equal => alpha
336                        .get_children()
337                        .zip(beta.get_children())
338                        .for_each(|x| stack.push(x)),
339                    Ordering::Less => return Ordering::Less,
340                    Ordering::Greater => return Ordering::Greater,
341                }
342            }
343            Ordering::Equal
344        })
345    }
346}
347
348impl<T: LambdaLanguageOfThought> LambdaExpr<'_, T> {
349    fn ordering(&self) -> usize {
350        match self {
351            LambdaExpr::Lambda(..) => 0,
352            LambdaExpr::BoundVariable(..) => 1,
353            LambdaExpr::FreeVariable(..) => 2,
354            LambdaExpr::Application { .. } => 3,
355            LambdaExpr::LanguageOfThoughtExpr(_) => 4,
356        }
357    }
358
359    fn cmp_expr(&self, other: &Self) -> std::cmp::Ordering {
360        self.ordering()
361            .cmp(&other.ordering())
362            .then_with(|| match (self, other) {
363                (LambdaExpr::Lambda(_, lambda_type), LambdaExpr::Lambda(_, o_type)) => {
364                    lambda_type.cmp(o_type)
365                }
366                (
367                    LambdaExpr::BoundVariable(x, lambda_type),
368                    LambdaExpr::BoundVariable(y, o_type),
369                ) => x.cmp(y).then(lambda_type.cmp(o_type)),
370                (LambdaExpr::FreeVariable(x, lambda_type), LambdaExpr::FreeVariable(y, o_type)) => {
371                    x.cmp(y).then(lambda_type.cmp(o_type))
372                }
373                (LambdaExpr::Application { .. }, LambdaExpr::Application { .. }) => Ordering::Equal,
374                (LambdaExpr::LanguageOfThoughtExpr(x), LambdaExpr::LanguageOfThoughtExpr(y)) => {
375                    x.cmp_expr(y)
376                }
377                _ => panic!("Previous check ensures they are the saame variant"),
378            })
379    }
380}
381
382impl<T: LambdaLanguageOfThought + HashLambda> Hash for RootedLambdaPool<'_, T> {
383    fn hash<H: std::hash::Hasher>(&self, state: &mut H) {
384        for x in self.pool.bfs_from(self.root).map(|(x, _)| self.pool.get(x)) {
385            match x {
386                LambdaExpr::Lambda(_, lambda_type) => {
387                    0.hash(state);
388                    lambda_type.hash(state);
389                }
390                LambdaExpr::BoundVariable(a, lambda_type) => {
391                    1.hash(state);
392                    a.hash(state);
393                    lambda_type.hash(state);
394                }
395                LambdaExpr::FreeVariable(free_var, lambda_type) => {
396                    2.hash(state);
397                    free_var.hash(state);
398                    lambda_type.hash(state);
399                }
400                LambdaExpr::Application { .. } => {
401                    3.hash(state);
402                }
403                LambdaExpr::LanguageOfThoughtExpr(x) => {
404                    4.hash(state);
405                    x.hash_expr(state);
406                }
407            }
408        }
409    }
410}
411
412///In order to hash a [`RootedLambdaPool`], this trait must be implemented.
413///It allows trees to be hashed without regard for the precise layout of their pools, only the
414///actual tree.
415pub trait HashLambda {
416    ///Hash the expression (without paying attention to subtrees which should be handled
417    ///[`RootedLambdaPool`]'s hash implementation)
418    fn hash_expr<H: std::hash::Hasher>(&self, state: &mut H);
419}
420
421impl<T: LambdaLanguageOfThought> LambdaExpr<'_, T> {
422    fn same_expr(&self, other: &Self) -> bool {
423        match self {
424            LambdaExpr::Lambda(_, lambda_type) => {
425                matches!(other, LambdaExpr::Lambda(_, other_type) if lambda_type == other_type)
426            }
427            LambdaExpr::BoundVariable(x, a) => {
428                matches!(other, LambdaExpr::BoundVariable(y, b) if x==y && a==b)
429            }
430            LambdaExpr::FreeVariable(free_var, lambda_type) => {
431                matches!(other, LambdaExpr::FreeVariable(o_var, o_type) if o_var == free_var && o_type == lambda_type)
432            }
433            LambdaExpr::Application { .. } => matches!(self, LambdaExpr::Application { .. }),
434            LambdaExpr::LanguageOfThoughtExpr(x) => {
435                matches!(other, LambdaExpr::LanguageOfThoughtExpr(y) if x.same_expr(y))
436            }
437        }
438    }
439}
440
441impl<'src, T: LambdaLanguageOfThought> RootedLambdaPool<'src, T> {
442    ///Creates an anonymous free variable with [`index`] of type [`t`]
443    #[must_use]
444    pub fn new_free_variable(index: usize, t: LambdaType) -> RootedLambdaPool<'src, T> {
445        RootedLambdaPool {
446            pool: LambdaPool(vec![LambdaExpr::FreeVariable(FreeVar::Anonymous(index), t)]),
447            root: LambdaExprRef(0),
448        }
449    }
450
451    ///Gets all free variables that must be bound in order to evaluate this lambda expression
452    pub fn free_variables(&self) -> impl Iterator<Item = (&FreeVar<'src>, &LambdaType)> {
453        self.pool.0.iter().filter_map(|x| {
454            if let LambdaExpr::FreeVariable(free_var, lambda_type) = x {
455                Some((free_var, lambda_type))
456            } else {
457                None
458            }
459        })
460    }
461
462    pub(crate) fn root(&self) -> LambdaExprRef {
463        self.root
464    }
465
466    ///Get the expression of a lambda term.
467    pub(crate) fn get(&self, x: LambdaExprRef) -> &LambdaExpr<'src, T> {
468        self.pool.get(x)
469    }
470
471    ///Get the length of a lambda tree
472    #[allow(clippy::len_without_is_empty)]
473    #[must_use]
474    pub fn len(&self) -> usize {
475        self.pool.0.len()
476    }
477}
478
479impl<'src, T: LambdaLanguageOfThought + Clone> RootedLambdaPool<'src, T> {
480    ///Clean up dangling references.
481    pub fn cleanup(&mut self) {
482        self.root = self.pool.cleanup(self.root);
483    }
484
485    ///The type of the lambda expression
486    ///
487    ///# Errors
488    ///Returns a [`TypeError`] if the underlying pool is malformed leading to no possible type
489    ///being extractible.
490    pub fn get_type(&self) -> Result<LambdaType, TypeError> {
491        self.pool.get_type(self.root)
492    }
493
494    ///Create a new lambda expression.
495    pub(crate) fn new(pool: LambdaPool<'src, T>, root: LambdaExprRef) -> Self {
496        RootedLambdaPool { pool, root }
497    }
498
499    ///Split into the pool and root seperately.
500    pub(crate) fn split(self) -> (LambdaPool<'src, T>, LambdaExprRef) {
501        (self.pool, self.root)
502    }
503
504    ///Combine two lambda expressions by applying one to the other. Returns [`None`] if that is
505    ///impossible.
506    ///
507    ///# Panics
508    ///Will panic if either pool is malformed such that no type can be found.
509    #[must_use]
510    pub fn merge(mut self, other: Self) -> Option<Self> {
511        let self_type = self.pool.get_type(self.root).expect("malformed type");
512        let other_type = other.pool.get_type(other.root).expect("malformed type");
513
514        let self_subformula = if self_type.can_apply(&other_type) {
515            true
516        } else if other_type.can_apply(&self_type) {
517            false
518        } else {
519            return None;
520        };
521
522        let (other_pool, other_root) = other.split();
523        let other_root = self.pool.extend_pool(other_root, other_pool);
524
525        self.root = self.pool.add(if self_subformula {
526            LambdaExpr::Application {
527                subformula: self.root,
528                argument: other_root,
529            }
530        } else {
531            LambdaExpr::Application {
532                subformula: other_root,
533                argument: self.root,
534            }
535        });
536
537        Some(self)
538    }
539
540    ///Applies other to self and returns None if the types do not correspond.
541    ///
542    ///# Panics
543    ///Will panic if either pool is malformed such that no type can be found.
544    #[must_use]
545    pub fn apply(mut self, other: Self) -> Option<Self> {
546        let self_type = self.pool.get_type(self.root).expect("malformed type");
547        let other_type = other.pool.get_type(other.root).expect("malformed type");
548
549        if !self_type.can_apply(&other_type) {
550            return None;
551        }
552        let (other_pool, other_root) = other.split();
553        let other_root = self.pool.extend_pool(other_root, other_pool);
554
555        self.root = self.pool.add(LambdaExpr::Application {
556            subformula: self.root,
557            argument: other_root,
558        });
559
560        Some(self)
561    }
562
563    ///Reduce a lambda expression
564    ///
565    ///# Errors
566    ///Will throw a [`ReductionError`] if there is something makes the reduction improper.
567    pub fn reduce(&mut self) -> Result<(), ReductionError> {
568        self.pool.reduce(self.root)?;
569        Ok(())
570    }
571
572    ///Convert a lambda expression to its executable version (should only be done if there are only
573    ///[`LambdaExpr::LanguageOfThoughtExpr`] expressions.
574    ///
575    ///# Errors
576    ///Will throw a [`T::ConversionError`] if there are any lambda terms left in the pool
577    pub fn into_pool(mut self) -> Result<T::Pool, T::ConversionError> {
578        self.cleanup();
579        T::to_pool(self)
580    }
581
582    ///Replace a free variable with a value.
583    ///
584    ///# Errors
585    ///Will return an error if a [`FreeVar`] with the same name but different type already exists
586    pub fn bind_free_variable(
587        &mut self,
588        fvar: FreeVar<'src>,
589        replacement: RootedLambdaPool<'src, T>,
590    ) -> Result<(), LambdaError> {
591        let (other_pool, other_root) = replacement.split();
592        let other_root = self.pool.extend_pool(other_root, other_pool);
593        self.pool.bind_free_variable(self.root, fvar, other_root)?;
594        //self.root = self.pool.cleanup(self.root);
595        Ok(())
596    }
597
598    ///Replace a free variable by lambda abstracting it. (e.g. $P(x_{free})$ to $\lambda x P(x)$).
599    ///
600    ///# Errors
601    ///Will throw an error if the free variable has the wrong type.
602    pub fn lambda_abstract_free_variable(
603        &mut self,
604        fvar: FreeVar<'src>,
605        lambda_type: LambdaType,
606        always_abstract: bool,
607    ) -> Result<(), LambdaError> {
608        self.reduce()?;
609        let vars = self
610            .pool
611            .bfs_from(self.root)
612            .filter_map(|(x, d)| match self.pool.get(x) {
613                LambdaExpr::FreeVariable(var, var_type) if *var == fvar => {
614                    if &lambda_type == var_type {
615                        Some(Ok((x, d)))
616                    } else {
617                        Some(Err(LambdaError::BadFreeVariable {
618                            free_var: var_type.clone(),
619                            lambda: lambda_type.clone(),
620                        }))
621                    }
622                }
623                _ => None,
624            })
625            .collect::<Result<Vec<_>, LambdaError>>()?;
626
627        if !vars.is_empty() || always_abstract {
628            for (x, lambda_depth) in vars {
629                *self.pool.get_mut(x) =
630                    LambdaExpr::BoundVariable(lambda_depth, lambda_type.clone());
631            }
632            self.root = self.pool.add(LambdaExpr::Lambda(self.root, lambda_type));
633        }
634        Ok(())
635    }
636
637    ///Apply a free variable to a function.
638    ///
639    ///# Errors
640    ///Will throw an error if there is an issue with the reduction
641    pub fn apply_new_free_variable(
642        &mut self,
643        fvar: FreeVar<'src>,
644    ) -> Result<LambdaType, LambdaError> {
645        let pool_type = self.pool.get_type(self.root)?;
646        let var_type = pool_type.lhs()?;
647        let argument = self
648            .pool
649            .add(LambdaExpr::FreeVariable(fvar, var_type.clone()));
650        self.root = self.pool.add(LambdaExpr::Application {
651            subformula: self.root,
652            argument,
653        });
654        self.reduce()?;
655        Ok(var_type.clone())
656    }
657}
658
659#[derive(Default, Debug, Clone, Eq, PartialEq, Hash)]
660pub(crate) struct LambdaPool<'a, T: LambdaLanguageOfThought>(pub(crate) Vec<LambdaExpr<'a, T>>);
661
662impl<'src, T: LambdaLanguageOfThought + Sized> LambdaPool<'src, T> {
663    pub(crate) fn extend_pool(
664        &mut self,
665        mut other_root: LambdaExprRef,
666        mut other_pool: LambdaPool<'src, T>,
667    ) -> LambdaExprRef {
668        let shift_n = u32::try_from(self.0.len()).unwrap();
669        let remap: Vec<_> = (0..u32::try_from(other_pool.0.len()).unwrap())
670            .map(|x| x + shift_n)
671            .collect();
672        other_pool.0.iter_mut().for_each(|x| x.remap_refs(&remap));
673        other_root.0 += shift_n;
674        self.0.append(&mut other_pool.0);
675        other_root
676    }
677
678    ///Convert from [`Vec<LambdaExpr<T>>`] to [`LambdaPool`]
679    pub fn from(x: Vec<LambdaExpr<'src, T>>) -> Self {
680        LambdaPool(x)
681    }
682
683    ///Create a new, empty [`LambdaPool`]
684    pub fn new<'c>() -> LambdaPool<'c, T> {
685        LambdaPool(vec![])
686    }
687
688    fn checked_get(&self, expr: LambdaExprRef) -> Option<&LambdaExpr<'src, T>> {
689        self.0.get(expr.0 as usize)
690    }
691
692    ///Get the [`LambdaExpr`] at an index.
693    pub fn get(&self, expr: LambdaExprRef) -> &LambdaExpr<'src, T> {
694        &self.0[expr.0 as usize]
695    }
696
697    pub fn get_mut<'a>(&'a mut self, expr: LambdaExprRef) -> &'a mut LambdaExpr<'src, T> {
698        &mut self.0[expr.0 as usize]
699    }
700
701    pub fn add(&mut self, expr: LambdaExpr<'src, T>) -> LambdaExprRef {
702        let idx = self.0.len();
703        self.0.push(expr);
704        LambdaExprRef(idx.try_into().expect("Too many exprs in the pool"))
705    }
706}
707
708///Iterate over a lambda pool in breadth-first search
709pub(crate) struct LambdaPoolBFSIterator<'a, 'src, T: LambdaLanguageOfThought> {
710    pool: &'a LambdaPool<'src, T>,
711    queue: VecDeque<(LambdaExprRef, Bvar)>,
712}
713
714impl<T: LambdaLanguageOfThought> LambdaExpr<'_, T> {
715    pub(crate) fn n_children(&self) -> usize {
716        match self {
717            LambdaExpr::BoundVariable(..) | LambdaExpr::FreeVariable(..) => 0,
718            LambdaExpr::Lambda(..) => 1,
719            LambdaExpr::Application { .. } => 2,
720            LambdaExpr::LanguageOfThoughtExpr(e) => e.n_children(),
721        }
722    }
723
724    pub(crate) fn get_children(&self) -> impl Iterator<Item = LambdaExprRef> {
725        match self {
726            LambdaExpr::Lambda(x, _) => ArgumentIterator::A([x].into_iter().copied()),
727            LambdaExpr::Application {
728                subformula,
729                argument,
730            } => ArgumentIterator::B([subformula, argument].into_iter().copied()),
731            LambdaExpr::BoundVariable(..) | LambdaExpr::FreeVariable(..) => {
732                ArgumentIterator::C(std::iter::empty())
733            }
734            LambdaExpr::LanguageOfThoughtExpr(x) => ArgumentIterator::D(x.get_children()),
735        }
736    }
737}
738
739impl<T: LambdaLanguageOfThought> Iterator for LambdaPoolBFSIterator<'_, '_, T> {
740    type Item = (LambdaExprRef, Bvar);
741
742    fn next(&mut self) -> Option<Self::Item> {
743        if let Some((x, lambda_depth)) = self.queue.pop_front() {
744            match self.pool.get(x) {
745                LambdaExpr::Lambda(x, _) => self.queue.push_back((*x, lambda_depth + 1)),
746                LambdaExpr::Application {
747                    subformula,
748                    argument,
749                } => {
750                    self.queue.push_back((*subformula, lambda_depth));
751                    self.queue.push_back((*argument, lambda_depth));
752                }
753                LambdaExpr::BoundVariable(..) | LambdaExpr::FreeVariable(..) => (),
754                LambdaExpr::LanguageOfThoughtExpr(x) => {
755                    let depth = lambda_depth + usize::from(x.inc_depth());
756
757                    x.get_children()
758                        .for_each(|x| self.queue.push_back((x, depth)));
759                }
760            }
761            Some((x, lambda_depth))
762        } else {
763            None
764        }
765    }
766}
767
768///Iterate over a lambda pool and return a mutable reference
769pub(crate) struct MutableLambdaPoolBFSIterator<'a, 'src: 'a, T: LambdaLanguageOfThought + 'a> {
770    pool: *mut LambdaPool<'src, T>,
771    queue: VecDeque<(LambdaExprRef, Bvar)>,
772    phantom: PhantomData<&'a ()>,
773}
774
775impl<'a, 'src: 'a, T: LambdaLanguageOfThought + 'a> MutableLambdaPoolBFSIterator<'a, 'src, T> {
776    fn new(pool: &mut LambdaPool<'src, T>, x: LambdaExprRef) -> Self {
777        Self {
778            pool: std::ptr::from_mut::<LambdaPool<'src, T>>(pool),
779            queue: VecDeque::from([(x, 0)]),
780            phantom: PhantomData,
781        }
782    }
783}
784
785impl<'a, 'src, T: LambdaLanguageOfThought> Iterator for MutableLambdaPoolBFSIterator<'a, 'src, T> {
786    type Item = (&'a mut LambdaExpr<'src, T>, usize, LambdaExprRef);
787
788    fn next(&mut self) -> Option<Self::Item> {
789        if let Some((x, lambda_depth)) = self.queue.pop_front() {
790            let expr = unsafe { self.pool.as_ref().unwrap() };
791            match expr.get(x) {
792                LambdaExpr::Lambda(x, _) => self.queue.push_back((*x, lambda_depth + 1)),
793                LambdaExpr::Application {
794                    subformula,
795                    argument,
796                } => {
797                    self.queue.push_back((*subformula, lambda_depth));
798                    self.queue.push_back((*argument, lambda_depth));
799                }
800                LambdaExpr::BoundVariable(..) | LambdaExpr::FreeVariable(..) => (),
801                LambdaExpr::LanguageOfThoughtExpr(x) => {
802                    let depth = lambda_depth + usize::from(x.inc_depth());
803
804                    x.get_children()
805                        .for_each(|x| self.queue.push_back((x, depth)));
806                }
807            }
808            Some((
809                unsafe { self.pool.as_mut().unwrap().get_mut(x) },
810                lambda_depth,
811                x,
812            ))
813        } else {
814            None
815        }
816    }
817}
818
819impl<'src, T: LambdaLanguageOfThought> LambdaPool<'src, T> {
820    pub(crate) fn bfs_from(&self, x: LambdaExprRef) -> LambdaPoolBFSIterator<'_, 'src, T> {
821        LambdaPoolBFSIterator {
822            pool: self,
823            queue: VecDeque::from([(x, 0)]),
824        }
825    }
826}
827impl<'src, T: LambdaLanguageOfThought> LambdaPool<'src, T> {
828    pub fn get_type(&self, x: LambdaExprRef) -> Result<LambdaType, TypeError> {
829        match self.get(x) {
830            LambdaExpr::BoundVariable(_, x) | LambdaExpr::FreeVariable(_, x) => Ok(x.clone()),
831            LambdaExpr::Lambda(s, x) => {
832                let result = self.get_type(*s);
833                Ok(LambdaType::compose(x.clone(), result?))
834            }
835            LambdaExpr::Application { subformula, .. } => {
836                let subformula_type = self.get_type(*subformula)?;
837                Ok(subformula_type.rhs()?.clone())
838            }
839            LambdaExpr::LanguageOfThoughtExpr(x) => Ok(x.get_type().clone()),
840        }
841    }
842
843    fn check_type_clash(&self, x: LambdaExprRef) -> Result<LambdaType, ReductionError> {
844        if let LambdaExpr::Application {
845            subformula,
846            argument,
847        } = self.get(x)
848        {
849            let argument_type = self.get_type(*argument)?;
850            let subformula_type = self.get_type(*subformula)?;
851            Ok(subformula_type.apply(&argument_type)?.clone())
852        } else {
853            Err(ReductionError::NotApplication(x))
854        }
855    }
856
857    pub(crate) fn bfs_from_mut<'a>(
858        &'a mut self,
859        x: LambdaExprRef,
860    ) -> MutableLambdaPoolBFSIterator<'a, 'src, T> {
861        MutableLambdaPoolBFSIterator::new(self, x)
862    }
863
864    fn get_next_app(&self, root: LambdaExprRef) -> Option<LambdaExprRef> {
865        self.bfs_from(root)
866            .map(|(x, _)| x)
867            .find(|x| match self.get(*x) {
868                LambdaExpr::Application { subformula, .. } => {
869                    matches!(self.get(*subformula), LambdaExpr::Lambda(..))
870                }
871                _ => false,
872            })
873    }
874}
875
876impl<'src, T: LambdaLanguageOfThought> LambdaPool<'src, T>
877where
878    T: Clone,
879{
880    fn bind_free_variable(
881        &mut self,
882        root: LambdaExprRef,
883        fvar: FreeVar<'src>,
884        replacement_root: LambdaExprRef,
885    ) -> Result<(), LambdaError> {
886        let arg_t = self.get_type(replacement_root)?;
887
888        let to_replace = self
889            .bfs_from(root)
890            .filter_map(|(x, d)| match self.get(x) {
891                LambdaExpr::FreeVariable(var, t) if *var == fvar => {
892                    if t == &arg_t {
893                        Some(Ok((x, d)))
894                    } else {
895                        Some(Err(LambdaError::BadFreeVariableApp {
896                            free_var: t.clone(),
897                            arg: arg_t.clone(),
898                        }))
899                    }
900                }
901                _ => None,
902            })
903            .collect::<Result<Vec<_>, LambdaError>>()?;
904
905        self.replace_section(&to_replace, replacement_root);
906        Ok(())
907    }
908
909    fn replace_section(&mut self, to_replace: &[(LambdaExprRef, usize)], to_copy: LambdaExprRef) {
910        let n = to_replace.len();
911        for (i, (x, depth)) in to_replace.iter().enumerate() {
912            if i == n - 1 {
913                for (x, d, _) in self.bfs_from_mut(to_copy) {
914                    if let LambdaExpr::BoundVariable(bound_depth, _) = x
915                        && *bound_depth >= d
916                    {
917                        *bound_depth += depth;
918                    }
919                }
920                //Last iteration so we don't need to copy anymore.
921                *self.get_mut(*x) = self.get(to_copy).clone();
922            } else {
923                let mut len = u32::try_from(self.0.len()).unwrap();
924                let mut first = true;
925                let mut head = None;
926                self.0.extend(
927                    self.bfs_from(to_copy)
928                        .filter_map(|(x, d)| {
929                            let mut expr = self.get(x).clone();
930                            if let LambdaExpr::BoundVariable(bound_depth, _) = &mut expr
931                                && *bound_depth >= d
932                            {
933                                *bound_depth += depth;
934                            }
935
936                            let old_len = len;
937                            len += u32::try_from(expr.n_children()).unwrap();
938                            expr.change_children((old_len..len).map(LambdaExprRef));
939                            if first {
940                                head = Some(expr);
941                                first = false;
942                                None
943                            } else {
944                                Some(expr)
945                            }
946                        })
947                        .collect::<Vec<_>>(),
948                );
949
950                *self.get_mut(*x) = head.unwrap();
951            }
952        }
953    }
954
955    fn beta_reduce(&mut self, app: LambdaExprRef) -> Result<(), ReductionError> {
956        //BFS over all children and then replace debruijn k w/ argument ref where k is the number
957        //of lambda abstractions we've gone under, e.g. (lambda 0 lambda 0 1)(u) -> lambda u lambda
958        //1
959        //
960        //swap position of lambda ref and subformula ref so the lambda now leads to this.
961        //
962        let Some(expr) = self.checked_get(app) else {
963            return Err(ReductionError::NotValidRef(app));
964        };
965
966        let (inner_term, argument, subformula_vars) = if let LambdaExpr::Application {
967            argument,
968            subformula,
969        } = expr
970        {
971            let inner_term = match self.get(*subformula) {
972                LambdaExpr::Lambda(x, ..) => {
973                    self.check_type_clash(app)?;
974                    *x
975                }
976                _ => {
977                    return Err(ReductionError::NotLambdaInApplication {
978                        app,
979                        lhs: *subformula,
980                    });
981                }
982            };
983
984            (
985                inner_term,
986                *argument,
987                self.bfs_from_mut(inner_term)
988                    .filter_map(|(expr, d, expr_ref)| {
989                        if let LambdaExpr::BoundVariable(b_d, _) = expr {
990                            match (*b_d).cmp(&d) {
991                                std::cmp::Ordering::Greater => {
992                                    //Decrement locally free variables
993                                    *b_d -= 1;
994                                    None
995                                }
996                                std::cmp::Ordering::Equal => Some((expr_ref, *b_d)),
997                                std::cmp::Ordering::Less => None,
998                            }
999                        } else {
1000                            None
1001                        }
1002                    })
1003                    .collect::<Vec<_>>(),
1004            )
1005        } else {
1006            return Err(ReductionError::NotApplication(app));
1007        };
1008
1009        //We used to swap this, but that will cause an insanely arcane bug.
1010        //This is because the same term may be referred to by multiple instructions so if you swap
1011        //them, it gets invalidated.
1012        self.replace_section(&subformula_vars, argument);
1013        self.0[app.0 as usize] = self.0[inner_term.0 as usize].clone();
1014        //self.0.swap(inner_term.0 as usize, app.0 as usize); <- BAD
1015
1016        Ok(())
1017    }
1018
1019    ///Iterates through a pool and de-allocates dangling refs and updates `ExprRefs` to new
1020    ///addresses. Basically garbage collection.
1021    pub(crate) fn cleanup(&mut self, root: LambdaExprRef) -> LambdaExprRef {
1022        let findable: HashSet<_> = self.bfs_from(root).map(|(x, _)| x.0).collect();
1023        let mut remap = (0..u32::try_from(self.0.len()).unwrap()).collect::<Vec<_>>();
1024        let mut adjustment = 0;
1025
1026        for i in &mut remap {
1027            if findable.contains(i) {
1028                *i -= adjustment;
1029            } else {
1030                adjustment += 1;
1031            }
1032        }
1033
1034        let mut i = 0;
1035        self.0.retain(|_| {
1036            i += 1;
1037            findable.contains(&(i - 1))
1038        });
1039        for x in &mut self.0 {
1040            x.remap_refs(&remap);
1041        }
1042        LambdaExprRef(remap[root.0 as usize])
1043    }
1044
1045    pub fn reduce(&mut self, root: LambdaExprRef) -> Result<(), ReductionError> {
1046        while let Some(x) = self.get_next_app(root) {
1047            self.beta_reduce(x)?;
1048        }
1049        Ok(())
1050    }
1051}
1052
1053impl<T: LambdaLanguageOfThought> LambdaExpr<'_, T> {
1054    pub(crate) fn change_children(&mut self, mut children: impl Iterator<Item = LambdaExprRef>) {
1055        match self {
1056            LambdaExpr::Lambda(lambda_expr_ref, _) => *lambda_expr_ref = children.next().unwrap(),
1057            LambdaExpr::BoundVariable(..) | LambdaExpr::FreeVariable(..) => (),
1058            LambdaExpr::Application {
1059                subformula,
1060                argument,
1061            } => {
1062                *subformula = children.next().unwrap();
1063                *argument = children.next().unwrap();
1064            }
1065            LambdaExpr::LanguageOfThoughtExpr(x) => x.change_children(children),
1066        }
1067    }
1068
1069    fn remap_refs(&mut self, remap: &[u32]) {
1070        match self {
1071            LambdaExpr::Lambda(x, _) => {
1072                *x = LambdaExprRef(remap[x.0 as usize]);
1073            }
1074            LambdaExpr::Application {
1075                subformula,
1076                argument,
1077            } => {
1078                *subformula = LambdaExprRef(remap[subformula.0 as usize]);
1079                *argument = LambdaExprRef(remap[argument.0 as usize]);
1080            }
1081            LambdaExpr::BoundVariable(..) | LambdaExpr::FreeVariable(..) => (),
1082            LambdaExpr::LanguageOfThoughtExpr(x) => x.remap_refs(remap),
1083        }
1084    }
1085}
1086
1087///Details about a [`RootedLambdaPool`]
1088#[derive(Debug, Clone, PartialEq, Eq, Hash)]
1089pub enum LambdaSummaryStats {
1090    ///The expression is correctly formed.
1091    WellFormed {
1092        ///What type is it
1093        lambda_type: LambdaType,
1094
1095        ///Is it a constant function?
1096        constant_function: bool,
1097
1098        ///How long is the expression?
1099        n_nodes: usize,
1100    },
1101
1102    ///Is there a problem with the expression
1103    Malformed,
1104}
1105
1106impl<T: LambdaLanguageOfThought + Clone + std::fmt::Debug> RootedLambdaPool<'_, T> {
1107    ///Convert an expression `phi` of type `x` and convert it to `lambda <x,t> P P(phi)`
1108    ///
1109    ///# Errors
1110    ///Will return a type error if the type of the lambda expression is malformed
1111    pub fn lift(&mut self) -> Result<(), TypeError> {
1112        let t =
1113            LambdaType::Composition(Box::new(self.get_type()?.clone()), Box::new(LambdaType::T));
1114
1115        let p = self.pool.add(LambdaExpr::BoundVariable(0, t.clone()));
1116        let apply = self.pool.add(LambdaExpr::Application {
1117            subformula: p,
1118            argument: self.root,
1119        });
1120        let lambda = self.pool.add(LambdaExpr::Lambda(apply, t));
1121        self.root = lambda;
1122
1123        Ok(())
1124    }
1125
1126    ///Get [`LambdaSummaryStats`] for an expression, e.g. how many context functions, size, etc.
1127    #[must_use]
1128    #[allow(clippy::missing_panics_doc)]
1129    pub fn stats(&self) -> LambdaSummaryStats {
1130        let lambda_type = self.get_type();
1131        if lambda_type.is_err() {
1132            return LambdaSummaryStats::Malformed;
1133        }
1134        let lambda_type = lambda_type.unwrap();
1135        let n_nodes = self.pool.0.len();
1136
1137        match self.all_lambda_has_variable(self.root) {
1138            Ok(has_variable) => LambdaSummaryStats::WellFormed {
1139                lambda_type,
1140                constant_function: !has_variable,
1141                n_nodes,
1142            },
1143
1144            Err(_) => LambdaSummaryStats::Malformed,
1145        }
1146    }
1147
1148    fn all_lambda_has_variable(&self, i: LambdaExprRef) -> Result<bool, LambdaError> {
1149        let mut found = vec![];
1150        let mut stack = vec![(i, vec![])];
1151        while let Some((expr_ref, mut lambdas)) = stack.pop() {
1152            match self.get(expr_ref) {
1153                LambdaExpr::Lambda(lambda_expr_ref, _) => {
1154                    found.push(false);
1155                    lambdas.push(found.len() - 1);
1156                    stack.push((*lambda_expr_ref, lambdas));
1157                }
1158                LambdaExpr::BoundVariable(d, _) => {
1159                    if let Some(index) = lambdas.len().checked_sub(d + 1) {
1160                        if let Some(found_index) = lambdas.get(index) {
1161                            if let Some(found) = found.get_mut(*found_index) {
1162                                *found = true;
1163                            } else {
1164                                return Err(LambdaError::BadBoundVariable {
1165                                    var: expr_ref,
1166                                    depth: lambdas.len(),
1167                                });
1168                            }
1169                        } else {
1170                            return Err(LambdaError::BadBoundVariable {
1171                                var: expr_ref,
1172                                depth: lambdas.len(),
1173                            });
1174                        }
1175                    } else {
1176                        return Err(LambdaError::BadBoundVariable {
1177                            var: expr_ref,
1178                            depth: lambdas.len(),
1179                        });
1180                    }
1181                }
1182                LambdaExpr::FreeVariable(..) => (),
1183                LambdaExpr::Application {
1184                    subformula,
1185                    argument,
1186                } => {
1187                    stack.push((*subformula, lambdas.clone()));
1188                    stack.push((*argument, lambdas));
1189                }
1190
1191                LambdaExpr::LanguageOfThoughtExpr(x) => {
1192                    if x.inc_depth() {
1193                        found.push(false);
1194                        lambdas.push(found.len() - 1);
1195                    }
1196                    stack.extend(x.get_children().map(|x| (x, lambdas.clone())));
1197                }
1198            }
1199        }
1200
1201        Ok(found.iter().all(|x| *x))
1202    }
1203}
1204
1205impl<'a, T: LambdaLanguageOfThought> From<LambdaPool<'a, T>> for Vec<Option<LambdaExpr<'a, T>>> {
1206    fn from(value: LambdaPool<'a, T>) -> Self {
1207        value.0.into_iter().map(Some).collect()
1208    }
1209}
1210
1211impl<'a, T: LambdaLanguageOfThought> TryFrom<Vec<Option<LambdaExpr<'a, T>>>> for LambdaPool<'a, T> {
1212    type Error = LambdaTryFromError;
1213
1214    fn try_from(value: Vec<Option<LambdaExpr<'a, T>>>) -> Result<Self, Self::Error> {
1215        match value.into_iter().collect::<Option<Vec<_>>>() {
1216            Some(x) => Ok(LambdaPool(x)),
1217            None => Err(LambdaTryFromError::HasNone),
1218        }
1219    }
1220}
1221
1222#[cfg(test)]
1223mod test {
1224
1225    use std::{
1226        collections::BTreeSet,
1227        hash::{DefaultHasher, Hasher},
1228    };
1229
1230    use super::*;
1231    use crate::language::{
1232        ActorOrEvent, BinOp, Expr, ExprPool, ExprRef, LanguageExpression, MonOp,
1233    };
1234
1235    #[test]
1236    fn ordering() -> anyhow::Result<()> {
1237        let x = [
1238            "a_0",
1239            "lambda a x (pa_man(x))",
1240            "lambda a x (pa_man(a_m))",
1241            "lambda a x (((lambda a y (pa_woman(y)))(a_m)) & pa_man(x))",
1242            "lambda a x (((lambda a y (pa_woman(a_m)))(a_m)) & pa_man(x))",
1243            "lambda a y (pa_woman(a_m))",
1244            "lambda a y (lambda a x (y))",
1245            "some(x, pa_man(x), True)",
1246            "some(x, pa_man(x), pa_man(x))",
1247            "some(x, True, pa_man(x))",
1248            "some(x, True, True)",
1249        ];
1250
1251        let set: BTreeSet<_> = x
1252            .into_iter()
1253            .map(RootedLambdaPool::parse)
1254            .collect::<Result<_, _>>()?;
1255        assert_eq!(set.len(), 11);
1256        let order: Vec<_> = set.into_iter().map(|x| x.to_string()).collect();
1257
1258        let sorted = vec![
1259            "a_0",
1260            "lambda a x lambda a y x",
1261            "lambda a x pa_man(x)",
1262            "lambda a x pa_man(a_m)",
1263            "lambda a x pa_woman(a_m)",
1264            "some(x, True, True)",
1265            "some(x, True, pa_man(x))",
1266            "some(x, pa_man(x), True)",
1267            "some(x, pa_man(x), pa_man(x))",
1268            "lambda a x (lambda a y pa_woman(y))(a_m) & pa_man(x)",
1269            "lambda a x (lambda a y pa_woman(a_m))(a_m) & pa_man(x)",
1270        ];
1271
1272        for (x, y) in order.into_iter().zip(sorted) {
1273            assert_eq!(x, y);
1274        }
1275
1276        Ok(())
1277    }
1278
1279    #[test]
1280    fn stats() -> anyhow::Result<()> {
1281        for (expr, constant_lambda) in [
1282            ("a_0", false),
1283            ("lambda a x (pa_man(x))", false),
1284            ("lambda a x (pa_man(a_m))", true),
1285            (
1286                "lambda a x (((lambda a y (pa_woman(y)))(a_m)) & pa_man(x))",
1287                false,
1288            ),
1289            (
1290                "lambda a x (((lambda a y (pa_woman(a_m)))(a_m)) & pa_man(x))",
1291                true,
1292            ),
1293            ("lambda a y (pa_woman(a_m))", true),
1294            ("lambda a y (lambda a x (y))", true),
1295            ("some(x, pa_man(x), True)", false),
1296            ("some(x, pa_man(x), pa_man(x))", false),
1297            ("some(x, True, pa_man(x))", false),
1298            ("some(x, True, True)", true),
1299        ] {
1300            let expr = RootedLambdaPool::parse(expr)?;
1301            match expr.stats() {
1302                LambdaSummaryStats::WellFormed {
1303                    constant_function, ..
1304                } => assert_eq!(constant_function, constant_lambda),
1305                LambdaSummaryStats::Malformed => panic!("{expr} should be well-formed!"),
1306            }
1307        }
1308        Ok(())
1309    }
1310
1311    fn k<'a, T: Default>(pos: u32) -> anyhow::Result<[LambdaExpr<'a, T>; 3]> {
1312        Ok([
1313            LambdaExpr::Lambda(LambdaExprRef(pos + 1), LambdaType::e().clone()),
1314            LambdaExpr::Lambda(LambdaExprRef(pos + 2), LambdaType::e().clone()),
1315            LambdaExpr::BoundVariable(1, LambdaType::e().clone()),
1316        ])
1317    }
1318
1319    #[test]
1320    fn complicated_lambda_language_of_thought() -> anyhow::Result<()> {
1321        let mut pool = LambdaPool::<Expr>(vec![
1322            LambdaExpr::Application {
1323                //John dances
1324                subformula: LambdaExprRef(1),
1325                argument: LambdaExprRef(4),
1326            },
1327            LambdaExpr::Lambda(LambdaExprRef(2), LambdaType::a().clone()),
1328            LambdaExpr::LanguageOfThoughtExpr(Expr::Unary(
1329                MonOp::Property("32", ActorOrEvent::Actor),
1330                ExprRef(3),
1331            )),
1332            LambdaExpr::BoundVariable(0, LambdaType::a().clone()),
1333            LambdaExpr::LanguageOfThoughtExpr(Expr::Actor("3")),
1334        ]);
1335        pool.reduce(LambdaExprRef(0))?;
1336        pool.cleanup(LambdaExprRef(0));
1337
1338        assert_eq!(
1339            pool.clone(),
1340            LambdaPool(vec![
1341                LambdaExpr::LanguageOfThoughtExpr(Expr::Unary(
1342                    MonOp::Property("32", ActorOrEvent::Actor),
1343                    ExprRef(1)
1344                )),
1345                LambdaExpr::LanguageOfThoughtExpr(Expr::Actor("3"))
1346            ]),
1347        );
1348
1349        let mut pool = LambdaPool(vec![
1350            LambdaExpr::Application {
1351                subformula: LambdaExprRef(1),
1352                argument: LambdaExprRef(5),
1353            },
1354            LambdaExpr::Lambda(LambdaExprRef(2), LambdaType::from_string("<a, t>")?),
1355            LambdaExpr::Application {
1356                subformula: LambdaExprRef(3),
1357                argument: LambdaExprRef(4),
1358            },
1359            LambdaExpr::BoundVariable(0, LambdaType::et().clone()),
1360            LambdaExpr::LanguageOfThoughtExpr(Expr::Actor("2")),
1361            LambdaExpr::Lambda(LambdaExprRef(6), LambdaType::a().clone()),
1362            LambdaExpr::LanguageOfThoughtExpr(Expr::Unary(
1363                MonOp::Property("36", ActorOrEvent::Actor),
1364                ExprRef(7),
1365            )),
1366            LambdaExpr::BoundVariable(0, LambdaType::a().clone()),
1367        ]);
1368        pool.reduce(LambdaExprRef(0))?;
1369        pool.cleanup(LambdaExprRef(0));
1370        assert_eq!(
1371            pool,
1372            LambdaPool(vec![
1373                LambdaExpr::LanguageOfThoughtExpr(Expr::Unary(
1374                    MonOp::Property("36", ActorOrEvent::Actor),
1375                    ExprRef(1)
1376                )),
1377                LambdaExpr::LanguageOfThoughtExpr(Expr::Actor("2")),
1378            ])
1379        );
1380
1381        let mut pool = LambdaPool(vec![
1382            LambdaExpr::Application {
1383                subformula: LambdaExprRef(1),
1384                argument: LambdaExprRef(6),
1385            },
1386            LambdaExpr::Lambda(LambdaExprRef(2), LambdaType::t().clone()),
1387            LambdaExpr::Lambda(LambdaExprRef(3), LambdaType::t().clone()),
1388            LambdaExpr::LanguageOfThoughtExpr(Expr::Binary(BinOp::And, ExprRef(4), ExprRef(5))), //10
1389            LambdaExpr::BoundVariable(1, LambdaType::t().clone()),
1390            LambdaExpr::BoundVariable(0, LambdaType::t().clone()),
1391            LambdaExpr::Application {
1392                //6
1393                subformula: LambdaExprRef(7),
1394                argument: LambdaExprRef(10),
1395            },
1396            LambdaExpr::Lambda(LambdaExprRef(8), LambdaType::a().clone()),
1397            LambdaExpr::LanguageOfThoughtExpr(Expr::Unary(
1398                MonOp::Property("36", ActorOrEvent::Actor),
1399                ExprRef(9),
1400            )),
1401            LambdaExpr::BoundVariable(0, LambdaType::a().clone()),
1402            LambdaExpr::LanguageOfThoughtExpr(Expr::Actor("2")),
1403        ]);
1404        pool.reduce(LambdaExprRef(0))?;
1405        pool.cleanup(LambdaExprRef(0));
1406
1407        assert_eq!(
1408            pool,
1409            LambdaPool(vec![
1410                LambdaExpr::Lambda(LambdaExprRef(1), LambdaType::t().clone()),
1411                LambdaExpr::LanguageOfThoughtExpr(Expr::Binary(BinOp::And, ExprRef(2), ExprRef(3))),
1412                LambdaExpr::LanguageOfThoughtExpr(Expr::Unary(
1413                    MonOp::Property("36", ActorOrEvent::Actor),
1414                    ExprRef(4)
1415                )),
1416                LambdaExpr::BoundVariable(0, LambdaType::t().clone()),
1417                LambdaExpr::LanguageOfThoughtExpr(Expr::Actor("2")),
1418            ])
1419        );
1420
1421        // [[[Mary sings] and]  [John dances]]
1422        let mut pool = LambdaPool::<Expr>(vec![
1423            LambdaExpr::Application {
1424                subformula: LambdaExprRef(6),
1425                argument: LambdaExprRef(1),
1426            },
1427            LambdaExpr::Application {
1428                //John dances
1429                subformula: LambdaExprRef(2),
1430                argument: LambdaExprRef(5),
1431            },
1432            LambdaExpr::Lambda(LambdaExprRef(3), LambdaType::a().clone()),
1433            LambdaExpr::LanguageOfThoughtExpr(Expr::Unary(
1434                MonOp::Property("32", ActorOrEvent::Actor),
1435                ExprRef(4),
1436            )),
1437            LambdaExpr::BoundVariable(0, LambdaType::a().clone()),
1438            LambdaExpr::LanguageOfThoughtExpr(Expr::Actor("3")),
1439            // 6
1440            //\lambda x. Mary sings and
1441            LambdaExpr::Application {
1442                subformula: LambdaExprRef(7),
1443                argument: LambdaExprRef(12),
1444            },
1445            LambdaExpr::Lambda(LambdaExprRef(8), LambdaType::t().clone()),
1446            LambdaExpr::Lambda(LambdaExprRef(9), LambdaType::t().clone()),
1447            LambdaExpr::LanguageOfThoughtExpr(Expr::Binary(BinOp::And, ExprRef(10), ExprRef(11))), //10
1448            LambdaExpr::BoundVariable(1, LambdaType::t().clone()),
1449            LambdaExpr::BoundVariable(0, LambdaType::t().clone()),
1450            LambdaExpr::Application {
1451                //13
1452                subformula: LambdaExprRef(13),
1453                argument: LambdaExprRef(16),
1454            },
1455            LambdaExpr::Lambda(LambdaExprRef(14), LambdaType::a().clone()),
1456            LambdaExpr::LanguageOfThoughtExpr(Expr::Unary(
1457                MonOp::Property("36", ActorOrEvent::Actor),
1458                ExprRef(15),
1459            )),
1460            LambdaExpr::BoundVariable(0, LambdaType::a().clone()),
1461            LambdaExpr::LanguageOfThoughtExpr(Expr::Actor("2")),
1462        ]);
1463        pool.reduce(LambdaExprRef(0))?;
1464        let root = pool.cleanup(LambdaExprRef(0));
1465        assert_eq!(
1466            pool,
1467            LambdaPool(vec![
1468                LambdaExpr::LanguageOfThoughtExpr(Expr::Binary(BinOp::And, ExprRef(2), ExprRef(3))),
1469                LambdaExpr::LanguageOfThoughtExpr(Expr::Actor("3")),
1470                LambdaExpr::LanguageOfThoughtExpr(Expr::Unary(
1471                    MonOp::Property("36", ActorOrEvent::Actor),
1472                    ExprRef(4)
1473                )),
1474                LambdaExpr::LanguageOfThoughtExpr(Expr::Unary(
1475                    MonOp::Property("32", ActorOrEvent::Actor),
1476                    ExprRef(1)
1477                )),
1478                LambdaExpr::LanguageOfThoughtExpr(Expr::Actor("2"))
1479            ])
1480        );
1481
1482        assert_eq!(
1483            RootedLambdaPool::new(pool, root).into_pool()?,
1484            LanguageExpression::new(
1485                ExprPool::from(vec![
1486                    Expr::Binary(BinOp::And, ExprRef(2), ExprRef(3)),
1487                    Expr::Actor("3"),
1488                    Expr::Unary(MonOp::Property("36", ActorOrEvent::Actor), ExprRef(4)),
1489                    Expr::Unary(MonOp::Property("32", ActorOrEvent::Actor), ExprRef(1)),
1490                    Expr::Actor("2")
1491                ]),
1492                ExprRef(root.0)
1493            )
1494        );
1495        Ok(())
1496    }
1497    #[test]
1498    fn type_check() -> anyhow::Result<()> {
1499        // [[[Mary sings] and]  [John dances]]
1500        let mut pool = LambdaPool::<()>(vec![
1501            LambdaExpr::Application {
1502                subformula: LambdaExprRef(1),
1503                argument: LambdaExprRef(3),
1504            },
1505            LambdaExpr::Lambda(LambdaExprRef(2), LambdaType::a().clone()),
1506            LambdaExpr::BoundVariable(0, LambdaType::t().clone()),
1507            LambdaExpr::FreeVariable("0".into(), LambdaType::t().clone()),
1508        ]);
1509        assert_eq!(
1510            pool.reduce(LambdaExprRef(0)).unwrap_err(),
1511            ReductionError::TypeError(TypeError::CantApply(
1512                LambdaType::t().clone(),
1513                LambdaType::at().clone()
1514            ))
1515        );
1516
1517        let mut pool = LambdaPool::<()>(vec![
1518            LambdaExpr::Application {
1519                subformula: LambdaExprRef(1),
1520                argument: LambdaExprRef(3),
1521            },
1522            LambdaExpr::Lambda(LambdaExprRef(2), LambdaType::a().clone()),
1523            LambdaExpr::BoundVariable(0, LambdaType::t().clone()),
1524            LambdaExpr::FreeVariable("0".into(), LambdaType::a().clone()),
1525        ]);
1526        assert!(pool.reduce(LambdaExprRef(0)).is_ok());
1527        Ok(())
1528    }
1529
1530    #[test]
1531    fn complicated_lambda() -> anyhow::Result<()> {
1532        // [[[Mary sings] and]  [John dances]]
1533        let mut pool = LambdaPool::<()>(vec![
1534            LambdaExpr::Application {
1535                subformula: LambdaExprRef(5),
1536                argument: LambdaExprRef(1),
1537            },
1538            LambdaExpr::Application {
1539                //John dances
1540                subformula: LambdaExprRef(2),
1541                argument: LambdaExprRef(4),
1542            },
1543            LambdaExpr::Lambda(LambdaExprRef(3), LambdaType::e().clone()),
1544            LambdaExpr::FreeVariable("0".into(), LambdaType::t().clone()),
1545            LambdaExpr::FreeVariable("2".into(), LambdaType::t().clone()),
1546            // 5
1547            //\lambda x. Mary sings and
1548            LambdaExpr::Application {
1549                subformula: LambdaExprRef(6),
1550                argument: LambdaExprRef(9),
1551            },
1552            LambdaExpr::Lambda(LambdaExprRef(7), LambdaType::t().clone()),
1553            LambdaExpr::Lambda(LambdaExprRef(8), LambdaType::t().clone()),
1554            LambdaExpr::BoundVariable(1, LambdaType::t().clone()),
1555            LambdaExpr::Application {
1556                //10
1557                subformula: LambdaExprRef(10),
1558                argument: LambdaExprRef(12),
1559            },
1560            LambdaExpr::Lambda(LambdaExprRef(11), LambdaType::e().clone()),
1561            LambdaExpr::FreeVariable("1337".into(), LambdaType::t().clone()),
1562            LambdaExpr::FreeVariable("5".into(), LambdaType::e().clone()),
1563        ]);
1564        pool.reduce(LambdaExprRef(0))?;
1565        pool.cleanup(LambdaExprRef(0));
1566        assert_eq!(
1567            pool,
1568            LambdaPool(vec![LambdaExpr::FreeVariable(
1569                "1337".into(),
1570                LambdaType::t().clone()
1571            )])
1572        );
1573        Ok(())
1574    }
1575
1576    #[test]
1577    fn test_lambda_calculus() -> anyhow::Result<()> {
1578        let mut pool = LambdaPool::<()>(
1579            k(0)?
1580                .into_iter()
1581                .chain([
1582                    LambdaExpr::FreeVariable("32".into(), LambdaType::e().clone()),
1583                    LambdaExpr::Application {
1584                        subformula: LambdaExprRef(0),
1585                        argument: LambdaExprRef(3),
1586                    },
1587                ])
1588                .collect(),
1589        );
1590        let root = LambdaExprRef(4);
1591        pool.beta_reduce(root)?;
1592        pool.cleanup(root);
1593
1594        assert_eq!(
1595            pool,
1596            LambdaPool(vec![
1597                LambdaExpr::FreeVariable("32".into(), LambdaType::e().clone()),
1598                LambdaExpr::Lambda(LambdaExprRef(0), LambdaType::e().clone())
1599            ])
1600        );
1601        Ok(())
1602    }
1603
1604    #[test]
1605    fn test_root_and_merger() -> anyhow::Result<()> {
1606        let man = RootedLambdaPool::parse("lambda a x (pa_man(x))")?;
1607
1608        let sleeps =
1609            RootedLambdaPool::parse("lambda a x (some_e(y, all_e, AgentOf(x, y) & pe_sleep(y)))")?;
1610        let every =
1611            RootedLambdaPool::parse("lambda <a,t> p (lambda <a,t> q every(x, p(x), q(x)))")?;
1612
1613        let phi = every.clone().merge(man.clone()).unwrap();
1614        let mut phi = phi.merge(sleeps.clone()).unwrap();
1615        println!("{phi}");
1616        phi.reduce()?;
1617        println!("{phi}");
1618        assert_eq!(
1619            phi,
1620            RootedLambdaPool::parse(
1621                "every(x, pa_man(x), some_e(y, all_e, AgentOf(x, y) & pe_sleep(y)))"
1622            )?
1623        );
1624        assert!(check_hashes(
1625            &phi,
1626            &RootedLambdaPool::parse(
1627                "every(x, pa_man(x), some_e(y, all_e, AgentOf(x, y) & pe_sleep(y)))",
1628            )?,
1629        ));
1630        let pool = phi.into_pool()?;
1631        assert_eq!(
1632            "every(x, pa_man(x), some_e(y, all_e, AgentOf(x, y) & pe_sleep(y)))",
1633            pool.to_string()
1634        );
1635        let phi = man.merge(every).unwrap();
1636        let mut phi = sleeps.merge(phi).unwrap();
1637        phi.reduce()?;
1638        assert_eq!(
1639            phi,
1640            RootedLambdaPool::parse(
1641                "every(x, pa_man(x), some_e(y, all_e, AgentOf(x, y) & pe_sleep(y)))",
1642            )?
1643        );
1644
1645        assert!(check_hashes(
1646            &phi,
1647            &RootedLambdaPool::parse(
1648                "every(x, pa_man(x), some_e(y, all_e, AgentOf(x, y) & pe_sleep(y)))",
1649            )?,
1650        ));
1651
1652        let pool = phi.into_pool()?;
1653        assert_eq!(
1654            "every(x, pa_man(x), some_e(y, all_e, AgentOf(x, y) & pe_sleep(y)))",
1655            pool.to_string()
1656        );
1657        Ok(())
1658    }
1659
1660    fn check_hashes<'src>(
1661        phi: &RootedLambdaPool<'src, Expr<'src>>,
1662        psi: &RootedLambdaPool<'src, Expr<'src>>,
1663    ) -> bool {
1664        let mut hasher1 = DefaultHasher::new();
1665        let mut hasher2 = DefaultHasher::new();
1666
1667        phi.hash(&mut hasher1);
1668        psi.hash(&mut hasher2);
1669
1670        hasher1.finish() == hasher2.finish()
1671    }
1672
1673    #[test]
1674    fn bind_free_variable() -> anyhow::Result<()> {
1675        let mut pool = RootedLambdaPool::parse("phi#t & True")?;
1676
1677        pool.bind_free_variable("phi".into(), RootedLambdaPool::parse("False")?)?;
1678        assert_eq!("False & True", pool.into_pool()?.to_string());
1679
1680        let input = RootedLambdaPool::parse("lambda a x every_e(y,pe_4,AgentOf(x,y))")?;
1681        let mut a = RootedLambdaPool::parse("(P#<a,t>(a_3) & ~P#<a,t>(a_1))")?;
1682
1683        a.bind_free_variable("P".into(), input)?;
1684        a.reduce()?;
1685        assert_eq!(
1686            a.to_string(),
1687            "every_e(x, pe_4, AgentOf(a_3, x)) & ~every_e(x, pe_4, AgentOf(a_1, x))"
1688        );
1689        Ok(())
1690    }
1691
1692    #[test]
1693    fn apply_new_free_variable() -> anyhow::Result<()> {
1694        let mut pool =
1695            RootedLambdaPool::parse("lambda <e,t> P (lambda <e,t> Q (lambda e x (P(x) & Q(x))))")?;
1696
1697        pool.apply_new_free_variable("X".into())?;
1698
1699        let gold_pool = RootedLambdaPool {
1700            pool: LambdaPool(vec![
1701                LambdaExpr::FreeVariable("X".into(), LambdaType::et().clone()),
1702                LambdaExpr::BoundVariable(0, LambdaType::e().clone()),
1703                LambdaExpr::Application {
1704                    subformula: LambdaExprRef(0),
1705                    argument: LambdaExprRef(1),
1706                },
1707                LambdaExpr::BoundVariable(1, LambdaType::et().clone()),
1708                LambdaExpr::BoundVariable(0, LambdaType::e().clone()),
1709                LambdaExpr::Application {
1710                    subformula: LambdaExprRef(3),
1711                    argument: LambdaExprRef(4),
1712                },
1713                LambdaExpr::LanguageOfThoughtExpr(Expr::Binary(BinOp::And, ExprRef(2), ExprRef(5))),
1714                LambdaExpr::Lambda(LambdaExprRef(6), LambdaType::e().clone()),
1715                LambdaExpr::Lambda(LambdaExprRef(7), LambdaType::et().clone()),
1716            ]),
1717            root: LambdaExprRef(8),
1718        };
1719        pool.cleanup();
1720        assert_eq!(pool, gold_pool);
1721        Ok(())
1722    }
1723
1724    #[test]
1725    fn lambda_abstraction() -> anyhow::Result<()> {
1726        let mut pool = RootedLambdaPool::parse(
1727            "lambda <e,t> P lambda <e,t> Q lambda e x Z#<e,t>(x) & P(x) & Q(x)",
1728        )?;
1729
1730        pool.lambda_abstract_free_variable("Z".into(), LambdaType::et().clone(), false)?;
1731
1732        let gold_pool = RootedLambdaPool {
1733            pool: LambdaPool(vec![
1734                LambdaExpr::BoundVariable(3, LambdaType::et().clone()),
1735                LambdaExpr::BoundVariable(0, LambdaType::e().clone()),
1736                LambdaExpr::Application {
1737                    subformula: LambdaExprRef(0),
1738                    argument: LambdaExprRef(1),
1739                },
1740                LambdaExpr::BoundVariable(2, LambdaType::et().clone()),
1741                LambdaExpr::BoundVariable(0, LambdaType::e().clone()),
1742                LambdaExpr::Application {
1743                    subformula: LambdaExprRef(3),
1744                    argument: LambdaExprRef(4),
1745                },
1746                LambdaExpr::LanguageOfThoughtExpr(Expr::Binary(BinOp::And, ExprRef(2), ExprRef(5))),
1747                LambdaExpr::BoundVariable(1, LambdaType::et().clone()),
1748                LambdaExpr::BoundVariable(0, LambdaType::e().clone()),
1749                LambdaExpr::Application {
1750                    subformula: LambdaExprRef(7),
1751                    argument: LambdaExprRef(8),
1752                },
1753                LambdaExpr::LanguageOfThoughtExpr(Expr::Binary(BinOp::And, ExprRef(6), ExprRef(9))),
1754                LambdaExpr::Lambda(LambdaExprRef(10), LambdaType::e().clone()),
1755                LambdaExpr::Lambda(LambdaExprRef(11), LambdaType::et().clone()),
1756                LambdaExpr::Lambda(LambdaExprRef(12), LambdaType::et().clone()),
1757                LambdaExpr::Lambda(LambdaExprRef(13), LambdaType::et().clone()),
1758            ]),
1759            root: LambdaExprRef(14),
1760        };
1761
1762        assert_eq!(pool, gold_pool);
1763        Ok(())
1764    }
1765
1766    #[test]
1767    fn could_time_out_if_swapping_instead_of_cloning() -> anyhow::Result<()> {
1768        let mut x = RootedLambdaPool::parse(
1769            "(lambda a x (PatientOf(x,e_0) & AgentOf(x, e_0)))((lambda a x (a_1))(a_0))",
1770        )?;
1771
1772        println!("{x}");
1773        x.reduce()?;
1774        println!("{x}");
1775        Ok(())
1776    }
1777
1778    #[test]
1779    fn lambda_abstraction_reduction() -> anyhow::Result<()> {
1780        let mut a = RootedLambdaPool::parse("a_1")?;
1781        let mut b = RootedLambdaPool::parse("(lambda t x (a_1))(pa_0(freeVar#a))")?;
1782
1783        a.lambda_abstract_free_variable("freeVar".into(), LambdaType::a().clone(), false)?;
1784        b.lambda_abstract_free_variable("freeVar".into(), LambdaType::a().clone(), false)?;
1785        println!("A:\t{a}");
1786        println!("B:\t{b}");
1787
1788        a.cleanup();
1789        b.cleanup();
1790        assert_eq!(a, b);
1791        Ok(())
1792    }
1793
1794    #[test]
1795    fn reduction_test() -> anyhow::Result<()> {
1796        let mut a = RootedLambdaPool::parse(
1797            "lambda a x (every_e(z, all_e, AgentOf(a_0, (lambda e y ((lambda e w (w))(y)))(z))))",
1798        )?;
1799        a.reduce()?;
1800
1801        let mut a = RootedLambdaPool::parse(
1802            "(lambda <a,t> P (P(a_3) & ~P(a_1)))(lambda a x (every_e(y,pe_4,AgentOf(x,y))))",
1803        )?;
1804
1805        a.pool.beta_reduce(a.root)?;
1806        a.root = a.pool.cleanup(a.root);
1807        println!("{a}");
1808        dbg!(&a);
1809
1810        let mut a = RootedLambdaPool::parse(
1811            "(lambda <a,t> P (P(a_3) & ~P(a_1)))(lambda a x (every_e(y,pe_4,AgentOf(x,y))))",
1812        )?;
1813
1814        a.reduce()?;
1815        assert_eq!(
1816            a.to_string(),
1817            "every_e(x, pe_4, AgentOf(a_3, x)) & ~every_e(x, pe_4, AgentOf(a_1, x))"
1818        );
1819
1820        Ok(())
1821    }
1822
1823    #[test]
1824    fn lift() -> anyhow::Result<()> {
1825        let mut e = RootedLambdaPool::parse("a_john")?;
1826        e.lift()?;
1827        assert_eq!(e.to_string(), "lambda <a,t> P P(a_john)");
1828
1829        Ok(())
1830    }
1831
1832    #[test]
1833    fn lambda_abstractions() -> anyhow::Result<()> {
1834        let mut e = RootedLambdaPool::parse(
1835            "(lambda t phi phi)(some_e(x, all_e, AgentOf(a_m, x) & PatientOf(blarg#a, x) & pe_likes(x)))",
1836        )?;
1837        e.reduce()?;
1838        e.lambda_abstract_free_variable(FreeVar::Named("blarg"), LambdaType::A, false)
1839            .unwrap();
1840        assert_eq!(
1841            e.to_string(),
1842            "lambda a x some_e(y, all_e, AgentOf(a_m, y) & PatientOf(x, y) & pe_likes(y))"
1843        );
1844        Ok(())
1845    }
1846
1847    #[test]
1848    fn is_constant_function() -> anyhow::Result<()> {
1849        let constants = [
1850            "lambda a x a_John",
1851            "lambda a x lambda a y pa_man(x)",
1852            "lambda a x some_e(y, all_e, pe_runs(y))",
1853        ];
1854        for s in constants {
1855            println!("{s}");
1856            let LambdaSummaryStats::WellFormed {
1857                lambda_type: _,
1858                constant_function,
1859                n_nodes: _,
1860            } = RootedLambdaPool::parse(s).unwrap().stats()
1861            else {
1862                panic!("{s} is poorly formed")
1863            };
1864            assert!(constant_function);
1865        }
1866
1867        let not_constants = [
1868            "lambda a x x",
1869            "lambda a x lambda a y pa_man(x) & pa_woman(y)",
1870        ];
1871        for s in not_constants {
1872            println!("{s}");
1873            let LambdaSummaryStats::WellFormed {
1874                lambda_type: _,
1875                constant_function,
1876                n_nodes: _,
1877            } = RootedLambdaPool::parse(s).unwrap().stats()
1878            else {
1879                panic!("{s} is poorly formed")
1880            };
1881            assert!(!constant_function);
1882        }
1883        Ok(())
1884    }
1885}
simple_semantics/lambda.rs

simple_semantics/
lambda.rs
