1
use conjure_cp::ast::Expression as Expr;
2
use conjure_cp::ast::GroundDomain;
3
use conjure_cp::ast::Moo;
4
use conjure_cp::ast::SymbolTable;
5
use conjure_cp::into_matrix_expr;
6
use conjure_cp::rule_engine::{
7
    ApplicationError::RuleNotApplicable, ApplicationResult, Reduction, register_rule,
8
};
9

            
10
use conjure_cp::ast::Atom;
11
use conjure_cp::ast::Expression;
12
use conjure_cp::ast::Literal;
13
use conjure_cp::ast::Metadata;
14
use conjure_cp::ast::Name;
15
use conjure_cp::rule_engine::ApplicationError;
16
use itertools::izip;
17

            
18
// takes a record field access and converts it to an atom via the representation rules
19
#[register_rule("Base", 2000, [RecordField])]
20
169872
fn index_record_to_atom(expr: &Expr, symbols: &SymbolTable) -> ApplicationResult {
21
    // annoyingly, let chaining only works in if-lets, not let-elses, otherwise I could avoid the
22
    // indentation here!
23
169872
    if let Expr::RecordField(_, subject, field_name) = expr
24
96
        && let Expr::Atomic(_, Atom::Reference(decl)) = &**subject
25
96
        && let Name::WithRepresentation(name, reprs) = &decl.name() as &Name
26
    {
27
96
        if reprs.first().is_none_or(|x| x.as_str() != "record_to_atom") {
28
            return Err(RuleNotApplicable);
29
96
        }
30

            
31
96
        let repr = symbols
32
96
            .get_representation(name, &["record_to_atom"])
33
96
            .unwrap()[0]
34
96
            .clone();
35

            
36
        // bind the domain to a variable so the borrowed entries outlive this statement
37
96
        let domain = decl.resolved_domain();
38
96
        let Some(GroundDomain::Record(entries)) = domain.as_deref() else {
39
            return Err(RuleNotApplicable);
40
        };
41

            
42
        // find the numerical index of the field name in the record, and convert it to an integer
43
        // literal for direct access (the representation indexes its variables by integer)
44
144
        let Some(idx) = entries.iter().position(|entry| &entry.name == field_name) else {
45
            return Err(RuleNotApplicable);
46
        };
47

            
48
96
        let index = Literal::Int(idx as i32 + 1);
49

            
50
96
        let indices_as_name = Name::Represented(Box::new((
51
96
            name.as_ref().clone(),
52
96
            "record_to_atom".into(),
53
96
            index.into(),
54
96
        )));
55

            
56
96
        let subject = repr.expression_down(symbols)?[&indices_as_name].clone();
57

            
58
96
        Ok(Reduction::pure(subject))
59
    } else {
60
169776
        Err(RuleNotApplicable)
61
    }
62
169872
}
63

            
64
// dealing with equality over 2 record variables
65
#[register_rule("Base", 2000, [Eq])]
66
169872
fn record_equality(expr: &Expr, _: &SymbolTable) -> ApplicationResult {
67
    // annoyingly, let chaining only works in if-lets, not let-elses, otherwise I could avoid the
68
    // indentation here!
69

            
70
    // check if both sides are record variables
71
169872
    if let Expr::Eq(_, left, right) = expr
72
5635
        && let Expr::Atomic(_, Atom::Reference(decl)) = &**left
73
2983
        && let Name::WithRepresentation(_, reprs) = &decl.name() as &Name
74
60
        && let Expr::Atomic(_, Atom::Reference(decl2)) = &**right
75
24
        && let Name::WithRepresentation(_, reprs2) = &decl2.name() as &Name
76

            
77
        // .. that have been represented with record_to_atom
78
24
        && reprs.first().is_none_or(|x| x.as_str() == "record_to_atom")
79
12
        && reprs2.first().is_none_or(|x| x.as_str() == "record_to_atom")
80
12
        && let Some(domain) = decl.resolved_domain()
81
12
        && let Some(domain2) = decl2.resolved_domain()
82

            
83
        // .. and have record variable domains
84
12
        && let GroundDomain::Record(entries) = domain.as_ref()
85
12
        && let GroundDomain::Record(entries2) = domain2.as_ref()
86

            
87
        // we only support equality over records of the same size
88
12
        && entries.len() == entries2.len()
89

            
90
        // assuming all record entry names must match for equality
91
24
        && izip!(entries,entries2).all(|(entry1,entry2)| entry1.name == entry2.name)
92
    {
93
12
        let mut equality_constraints = vec![];
94
        // unroll the equality into equality constraints for each field
95
24
        for entry in entries {
96
24
            let left_elem =
97
24
                Expression::RecordField(Metadata::new(), Moo::clone(left), entry.name.clone());
98
24
            let right_elem =
99
24
                Expression::RecordField(Metadata::new(), Moo::clone(right), entry.name.clone());
100
24

            
101
24
            equality_constraints.push(Expression::Eq(
102
24
                Metadata::new(),
103
24
                Moo::new(left_elem),
104
24
                Moo::new(right_elem),
105
24
            ));
106
24
        }
107

            
108
12
        let new_expr = Expression::And(
109
12
            Metadata::new(),
110
12
            Moo::new(into_matrix_expr!(equality_constraints)),
111
12
        );
112

            
113
12
        Ok(Reduction::pure(new_expr))
114
    } else {
115
169860
        Err(RuleNotApplicable)
116
    }
117
169872
}
118

            
119
// dealing with equality where the left is a record variable, and the right is a constant record
120
#[register_rule("Base", 2000, [Eq])]
121
169872
fn record_to_const(expr: &Expr, _: &SymbolTable) -> ApplicationResult {
122
169872
    if let Expr::Eq(_, left, right) = expr
123
5635
        && let Expr::Atomic(_, Atom::Reference(decl)) = &**left
124
2983
        && let Name::WithRepresentation(_, reprs) = &decl.name() as &Name
125
60
        && reprs.first().is_none_or(|x| x.as_str() == "record_to_atom")
126
    {
127
24
        let domain = decl
128
24
            .resolved_domain()
129
24
            .ok_or(ApplicationError::DomainError)?;
130

            
131
24
        let GroundDomain::Record(entries) = domain.as_ref() else {
132
            return Err(RuleNotApplicable);
133
        };
134

            
135
24
        let Some(rhs_record_names) = crate::utils::constant_record_names(right.as_ref()) else {
136
12
            return Err(RuleNotApplicable);
137
        };
138

            
139
12
        if entries.len() != rhs_record_names.len() {
140
            return Err(RuleNotApplicable);
141
12
        }
142

            
143
24
        for i in 0..entries.len() {
144
24
            if entries[i].name != rhs_record_names[i] {
145
                return Err(RuleNotApplicable);
146
24
            }
147
        }
148
12
        let mut equality_constraints = vec![];
149
24
        for entry in entries {
150
24
            let left_elem =
151
24
                Expression::RecordField(Metadata::new(), Moo::clone(left), entry.name.clone());
152
24
            let right_elem =
153
24
                Expression::RecordField(Metadata::new(), Moo::clone(right), entry.name.clone());
154
24

            
155
24
            equality_constraints.push(Expression::Eq(
156
24
                Metadata::new(),
157
24
                Moo::new(left_elem),
158
24
                Moo::new(right_elem),
159
24
            ));
160
24
        }
161
12
        let new_expr = Expression::And(
162
12
            Metadata::new(),
163
12
            Moo::new(into_matrix_expr!(equality_constraints)),
164
12
        );
165
12
        Ok(Reduction::pure(new_expr))
166
    } else {
167
169848
        Err(RuleNotApplicable)
168
    }
169
169872
}