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
301520
pub fn debug_assert_model_well_formed(model: &Model, origin: &str) {
21
301520
    debug_assert_root_at_top_level_only(model, origin);
22
301520
    debug_assert_all_names_resolved(model, origin);
23
301520
}
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
301520
pub fn debug_assert_all_names_resolved(model: &Model, origin: &str) {
32
301520
    let mut declared_names: BTreeSet<Name> = BTreeSet::new();
33
301520
    let mut referenced_names: BTreeSet<Name> = BTreeSet::new();
34

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

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

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

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

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

            
72
301520
    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
301520
    }
82

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

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

            
99
301520
    debug_assert!(
100
301520
        unresolved.is_empty(),
101
        "Model from '{origin}' contains unresolved names: {unresolved:?}"
102
    );
103
301520
}
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
139725264
fn canonical_resolution_name(name: &Name) -> &Name {
111
139725264
    match name {
112
        // Names wrapped in a selected representation still resolve through the source declaration.
113
306552
        Name::WithRepresentation(inner, _) => canonical_resolution_name(inner),
114
139418712
        _ => name,
115
    }
116
139725264
}
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
301520
pub fn debug_assert_root_at_top_level_only(model: &Model, origin: &str) {
121
301520
    debug_assert!(
122
301520
        matches!(model.root(), Expression::Root(_, _)),
123
        "Model from '{origin}' does not have Root at top-level"
124
    );
125

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

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

            
143
301520
    let total_root_count = root_count_in_main_tree + root_count_in_clauses;
144
301520
    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
301520
}
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
301520
fn collect_reachable_symbol_tables(model: &Model) -> Vec<SymbolTablePtr> {
156
301520
    let mut pending_tables: Vec<SymbolTablePtr> = vec![model.symbols_ptr_unchecked().clone()];
157
301520
    pending_tables.extend(Biplate::<SymbolTablePtr>::universe_bi(model.root()));
158

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

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

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

            
172
775964
    while let Some(table_ptr) = pending_tables.pop() {
173
474444
        if !seen_tables.insert(table_ptr.id()) {
174
42824
            continue;
175
431620
        }
176

            
177
431620
        let parent = table_ptr.read().parent().clone();
178
431620
        if let Some(parent) = parent {
179
130100
            pending_tables.push(parent);
180
301520
        }
181

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

            
185
301520
    out
186
301520
}