ttt/
substitute.rs

1use std::any::{TypeId, type_name};
2
3use thiserror::Error;
4
5#[derive(Debug, Error, PartialEq, Clone)]
6#[error(
7    "Tried to substitute a variable of kind {} for an expression of kind {}",
8    substitutand_type_name,
9    substitutee_type_name
10)]
11pub struct SubstError {
12    substitutee_type: TypeId,
13    substitutand_type: TypeId,
14    substitutee_type_name: &'static str,
15    substitutand_type_name: &'static str,
16}
17
18impl SubstError {
19    pub fn new<T, U>() -> Self
20    where
21        T: 'static,
22        U: 'static,
23    {
24        Self {
25            substitutee_type: TypeId::of::<T>(),
26            substitutand_type: TypeId::of::<U>(),
27            substitutee_type_name: type_name::<T>(),
28            substitutand_type_name: type_name::<U>(),
29        }
30    }
31}
32
33/// A syntax node which admits a substitution operation.
34pub trait Substitute<SubstExpr> {
35    /// The result of substituting an expression for a variable in this term. For
36    /// most AST types this will be `Self`.
37    type Target;
38
39    /// The type of errors which may occur during substitution.
40    /// In the simple case where `SubstExpr == Target` this should usually be set to
41    /// `std::convert::Infallible`.
42    /// However, in more complex cases you may want to implement `Substitute<E>` for other values of `E` (such as where you have mutually recursive expression types, each which may contain variables).
43    /// In such cases `substitute` must handle the case where the variable index refers to a position in the wrong type of expression.
44    /// N.B. currently the derive macro for `Substitute` will always use `SubstError` as the error type.
45    type Error;
46
47    /// Substitute `expr` into any variables in the expression matching the specified
48    /// de Bruijn index.
49    fn substitute(
50        &self,
51        expr: &SubstExpr,
52        var: usize,
53    ) -> Result<Self::Target, Self::Error>;
54}
55
56impl<T, U> Substitute<U> for Box<T>
57where
58    T: Substitute<U>,
59{
60    type Target = Box<T::Target>;
61    type Error = T::Error;
62
63    fn substitute(
64        &self,
65        expr: &U,
66        var: usize,
67    ) -> Result<Self::Target, Self::Error> {
68        Ok(Box::new((**self).substitute(expr, var)?))
69    }
70}
ttt/substitute.rs

ttt/
substitute.rs
