Lines
95.08 %
Functions
45.45 %
use conjure_cp::ast::Expression as Expr;
use conjure_cp::ast::GroundDomain;
use conjure_cp::ast::Moo;
use conjure_cp::ast::SymbolTable;
use conjure_cp::into_matrix_expr;
use conjure_cp::matrix_expr;
use conjure_cp::rule_engine::{
ApplicationError::RuleNotApplicable, ApplicationResult, Reduction, register_rule,
};
use conjure_cp::ast::Atom;
use conjure_cp::ast::Expression;
use conjure_cp::ast::Literal;
use conjure_cp::ast::Metadata;
use conjure_cp::ast::Name;
use conjure_cp::rule_engine::ApplicationError;
use itertools::izip;
//takes a safe index expression and converts it to an atom via the representation rules
#[register_rule(("Base", 2000))]
fn index_record_to_atom(expr: &Expr, symbols: &SymbolTable) -> ApplicationResult {
// annoyingly, let chaining only works in if-lets, not let-elses,otherwise I could avoid the
// indentation here!
if let Expr::SafeIndex(_, subject, indices) = expr
&& let Expr::Atomic(_, Atom::Reference(decl)) = &**subject
&& let Name::WithRepresentation(name, reprs) = &decl.name() as &Name
{
if reprs.first().is_none_or(|x| x.as_str() != "record_to_atom") {
return Err(RuleNotApplicable);
}
// tuples are always one dimensional
if indices.len() != 1 {
let repr = symbols
.get_representation(name, &["record_to_atom"])
.unwrap()[0]
.clone();
let Some(GroundDomain::Record(_)) = decl.resolved_domain().as_deref() else {
assert_eq!(
indices.len(),
1,
"record indexing is always one dimensional"
);
let index = indices[0].clone();
// during the conversion from unsafe index to safe index in bubbling
// we convert the field name to a literal integer for direct access
let Some(index) = index.into_literal() else {
return Err(RuleNotApplicable); // we don't support non-literal indices
let indices_as_name = Name::Represented(Box::new((
name.as_ref().clone(),
"record_to_atom".into(),
index.into(),
)));
let subject = repr.expression_down(symbols)?[&indices_as_name].clone();
Ok(Reduction::pure(subject))
} else {
Err(RuleNotApplicable)
#[register_rule(("Bubble", 8000))]
fn record_index_to_bubble(expr: &Expr, _: &SymbolTable) -> ApplicationResult {
if let Expr::UnsafeIndex(_, subject, indices) = expr
&& let Name::WithRepresentation(_, reprs) = &decl.name() as &Name
let domain = subject
.domain_of()
.ok_or(ApplicationError::DomainError)?
.resolve()
.ok_or(ApplicationError::DomainError)?;
let GroundDomain::Record(elems) = domain.as_ref() else {
let Expr::Atomic(_, Atom::Reference(decl)) = index else {
let name: &Name = &decl.name();
// find what numerical index in elems matches the entry name
let Some(idx) = elems.iter().position(|x| &x.name == name) else {
// converting to an integer for direct access
let idx = Expr::Atomic(Metadata::new(), Atom::Literal(Literal::Int(idx as i32 + 1)));
let bubble_constraint = Moo::new(Expression::And(
Metadata::new(),
Moo::new(matrix_expr![
Expression::Leq(
Moo::new(idx.clone()),
Moo::new(Expression::Atomic(
Atom::Literal(Literal::Int(elems.len() as i32))
))
),
Expression::Geq(
Atom::Literal(Literal::Int(1))
)
]),
));
let new_expr = Moo::new(Expression::SafeIndex(
subject.clone(),
Vec::from([idx]),
Ok(Reduction::pure(Expression::Bubble(
new_expr,
bubble_constraint,
)))
// dealing with equality over 2 record variables
fn record_equality(expr: &Expr, _: &SymbolTable) -> ApplicationResult {
// annoyingly, let chaining only works in if-lets, not let-elses, otherwise I could avoid the
// check if both sides are record variables
if let Expr::Eq(_, left, right) = expr
&& let Expr::Atomic(_, Atom::Reference(decl)) = &**left
&& let Expr::Atomic(_, Atom::Reference(decl2)) = &**right
&& let Name::WithRepresentation(_, reprs2) = &decl2.name() as &Name
// .. that have been represented with record_to_atom
&& reprs.first().is_none_or(|x| x.as_str() == "record_to_atom")
&& reprs2.first().is_none_or(|x| x.as_str() == "record_to_atom")
&& let Some(domain) = decl.resolved_domain()
&& let Some(domain2) = decl2.resolved_domain()
// .. and have record variable domains
&& let GroundDomain::Record(entries) = domain.as_ref()
&& let GroundDomain::Record(entries2) = domain2.as_ref()
// we only support equality over records of the same size
&& entries.len() == entries2.len()
// assuming all record entry names must match for equality
&& izip!(entries,entries2).all(|(entry1,entry2)| entry1.name == entry2.name)
let mut equality_constraints = vec![];
// unroll the equality into equality constraints for each field
for i in 0..entries.len() {
let left_elem = Expression::SafeIndex(
Moo::clone(left),
vec![Expression::Atomic(
Atom::Literal(Literal::Int((i + 1) as i32)),
)],
let right_elem = Expression::SafeIndex(
Moo::clone(right),
equality_constraints.push(Expression::Eq(
Moo::new(left_elem),
Moo::new(right_elem),
let new_expr = Expression::And(
Moo::new(into_matrix_expr!(equality_constraints)),
Ok(Reduction::pure(new_expr))
// dealing with equality where the left is a record variable, and the right is a constant record
fn record_to_const(expr: &Expr, _: &SymbolTable) -> ApplicationResult {
let domain = decl
.resolved_domain()
let GroundDomain::Record(entries) = domain.as_ref() else {
let Some(rhs_record_names) = crate::utils::constant_record_names(right.as_ref()) else {
if entries.len() != rhs_record_names.len() {
if entries[i].name != rhs_record_names[i] {