conjure_core/rules/
select_representation.rs

Help
1use conjure_core::ast::Expression as Expr;
2use conjure_core::ast::SymbolTable;
3use conjure_core::rule_engine::{
4    register_rule, ApplicationError::RuleNotApplicable, ApplicationResult, Reduction,
5};
6use itertools::Itertools;
7
8use crate::ast::Atom;
9use crate::ast::Domain;
10use crate::ast::Name;
11use crate::bug;
12use crate::metadata::Metadata;
13use crate::representation::Representation;
14
15#[register_rule(("Base", 8000))]
16fn select_representation(expr: &Expr, symbols: &SymbolTable) -> ApplicationResult {
17    // thing we are representing must be a reference
18    let Expr::Atomic(_, Atom::Reference(name)) = expr else {
19        return Err(RuleNotApplicable);
20    };
21
22    // thing we are representing must be a variable
23    symbols
24        .lookup(name)
25        .ok_or(RuleNotApplicable)?
26        .as_var()
27        .ok_or(RuleNotApplicable)?;
28
29    if !needs_representation(name, symbols) {
30        return Err(RuleNotApplicable);
31    }
32
33    let mut symbols = symbols.clone();
34    let representation =
35        get_or_create_representation(name, &mut symbols).ok_or(RuleNotApplicable)?;
36
37    let representation_names = representation
38        .into_iter()
39        .map(|x| x.repr_name().to_string())
40        .collect_vec();
41
42    let new_name = Name::WithRepresentation(Box::new(name.clone()), representation_names);
43
44    Ok(Reduction::with_symbols(
45        Expr::Atomic(Metadata::new(), Atom::Reference(new_name)),
46        symbols,
47    ))
48}
49
50/// Returns whether `name` needs representing.
51///
52/// # Panics
53///
54///   + If `name` is not in `symbols`.
55fn needs_representation(name: &Name, symbols: &SymbolTable) -> bool {
56    // might be more logic here in the future?
57    domain_needs_representation(&symbols.resolve_domain(name).unwrap())
58}
59
60/// Returns whether `domain` needs representing.
61fn domain_needs_representation(domain: &Domain) -> bool {
62    // very simple implementation for now
63    match domain {
64        Domain::BoolDomain | Domain::IntDomain(_) => false,
65        Domain::DomainSet(_, _) | Domain::DomainMatrix(_, _) => true,
66        Domain::DomainReference(_) => unreachable!("domain should be resolved"),
67    }
68}
69
70/// Returns representations for `name`, creating them if they don't exist.
71///
72///
73/// Returns None if there is no valid representation for `name`.
74///
75/// # Panics
76///
77///   + If `name` is not in `symbols`.
78fn get_or_create_representation(
79    name: &Name,
80    symbols: &mut SymbolTable,
81) -> Option<Vec<Box<dyn Representation>>> {
82    // TODO: pick representations recursively for nested abstract domains: e.g. sets in sets.
83
84    match symbols.resolve_domain(name).unwrap() {
85        Domain::DomainSet(_, _) => None,
86        Domain::DomainMatrix(elem_domain, _) => {
87            // easy, only one possible representation
88
89            if domain_needs_representation(elem_domain.as_ref()) {
90                bug!("representing nested abstract domains is not implemented");
91            }
92
93            symbols.get_or_add_representation(name, &["matrix_to_atom"])
94        }
95        _ => unreachable!("non abstract domains should never need representations"),
96    }
97}
conjure_core/rules/select_representation.rs

conjure_core/rules/
select_representation.rs
