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

simple_semantics/
lambda.rs
