Method insert_expression

src/transform/src/cse/anf.rs:129–313

Ensures `self` contains bindings for all of `relation`'s subexpressions, including itself, and replaces `relation` with a reference to its corresponding identifier. The algorithm performs a post-order traversal of the expression tree, binding each distinct expression to a new local identifier and replacing each expression with a reference to the identifier for the expression. It maintains the inv

(
        &mut self,
        id_gen: &mut IdGen,
        relation: &mut MirRelationExpr,
    )

    /// can break if `body` acquires a reference to an arranged term, as that arrangement is not
    /// available outside the loop).
    fn insert_expression(
        &mut self,
        id_gen: &mut IdGen,
        relation: &mut MirRelationExpr,
    ) -> Result<(), crate::TransformError> {
        self.checked_recur_mut(|this| {
            match relation {
                MirRelationExpr::LetRec {
                    ids,
                    values,
                    body,
                    limits,
                } => {
                    // Used for `zip_eq`.
                    use itertools::Itertools;

                    // Introduce a new copy of `self`, which will be specific to this scope.
                    // This makes expressions used in the outer scope available for re-use.
                    // We will discard `scoped_anf` once we have processed the `LetRec`.
                    let mut scoped_anf = this.clone();

                    // Used to distinguish new bindings from old bindings.
                    // This is needed to extract from `scoped_anf` only the bindings added
                    // in this block, and not those inherited from `self`.
                    let id_boundary = id_gen.allocate_id();

                    // Each identifier in `ids` will be given *two* new identifiers,
                    // initially one "before" and then once bound another one "after".
                    // The two identifiers are important to distinguish references to the
                    // binding "before" it is refreshed, and "after" it is refreshed.
                    // We can equate two "before" references and two "after" references,
                    // but we must not equate a "before" and an "after" reference.

                    // For each bound identifier from `ids`, a temporary identifier for the "before" version.
                    let before_ids = ids
                        .iter()
                        .map(|_id| LocalId::new(id_gen.allocate_id()))
                        .collect::<Vec<_>>();
                    let mut after_ids = Vec::new();

                    // Install the "before" rebindings to start.
                    // These rebindings will be used for each binding until we process the binding.
                    scoped_anf
                        .rebindings
                        .extend(ids.iter().zip_eq(before_ids.iter()).map(|(x, y)| (*x, *y)));

                    // Convert each bound expression into a sequence of let bindings, which are appended
                    // to the sequence of let bindings from prior bound expressions.
                    // After visiting the expression, we'll update the binding for the `id` to its "after"
                    // identifier.
                    for (index, value) in values.iter_mut().enumerate() {
                        scoped_anf.insert_expression(id_gen, value)?;
                        // Update the binding for `ids[index]` from its "before" id to a new "after" id.
                        let new_id = id_gen.allocate_id();
                        after_ids.push(new_id);
                        scoped_anf
                            .rebindings
                            .insert(ids[index].clone(), LocalId::new(new_id));