1
//! Debug-only structural assertions for AST/model integrity.
2
//!
3
//! The assertions in this module validate a few key invariants:
4
//! - `Root` exists exactly once, at the top-level model root, and nowhere else.
5
//! - all referenced names resolve to declarations present in reachable symbol tables.
6
//! - a combined model well-formedness check that applies all assertions.
7

            
8
use super::Model;
9

            
10
#[cfg(debug_assertions)]
11
use std::collections::{BTreeSet, HashSet};
12

            
13
#[cfg(debug_assertions)]
14
use super::{Expression, Name, Reference, SymbolTablePtr, serde::HasId};
15
#[cfg(debug_assertions)]
16
use uniplate::Biplate;
17

            
18
/// Debug-assert that a model is well-formed by applying all AST assertions in this module.
19
#[cfg(debug_assertions)]
20
444360
pub fn debug_assert_model_well_formed(model: &Model, origin: &str) {
21
444360
    debug_assert_root_at_top_level_only(model, origin);
22
444360
    debug_assert_all_names_resolved(model, origin);
23
444360
}
24

            
25
/// Debug-assert that a model is well-formed by applying all AST assertions in this module.
26
#[cfg(not(debug_assertions))]
27
pub fn debug_assert_model_well_formed(_model: &Model, _origin: &str) {}
28

            
29
/// Debug-assert that all names referenced by expressions/domains resolve to declared symbols.
30
#[cfg(debug_assertions)]
31
444360
pub fn debug_assert_all_names_resolved(model: &Model, origin: &str) {
32
444360
    let mut declared_names: BTreeSet<Name> = BTreeSet::new();
33
444360
    let mut referenced_names: BTreeSet<Name> = BTreeSet::new();
34

            
35
651180
    for table_ptr in collect_reachable_symbol_tables(model) {
36
651180
        let table = table_ptr.read();
37

            
38
18943180
        for (name, decl) in table.iter_local() {
39
18943180
            declared_names.insert(name.clone());
40

            
41
18943180
            if let Some(expr) = decl.as_value_letting() {
42
402240
                referenced_names.extend(Biplate::<Reference>::universe_bi(&*expr).into_iter().map(
43
484380
                    |reference| {
44
484380
                        let name = reference.name();
45
484380
                        canonical_resolution_name(&name).clone()
46
484380
                    },
47
                ));
48
18540940
            }
49

            
50
18943180
            if let Some(domain) = decl.domain() {
51
18942980
                referenced_names.extend(
52
18942980
                    Biplate::<Reference>::universe_bi(domain.as_ref())
53
18942980
                        .into_iter()
54
18942980
                        .map(|reference| {
55
424740
                            let name = reference.name();
56
424740
                            canonical_resolution_name(&name).clone()
57
424740
                        }),
58
                );
59
200
            }
60
        }
61
    }
62

            
63
444360
    referenced_names.extend(
64
444360
        Biplate::<Reference>::universe_bi(model.root())
65
444360
            .into_iter()
66
8873480
            .map(|reference| {
67
8873420
                let name = reference.name();
68
8873420
                canonical_resolution_name(&name).clone()
69
8873420
            }),
70
    );
71

            
72
444360
    if let Some(dominance) = &model.dominance {
73
        referenced_names.extend(
74
            Biplate::<Reference>::universe_bi(dominance)
75
                .into_iter()
76
                .map(|reference| {
77
                    let name = reference.name();
78
                    canonical_resolution_name(&name).clone()
79
                }),
80
        );
81
444360
    }
82

            
83
30651600
    for clause in model.clauses() {
84
65962460
        for literal in clause.iter() {
85
65962460
            referenced_names.extend(Biplate::<Reference>::universe_bi(literal).into_iter().map(
86
65962460
                |reference| {
87
65962460
                    let name = reference.name();
88
65962460
                    canonical_resolution_name(&name).clone()
89
65962460
                },
90
            ));
91
        }
92
    }
93

            
94
444360
    let unresolved: Vec<Name> = referenced_names
95
444360
        .difference(&declared_names)
96
444360
        .cloned()
97
444360
        .collect();
98

            
99
444360
    debug_assert!(
100
444360
        unresolved.is_empty(),
101
        "Model from '{origin}' contains unresolved names: {unresolved:?}"
102
    );
103
444360
}
104

            
105
/// Debug-assert that all names referenced by expressions/domains resolve to declared symbols.
106
#[cfg(not(debug_assertions))]
107
pub fn debug_assert_all_names_resolved(_model: &Model, _origin: &str) {}
108

            
109
#[cfg(debug_assertions)]
110
76218880
fn canonical_resolution_name(name: &Name) -> &Name {
111
76218880
    match name {
112
        // Names wrapped in a selected representation still resolve through the source declaration.
113
473880
        Name::WithRepresentation(inner, _) => canonical_resolution_name(inner),
114
75745000
        _ => name,
115
    }
116
76218880
}
117

            
118
/// Debug-assert that there is exactly one `Root` expression, and it is the model's top-level root.
119
#[cfg(debug_assertions)]
120
444360
pub fn debug_assert_root_at_top_level_only(model: &Model, origin: &str) {
121
444360
    debug_assert!(
122
444360
        matches!(model.root(), Expression::Root(_, _)),
123
        "Model from '{origin}' does not have Root at top-level"
124
    );
125

            
126
444360
    let root_count_in_main_tree = Biplate::<Expression>::universe_bi(model)
127
444360
        .iter()
128
19504310
        .filter(|expr| matches!(expr, Expression::Root(_, _)))
129
444360
        .count();
130

            
131
444360
    let root_count_in_clauses = model
132
444360
        .clauses()
133
444360
        .iter()
134
30651600
        .flat_map(|clause| clause.iter())
135
65962520
        .map(|expr| {
136
65962460
            Biplate::<Expression>::universe_bi(expr)
137
65962460
                .iter()
138
103766240
                .filter(|inner| matches!(inner, Expression::Root(_, _)))
139
65962460
                .count()
140
65962460
        })
141
444360
        .sum::<usize>();
142

            
143
444360
    let total_root_count = root_count_in_main_tree + root_count_in_clauses;
144
444360
    debug_assert_eq!(
145
        total_root_count, 1,
146
        "Model from '{origin}' should contain exactly one Root expression at top-level, found {total_root_count}"
147
    );
148
444360
}
149

            
150
/// Debug-assert that there is exactly one `Root` expression, and it is the model's top-level root.
151
#[cfg(not(debug_assertions))]
152
pub fn debug_assert_root_at_top_level_only(_model: &Model, _origin: &str) {}
153

            
154
#[cfg(debug_assertions)]
155
444360
fn collect_reachable_symbol_tables(model: &Model) -> Vec<SymbolTablePtr> {
156
444360
    let mut pending_tables: Vec<SymbolTablePtr> = vec![model.symbols_ptr_unchecked().clone()];
157
444360
    pending_tables.extend(Biplate::<SymbolTablePtr>::universe_bi(model.root()));
158

            
159
444360
    if let Some(dominance) = &model.dominance {
160
        pending_tables.extend(Biplate::<SymbolTablePtr>::universe_bi(dominance));
161
444360
    }
162

            
163
30651600
    for clause in model.clauses() {
164
65962460
        for literal in clause.iter() {
165
65962460
            pending_tables.extend(Biplate::<SymbolTablePtr>::universe_bi(literal));
166
65962460
        }
167
    }
168

            
169
444360
    let mut seen_tables = HashSet::new();
170
444360
    let mut out = Vec::new();
171

            
172
1161360
    while let Some(table_ptr) = pending_tables.pop() {
173
717000
        if !seen_tables.insert(table_ptr.id()) {
174
65820
            continue;
175
651180
        }
176

            
177
651180
        let parent = table_ptr.read().parent().clone();
178
651180
        if let Some(parent) = parent {
179
206820
            pending_tables.push(parent);
180
444360
        }
181

            
182
651180
        out.push(table_ptr);
183
    }
184

            
185
444360
    out
186
444360
}