conjure_core/rules/
subsitute_lettings.rs

Help
1use std::rc::Rc;
2
3use conjure_macros::register_rule;
4
5use crate::{
6    ast::{Atom, Expression as Expr, SymbolTable},
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))]
19fn substitute_value_lettings(expr: &Expr, symbols: &SymbolTable) -> ApplicationResult {
20    let Expr::Atomic(_, Atom::Reference(name)) = expr else {
21        return Err(RuleNotApplicable);
22    };
23
24    let decl = symbols.lookup(name).ok_or(RuleNotApplicable)?;
25    let value = decl.as_value_letting().ok_or(RuleNotApplicable)?;
26
27    Ok(Reduction::pure(value.clone()))
28}
29
30/// Substitutes domain lettings for their values in the symbol table.
31#[register_rule(("Base", 5000))]
32fn substitute_domain_lettings(expr: &Expr, symbols: &SymbolTable) -> ApplicationResult {
33    let Expr::Root(_, _) = expr else {
34        return Err(RuleNotApplicable);
35    };
36
37    let mut new_symbols = symbols.clone();
38    let mut has_changed = false;
39
40    for (_, mut decl) in symbols.clone().into_iter_local() {
41        let Some(mut var) = decl.as_var().cloned() else {
42            continue;
43        };
44
45        let old_domain = var.domain;
46        var.domain = old_domain.clone().resolve(symbols);
47        if old_domain != var.domain {
48            *(Rc::make_mut(&mut decl).as_var_mut().unwrap()) = var;
49            has_changed = true;
50            new_symbols.update_insert(decl);
51        };
52    }
53    if has_changed {
54        Ok(Reduction::with_symbols(expr.clone(), new_symbols))
55    } else {
56        Err(RuleNotApplicable)
57    }
58}
conjure_core/rules/subsitute_lettings.rs

conjure_core/rules/
subsitute_lettings.rs
