1 
use conjure_cp::rule_engine::register_rule;
2 

            

        

            

                3
            

            

                
            

            

                
use conjure_cp::ast::DomainPtr;

            

        

            

                4
            

            

                
            

            

                
use conjure_cp::{

            

        

            

                5
            

            

                
            

            

                
    ast::{Atom, Expression as Expr, SymbolTable},

            

        

            

                6
            

            

                
            

            

                
    bug,

            

        

            

                7
            

            

                
            

            

                
    rule_engine::{ApplicationError::RuleNotApplicable, ApplicationResult, Reduction},

            

        

            

                8
            

            

                
            

            

                
};

            

        

            

                9
            

            

                
            

            

                

            

        

            

                10
            

            

                
            

            

                
/// Substitutes value lettings for their values.

            

        

            

                11
            

            

                
            

            

                
///

            

        

            

                12
            

            

                
            

            

                
/// # Priority

            

        

            

                13
            

            

                
            

            

                
///

            

        

            

                14
            

            

                
            

            

                
/// This rule must have a higher priority than solver-flattening rules (which should be priority 4000).

            

        

            

                15
            

            

                
            

            

                
///

            

        

            

                16
            

            

                
            

            

                
/// Otherwise, the letting may be put into a flat constraint, as it is a reference. At this point

            

        

            

                17
            

            

                
            

            

                
/// it ceases to be an expression, so we cannot match over it.

            

        

            

                18
            

            

                
            

            

                
#[register_rule(("Base", 5000))]

            

        

            

                19
            

            

                
            

            

                
fn substitute_value_lettings(expr: &Expr, _: &SymbolTable) -> ApplicationResult {

            

        

            

                20
            

            

                
            

            

                
    let Expr::Atomic(_, Atom::Reference(decl)) = expr else {

            

        

            

                21
            

            

                
            

            

                
        return Err(RuleNotApplicable);

            

        

            

                22
            

            

                
            

            

                
    };

            

        

            

                23
            

            

                
            

            

                

            

        

            

                24
            

            

                
            

            

                
    let value = decl.ptr().as_value_letting().ok_or(RuleNotApplicable)?;

            

        

            

                25
            

            

                
            

            

                

            

        

            

                26
            

            

                
            

            

                
    Ok(Reduction::pure(value.clone()))

            

        

            

                27
            

            

                
            

            

                
}

            

        

            

                28
            

            

                
            

            

                

            

        

            

                29
            

            

                
            

            

                
/// Substitutes domain lettings for their values in the symbol table.

            

        

            

                30
            

            

                
            

            

                
#[register_rule(("Base", 5000))]

            

        

            

                31
            

            

                
            

            

                
fn substitute_domain_lettings(expr: &Expr, symbols: &SymbolTable) -> ApplicationResult {

            

        

            

                32
            

            

                
            

            

                
    let Expr::Root(_, _) = expr else {

            

        

            

                33
            

            

                
            

            

                
        return Err(RuleNotApplicable);

            

        

            

                34
            

            

                
            

            

                
    };

            

        

            

                35
            

            

                
            

            

                

            

        

            

                36
            

            

                
            

            

                
    let mut new_symbols = symbols.clone();

            

        

            

                37
            

            

                
            

            

                
    let mut has_changed = false;

            

        

            

                38
            

            

                
            

            

                

            

        

            

                39
            

            

                
            

            

                
    for (_, mut decl) in symbols.clone().into_iter_local() {

            

        

            

                40
            

            

                
            

            

                
        let Some(mut var) = decl.as_var().map(|x| x.clone()) else {

            

        

            

                41
            

            

                
            

            

                
            continue;

            

        

            

                42
            

            

                
            

            

                
        };

            

        

            

                43
            

            

                
            

            

                

            

        

            

                44
            

            

                
            

            

                
        let old_domain = var.domain;

            

        

            

                45
            

            

                
            

            

                
        let domain_gd = old_domain

            

        

            

                46
            

            

                
            

            

                
            .resolve()

            

        

            

                47
            

            

                
            

            

                
            .unwrap_or_else(|| bug!("Domain of {} could not be resolved", decl.name()));

            

        

            

                48
            

            

                
            

            

                
        var.domain = DomainPtr::from(domain_gd);

            

        

            

                49
            

            

                
            

            

                
        if old_domain != var.domain {

            

        

            

                50
            

            

                
            

            

                
            decl.as_var_mut().unwrap().domain = var.domain;

            

        

            

                51
            

            

                
            

            

                
            has_changed = true;

            

        

            

                52
            

            

                
            

            

                
            new_symbols.update_insert(decl);

            

        

            

                53
            

            

                
            

            

                
        };

            

        

            

                54
            

            

                
            

            

                
    }

            

        

            

                55
            

            

                
            

            

                
    if has_changed {

            

        

            

                56
            

            

                
            

            

                
        Ok(Reduction::with_symbols(expr.clone(), new_symbols))

            

        

            

                57
            

            

                
            

            

                
    } else {

            

        

            

                58
            

            

                
            

            

                
        Err(RuleNotApplicable)

            

        

            

                59
            

            

                
            

            

                
    }

            

        

            

                60
            

            

                
            

            

                
}