conjure_core/rules/
subsitute_lettings.rs

1use std::rc::Rc;
2
3use conjure_macros::register_rule;
4
5use crate::{
6    ast::{Atom, Domain, Expression as Expr, SymbolTable},
7    bug,
8    rule_engine::{ApplicationError::RuleNotApplicable, ApplicationResult, Reduction},
9};
10
11/// Substitutes value lettings for their values.
12///
13/// # Priority
14///
15/// This rule must have a higher priority than solver-flattening rules (which should be priority 4000).
16///
17/// Otherwise, the letting may be put into a flat constraint, as it is a reference. At this point
18/// it ceases to be an expression, so we cannot match over it.
19#[register_rule(("Base", 5000))]
20fn substitute_value_lettings(expr: &Expr, symbols: &SymbolTable) -> ApplicationResult {
21    let Expr::Atomic(_, Atom::Reference(name)) = expr else {
22        return Err(RuleNotApplicable);
23    };
24
25    let decl = symbols.lookup(name).ok_or(RuleNotApplicable)?;
26    let value = decl.as_value_letting().ok_or(RuleNotApplicable)?;
27
28    Ok(Reduction::pure(value.clone()))
29}
30
31/// Substitutes domain lettings for their values in the symbol table.
32#[register_rule(("Base", 5000))]
33fn substitute_domain_lettings(expr: &Expr, symbols: &SymbolTable) -> ApplicationResult {
34    let mut new_symbols = symbols.clone();
35    let mut has_changed = false;
36
37    for (_, mut decl) in symbols.clone().into_iter() {
38        let Some(mut var) = decl.as_var().cloned() else {
39            continue;
40        };
41
42        if let Domain::DomainReference(ref d) = var.domain {
43            var.domain = symbols.domain(d).unwrap_or_else(|| {
44                bug!(
45                    "rule substitute_domain_lettings: domain reference {} does not exist",
46                    d
47                )
48            });
49            *(Rc::make_mut(&mut decl).as_var_mut().unwrap()) = var;
50            has_changed = true;
51        };
52
53        new_symbols.update_insert(decl);
54    }
55    if has_changed {
56        Ok(Reduction::with_symbols(expr.clone(), new_symbols))
57    } else {
58        Err(RuleNotApplicable)
59    }
60}
conjure_core/rules/subsitute_lettings.rs

conjure_core/rules/
subsitute_lettings.rs
